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