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>
20 #include <util/fresh_symbol.h>
21 #include <util/message.h>
22 #include <util/pointer_expr.h>
24 #include <util/string_constant.h>
25 
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 RETURN:
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  code_assignt assign = target->get_assign();
521 
522  exprt &lhs = assign.lhs();
523  exprt &rhs = assign.rhs();
524 
525  if(has_string_macros(lhs))
526  {
527  replace_string_macros(lhs, true, target->source_location);
528  move_lhs_arithmetic(lhs, rhs);
529  }
530 
531  if(has_string_macros(rhs))
532  replace_string_macros(rhs, false, target->source_location);
533 
534  target->set_assign(assign);
535  }
536 
537  const typet &type = target->get_assign().lhs().type();
538 
539  if(type.id() == ID_pointer || type.id() == ID_array)
540  return abstract_pointer_assign(dest, target);
541  else if(is_char_type(type))
542  return abstract_char_assign(dest, target);
543 
544  return target;
545 }
546 
548  goto_programt::targett target)
549 {
550  code_function_callt call = target->get_function_call();
551 
552  code_function_callt::argumentst &arguments=call.arguments();
554 
555  for(const auto &arg : arguments)
556  {
557  const typet &abstract_type = build_abstraction_type(arg.type());
558  if(abstract_type.is_nil())
559  continue;
560 
561  str_args.push_back(exprt());
562  // if function takes void*, build for `arg` will fail if actual parameter
563  // is of some other pointer type; then just introduce an unknown
564  if(build_wrap(arg, str_args.back(), false))
565  str_args.back()=build_unknown(abstract_type, false);
566  // array -> pointer translation
567  if(str_args.back().type().id()==ID_array &&
568  abstract_type.id()==ID_pointer)
569  {
570  INVARIANT(
571  str_args.back().type().subtype() == abstract_type.subtype(),
572  "argument array type differs from formal parameter pointer type");
573 
574  index_exprt idx(str_args.back(), from_integer(0, index_type()));
575  // disable bounds check on that one
576  idx.set(ID_C_bounds_check, false);
577 
578  str_args.back()=address_of_exprt(idx);
579  }
580 
581  if(!is_ptr_argument(abstract_type))
582  str_args.back()=address_of_exprt(str_args.back());
583  }
584 
585  if(!str_args.empty())
586  {
587  arguments.insert(arguments.end(), str_args.begin(), str_args.end());
588 
589  code_typet::parameterst &parameters =
590  to_code_type(call.function().type()).parameters();
591  for(const auto &arg : str_args)
592  parameters.push_back(code_typet::parametert{arg.type()});
593 
594  target->set_function_call(call);
595  }
596 }
597 
599 {
600  if(expr.id()=="is_zero_string" ||
601  expr.id()=="zero_string_length" ||
602  expr.id()=="buffer_size")
603  return true;
604 
605  forall_operands(it, expr)
606  if(has_string_macros(*it))
607  return true;
608 
609  return false;
610 }
611 
613  exprt &expr,
614  bool lhs,
615  const source_locationt &source_location)
616 {
617  if(expr.id()=="is_zero_string")
618  {
619  PRECONDITION(expr.operands().size() == 1);
620  exprt tmp =
621  build(to_unary_expr(expr).op(), whatt::IS_ZERO, lhs, source_location);
622  expr.swap(tmp);
623  }
624  else if(expr.id()=="zero_string_length")
625  {
626  PRECONDITION(expr.operands().size() == 1);
627  exprt tmp =
628  build(to_unary_expr(expr).op(), whatt::LENGTH, lhs, source_location);
629  expr.swap(tmp);
630  }
631  else if(expr.id()=="buffer_size")
632  {
633  PRECONDITION(expr.operands().size() == 1);
634  exprt tmp =
635  build(to_unary_expr(expr).op(), whatt::SIZE, false, source_location);
636  expr.swap(tmp);
637  }
638  else
639  Forall_operands(it, expr)
640  replace_string_macros(*it, lhs, source_location);
641 }
642 
644  const exprt &pointer,
645  whatt what,
646  bool write,
647  const source_locationt &source_location)
648 {
649  // take care of pointer typecasts now
650  if(pointer.id()==ID_typecast)
651  {
652  // cast from another pointer type?
653  if(to_typecast_expr(pointer).op().type().id() != ID_pointer)
654  return build_unknown(what, write);
655 
656  // recursive call
657  return build(to_typecast_expr(pointer).op(), what, write, source_location);
658  }
659 
660  exprt str_struct;
661  if(build_wrap(pointer, str_struct, write))
662  UNREACHABLE;
663 
664  exprt result=member(str_struct, what);
665 
666  if(what==whatt::LENGTH || what==whatt::SIZE)
667  {
668  // adjust for offset
669  exprt offset = pointer_offset(pointer);
670  typet result_type = result.type();
672  minus_exprt(
673  typecast_exprt::conditional_cast(result, offset.type()), offset),
674  result_type);
675  }
676 
677  return result;
678 }
679 
681 {
682  const typet &eff_type=ns.follow(type);
683  abstraction_types_mapt::const_iterator map_entry=
684  abstraction_types_map.find(eff_type);
685  if(map_entry!=abstraction_types_map.end())
686  return map_entry->second;
687 
689  tmp.swap(abstraction_types_map);
690  build_abstraction_type_rec(eff_type, tmp);
691 
692  abstraction_types_map.swap(tmp);
693  map_entry=tmp.find(eff_type);
694  CHECK_RETURN(map_entry != tmp.end());
695  return abstraction_types_map.insert(
696  std::make_pair(eff_type, map_entry->second)).first->second;
697 }
698 
700  const abstraction_types_mapt &known)
701 {
702  const typet &eff_type=ns.follow(type);
703  abstraction_types_mapt::const_iterator known_entry=known.find(eff_type);
704  if(known_entry!=known.end())
705  return known_entry->second;
706 
707  ::std::pair<abstraction_types_mapt::iterator, bool> map_entry(
708  abstraction_types_map.insert(::std::make_pair(eff_type, typet{ID_nil})));
709  if(!map_entry.second)
710  return map_entry.first->second;
711 
712  if(eff_type.id()==ID_array || eff_type.id()==ID_pointer)
713  {
714  // char* or void* or char[]
715  if(is_char_type(eff_type.subtype()) ||
716  eff_type.subtype().id()==ID_empty)
717  map_entry.first->second=pointer_type(string_struct);
718  else
719  {
720  const typet &subt=build_abstraction_type_rec(eff_type.subtype(), known);
721  if(!subt.is_nil())
722  {
723  if(eff_type.id()==ID_array)
724  map_entry.first->second=
725  array_typet(subt, to_array_type(eff_type).size());
726  else
727  map_entry.first->second=pointer_type(subt);
728  }
729  }
730  }
731  else if(eff_type.id()==ID_struct || eff_type.id()==ID_union)
732  {
733  const struct_union_typet &struct_union_type=to_struct_union_type(eff_type);
734 
736  for(const auto &comp : struct_union_type.components())
737  {
738  if(comp.get_anonymous())
739  continue;
740  typet subt=build_abstraction_type_rec(comp.type(), known);
741  if(subt.is_nil())
742  // also precludes structs with pointers to the same datatype
743  continue;
744 
745  new_comp.push_back(struct_union_typet::componentt());
746  new_comp.back().set_name(comp.get_name());
747  new_comp.back().set_pretty_name(comp.get_pretty_name());
748  new_comp.back().type()=subt;
749  }
750  if(!new_comp.empty())
751  {
752  struct_union_typet t(eff_type.id());
753  t.components().swap(new_comp);
754  map_entry.first->second=t;
755  }
756  }
757 
758  return map_entry.first->second;
759 }
760 
761 bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
762 {
763  const typet &abstract_type=build_abstraction_type(object.type());
764  if(abstract_type.is_nil())
765  return true;
766 
767  if(object.id()==ID_typecast)
768  {
769  if(build(to_typecast_expr(object).op(), dest, write))
770  return true;
771 
772  return dest.type() != abstract_type ||
773  (dest.type().id() == ID_array && abstract_type.id() == ID_pointer &&
774  dest.type().subtype() == abstract_type.subtype());
775  }
776 
777  if(object.id()==ID_string_constant)
778  {
779  const std::string &str_value =
780  id2string(to_string_constant(object).get_value());
781  // make sure we handle the case of a string constant with string-terminating
782  // \0 in it
783  const std::size_t str_len =
784  std::min(str_value.size(), str_value.find('\0'));
785  return build_symbol_constant(str_len, str_len+1, dest);
786  }
787 
788  if(object.id()==ID_array && is_char_type(object.type().subtype()))
789  return build_array(to_array_expr(object), dest, write);
790 
791  // other constants aren't useful
792  if(object.is_constant())
793  return true;
794 
795  if(object.id()==ID_symbol)
796  return build_symbol(to_symbol_expr(object), dest);
797 
798  if(object.id()==ID_if)
799  return build_if(to_if_expr(object), dest, write);
800 
801  if(object.id()==ID_member)
802  {
803  const member_exprt &o_mem=to_member_expr(object);
804  dest=member_exprt(exprt(), o_mem.get_component_name(), abstract_type);
805  return build_wrap(
806  o_mem.struct_op(), to_member_expr(dest).compound(), write);
807  }
808 
809  if(object.id()==ID_dereference)
810  {
811  const dereference_exprt &o_deref=to_dereference_expr(object);
812  dest=dereference_exprt(exprt(), abstract_type);
813  return build_wrap(
814  o_deref.pointer(), to_dereference_expr(dest).pointer(), write);
815  }
816 
817  if(object.id()==ID_index)
818  {
819  const index_exprt &o_index=to_index_expr(object);
820  dest=index_exprt(exprt(), o_index.index(), abstract_type);
821  return build_wrap(o_index.array(), to_index_expr(dest).array(), write);
822  }
823 
824  // handle pointer stuff
825  if(object.type().id()==ID_pointer)
826  return build_pointer(object, dest, write);
827 
828  return true;
829 }
830 
832  exprt &dest, bool write)
833 {
834  if_exprt new_if(o_if.cond(), exprt(), exprt());
835 
836  // recursive calls
837  bool op1_err=build_wrap(o_if.true_case(), new_if.true_case(), write);
838  bool op2_err=build_wrap(o_if.false_case(), new_if.false_case(), write);
839  if(op1_err && op2_err)
840  return true;
841  // at least one of them gave proper results
842  if(op1_err)
843  {
844  new_if.type()=new_if.false_case().type();
845  new_if.true_case()=build_unknown(new_if.type(), write);
846  }
847  else if(op2_err)
848  {
849  new_if.type()=new_if.true_case().type();
850  new_if.false_case()=build_unknown(new_if.type(), write);
851  }
852  else
853  new_if.type()=new_if.true_case().type();
854 
855  dest.swap(new_if);
856  return false;
857 }
858 
860  exprt &dest, bool write)
861 {
862  PRECONDITION(is_char_type(object.type().subtype()));
863 
864  // writing is invalid
865  if(write)
866  return true;
867 
868  const exprt &a_size=to_array_type(object.type()).size();
869  const auto size = numeric_cast<mp_integer>(a_size);
870  // don't do anything, if we cannot determine the size
871  if(!size.has_value())
872  return true;
873  INVARIANT(
874  *size == object.operands().size(),
875  "wrong number of array object arguments");
876 
877  exprt::operandst::const_iterator it=object.operands().begin();
878  for(mp_integer i = 0; i < *size; ++i, ++it)
879  if(it->is_zero())
880  return build_symbol_constant(i, *size, dest);
881 
882  return true;
883 }
884 
886  exprt &dest, bool write)
887 {
888  PRECONDITION(object.type().id() == ID_pointer);
889 
890  pointer_arithmetict ptr(object);
891  if(ptr.pointer.id()==ID_address_of)
892  {
894 
895  if(a.object().id()==ID_index)
896  return build_wrap(to_index_expr(a.object()).array(), dest, write);
897 
898  // writing is invalid
899  if(write)
900  return true;
901 
902  if(build_wrap(a.object(), dest, write))
903  return true;
904  dest=address_of_exprt(dest);
905  return false;
906  }
907  else if(ptr.pointer.id()==ID_symbol &&
908  is_char_type(object.type().subtype()))
909  // recursive call; offset will be handled by pointer_offset in SIZE/LENGTH
910  // checks
911  return build_wrap(ptr.pointer, dest, write);
912 
913  // we don't handle other pointer arithmetic
914  return true;
915 }
916 
918 {
919  typet type=build_type(what);
920 
921  if(write)
922  return exprt(ID_null_object, type);
923 
924  exprt result;
925 
926  switch(what)
927  {
928  case whatt::IS_ZERO:
929  result = from_integer(0, type);
930  break;
931 
932  case whatt::LENGTH:
933  case whatt::SIZE:
934  result = side_effect_expr_nondett(type, source_locationt());
935  break;
936  }
937 
938  return result;
939 }
940 
942 {
943  if(write)
944  return exprt(ID_null_object, type);
945 
946  // create an uninitialized dummy symbol
947  // because of a lack of contextual information we can't build a nice name
948  // here, but moving that into locals should suffice for proper operation
949  irep_idt identifier=
950  "$tmp::nondet_str#str$"+std::to_string(++temporary_counter);
951  // ensure decl and initialization
952  locals[identifier]=identifier;
953 
954  auxiliary_symbolt new_symbol;
955  new_symbol.type=type;
956  new_symbol.value.make_nil();
957  new_symbol.name=identifier;
958  new_symbol.module="$tmp";
959  new_symbol.base_name=identifier;
960  new_symbol.mode=ID_C;
961  new_symbol.pretty_name=identifier;
962 
963  symbol_table.insert(std::move(new_symbol));
964 
965  return ns.lookup(identifier).symbol_expr();
966 }
967 
969 {
970  const symbolt &symbol=ns.lookup(sym.get_identifier());
971 
972  const typet &abstract_type=build_abstraction_type(symbol.type);
973  CHECK_RETURN(!abstract_type.is_nil());
974 
975  irep_idt identifier;
976 
977  if(symbol.is_parameter)
978  {
979  const auto parameter_map_entry = parameter_map.find(symbol.name);
980  if(parameter_map_entry == parameter_map.end())
981  return true;
982  identifier = parameter_map_entry->second;
983  }
984  else if(symbol.is_static_lifetime)
985  {
986  std::string sym_suffix_before = sym_suffix;
987  sym_suffix = "#str";
988  identifier = id2string(symbol.name) + sym_suffix;
989  if(symbol_table.symbols.find(identifier) == symbol_table.symbols.end())
990  build_new_symbol(symbol, identifier, abstract_type);
991  sym_suffix = sym_suffix_before;
992  }
993  else
994  {
995  identifier=id2string(symbol.name)+sym_suffix;
996  if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
997  build_new_symbol(symbol, identifier, abstract_type);
998  }
999 
1000  const symbolt &str_symbol=ns.lookup(identifier);
1001  dest=str_symbol.symbol_expr();
1002  if(symbol.is_parameter && !is_ptr_argument(abstract_type))
1003  dest = dereference_exprt{dest};
1004 
1005  return false;
1006 }
1007 
1009  const irep_idt &identifier, const typet &type)
1010 {
1011  if(!symbol.is_static_lifetime)
1012  locals[symbol.name]=identifier;
1013 
1014  auxiliary_symbolt new_symbol;
1015  new_symbol.type=type;
1016  new_symbol.value.make_nil();
1017  new_symbol.location=symbol.location;
1018  new_symbol.name=identifier;
1019  new_symbol.module=symbol.module;
1020  new_symbol.base_name=id2string(symbol.base_name)+sym_suffix;
1021  new_symbol.mode=symbol.mode;
1022  new_symbol.pretty_name=
1023  id2string(symbol.pretty_name.empty()?symbol.base_name:symbol.pretty_name)+
1024  sym_suffix;
1025  new_symbol.is_static_lifetime=symbol.is_static_lifetime;
1026  new_symbol.is_thread_local=symbol.is_thread_local;
1027 
1028  symbol_table.insert(std::move(new_symbol));
1029 
1030  if(symbol.is_static_lifetime)
1031  {
1032  goto_programt::targett dummy_loc =
1034  dummy_loc->source_location=symbol.location;
1035  make_decl_and_def(initialization, dummy_loc, identifier, symbol.name);
1036  initialization.instructions.erase(dummy_loc);
1037  }
1038 }
1039 
1041  const mp_integer &zero_length,
1042  const mp_integer &buf_size,
1043  exprt &dest)
1044 {
1045  irep_idt base="$string_constant_str_"+integer2string(zero_length)
1046  +"_"+integer2string(buf_size);
1047  irep_idt identifier="string_abstraction::"+id2string(base);
1048 
1049  if(symbol_table.symbols.find(identifier)==
1050  symbol_table.symbols.end())
1051  {
1052  auxiliary_symbolt new_symbol;
1053  new_symbol.type=string_struct;
1054  new_symbol.value.make_nil();
1055  new_symbol.name=identifier;
1056  new_symbol.base_name=base;
1057  new_symbol.mode=ID_C;
1058  new_symbol.pretty_name=base;
1059  new_symbol.is_static_lifetime=true;
1060  new_symbol.is_thread_local=false;
1061  new_symbol.is_file_local=false;
1062 
1063  {
1064  struct_exprt value(
1066  from_integer(zero_length, build_type(whatt::LENGTH)),
1067  from_integer(buf_size, build_type(whatt::SIZE))},
1068  string_struct);
1069 
1070  // initialization
1072  code_assignt(new_symbol.symbol_expr(), value)));
1073  }
1074 
1075  symbol_table.insert(std::move(new_symbol));
1076  }
1077 
1078  dest=address_of_exprt(symbol_exprt(identifier, string_struct));
1079 
1080  return false;
1081 }
1082 
1084 {
1085  while(lhs.id() == ID_typecast)
1086  {
1087  typecast_exprt lhs_tc = to_typecast_expr(lhs);
1088  rhs = typecast_exprt::conditional_cast(rhs, lhs_tc.op().type());
1089  lhs.swap(lhs_tc.op());
1090  }
1091 
1092  if(lhs.id()==ID_minus)
1093  {
1094  // move op1 to rhs
1095  exprt rest = to_minus_expr(lhs).op0();
1096  rhs = plus_exprt(rhs, to_minus_expr(lhs).op1());
1097  rhs.type()=lhs.type();
1098  lhs=rest;
1099  }
1100 
1101  while(lhs.id() == ID_typecast)
1102  {
1103  typecast_exprt lhs_tc = to_typecast_expr(lhs);
1104  rhs = typecast_exprt::conditional_cast(rhs, lhs_tc.op().type());
1105  lhs.swap(lhs_tc.op());
1106  }
1107 }
1108 
1110  goto_programt &dest,
1111  const goto_programt::targett target)
1112 {
1113  const code_assignt &assign = target->get_assign();
1114 
1115  const exprt &lhs = assign.lhs();
1116  const exprt rhs = assign.rhs();
1117  const exprt *rhsp = &(assign.rhs());
1118 
1119  while(rhsp->id()==ID_typecast)
1120  rhsp = &(to_typecast_expr(*rhsp).op());
1121 
1122  const typet &abstract_type=build_abstraction_type(lhs.type());
1123  if(abstract_type.is_nil())
1124  return target;
1125 
1126  exprt new_lhs, new_rhs;
1127  if(build_wrap(lhs, new_lhs, true))
1128  return target;
1129 
1130  bool unknown=(abstract_type!=build_abstraction_type(rhsp->type()) ||
1131  build_wrap(rhs, new_rhs, false));
1132  if(unknown)
1133  new_rhs=build_unknown(abstract_type, false);
1134 
1135  if(lhs.type().id()==ID_pointer && !unknown)
1136  {
1137  goto_programt::instructiont assignment;
1138  assignment = goto_programt::make_assignment(
1139  code_assignt(new_lhs, new_rhs), target->source_location);
1140  assignment.code_nonconst().add_source_location() = target->source_location;
1141  dest.insert_before_swap(target, assignment);
1142 
1143  return std::next(target);
1144  }
1145  else
1146  {
1147  return value_assignments(dest, target, new_lhs, new_rhs);
1148  }
1149 }
1150 
1152  goto_programt &dest,
1153  goto_programt::targett target)
1154 {
1155  const code_assignt &assign = target->get_assign();
1156 
1157  const exprt &lhs = assign.lhs();
1158  const exprt *rhsp = &(assign.rhs());
1159 
1160  while(rhsp->id()==ID_typecast)
1161  rhsp = &(to_typecast_expr(*rhsp).op());
1162 
1163  // we only care if the constant zero is assigned
1164  if(!rhsp->is_zero())
1165  return target;
1166 
1167  // index into a character array
1168  if(lhs.id()==ID_index)
1169  {
1170  const index_exprt &i_lhs=to_index_expr(lhs);
1171 
1172  exprt new_lhs;
1173  if(!build_wrap(i_lhs.array(), new_lhs, true))
1174  {
1175  exprt i2=member(new_lhs, whatt::LENGTH);
1176  INVARIANT(
1177  i2.is_not_nil(),
1178  "failed to create length-component for the left-hand-side");
1179 
1180  exprt new_length=i_lhs.index();
1181  make_type(new_length, i2.type());
1182 
1183  if_exprt min_expr(binary_relation_exprt(new_length, ID_lt, i2),
1184  new_length, i2);
1185 
1186  return char_assign(dest, target, new_lhs, i2, min_expr);
1187  }
1188  }
1189  else if(lhs.id()==ID_dereference)
1190  {
1191  pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
1192  exprt new_lhs;
1193  if(!build_wrap(ptr.pointer, new_lhs, true))
1194  {
1195  const exprt i2=member(new_lhs, whatt::LENGTH);
1196  INVARIANT(
1197  i2.is_not_nil(),
1198  "failed to create length-component for the left-hand-side");
1199 
1201  return
1202  char_assign(
1203  dest,
1204  target,
1205  new_lhs,
1206  i2,
1207  ptr.offset.is_nil()?
1209  ptr.offset);
1210  }
1211  }
1212 
1213  return target;
1214 }
1215 
1217  goto_programt &dest,
1218  goto_programt::targett target,
1219  const exprt &new_lhs,
1220  const exprt &lhs,
1221  const exprt &rhs)
1222 {
1223  goto_programt tmp;
1224 
1225  const exprt i1=member(new_lhs, whatt::IS_ZERO);
1226  INVARIANT(
1227  i1.is_not_nil(),
1228  "failed to create is_zero-component for the left-hand-side");
1229 
1231  code_assignt(i1, from_integer(1, i1.type())), target->source_location));
1232  assignment1->code_nonconst().add_source_location() = target->source_location;
1233 
1235  code_assignt(lhs, rhs), target->source_location));
1236  assignment2->code_nonconst().add_source_location() = target->source_location;
1237 
1239  assignment2->code_nonconst().op0(), assignment2->code_nonconst().op1());
1240 
1241  dest.insert_before_swap(target, tmp);
1242  ++target;
1243  ++target;
1244 
1245  return target;
1246 }
1247 
1249  goto_programt &dest,
1250  goto_programt::targett target,
1251  const exprt &lhs,
1252  const exprt &rhs)
1253 {
1254  if(rhs.id()==ID_if)
1255  return value_assignments_if(dest, target, lhs, to_if_expr(rhs));
1256 
1257  PRECONDITION(lhs.type() == rhs.type());
1258 
1259  if(lhs.type().id()==ID_array)
1260  {
1261  const exprt &a_size=to_array_type(lhs.type()).size();
1262  const auto size = numeric_cast<mp_integer>(a_size);
1263  // don't do anything, if we cannot determine the size
1264  if(!size.has_value())
1265  return target;
1266  for(mp_integer i = 0; i < *size; ++i)
1267  target=value_assignments(dest, target,
1268  index_exprt(lhs, from_integer(i, a_size.type())),
1269  index_exprt(rhs, from_integer(i, a_size.type())));
1270  }
1271  else if(lhs.type().id() == ID_pointer)
1272  return value_assignments(
1273  dest, target, dereference_exprt{lhs}, dereference_exprt{rhs});
1274  else if(lhs.type()==string_struct)
1275  return value_assignments_string_struct(dest, target, lhs, rhs);
1276  else if(lhs.type().id()==ID_struct || lhs.type().id()==ID_union)
1277  {
1278  const struct_union_typet &struct_union_type=
1279  to_struct_union_type(lhs.type());
1280 
1281  for(const auto &comp : struct_union_type.components())
1282  {
1283  INVARIANT(
1284  !comp.get_name().empty(), "struct/union components must have a name");
1285 
1286  target=value_assignments(dest, target,
1287  member_exprt(lhs, comp.get_name(), comp.type()),
1288  member_exprt(rhs, comp.get_name(), comp.type()));
1289  }
1290  }
1291 
1292  return target;
1293 }
1294 
1296  goto_programt &dest,
1297  goto_programt::targett target,
1298  const exprt &lhs, const if_exprt &rhs)
1299 {
1300  goto_programt tmp;
1301 
1302  goto_programt::targett goto_else =
1304  boolean_negate(rhs.cond()), target->source_location));
1305  goto_programt::targett goto_out = tmp.add(
1307  goto_programt::targett else_target =
1308  tmp.add(goto_programt::make_skip(target->source_location));
1309  goto_programt::targett out_target =
1310  tmp.add(goto_programt::make_skip(target->source_location));
1311 
1312  goto_else->complete_goto(else_target);
1313  goto_out->complete_goto(out_target);
1314 
1315  value_assignments(tmp, goto_out, lhs, rhs.true_case());
1316  value_assignments(tmp, else_target, lhs, rhs.false_case());
1317 
1318  goto_programt::targett last=target;
1319  ++last;
1320  dest.insert_before_swap(target, tmp);
1321  --last;
1322 
1323  return last;
1324 }
1325 
1327  goto_programt &dest,
1328  goto_programt::targett target,
1329  const exprt &lhs, const exprt &rhs)
1330 {
1331  // copy all the values
1332  goto_programt tmp;
1333 
1334  {
1336  member(lhs, whatt::IS_ZERO),
1337  member(rhs, whatt::IS_ZERO),
1338  target->source_location));
1339  assignment->code_nonconst().add_source_location() = target->source_location;
1340  }
1341 
1342  {
1344  member(lhs, whatt::LENGTH),
1345  member(rhs, whatt::LENGTH),
1346  target->source_location));
1347  assignment->code_nonconst().add_source_location() = target->source_location;
1348  }
1349 
1350  {
1352  member(lhs, whatt::SIZE),
1353  member(rhs, whatt::SIZE),
1354  target->source_location));
1355  assignment->code_nonconst().add_source_location() = target->source_location;
1356  }
1357 
1358  goto_programt::targett last=target;
1359  ++last;
1360  dest.insert_before_swap(target, tmp);
1361  --last;
1362 
1363  return last;
1364 }
1365 
1367 {
1368  if(a.is_nil())
1369  return a;
1370 
1373  "either the expression is not a string or it is not a pointer to one");
1374 
1375  exprt struct_op=
1376  a.type().id()==ID_pointer?
1378 
1379  irep_idt component_name;
1380 
1381  switch(what)
1382  {
1383  case whatt::IS_ZERO: component_name="is_zero"; break;
1384  case whatt::SIZE: component_name="size"; break;
1385  case whatt::LENGTH: component_name="length"; break;
1386  }
1387 
1388  return member_exprt(struct_op, component_name, build_type(what));
1389 }
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:1185
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:141
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:86
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1788
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:328
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
string_abstractiont::member
exprt member(const exprt &a, whatt what)
Definition: string_abstraction.cpp:1366
string_abstractiont::build_type
static typet build_type(whatt what)
Definition: string_abstraction.cpp:105
string_abstractiont::build
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
Definition: string_abstraction.cpp:643
string_abstractiont::abstract_assign
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
Definition: string_abstraction.cpp:515
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
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:1411
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:339
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:208
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:442
pointer_arithmetic.h
irept::make_nil
void make_nil()
Definition: irep.h:465
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:535
fresh_symbol.h
Fresh auxiliary symbol creation.
string_abstractiont::build_pointer
bool build_pointer(const exprt &object, exprt &dest, bool write)
Definition: string_abstraction.cpp:885
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
string_abstractiont::abstraction_types_map
abstraction_types_mapt abstraction_types_map
Definition: string_abstraction.h:58
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:56
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
pointer_predicates.h
Various predicates over pointers in programs.
string_abstractiont::string_struct
typet string_struct
Definition: string_abstraction.h:147
string_abstractiont::whatt::LENGTH
@ LENGTH
string_abstractiont::locals
localst locals
Definition: string_abstraction.h:151
c_bool_type
typet c_bool_type()
Definition: c_types.cpp:108
symbol_table_baset::sorted_symbol_names
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...
Definition: symbol_table_base.cpp:36
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
string_abstractiont::abstract
goto_programt::targett abstract(goto_programt &dest, goto_programt::targett it)
Definition: string_abstraction.cpp:462
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:670
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
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:134
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt
dstringt irep_idt
Definition: irep.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:147
string_abstractiont::build_abstraction_type_rec
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
Definition: string_abstraction.cpp:699
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:80
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:904
string_abstractiont::is_ptr_string_struct
bool is_ptr_string_struct(const typet &type) const
Definition: string_abstraction.cpp:59
string_abstractiont::add_parameter
code_typet::parametert add_parameter(const symbolt &fct_symbol, const typet &type, const irep_idt &identifier)
Definition: string_abstraction.cpp:213
string_abstractiont::abstract_function_call
void abstract_function_call(goto_programt::targett it)
Definition: string_abstraction.cpp:547
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
string_abstraction
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
Definition: string_abstraction.cpp:69
multi_ary_exprt::op2
exprt & op2()
Definition: std_expr.h:772
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:914
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:1008
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2123
string_abstractiont::abstract_char_assign
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
Definition: string_abstraction.cpp:1151
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:1248
string_abstractiont::make_type
void make_type(exprt &dest, const typet &type)
Definition: string_abstraction.h:80
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:69
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1582
array_typet::size
const exprt & size() const
Definition: std_types.h:765
string_abstractiont::whatt
whatt
Definition: string_abstraction.h:119
string_abstractiont::sym_suffix
std::string sym_suffix
Definition: string_abstraction.h:51
THROW
@ THROW
Definition: goto_program.h:51
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
string_abstractiont::abstraction_types_mapt
::std::map< typet, typet > abstraction_types_mapt
Definition: string_abstraction.h:57
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:141
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
GOTO
@ GOTO
Definition: goto_program.h:35
string_abstractiont::has_string_macros
static bool has_string_macros(const exprt &expr)
Definition: string_abstraction.cpp:598
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
string_abstractiont::symbol_table
symbol_tablet & symbol_table
Definition: string_abstraction.h:52
string_abstractiont
Replace all uses of char * by a struct that carries that string, and also the underlying allocation a...
Definition: string_abstraction.h:31
string_abstractiont::build_unknown
exprt build_unknown(whatt what, bool write)
Definition: string_abstraction.cpp:917
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
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
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:835
string_abstractiont::declare_define_locals
void declare_define_locals(goto_programt &dest)
Definition: string_abstraction.cpp:260
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2557
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1316
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:399
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:129
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:326
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
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:397
string_abstractiont::parameter_map
localst parameter_map
Definition: string_abstraction.h:152
index_exprt::index
exprt & index()
Definition: std_expr.h:1268
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:34
string_abstractiont::ns
namespacet ns
Definition: string_abstraction.h:53
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
irept::swap
void swap(irept &irep)
Definition: irep.h:453
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
string_abstractiont::build_new_symbol
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
Definition: string_abstraction.cpp:1008
code_typet
Base type of functions.
Definition: std_types.h:533
pointer_arithmetict::offset
exprt offset
Definition: pointer_arithmetic.h:17
OTHER
@ OTHER
Definition: goto_program.h:38
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
string_abstractiont::build_abstraction_type
const typet & build_abstraction_type(const typet &type)
Definition: string_abstraction.cpp:680
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
dstringt::empty
bool empty() const
Definition: dstring.h:88
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
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:1216
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:43
SKIP
@ SKIP
Definition: goto_program.h:39
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
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:1295
string_abstractiont::initialization
goto_programt initialization
Definition: string_abstraction.h:148
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:38
main
int main(int argc, char *argv[])
Definition: file_converter.cpp:41
minus_exprt
Binary minus.
Definition: std_expr.h:889
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:767
string_abstractiont::build_wrap
bool build_wrap(const exprt &object, exprt &dest, bool write)
Definition: string_abstraction.cpp:28
string_abstractiont::replace_string_macros
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
Definition: string_abstraction.cpp:612
is_ptr_argument
static bool is_ptr_argument(const typet &type)
Definition: string_abstraction.cpp:64
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:653
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:1968
RETURN
@ RETURN
Definition: goto_program.h:46
string_abstractiont::add_str_parameters
void add_str_parameters(symbolt &fct_symbol, goto_functiont::parameter_identifierst &parameter_identifiers)
Definition: string_abstraction.cpp:186
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:91
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
struct_union_typet::componentt
Definition: std_types.h:63
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
expr_util.h
Deprecated expression utility functions.
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
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:1109
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
CATCH
@ CATCH
Definition: goto_program.h:52
array_typet
Arrays with given size.
Definition: std_types.h:757
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2113
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
DECL
@ DECL
Definition: goto_program.h:48
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
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:54
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
ASSUME
@ ASSUME
Definition: goto_program.h:36
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
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:1040
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:2103
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
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:295
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
code_typet::parametert
Definition: std_types.h:550
START_THREAD
@ START_THREAD
Definition: goto_program.h:40
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:50
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
string_abstractiont::whatt::IS_ZERO
@ IS_ZERO
goto_functiont::parameter_identifierst
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:31
string_abstractiont::build_array
bool build_array(const array_exprt &object, exprt &dest, bool write)
Definition: string_abstraction.cpp:859
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:45
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2541
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
DEAD
@ DEAD
Definition: goto_program.h:49
exprt::operands
operandst & operands()
Definition: expr.h:96
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:1242
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:44
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:590
string_abstractiont::move_lhs_arithmetic
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
Definition: string_abstraction.cpp:1083
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
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
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
LOCATION
@ LOCATION
Definition: goto_program.h:42
ASSERT
@ ASSERT
Definition: goto_program.h:37
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
string_abstractiont::build_if
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
Definition: string_abstraction.cpp:831
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
string_abstractiont::message_handler
message_handlert & message_handler
Definition: string_abstraction.h:55
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
string_abstractiont::operator()
void operator()(goto_programt &dest)
Definition: string_abstraction.cpp:176
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:1381
goto_programt::instructiont::code_nonconst
codet & code_nonconst()
Set the code represented by this instruction.
Definition: goto_program.h:193
c_types.h
string_abstractiont::build_symbol
bool build_symbol(const symbol_exprt &sym, exprt &dest)
Definition: string_abstraction.cpp:968
get_fresh_aux_symbol
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 ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
END_THREAD
@ END_THREAD
Definition: goto_program.h:41
goto_programt::swap
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:761
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1605
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:1326
string_abstractiont::apply
void apply(goto_modelt &goto_model)
Apply string abstraction to goto_model.
Definition: string_abstraction.cpp:121
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106