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