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