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