cprover
string_abstraction.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String Abstraction
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "string_abstraction.h"
13 
14 #include <algorithm>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/expr_util.h>
19 #include <util/fresh_symbol.h>
20 #include <util/message.h>
21 #include <util/pointer_expr.h>
23 #include <util/string_constant.h>
24 
25 #include "goto_model.h"
26 #include "pointer_arithmetic.h"
27 
29  const exprt &object,
30  exprt &dest, bool write)
31 {
32  // debugging
33  if(build(object, dest, write))
34  return true;
35 
36  // extra consistency check
37  // use
38  // #define build_wrap(a,b,c) build(a,b,c)
39  // to avoid it
40  const typet &a_t=build_abstraction_type(object.type());
41  /*assert(dest.type() == a_t ||
42  (dest.type().id()==ID_array && a_t.id()==ID_pointer &&
43  dest.type().subtype() == a_t.subtype()));
44  */
45  if(
46  dest.type() != a_t &&
47  !(dest.type().id() == ID_array && a_t.id() == ID_pointer &&
48  dest.type().subtype() == a_t.subtype()))
49  {
51  log.warning() << "warning: inconsistent abstract type for "
52  << object.pretty() << messaget::eom;
53  return true;
54  }
55 
56  return false;
57 }
58 
60 {
61  return type.id() == ID_pointer && type.subtype() == string_struct;
62 }
63 
64 static inline bool is_ptr_argument(const typet &type)
65 {
66  return type.id()==ID_pointer;
67 }
68 
70  symbol_tablet &symbol_table,
71  message_handlert &message_handler,
72  goto_functionst &dest)
73 {
74  string_abstractiont string_abstraction(symbol_table, message_handler);
75  string_abstraction(dest);
76 }
77 
79  goto_modelt &goto_model,
80  message_handlert &message_handler)
81 {
82  string_abstractiont{goto_model.symbol_table, message_handler}.apply(
83  goto_model);
84 }
85 
87  symbol_tablet &_symbol_table,
88  message_handlert &_message_handler)
89  : sym_suffix("#str$fcn"),
90  symbol_table(_symbol_table),
91  ns(_symbol_table),
92  temporary_counter(0),
93  message_handler(_message_handler)
94 {
95  struct_typet s({{"is_zero", build_type(whatt::IS_ZERO)},
96  {"length", build_type(whatt::LENGTH)},
97  {"size", build_type(whatt::SIZE)}});
98  s.components()[0].set_pretty_name("is_zero");
99  s.components()[1].set_pretty_name("length");
100  s.components()[2].set_pretty_name("size");
101 
102  string_struct = std::move(s);
103 }
104 
106 {
107  typet type;
108 
109  // clang-format off
110  switch(what)
111  {
112  case whatt::IS_ZERO: type=c_bool_type(); break;
113  case whatt::LENGTH: type=size_type(); break;
114  case whatt::SIZE: type=size_type(); break;
115  }
116  // clang-format on
117 
118  return type;
119 }
120 
122 {
123  operator()(goto_model.goto_functions);
124 }
125 
127 {
128  // iterate over all previously known symbols as the body of the loop modifies
129  // the symbol table and can thus invalidate iterators
130  for(auto &sym_name : symbol_table.sorted_symbol_names())
131  {
132  const typet &type = symbol_table.lookup_ref(sym_name).type;
133 
134  if(type.id() != ID_code)
135  continue;
136 
137  sym_suffix = "#str$" + id2string(sym_name);
138 
139  goto_functionst::function_mapt::iterator fct_entry =
140  dest.function_map.find(sym_name);
141  if(fct_entry != dest.function_map.end())
142  {
145  fct_entry->second.parameter_identifiers);
146  }
147  else
148  {
150  to_code_type(type).parameters().size(), irep_idt{});
152  }
153  }
154 
155  for(auto &gf_entry : dest.function_map)
156  {
157  sym_suffix = "#str$" + id2string(gf_entry.first);
158  abstract(gf_entry.second.body);
159  }
160 
161  // do we have a main?
162  goto_functionst::function_mapt::iterator
163  m_it=dest.function_map.find(dest.entry_point());
164 
165  if(m_it!=dest.function_map.end())
166  {
167  goto_programt &main=m_it->second.body;
168 
169  // do initialization
171  main.swap(initialization);
173  }
174 }
175 
177 {
178  abstract(dest);
179 
180  // do initialization
182  dest.swap(initialization);
184 }
185 
187  symbolt &fct_symbol,
188  goto_functiont::parameter_identifierst &parameter_identifiers)
189 {
190  code_typet &fct_type = to_code_type(fct_symbol.type);
191  PRECONDITION(fct_type.parameters().size() == parameter_identifiers.size());
192 
193  code_typet::parameterst str_args;
194 
195  goto_functiont::parameter_identifierst::const_iterator param_id_it =
196  parameter_identifiers.begin();
197  for(const auto &parameter : fct_type.parameters())
198  {
199  const typet &abstract_type = build_abstraction_type(parameter.type());
200  if(abstract_type.is_nil())
201  continue;
202 
203  str_args.push_back(add_parameter(fct_symbol, abstract_type, *param_id_it));
204  ++param_id_it;
205  }
206 
207  for(const auto &new_param : str_args)
208  parameter_identifiers.push_back(new_param.get_identifier());
209  fct_type.parameters().insert(
210  fct_type.parameters().end(), str_args.begin(), str_args.end());
211 }
212 
214  const symbolt &fct_symbol,
215  const typet &type,
216  const irep_idt &identifier)
217 {
218  typet final_type=is_ptr_argument(type)?
219  type:pointer_type(type);
220 
221  symbolt &param_symbol = get_fresh_aux_symbol(
222  final_type,
223  id2string(identifier.empty() ? fct_symbol.name : identifier),
224  id2string(
225  identifier.empty() ? fct_symbol.base_name
226  : ns.lookup(identifier).base_name) +
227  "#str",
228  fct_symbol.location,
229  fct_symbol.mode,
230  symbol_table);
231  param_symbol.is_parameter = true;
232  param_symbol.value.make_nil();
233 
234  code_typet::parametert str_parameter{final_type};
235  str_parameter.add_source_location() = fct_symbol.location;
236  str_parameter.set_base_name(param_symbol.base_name);
237  str_parameter.set_identifier(param_symbol.name);
238 
239  if(!identifier.empty())
240  parameter_map.insert(std::make_pair(identifier, param_symbol.name));
241 
242  return str_parameter;
243 }
244 
246 {
247  locals.clear();
248 
250  it=abstract(dest, it);
251 
252  if(locals.empty())
253  return;
254 
255  // go over it again for the newly added locals
256  declare_define_locals(dest);
257  locals.clear();
258 }
259 
261 {
262  typedef std::unordered_map<irep_idt, goto_programt::targett> available_declst;
263  available_declst available_decls;
264 
266  if(it->is_decl())
267  // same name may exist several times due to inlining, make sure the first
268  // declaration is used
269  available_decls.insert(
270  std::make_pair(it->decl_symbol().get_identifier(), it));
271 
272  // declare (and, if necessary, define) locals
273  for(const auto &l : locals)
274  {
275  goto_programt::targett ref_instr=dest.instructions.begin();
276  bool has_decl=false;
277 
278  available_declst::const_iterator entry=available_decls.find(l.first);
279 
280  if(available_declst::const_iterator(available_decls.end())!=entry)
281  {
282  ref_instr=entry->second;
283  has_decl=true;
284  }
285 
286  goto_programt tmp;
287  make_decl_and_def(tmp, ref_instr, l.second, l.first);
288 
289  if(has_decl)
290  ++ref_instr;
291  dest.insert_before_swap(ref_instr, tmp);
292  }
293 }
294 
296  goto_programt::targett ref_instr,
297  const irep_idt &identifier,
298  const irep_idt &source_sym)
299 {
300  const symbolt &symbol=ns.lookup(identifier);
301  symbol_exprt sym_expr=symbol.symbol_expr();
302 
303  goto_programt::targett decl1 =
304  dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location));
305  decl1->code_nonconst().add_source_location() = ref_instr->source_location;
306 
307  exprt val=symbol.value;
308  // initialize pointers with suitable objects
309  if(val.is_nil())
310  {
311  const symbolt &orig=ns.lookup(source_sym);
312  val=make_val_or_dummy_rec(dest, ref_instr, symbol, ns.follow(orig.type));
313  }
314 
315  // may still be nil (structs, then assignments have been done already)
316  if(val.is_not_nil())
317  {
318  goto_programt::targett assignment1 =
320  code_assignt(sym_expr, val), ref_instr->source_location));
321  assignment1->code_nonconst().add_source_location() =
322  ref_instr->source_location;
323  }
324 }
325 
327  goto_programt::targett ref_instr,
328  const symbolt &symbol, const typet &source_type)
329 {
330  const typet &eff_type=ns.follow(symbol.type);
331 
332  if(eff_type.id()==ID_array || eff_type.id()==ID_pointer)
333  {
334  const typet &source_subt=is_ptr_string_struct(eff_type)?
335  source_type:ns.follow(source_type.subtype());
337  dest, ref_instr, symbol, irep_idt(),
338  eff_type.subtype(), source_subt);
339 
340  if(eff_type.id()==ID_array)
341  return array_of_exprt(sym_expr, to_array_type(eff_type));
342  else
343  return address_of_exprt(sym_expr);
344  }
345  else if(
346  eff_type.id() == ID_union ||
347  (eff_type.id() == ID_struct && eff_type != string_struct))
348  {
349  const struct_union_typet &su_source=to_struct_union_type(source_type);
350  const struct_union_typet::componentst &s_components=
351  su_source.components();
352  const struct_union_typet &struct_union_type=to_struct_union_type(eff_type);
353  const struct_union_typet::componentst &components=
354  struct_union_type.components();
355  unsigned seen=0;
356 
357  struct_union_typet::componentst::const_iterator it2=components.begin();
358  for(struct_union_typet::componentst::const_iterator
359  it=s_components.begin();
360  it!=s_components.end() && it2!=components.end();
361  ++it)
362  {
363  if(it->get_name()!=it2->get_name())
364  continue;
365 
366  const typet &eff_sub_type=ns.follow(it2->type());
367  if(eff_sub_type.id()==ID_pointer ||
368  eff_sub_type.id()==ID_array ||
369  eff_sub_type.id()==ID_struct ||
370  eff_sub_type.id()==ID_union)
371  {
373  dest, ref_instr, symbol, it2->get_name(),
374  it2->type(), ns.follow(it->type()));
375 
376  member_exprt member(symbol.symbol_expr(), it2->get_name(), it2->type());
377 
378  goto_programt::targett assignment1 =
380  code_assignt(member, sym_expr), ref_instr->source_location));
381  assignment1->code_nonconst().add_source_location() =
382  ref_instr->source_location;
383  }
384 
385  ++seen;
386  ++it2;
387  }
388 
389  INVARIANT(
390  components.size() == seen,
391  "some of the symbol's component names were not found in the source");
392  }
393 
394  return nil_exprt();
395 }
396 
398  goto_programt &dest,
399  goto_programt::targett ref_instr,
400  const symbolt &symbol,
401  const irep_idt &component_name,
402  const typet &type,
403  const typet &source_type)
404 {
405  std::string suffix="$strdummy";
406  if(!component_name.empty())
407  suffix="#"+id2string(component_name)+suffix;
408 
409  irep_idt dummy_identifier=id2string(symbol.name)+suffix;
410 
411  auxiliary_symbolt new_symbol;
412  new_symbol.type=type;
413  new_symbol.value.make_nil();
414  new_symbol.location=ref_instr->source_location;
415  new_symbol.name=dummy_identifier;
416  new_symbol.module=symbol.module;
417  new_symbol.base_name=id2string(symbol.base_name)+suffix;
418  new_symbol.mode=symbol.mode;
419  new_symbol.pretty_name=id2string(
420  symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+suffix;
421 
422  symbol_exprt sym_expr=new_symbol.symbol_expr();
423 
424  // make sure it is declared before the recursive call
426  dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location));
427  decl->code_nonconst().add_source_location() = ref_instr->source_location;
428 
429  // set the value - may be nil
430  if(
431  source_type.id() == ID_array && is_char_type(source_type.subtype()) &&
432  type == string_struct)
433  {
434  new_symbol.value = struct_exprt(
435  {build_unknown(whatt::IS_ZERO, false),
437  to_array_type(source_type).size().id() == ID_infinity
438  ? build_unknown(whatt::SIZE, false)
439  : to_array_type(source_type).size()},
440  string_struct);
441 
443  }
444  else
445  new_symbol.value=
446  make_val_or_dummy_rec(dest, ref_instr, new_symbol, source_type);
447 
448  if(new_symbol.value.is_not_nil())
449  {
450  goto_programt::targett assignment1 =
452  code_assignt(sym_expr, new_symbol.value), ref_instr->source_location));
453  assignment1->code_nonconst().add_source_location() =
454  ref_instr->source_location;
455  }
456 
457  symbol_table.insert(std::move(new_symbol));
458 
459  return sym_expr;
460 }
461 
463  goto_programt &dest,
465 {
466  switch(it->type)
467  {
468  case ASSIGN:
469  it=abstract_assign(dest, it);
470  break;
471 
472  case GOTO:
473  case ASSERT:
474  case ASSUME:
475  if(has_string_macros(it->get_condition()))
476  {
477  exprt tmp = it->get_condition();
478  replace_string_macros(tmp, false, it->source_location);
479  it->set_condition(tmp);
480  }
481  break;
482 
483  case FUNCTION_CALL:
485  break;
486 
487  case SET_RETURN_VALUE:
488  // use remove_returns
489  UNREACHABLE;
490  break;
491 
492  case END_FUNCTION:
493  case START_THREAD:
494  case END_THREAD:
495  case ATOMIC_BEGIN:
496  case ATOMIC_END:
497  case DECL:
498  case DEAD:
499  case CATCH:
500  case THROW:
501  case SKIP:
502  case OTHER:
503  case LOCATION:
504  break;
505 
506  case INCOMPLETE_GOTO:
507  case NO_INSTRUCTION_TYPE:
508  UNREACHABLE;
509  break;
510  }
511 
512  return it;
513 }
514 
516  goto_programt &dest,
517  goto_programt::targett target)
518 {
519  {
520  exprt &lhs = target->assign_lhs_nonconst();
521  exprt &rhs = target->assign_rhs_nonconst();
522 
523  if(has_string_macros(lhs))
524  {
525  replace_string_macros(lhs, true, target->source_location);
526  move_lhs_arithmetic(lhs, rhs);
527  }
528 
529  if(has_string_macros(rhs))
530  replace_string_macros(rhs, false, target->source_location);
531  }
532 
533  const typet &type = target->assign_lhs().type();
534 
535  if(type.id() == ID_pointer || type.id() == ID_array)
536  return abstract_pointer_assign(dest, target);
537  else if(is_char_type(type))
538  return abstract_char_assign(dest, target);
539 
540  return target;
541 }
542 
544  goto_programt::targett target)
545 {
546  auto arguments = as_const(*target).call_arguments();
548 
549  for(const auto &arg : arguments)
550  {
551  const typet &abstract_type = build_abstraction_type(arg.type());
552  if(abstract_type.is_nil())
553  continue;
554 
555  str_args.push_back(exprt());
556  // if function takes void*, build for `arg` will fail if actual parameter
557  // is of some other pointer type; then just introduce an unknown
558  if(build_wrap(arg, str_args.back(), false))
559  str_args.back()=build_unknown(abstract_type, false);
560  // array -> pointer translation
561  if(str_args.back().type().id()==ID_array &&
562  abstract_type.id()==ID_pointer)
563  {
564  INVARIANT(
565  str_args.back().type().subtype() == abstract_type.subtype(),
566  "argument array type differs from formal parameter pointer type");
567 
568  index_exprt idx(str_args.back(), from_integer(0, index_type()));
569  // disable bounds check on that one
570  idx.set(ID_C_bounds_check, false);
571 
572  str_args.back()=address_of_exprt(idx);
573  }
574 
575  if(!is_ptr_argument(abstract_type))
576  str_args.back()=address_of_exprt(str_args.back());
577  }
578 
579  if(!str_args.empty())
580  {
581  arguments.insert(arguments.end(), str_args.begin(), str_args.end());
582 
583  auto &parameters =
584  to_code_type(target->call_function().type()).parameters();
585  for(const auto &arg : str_args)
586  parameters.push_back(code_typet::parametert{arg.type()});
587 
588  target->call_arguments() = std::move(arguments);
589  }
590 }
591 
593 {
594  if(expr.id()=="is_zero_string" ||
595  expr.id()=="zero_string_length" ||
596  expr.id()=="buffer_size")
597  return true;
598 
599  forall_operands(it, expr)
600  if(has_string_macros(*it))
601  return true;
602 
603  return false;
604 }
605 
607  exprt &expr,
608  bool lhs,
609  const source_locationt &source_location)
610 {
611  if(expr.id()=="is_zero_string")
612  {
613  PRECONDITION(expr.operands().size() == 1);
614  exprt tmp =
615  build(to_unary_expr(expr).op(), whatt::IS_ZERO, lhs, source_location);
616  expr.swap(tmp);
617  }
618  else if(expr.id()=="zero_string_length")
619  {
620  PRECONDITION(expr.operands().size() == 1);
621  exprt tmp =
622  build(to_unary_expr(expr).op(), whatt::LENGTH, lhs, source_location);
623  expr.swap(tmp);
624  }
625  else if(expr.id()=="buffer_size")
626  {
627  PRECONDITION(expr.operands().size() == 1);
628  exprt tmp =
629  build(to_unary_expr(expr).op(), whatt::SIZE, false, source_location);
630  expr.swap(tmp);
631  }
632  else
633  Forall_operands(it, expr)
634  replace_string_macros(*it, lhs, source_location);
635 }
636 
638  const exprt &pointer,
639  whatt what,
640  bool write,
641  const source_locationt &source_location)
642 {
643  // take care of pointer typecasts now
644  if(pointer.id()==ID_typecast)
645  {
646  // cast from another pointer type?
647  if(to_typecast_expr(pointer).op().type().id() != ID_pointer)
648  return build_unknown(what, write);
649 
650  // recursive call
651  return build(to_typecast_expr(pointer).op(), what, write, source_location);
652  }
653 
654  exprt str_struct;
655  if(build_wrap(pointer, str_struct, write))
656  UNREACHABLE;
657 
658  exprt result=member(str_struct, what);
659 
660  if(what==whatt::LENGTH || what==whatt::SIZE)
661  {
662  // adjust for offset
663  exprt offset = pointer_offset(pointer);
664  typet result_type = result.type();
666  minus_exprt(
667  typecast_exprt::conditional_cast(result, offset.type()), offset),
668  result_type);
669  }
670 
671  return result;
672 }
673 
675 {
676  const typet &eff_type=ns.follow(type);
677  abstraction_types_mapt::const_iterator map_entry=
678  abstraction_types_map.find(eff_type);
679  if(map_entry!=abstraction_types_map.end())
680  return map_entry->second;
681 
683  tmp.swap(abstraction_types_map);
684  build_abstraction_type_rec(eff_type, tmp);
685 
686  abstraction_types_map.swap(tmp);
687  map_entry=tmp.find(eff_type);
688  CHECK_RETURN(map_entry != tmp.end());
689  return abstraction_types_map.insert(
690  std::make_pair(eff_type, map_entry->second)).first->second;
691 }
692 
694  const abstraction_types_mapt &known)
695 {
696  const typet &eff_type=ns.follow(type);
697  abstraction_types_mapt::const_iterator known_entry=known.find(eff_type);
698  if(known_entry!=known.end())
699  return known_entry->second;
700 
701  ::std::pair<abstraction_types_mapt::iterator, bool> map_entry(
702  abstraction_types_map.insert(::std::make_pair(eff_type, typet{ID_nil})));
703  if(!map_entry.second)
704  return map_entry.first->second;
705 
706  if(eff_type.id()==ID_array || eff_type.id()==ID_pointer)
707  {
708  // char* or void* or char[]
709  if(is_char_type(eff_type.subtype()) ||
710  eff_type.subtype().id()==ID_empty)
711  map_entry.first->second=pointer_type(string_struct);
712  else
713  {
714  const typet &subt=build_abstraction_type_rec(eff_type.subtype(), known);
715  if(!subt.is_nil())
716  {
717  if(eff_type.id()==ID_array)
718  map_entry.first->second=
719  array_typet(subt, to_array_type(eff_type).size());
720  else
721  map_entry.first->second=pointer_type(subt);
722  }
723  }
724  }
725  else if(eff_type.id()==ID_struct || eff_type.id()==ID_union)
726  {
727  const struct_union_typet &struct_union_type=to_struct_union_type(eff_type);
728 
730  for(const auto &comp : struct_union_type.components())
731  {
732  if(comp.get_anonymous())
733  continue;
734  typet subt=build_abstraction_type_rec(comp.type(), known);
735  if(subt.is_nil())
736  // also precludes structs with pointers to the same datatype
737  continue;
738 
739  new_comp.push_back(struct_union_typet::componentt());
740  new_comp.back().set_name(comp.get_name());
741  new_comp.back().set_pretty_name(comp.get_pretty_name());
742  new_comp.back().type()=subt;
743  }
744  if(!new_comp.empty())
745  {
746  struct_union_typet t(eff_type.id());
747  t.components().swap(new_comp);
748  map_entry.first->second=t;
749  }
750  }
751 
752  return map_entry.first->second;
753 }
754 
755 bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
756 {
757  const typet &abstract_type=build_abstraction_type(object.type());
758  if(abstract_type.is_nil())
759  return true;
760 
761  if(object.id()==ID_typecast)
762  {
763  if(build(to_typecast_expr(object).op(), dest, write))
764  return true;
765 
766  return dest.type() != abstract_type ||
767  (dest.type().id() == ID_array && abstract_type.id() == ID_pointer &&
768  dest.type().subtype() == abstract_type.subtype());
769  }
770 
771  if(object.id()==ID_string_constant)
772  {
773  const std::string &str_value =
774  id2string(to_string_constant(object).get_value());
775  // make sure we handle the case of a string constant with string-terminating
776  // \0 in it
777  const std::size_t str_len =
778  std::min(str_value.size(), str_value.find('\0'));
779  return build_symbol_constant(str_len, str_len+1, dest);
780  }
781 
782  if(object.id()==ID_array && is_char_type(object.type().subtype()))
783  return build_array(to_array_expr(object), dest, write);
784 
785  // other constants aren't useful
786  if(object.is_constant())
787  return true;
788 
789  if(object.id()==ID_symbol)
790  return build_symbol(to_symbol_expr(object), dest);
791 
792  if(object.id()==ID_if)
793  return build_if(to_if_expr(object), dest, write);
794 
795  if(object.id()==ID_member)
796  {
797  const member_exprt &o_mem=to_member_expr(object);
798  dest=member_exprt(exprt(), o_mem.get_component_name(), abstract_type);
799  return build_wrap(
800  o_mem.struct_op(), to_member_expr(dest).compound(), write);
801  }
802 
803  if(object.id()==ID_dereference)
804  {
805  const dereference_exprt &o_deref=to_dereference_expr(object);
806  dest=dereference_exprt(exprt(), abstract_type);
807  return build_wrap(
808  o_deref.pointer(), to_dereference_expr(dest).pointer(), write);
809  }
810 
811  if(object.id()==ID_index)
812  {
813  const index_exprt &o_index=to_index_expr(object);
814  dest=index_exprt(exprt(), o_index.index(), abstract_type);
815  return build_wrap(o_index.array(), to_index_expr(dest).array(), write);
816  }
817 
818  // handle pointer stuff
819  if(object.type().id()==ID_pointer)
820  return build_pointer(object, dest, write);
821 
822  return true;
823 }
824 
826  exprt &dest, bool write)
827 {
828  if_exprt new_if(o_if.cond(), exprt(), exprt());
829 
830  // recursive calls
831  bool op1_err=build_wrap(o_if.true_case(), new_if.true_case(), write);
832  bool op2_err=build_wrap(o_if.false_case(), new_if.false_case(), write);
833  if(op1_err && op2_err)
834  return true;
835  // at least one of them gave proper results
836  if(op1_err)
837  {
838  new_if.type()=new_if.false_case().type();
839  new_if.true_case()=build_unknown(new_if.type(), write);
840  }
841  else if(op2_err)
842  {
843  new_if.type()=new_if.true_case().type();
844  new_if.false_case()=build_unknown(new_if.type(), write);
845  }
846  else
847  new_if.type()=new_if.true_case().type();
848 
849  dest.swap(new_if);
850  return false;
851 }
852 
854  exprt &dest, bool write)
855 {
856  PRECONDITION(is_char_type(object.type().subtype()));
857 
858  // writing is invalid
859  if(write)
860  return true;
861 
862  const exprt &a_size=to_array_type(object.type()).size();
863  const auto size = numeric_cast<mp_integer>(a_size);
864  // don't do anything, if we cannot determine the size
865  if(!size.has_value())
866  return true;
867  INVARIANT(
868  *size == object.operands().size(),
869  "wrong number of array object arguments");
870 
871  exprt::operandst::const_iterator it=object.operands().begin();
872  for(mp_integer i = 0; i < *size; ++i, ++it)
873  if(it->is_zero())
874  return build_symbol_constant(i, *size, dest);
875 
876  return true;
877 }
878 
880  exprt &dest, bool write)
881 {
882  PRECONDITION(object.type().id() == ID_pointer);
883 
884  pointer_arithmetict ptr(object);
885  if(ptr.pointer.id()==ID_address_of)
886  {
888 
889  if(a.object().id()==ID_index)
890  return build_wrap(to_index_expr(a.object()).array(), dest, write);
891 
892  // writing is invalid
893  if(write)
894  return true;
895 
896  if(build_wrap(a.object(), dest, write))
897  return true;
898  dest=address_of_exprt(dest);
899  return false;
900  }
901  else if(ptr.pointer.id()==ID_symbol &&
902  is_char_type(object.type().subtype()))
903  // recursive call; offset will be handled by pointer_offset in SIZE/LENGTH
904  // checks
905  return build_wrap(ptr.pointer, dest, write);
906 
907  // we don't handle other pointer arithmetic
908  return true;
909 }
910 
912 {
913  typet type=build_type(what);
914 
915  if(write)
916  return exprt(ID_null_object, type);
917 
918  exprt result;
919 
920  switch(what)
921  {
922  case whatt::IS_ZERO:
923  result = from_integer(0, type);
924  break;
925 
926  case whatt::LENGTH:
927  case whatt::SIZE:
928  result = side_effect_expr_nondett(type, source_locationt());
929  break;
930  }
931 
932  return result;
933 }
934 
936 {
937  if(write)
938  return exprt(ID_null_object, type);
939 
940  // create an uninitialized dummy symbol
941  // because of a lack of contextual information we can't build a nice name
942  // here, but moving that into locals should suffice for proper operation
943  irep_idt identifier=
944  "$tmp::nondet_str#str$"+std::to_string(++temporary_counter);
945  // ensure decl and initialization
946  locals[identifier]=identifier;
947 
948  auxiliary_symbolt new_symbol;
949  new_symbol.type=type;
950  new_symbol.value.make_nil();
951  new_symbol.name=identifier;
952  new_symbol.module="$tmp";
953  new_symbol.base_name=identifier;
954  new_symbol.mode=ID_C;
955  new_symbol.pretty_name=identifier;
956 
957  symbol_table.insert(std::move(new_symbol));
958 
959  return ns.lookup(identifier).symbol_expr();
960 }
961 
963 {
964  const symbolt &symbol=ns.lookup(sym.get_identifier());
965 
966  const typet &abstract_type=build_abstraction_type(symbol.type);
967  CHECK_RETURN(!abstract_type.is_nil());
968 
969  irep_idt identifier;
970 
971  if(symbol.is_parameter)
972  {
973  const auto parameter_map_entry = parameter_map.find(symbol.name);
974  if(parameter_map_entry == parameter_map.end())
975  return true;
976  identifier = parameter_map_entry->second;
977  }
978  else if(symbol.is_static_lifetime)
979  {
980  std::string sym_suffix_before = sym_suffix;
981  sym_suffix = "#str";
982  identifier = id2string(symbol.name) + sym_suffix;
983  if(symbol_table.symbols.find(identifier) == symbol_table.symbols.end())
984  build_new_symbol(symbol, identifier, abstract_type);
985  sym_suffix = sym_suffix_before;
986  }
987  else
988  {
989  identifier=id2string(symbol.name)+sym_suffix;
990  if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
991  build_new_symbol(symbol, identifier, abstract_type);
992  }
993 
994  const symbolt &str_symbol=ns.lookup(identifier);
995  dest=str_symbol.symbol_expr();
996  if(symbol.is_parameter && !is_ptr_argument(abstract_type))
997  dest = dereference_exprt{dest};
998 
999  return false;
1000 }
1001 
1003  const irep_idt &identifier, const typet &type)
1004 {
1005  if(!symbol.is_static_lifetime)
1006  locals[symbol.name]=identifier;
1007 
1008  auxiliary_symbolt new_symbol;
1009  new_symbol.type=type;
1010  new_symbol.value.make_nil();
1011  new_symbol.location=symbol.location;
1012  new_symbol.name=identifier;
1013  new_symbol.module=symbol.module;
1014  new_symbol.base_name=id2string(symbol.base_name)+sym_suffix;
1015  new_symbol.mode=symbol.mode;
1016  new_symbol.pretty_name=
1017  id2string(symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+
1018  sym_suffix;
1019  new_symbol.is_static_lifetime=symbol.is_static_lifetime;
1020  new_symbol.is_thread_local=symbol.is_thread_local;
1021 
1022  symbol_table.insert(std::move(new_symbol));
1023 
1024  if(symbol.is_static_lifetime)
1025  {
1026  goto_programt::targett dummy_loc =
1028  dummy_loc->source_location=symbol.location;
1029  make_decl_and_def(initialization, dummy_loc, identifier, symbol.name);
1030  initialization.instructions.erase(dummy_loc);
1031  }
1032 }
1033 
1035  const mp_integer &zero_length,
1036  const mp_integer &buf_size,
1037  exprt &dest)
1038 {
1039  irep_idt base="$string_constant_str_"+integer2string(zero_length)
1040  +"_"+integer2string(buf_size);
1041  irep_idt identifier="string_abstraction::"+id2string(base);
1042 
1043  if(symbol_table.symbols.find(identifier)==
1044  symbol_table.symbols.end())
1045  {
1046  auxiliary_symbolt new_symbol;
1047  new_symbol.type=string_struct;
1048  new_symbol.value.make_nil();
1049  new_symbol.name=identifier;
1050  new_symbol.base_name=base;
1051  new_symbol.mode=ID_C;
1052  new_symbol.pretty_name=base;
1053  new_symbol.is_static_lifetime=true;
1054  new_symbol.is_thread_local=false;
1055  new_symbol.is_file_local=false;
1056 
1057  {
1058  struct_exprt value(
1060  from_integer(zero_length, build_type(whatt::LENGTH)),
1061  from_integer(buf_size, build_type(whatt::SIZE))},
1062  string_struct);
1063 
1064  // initialization
1066  code_assignt(new_symbol.symbol_expr(), value)));
1067  }
1068 
1069  symbol_table.insert(std::move(new_symbol));
1070  }
1071 
1072  dest=address_of_exprt(symbol_exprt(identifier, string_struct));
1073 
1074  return false;
1075 }
1076 
1078 {
1079  while(lhs.id() == ID_typecast)
1080  {
1081  typecast_exprt lhs_tc = to_typecast_expr(lhs);
1082  rhs = typecast_exprt::conditional_cast(rhs, lhs_tc.op().type());
1083  lhs.swap(lhs_tc.op());
1084  }
1085 
1086  if(lhs.id()==ID_minus)
1087  {
1088  // move op1 to rhs
1089  exprt rest = to_minus_expr(lhs).op0();
1090  rhs = plus_exprt(rhs, to_minus_expr(lhs).op1());
1091  rhs.type()=lhs.type();
1092  lhs=rest;
1093  }
1094 
1095  while(lhs.id() == ID_typecast)
1096  {
1097  typecast_exprt lhs_tc = to_typecast_expr(lhs);
1098  rhs = typecast_exprt::conditional_cast(rhs, lhs_tc.op().type());
1099  lhs.swap(lhs_tc.op());
1100  }
1101 }
1102 
1104  goto_programt &dest,
1105  const goto_programt::targett target)
1106 {
1107  const exprt &lhs = target->assign_lhs();
1108  const exprt rhs = target->assign_rhs();
1109  const exprt *rhsp = &(target->assign_rhs());
1110 
1111  while(rhsp->id()==ID_typecast)
1112  rhsp = &(to_typecast_expr(*rhsp).op());
1113 
1114  const typet &abstract_type=build_abstraction_type(lhs.type());
1115  if(abstract_type.is_nil())
1116  return target;
1117 
1118  exprt new_lhs, new_rhs;
1119  if(build_wrap(lhs, new_lhs, true))
1120  return target;
1121 
1122  bool unknown=(abstract_type!=build_abstraction_type(rhsp->type()) ||
1123  build_wrap(rhs, new_rhs, false));
1124  if(unknown)
1125  new_rhs=build_unknown(abstract_type, false);
1126 
1127  if(lhs.type().id()==ID_pointer && !unknown)
1128  {
1129  goto_programt::instructiont assignment;
1130  assignment = goto_programt::make_assignment(
1131  code_assignt(new_lhs, new_rhs), target->source_location);
1132  assignment.code_nonconst().add_source_location() = target->source_location;
1133  dest.insert_before_swap(target, assignment);
1134 
1135  return std::next(target);
1136  }
1137  else
1138  {
1139  return value_assignments(dest, target, new_lhs, new_rhs);
1140  }
1141 }
1142 
1144  goto_programt &dest,
1145  goto_programt::targett target)
1146 {
1147  const exprt &lhs = target->assign_lhs();
1148  const exprt *rhsp = &(target->assign_rhs());
1149 
1150  while(rhsp->id()==ID_typecast)
1151  rhsp = &(to_typecast_expr(*rhsp).op());
1152 
1153  // we only care if the constant zero is assigned
1154  if(!rhsp->is_zero())
1155  return target;
1156 
1157  // index into a character array
1158  if(lhs.id()==ID_index)
1159  {
1160  const index_exprt &i_lhs=to_index_expr(lhs);
1161 
1162  exprt new_lhs;
1163  if(!build_wrap(i_lhs.array(), new_lhs, true))
1164  {
1165  exprt i2=member(new_lhs, whatt::LENGTH);
1166  INVARIANT(
1167  i2.is_not_nil(),
1168  "failed to create length-component for the left-hand-side");
1169 
1170  exprt new_length=i_lhs.index();
1171  make_type(new_length, i2.type());
1172 
1173  if_exprt min_expr(binary_relation_exprt(new_length, ID_lt, i2),
1174  new_length, i2);
1175 
1176  return char_assign(dest, target, new_lhs, i2, min_expr);
1177  }
1178  }
1179  else if(lhs.id()==ID_dereference)
1180  {
1181  pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
1182  exprt new_lhs;
1183  if(!build_wrap(ptr.pointer, new_lhs, true))
1184  {
1185  const exprt i2=member(new_lhs, whatt::LENGTH);
1186  INVARIANT(
1187  i2.is_not_nil(),
1188  "failed to create length-component for the left-hand-side");
1189 
1191  return
1192  char_assign(
1193  dest,
1194  target,
1195  new_lhs,
1196  i2,
1197  ptr.offset.is_nil()?
1199  ptr.offset);
1200  }
1201  }
1202 
1203  return target;
1204 }
1205 
1207  goto_programt &dest,
1208  goto_programt::targett target,
1209  const exprt &new_lhs,
1210  const exprt &lhs,
1211  const exprt &rhs)
1212 {
1213  goto_programt tmp;
1214 
1215  const exprt i1=member(new_lhs, whatt::IS_ZERO);
1216  INVARIANT(
1217  i1.is_not_nil(),
1218  "failed to create is_zero-component for the left-hand-side");
1219 
1221  code_assignt(i1, from_integer(1, i1.type())), target->source_location));
1222  assignment1->code_nonconst().add_source_location() = target->source_location;
1223 
1225  code_assignt(lhs, rhs), target->source_location));
1226  assignment2->code_nonconst().add_source_location() = target->source_location;
1227 
1229  assignment2->code_nonconst().op0(), assignment2->code_nonconst().op1());
1230 
1231  dest.insert_before_swap(target, tmp);
1232  ++target;
1233  ++target;
1234 
1235  return target;
1236 }
1237 
1239  goto_programt &dest,
1240  goto_programt::targett target,
1241  const exprt &lhs,
1242  const exprt &rhs)
1243 {
1244  if(rhs.id()==ID_if)
1245  return value_assignments_if(dest, target, lhs, to_if_expr(rhs));
1246 
1247  PRECONDITION(lhs.type() == rhs.type());
1248 
1249  if(lhs.type().id()==ID_array)
1250  {
1251  const exprt &a_size=to_array_type(lhs.type()).size();
1252  const auto size = numeric_cast<mp_integer>(a_size);
1253  // don't do anything, if we cannot determine the size
1254  if(!size.has_value())
1255  return target;
1256  for(mp_integer i = 0; i < *size; ++i)
1257  target=value_assignments(dest, target,
1258  index_exprt(lhs, from_integer(i, a_size.type())),
1259  index_exprt(rhs, from_integer(i, a_size.type())));
1260  }
1261  else if(lhs.type().id() == ID_pointer)
1262  return value_assignments(
1263  dest, target, dereference_exprt{lhs}, dereference_exprt{rhs});
1264  else if(lhs.type()==string_struct)
1265  return value_assignments_string_struct(dest, target, lhs, rhs);
1266  else if(lhs.type().id()==ID_struct || lhs.type().id()==ID_union)
1267  {
1268  const struct_union_typet &struct_union_type=
1269  to_struct_union_type(lhs.type());
1270 
1271  for(const auto &comp : struct_union_type.components())
1272  {
1273  INVARIANT(
1274  !comp.get_name().empty(), "struct/union components must have a name");
1275 
1276  target=value_assignments(dest, target,
1277  member_exprt(lhs, comp.get_name(), comp.type()),
1278  member_exprt(rhs, comp.get_name(), comp.type()));
1279  }
1280  }
1281 
1282  return target;
1283 }
1284 
1286  goto_programt &dest,
1287  goto_programt::targett target,
1288  const exprt &lhs, const if_exprt &rhs)
1289 {
1290  goto_programt tmp;
1291 
1292  goto_programt::targett goto_else =
1294  boolean_negate(rhs.cond()), target->source_location));
1295  goto_programt::targett goto_out = tmp.add(
1297  goto_programt::targett else_target =
1298  tmp.add(goto_programt::make_skip(target->source_location));
1299  goto_programt::targett out_target =
1300  tmp.add(goto_programt::make_skip(target->source_location));
1301 
1302  goto_else->complete_goto(else_target);
1303  goto_out->complete_goto(out_target);
1304 
1305  value_assignments(tmp, goto_out, lhs, rhs.true_case());
1306  value_assignments(tmp, else_target, lhs, rhs.false_case());
1307 
1308  goto_programt::targett last=target;
1309  ++last;
1310  dest.insert_before_swap(target, tmp);
1311  --last;
1312 
1313  return last;
1314 }
1315 
1317  goto_programt &dest,
1318  goto_programt::targett target,
1319  const exprt &lhs, const exprt &rhs)
1320 {
1321  // copy all the values
1322  goto_programt tmp;
1323 
1324  {
1326  member(lhs, whatt::IS_ZERO),
1327  member(rhs, whatt::IS_ZERO),
1328  target->source_location));
1329  assignment->code_nonconst().add_source_location() = target->source_location;
1330  }
1331 
1332  {
1334  member(lhs, whatt::LENGTH),
1335  member(rhs, whatt::LENGTH),
1336  target->source_location));
1337  assignment->code_nonconst().add_source_location() = target->source_location;
1338  }
1339 
1340  {
1342  member(lhs, whatt::SIZE),
1343  member(rhs, whatt::SIZE),
1344  target->source_location));
1345  assignment->code_nonconst().add_source_location() = target->source_location;
1346  }
1347 
1348  goto_programt::targett last=target;
1349  ++last;
1350  dest.insert_before_swap(target, tmp);
1351  --last;
1352 
1353  return last;
1354 }
1355 
1357 {
1358  if(a.is_nil())
1359  return a;
1360 
1363  "either the expression is not a string or it is not a pointer to one");
1364 
1365  exprt struct_op=
1366  a.type().id()==ID_pointer?
1368 
1369  irep_idt component_name;
1370 
1371  switch(what)
1372  {
1373  case whatt::IS_ZERO: component_name="is_zero"; break;
1374  case whatt::SIZE: component_name="size"; break;
1375  case whatt::LENGTH: component_name="length"; break;
1376  }
1377 
1378  return member_exprt(struct_op, component_name, build_type(what));
1379 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
bitvector_typet index_type()
Definition: c_types.cpp:16
unsignedbv_typet size_type()
Definition: c_types.cpp:58
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
typet c_bool_type()
Definition: c_types.cpp:108
Operator to return the address of an object.
Definition: pointer_expr.h:341
exprt & object()
Definition: pointer_expr.h:350
Array constructor from list of elements.
Definition: std_expr.h:1467
Array constructor from single element.
Definition: std_expr.h:1402
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:771
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
exprt & op0()
Definition: expr.h:99
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
A codet representing an assignment in the program.
Definition: std_code.h:293
exprt::operandst argumentst
Definition: std_code.h:1222
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const parameterst & parameters() const
Definition: std_types.h:655
Operator to dereference a pointer.
Definition: pointer_expr.h:628
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:28
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
codet & code_nonconst()
Set the code represented by this instruction.
Definition: goto_program.h:191
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
void clear()
Clear the goto program.
Definition: goto_program.h:847
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:673
instructionst::iterator targett
Definition: goto_program.h:646
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:841
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:978
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
Definition: std_expr.h:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
exprt & cond()
Definition: std_expr.h:2189
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
void swap(irept &irep)
Definition: irep.h:453
bool is_nil() const
Definition: irep.h:387
Extract member of struct or union.
Definition: std_expr.h:2613
const exprt & struct_op() const
Definition: std_expr.h:2643
irep_idt get_component_name() const
Definition: std_expr.h:2627
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
Binary minus.
Definition: std_expr.h:973
exprt & op2()
Definition: std_expr.h:856
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2820
The plus expression Associativity is not specified.
Definition: std_expr.h:914
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
Replace all uses of char * by a struct that carries that string, and also the underlying allocation a...
goto_programt::targett abstract(goto_programt &dest, goto_programt::targett it)
goto_programt::targett value_assignments_if(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
goto_programt::targett value_assignments_string_struct(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
void declare_define_locals(goto_programt &dest)
exprt make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
bool build_symbol_constant(const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
static typet build_type(whatt what)
goto_programt::targett abstract_pointer_assign(goto_programt &dest, goto_programt::targett it)
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
exprt build_unknown(whatt what, bool write)
string_abstractiont(symbol_tablet &_symbol_table, message_handlert &_message_handler)
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
bool is_ptr_string_struct(const typet &type) const
message_handlert & message_handler
::std::map< typet, typet > abstraction_types_mapt
goto_programt initialization
goto_programt::targett value_assignments(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
symbol_exprt add_dummy_symbol_and_value(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const irep_idt &component_name, const typet &type, const typet &source_type)
bool build_wrap(const exprt &object, exprt &dest, bool write)
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
bool build_array(const array_exprt &object, exprt &dest, bool write)
void apply(goto_modelt &goto_model)
Apply string abstraction to goto_model.
bool build_symbol(const symbol_exprt &sym, exprt &dest)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
void operator()(goto_programt &dest)
abstraction_types_mapt abstraction_types_map
goto_programt::targett char_assign(goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
code_typet::parametert add_parameter(const symbolt &fct_symbol, const typet &type, const irep_idt &identifier)
bool build_pointer(const exprt &object, exprt &dest, bool write)
void abstract_function_call(goto_programt::targett it)
exprt member(const exprt &a, whatt what)
static bool has_string_macros(const exprt &expr)
void make_type(exprt &dest, const typet &type)
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
void make_decl_and_def(goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
void add_str_parameters(symbolt &fct_symbol, goto_functiont::parameter_identifierst &parameter_identifiers)
bool is_char_type(const typet &type) const
symbol_tablet & symbol_table
const typet & build_abstraction_type(const typet &type)
Struct constructor from list of elements.
Definition: std_expr.h:1668
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
std::vector< irep_idt > sorted_symbol_names() const
Build and return a lexicographically sorted vector of symbol names from all symbols stored in this sy...
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_file_local
Definition: symbol.h:66
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:65
bool is_parameter
Definition: symbol.h:67
bool is_thread_local
Definition: symbol.h:65
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2802
Semantic type conversion.
Definition: std_expr.h:1866
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
source_locationt & add_source_location()
Definition: type.h:76
const exprt & op() const
Definition: std_expr.h:293
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:125
Deprecated expression utility functions.
int main(int argc, char *argv[])
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
@ FUNCTION_CALL
Definition: goto_program.h:47
@ ATOMIC_END
Definition: goto_program.h:42
@ DEAD
Definition: goto_program.h:46
@ END_FUNCTION
Definition: goto_program.h:40
@ ASSIGN
Definition: goto_program.h:44
@ ASSERT
Definition: goto_program.h:34
@ SET_RETURN_VALUE
Definition: goto_program.h:43
@ ATOMIC_BEGIN
Definition: goto_program.h:41
@ CATCH
Definition: goto_program.h:49
@ END_THREAD
Definition: goto_program.h:38
@ SKIP
Definition: goto_program.h:36
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:31
@ START_THREAD
Definition: goto_program.h:37
@ THROW
Definition: goto_program.h:48
@ DECL
Definition: goto_program.h:45
@ OTHER
Definition: goto_program.h:35
@ GOTO
Definition: goto_program.h:32
@ INCOMPLETE_GOTO
Definition: goto_program.h:50
@ ASSUME
Definition: goto_program.h:33
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
exprt pointer_offset(const exprt &pointer)
Various predicates over pointers in programs.
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1497
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1691
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
static bool is_ptr_argument(const typet &type)
String Abstraction.
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.