cprover
value_set_fi.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set (Flow Insensitive, Sharing)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "value_set_fi.h"
13 
14 #include <iterator>
15 #include <ostream>
16 
17 #include <util/arith_tools.h>
18 #include <util/byte_operators.h>
19 #include <util/pointer_expr.h>
20 #include <util/prefix.h>
21 #include <util/simplify_expr.h>
22 #include <util/std_code.h>
23 #include <util/std_expr.h>
24 #include <util/symbol_table.h>
25 
26 #include <langapi/language_util.h>
27 #include <util/c_types.h>
28 
30 
33 
34 static const char *alloc_adapter_prefix="alloc_adaptor::";
35 
37  const namespacet &ns,
38  std::ostream &out) const
39 {
40  for(valuest::const_iterator
41  v_it=values.begin();
42  v_it!=values.end();
43  v_it++)
44  {
45  irep_idt identifier, display_name;
46 
47  const entryt &e=v_it->second;
48 
49  if(has_prefix(id2string(e.identifier), "value_set::dynamic_object"))
50  {
51  display_name=id2string(e.identifier)+e.suffix;
52  identifier.clear();
53  }
54  else
55  {
56  #if 0
57  const symbolt &symbol=ns.lookup(id2string(e.identifier));
58  display_name=symbol.display_name()+e.suffix;
59  identifier=symbol.name;
60  #else
61  identifier=id2string(e.identifier);
62  display_name=id2string(identifier)+e.suffix;
63  #endif
64  }
65 
66  out << display_name;
67 
68  out << " = { ";
69 
70  object_mapt object_map;
71  flatten(e, object_map);
72 
73  std::size_t width=0;
74 
75  const auto &entries = object_map.read();
76  for(object_map_dt::const_iterator o_it = entries.begin();
77  o_it != entries.end();
78  ++o_it)
79  {
80  const exprt &o=object_numbering[o_it->first];
81 
82  std::string result;
83 
84  if(o.id()==ID_invalid || o.id()==ID_unknown)
85  {
86  result="<";
87  result+=from_expr(ns, identifier, o);
88  result+=", *, "; // offset unknown
89  if(o.type().id()==ID_unknown)
90  result+='*';
91  else
92  result+=from_type(ns, identifier, o.type());
93  result+='>';
94  }
95  else
96  {
97  result="<"+from_expr(ns, identifier, o)+", ";
98 
99  if(o_it->second)
100  result += integer2string(*o_it->second);
101  else
102  result+='*';
103 
104  result+=", ";
105 
106  if(o.type().id()==ID_unknown)
107  result+='*';
108  else
109  result+=from_type(ns, identifier, o.type());
110 
111  result+='>';
112  }
113 
114  out << result;
115 
116  width+=result.size();
117 
119  next++;
120 
121  if(next != entries.end())
122  {
123  out << ", ";
124  if(width>=40)
125  out << "\n ";
126  }
127  }
128 
129  out << " } \n";
130  }
131 }
132 
134  const entryt &e,
135  object_mapt &dest) const
136 {
137  #if 0
138  std::cout << "FLATTEN: " << e.identifier << e.suffix << '\n';
139  #endif
140 
141  flatten_seent seen;
142  flatten_rec(e, dest, seen);
143 
144  #if 0
145  std::cout << "FLATTEN: Done.\n";
146  #endif
147 }
148 
150  const entryt &e,
151  object_mapt &dest,
152  flatten_seent &seen) const
153 {
154  #if 0
155  std::cout << "FLATTEN_REC: " << e.identifier << e.suffix << '\n';
156  #endif
157 
158  std::string identifier = id2string(e.identifier);
159  assert(seen.find(identifier + e.suffix)==seen.end());
160 
161  bool generalize_index = false;
162 
163  seen.insert(identifier + e.suffix);
164 
165  for(const auto &object_entry : e.object_map.read())
166  {
167  const exprt &o = object_numbering[object_entry.first];
168 
169  if(o.type().id()=="#REF#")
170  {
171  if(seen.find(o.get(ID_identifier))!=seen.end())
172  {
173  generalize_index = true;
174  continue;
175  }
176 
177  valuest::const_iterator fi = values.find(o.get(ID_identifier));
178  if(fi==values.end())
179  {
180  // this is some static object, keep it in.
181  const symbol_exprt se(o.get(ID_identifier), o.type().subtype());
182  insert(dest, se, 0);
183  }
184  else
185  {
186  object_mapt temp;
187  flatten_rec(fi->second, temp, seen);
188 
189  for(object_map_dt::iterator t_it=temp.write().begin();
190  t_it!=temp.write().end();
191  t_it++)
192  {
193  if(t_it->second && object_entry.second)
194  {
195  *t_it->second += *object_entry.second;
196  }
197  else
198  t_it->second.reset();
199  }
200 
201  for(const auto &object_entry : temp.read())
202  insert(dest, object_entry);
203  }
204  }
205  else
206  insert(dest, object_entry);
207  }
208 
209  if(generalize_index) // this means we had recursive symbols in there
210  {
211  for(auto &object_entry : dest.write())
212  object_entry.second.reset();
213  }
214 
215  seen.erase(identifier + e.suffix);
216 }
217 
219 {
220  const exprt &object=object_numbering[it.first];
221 
222  if(object.id()==ID_invalid ||
223  object.id()==ID_unknown)
224  return object;
225 
227 
228  od.object()=object;
229 
230  if(it.second)
231  od.offset() = from_integer(*it.second, index_type());
232 
233  od.type()=od.object().type();
234 
235  return std::move(od);
236 }
237 
239 {
240  UNREACHABLE;
241  bool result=false;
242 
243  for(valuest::const_iterator
244  it=new_values.begin();
245  it!=new_values.end();
246  it++)
247  {
248  valuest::iterator it2=values.find(it->first);
249 
250  if(it2==values.end())
251  {
252  // we always track these
253  if(has_prefix(id2string(it->second.identifier),
254  "value_set::dynamic_object") ||
255  has_prefix(id2string(it->second.identifier),
256  "value_set::return_value"))
257  {
258  values.insert(*it);
259  result=true;
260  }
261 
262  continue;
263  }
264 
265  entryt &e=it2->second;
266  const entryt &new_e=it->second;
267 
268  if(make_union(e.object_map, new_e.object_map))
269  result=true;
270  }
271 
272  changed = result;
273 
274  return result;
275 }
276 
277 bool value_set_fit::make_union(object_mapt &dest, const object_mapt &src) const
278 {
279  bool result=false;
280 
281  for(const auto &object_entry : src.read())
282  {
283  if(insert(dest, object_entry))
284  result=true;
285  }
286 
287  return result;
288 }
289 
290 std::vector<exprt>
291 value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
292 {
293  object_mapt object_map;
294  get_value_set(expr, object_map, ns);
295 
296  object_mapt flat_map;
297 
298  for(const auto &object_entry : object_map.read())
299  {
300  const exprt &object = object_numbering[object_entry.first];
301  if(object.type().id()=="#REF#")
302  {
303  assert(object.id()==ID_symbol);
304 
305  const irep_idt &ident = object.get(ID_identifier);
306  valuest::const_iterator v_it = values.find(ident);
307 
308  if(v_it!=values.end())
309  {
310  object_mapt temp;
311  flatten(v_it->second, temp);
312 
313  for(object_map_dt::iterator t_it=temp.write().begin();
314  t_it!=temp.write().end();
315  t_it++)
316  {
317  if(t_it->second && object_entry.second)
318  {
319  *t_it->second += *object_entry.second;
320  }
321  else
322  t_it->second.reset();
323 
324  flat_map.write()[t_it->first]=t_it->second;
325  }
326  }
327  }
328  else
329  flat_map.write()[object_entry.first] = object_entry.second;
330  }
331 
332  std::vector<exprt> result;
333  for(const auto &object_entry : flat_map.read())
334  result.push_back(to_expr(object_entry));
335 
336 #if 0
337  // Sanity check!
338  for(std::list<exprt>::const_iterator it=value_set.begin();
339  it!=value_set.end();
340  it++)
341  assert(it->type().id()!="#REF");
342 #endif
343 
344 #if 0
345  for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
346  std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
347 #endif
348 
349  return result;
350 }
351 
353  const exprt &expr,
354  object_mapt &dest,
355  const namespacet &ns) const
356 {
357  exprt tmp(expr);
358  simplify(tmp, ns);
359 
360  gvs_recursion_sett recset;
361  get_value_set_rec(tmp, dest, "", tmp.type(), ns, recset);
362 }
363 
365  const exprt &expr,
366  object_mapt &dest,
367  const std::string &suffix,
368  const typet &original_type,
369  const namespacet &ns,
370  gvs_recursion_sett &recursion_set) const
371 {
372  #if 0
373  std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr)
374  << '\n';
375  std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
376  std::cout << '\n';
377  #endif
378 
379  if(expr.type().id()=="#REF#")
380  {
381  valuest::const_iterator fi = values.find(expr.get(ID_identifier));
382 
383  if(fi!=values.end())
384  {
385  for(const auto &object_entry : fi->second.object_map.read())
386  {
388  object_numbering[object_entry.first],
389  dest,
390  suffix,
391  original_type,
392  ns,
393  recursion_set);
394  }
395  return;
396  }
397  else
398  {
399  insert(dest, exprt(ID_unknown, original_type));
400  return;
401  }
402  }
403  else if(expr.id()==ID_unknown || expr.id()==ID_invalid)
404  {
405  insert(dest, exprt(ID_unknown, original_type));
406  return;
407  }
408  else if(expr.id()==ID_index)
409  {
410  const typet &type = to_index_expr(expr).array().type();
411 
412  DATA_INVARIANT(type.id()==ID_array ||
413  type.id()=="#REF#",
414  "operand 0 of index expression must be an array");
415 
417  to_index_expr(expr).array(),
418  dest,
419  "[]" + suffix,
420  original_type,
421  ns,
422  recursion_set);
423 
424  return;
425  }
426  else if(expr.id()==ID_member)
427  {
428  const auto &compound = to_member_expr(expr).compound();
429 
430  if(compound.is_not_nil())
431  {
432  const typet &type = ns.follow(compound.type());
433 
435  type.id() == ID_struct || type.id() == ID_union,
436  "operand 0 of member expression must be struct or union");
437 
438  const std::string &component_name =
439  id2string(to_member_expr(expr).get_component_name());
440 
442  compound,
443  dest,
444  "." + component_name + suffix,
445  original_type,
446  ns,
447  recursion_set);
448 
449  return;
450  }
451  }
452  else if(expr.id()==ID_symbol)
453  {
454  // just keep a reference to the ident in the set
455  // (if it exists)
456  irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix;
457  valuest::const_iterator v_it=values.find(ident);
458 
460  {
461  insert(dest, expr, 0);
462  return;
463  }
464  else if(v_it!=values.end())
465  {
466  typet t("#REF#");
467  t.subtype() = expr.type();
468  symbol_exprt sym(ident, t);
469  insert(dest, sym, 0);
470  return;
471  }
472  }
473  else if(expr.id()==ID_if)
474  {
476  to_if_expr(expr).true_case(),
477  dest,
478  suffix,
479  original_type,
480  ns,
481  recursion_set);
483  to_if_expr(expr).false_case(),
484  dest,
485  suffix,
486  original_type,
487  ns,
488  recursion_set);
489 
490  return;
491  }
492  else if(expr.id()==ID_address_of)
493  {
494  get_reference_set_sharing(to_address_of_expr(expr).object(), dest, ns);
495 
496  return;
497  }
498  else if(expr.id()==ID_dereference)
499  {
500  object_mapt reference_set;
501  get_reference_set_sharing(expr, reference_set, ns);
502  const object_map_dt &object_map=reference_set.read();
503 
504  if(object_map.begin()!=object_map.end())
505  {
506  for(const auto &object_entry : object_map)
507  {
508  const exprt &object = object_numbering[object_entry.first];
509  get_value_set_rec(object, dest, suffix,
510  original_type, ns, recursion_set);
511  }
512 
513  return;
514  }
515  }
516  else if(expr.is_constant())
517  {
518  // check if NULL
519  if(expr.get(ID_value)==ID_NULL &&
520  expr.type().id()==ID_pointer)
521  {
522  insert(dest, exprt(ID_null_object, expr.type().subtype()), 0);
523  return;
524  }
525  }
526  else if(expr.id()==ID_typecast)
527  {
529  to_typecast_expr(expr).op(),
530  dest,
531  suffix,
532  original_type,
533  ns,
534  recursion_set);
535 
536  return;
537  }
538  else if(expr.id()==ID_plus || expr.id()==ID_minus)
539  {
540  if(expr.operands().size()<2)
541  throw expr.id_string()+" expected to have at least two operands";
542 
543  if(expr.type().id()==ID_pointer)
544  {
545  // find the pointer operand
546  const exprt *ptr_operand=nullptr;
547 
548  forall_operands(it, expr)
549  if(it->type().id()==ID_pointer)
550  {
551  if(ptr_operand==nullptr)
552  ptr_operand=&(*it);
553  else
554  throw "more than one pointer operand in pointer arithmetic";
555  }
556 
557  if(ptr_operand==nullptr)
558  throw "pointer type sum expected to have pointer operand";
559 
560  object_mapt pointer_expr_set;
561  get_value_set_rec(*ptr_operand, pointer_expr_set, "",
562  ptr_operand->type(), ns, recursion_set);
563 
564  for(const auto &object_entry : pointer_expr_set.read())
565  {
566  offsett offset = object_entry.second;
567 
568  if(offset_is_zero(offset) && expr.operands().size() == 2)
569  {
570  if(to_binary_expr(expr).op0().type().id() != ID_pointer)
571  {
572  const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op0());
573  if(!i.has_value())
574  offset.reset();
575  else
576  *offset = (expr.id() == ID_plus) ? *i : -*i;
577  }
578  else
579  {
580  const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op1());
581  if(!i.has_value())
582  offset.reset();
583  else
584  *offset = (expr.id() == ID_plus) ? *i : -*i;
585  }
586  }
587  else
588  offset.reset();
589 
590  insert(dest, object_entry.first, offset);
591  }
592 
593  return;
594  }
595  }
596  else if(expr.id()==ID_side_effect)
597  {
598  const irep_idt &statement = to_side_effect_expr(expr).get_statement();
599 
600  if(statement==ID_function_call)
601  {
602  // these should be gone
603  throw "unexpected function_call sideeffect";
604  }
605  else if(statement==ID_allocate)
606  {
607  if(expr.type().id()!=ID_pointer)
608  throw "malloc expected to return pointer type";
609 
610  PRECONDITION(suffix.empty());
611 
612  const typet &dynamic_type=
613  static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
614 
615  dynamic_object_exprt dynamic_object(dynamic_type);
616  // let's make up a `unique' number for this object...
617  dynamic_object.set_instance(
618  (from_function << 16) | from_target_index);
619  dynamic_object.valid()=true_exprt();
620 
621  insert(dest, dynamic_object, 0);
622  return;
623  }
624  else if(statement==ID_cpp_new ||
625  statement==ID_cpp_new_array)
626  {
627  PRECONDITION(suffix.empty());
628  assert(expr.type().id()==ID_pointer);
629 
631  dynamic_object.set_instance(
632  (from_function << 16) | from_target_index);
633  dynamic_object.valid()=true_exprt();
634 
635  insert(dest, dynamic_object, 0);
636  return;
637  }
638  }
639  else if(expr.id()==ID_struct)
640  {
641  // this is like a static struct object
642  insert(dest, address_of_exprt(expr), 0);
643  return;
644  }
645  else if(expr.id()==ID_with)
646  {
647  // these are supposed to be done by assign()
648  throw "unexpected value in get_value_set: "+expr.id_string();
649  }
650  else if(expr.id()==ID_array_of ||
651  expr.id()==ID_array)
652  {
653  // an array constructor, possibly containing addresses
654  forall_operands(it, expr)
655  get_value_set_rec(*it, dest, suffix, original_type, ns, recursion_set);
656  }
657  else if(expr.id()==ID_dynamic_object)
658  {
661 
662  const std::string name=
663  "value_set::dynamic_object"+
664  std::to_string(dynamic_object.get_instance())+
665  suffix;
666 
667  // look it up
668  valuest::const_iterator v_it=values.find(name);
669 
670  if(v_it!=values.end())
671  {
672  make_union(dest, v_it->second.object_map);
673  return;
674  }
675  }
676 
677  insert(dest, exprt(ID_unknown, original_type));
678 }
679 
681  const exprt &src,
682  exprt &dest) const
683 {
684  // remove pointer typecasts
685  if(src.id()==ID_typecast)
686  {
687  assert(src.type().id()==ID_pointer);
688 
689  dereference_rec(to_typecast_expr(src).op(), dest);
690  }
691  else
692  dest=src;
693 }
694 
696  const exprt &expr,
697  expr_sett &dest,
698  const namespacet &ns) const
699 {
700  object_mapt object_map;
701  get_reference_set_sharing(expr, object_map, ns);
702 
703  for(const auto &object_entry : object_map.read())
704  {
705  const exprt &object = object_numbering[object_entry.first];
706 
707  if(object.type().id() == "#REF#")
708  {
709  const irep_idt &ident = object.get(ID_identifier);
710  valuest::const_iterator vit = values.find(ident);
711  if(vit==values.end())
712  {
713  // Assume the variable never was assigned,
714  // so assume it's reference set is unknown.
715  dest.insert(exprt(ID_unknown, object.type()));
716  }
717  else
718  {
719  object_mapt omt;
720  flatten(vit->second, omt);
721 
722  for(object_map_dt::iterator t_it=omt.write().begin();
723  t_it!=omt.write().end();
724  t_it++)
725  {
726  if(t_it->second && object_entry.second)
727  {
728  *t_it->second += *object_entry.second;
729  }
730  else
731  t_it->second.reset();
732  }
733 
734  for(const auto &o : omt.read())
735  dest.insert(to_expr(o));
736  }
737  }
738  else
739  dest.insert(to_expr(object_entry));
740  }
741 }
742 
744  const exprt &expr,
745  expr_sett &dest,
746  const namespacet &ns) const
747 {
748  object_mapt object_map;
749  get_reference_set_sharing(expr, object_map, ns);
750 
751  for(const auto &object_entry : object_map.read())
752  dest.insert(to_expr(object_entry));
753 }
754 
756  const exprt &expr,
757  object_mapt &dest,
758  const namespacet &ns) const
759 {
760  #if 0
761  std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
762  << '\n';
763  #endif
764 
765  if(expr.type().id()=="#REF#")
766  {
767  valuest::const_iterator fi = values.find(expr.get(ID_identifier));
768  if(fi!=values.end())
769  {
770  for(const auto &object_entry : fi->second.object_map.read())
771  {
773  object_numbering[object_entry.first], dest, ns);
774  }
775  return;
776  }
777  }
778  else if(expr.id()==ID_symbol ||
779  expr.id()==ID_dynamic_object ||
780  expr.id()==ID_string_constant)
781  {
782  if(expr.type().id()==ID_array &&
783  expr.type().subtype().id()==ID_array)
784  insert(dest, expr);
785  else
786  insert(dest, expr, 0);
787 
788  return;
789  }
790  else if(expr.id()==ID_dereference)
791  {
792  gvs_recursion_sett recset;
793  object_mapt temp;
795  to_dereference_expr(expr).pointer(),
796  temp,
797  "",
798  to_dereference_expr(expr).pointer().type(),
799  ns,
800  recset);
801 
802  // REF's need to be dereferenced manually!
803  for(const auto &object_entry : temp.read())
804  {
805  const exprt &obj = object_numbering[object_entry.first];
806  if(obj.type().id()=="#REF#")
807  {
808  const irep_idt &ident = obj.get(ID_identifier);
809  valuest::const_iterator v_it = values.find(ident);
810 
811  if(v_it!=values.end())
812  {
813  object_mapt t2;
814  flatten(v_it->second, t2);
815 
816  for(object_map_dt::iterator t_it=t2.write().begin();
817  t_it!=t2.write().end();
818  t_it++)
819  {
820  if(t_it->second && object_entry.second)
821  {
822  *t_it->second += *object_entry.second;
823  }
824  else
825  t_it->second.reset();
826  }
827 
828  for(const auto &t2_object_entry : t2.read())
829  insert(dest, t2_object_entry);
830  }
831  else
832  insert(dest, exprt(ID_unknown, obj.type().subtype()));
833  }
834  else
835  insert(dest, object_entry);
836  }
837 
838  #if 0
839  for(expr_sett::const_iterator it=value_set.begin();
840  it!=value_set.end();
841  it++)
842  std::cout << "VALUE_SET: " << format(*it) << '\n';
843  #endif
844 
845  return;
846  }
847  else if(expr.id()==ID_index)
848  {
849  const exprt &array = to_index_expr(expr).array();
850  const exprt &offset = to_index_expr(expr).index();
851  const typet &array_type = array.type();
852 
854  array_type.id() == ID_array, "index takes array-typed operand");
855 
856  object_mapt array_references;
857  get_reference_set_sharing(array, array_references, ns);
858 
859  const object_map_dt &object_map=array_references.read();
860 
861  for(const auto &object_entry : object_map)
862  {
863  const exprt &object = object_numbering[object_entry.first];
864 
865  if(object.id()==ID_unknown)
866  insert(dest, exprt(ID_unknown, expr.type()));
867  else
868  {
869  index_exprt index_expr(
870  object, from_integer(0, index_type()), expr.type());
871 
872  exprt casted_index;
873 
874  // adjust type?
875  if(object.type().id() != "#REF#" && object.type() != array_type)
876  casted_index = typecast_exprt(index_expr, array.type());
877  else
878  casted_index = index_expr;
879 
880  offsett o = object_entry.second;
881  const auto i = numeric_cast<mp_integer>(offset);
882 
883  if(offset.is_zero())
884  {
885  }
886  else if(i.has_value() && offset_is_zero(o))
887  *o = *i;
888  else
889  o.reset();
890 
891  insert(dest, casted_index, o);
892  }
893  }
894 
895  return;
896  }
897  else if(expr.id()==ID_member)
898  {
899  const irep_idt &component_name=expr.get(ID_component_name);
900 
901  const exprt &struct_op = to_member_expr(expr).compound();
902 
903  object_mapt struct_references;
904  get_reference_set_sharing(struct_op, struct_references, ns);
905 
906  for(const auto &object_entry : struct_references.read())
907  {
908  const exprt &object = object_numbering[object_entry.first];
909  const typet &obj_type = object.type();
910 
911  if(object.id()==ID_unknown)
912  insert(dest, exprt(ID_unknown, expr.type()));
913  else if(
914  object.id() == ID_dynamic_object && obj_type.id() != ID_struct &&
915  obj_type.id() != ID_union && obj_type.id() != ID_struct_tag &&
916  obj_type.id() != ID_union_tag)
917  {
918  // we catch dynamic objects of the wrong type,
919  // to avoid non-integral typecasts.
920  insert(dest, exprt(ID_unknown, expr.type()));
921  }
922  else
923  {
924  offsett o = object_entry.second;
925 
926  member_exprt member_expr(object, component_name, expr.type());
927 
928  // adjust type?
929  if(ns.follow(struct_op.type())!=ns.follow(object.type()))
930  {
931  member_expr.compound() =
932  typecast_exprt(member_expr.compound(), struct_op.type());
933  }
934 
935  insert(dest, member_expr, o);
936  }
937  }
938 
939  return;
940  }
941  else if(expr.id()==ID_if)
942  {
943  get_reference_set_sharing_rec(to_if_expr(expr).true_case(), dest, ns);
944  get_reference_set_sharing_rec(to_if_expr(expr).false_case(), dest, ns);
945  return;
946  }
947 
948  insert(dest, exprt(ID_unknown, expr.type()));
949 }
950 
952  const exprt &lhs,
953  const exprt &rhs,
954  const namespacet &ns)
955 {
956  #if 0
957  std::cout << "ASSIGN LHS: " << format(lhs) << '\n';
958  std::cout << "ASSIGN RHS: " << format(rhs) << '\n';
959  #endif
960 
961  if(rhs.id()==ID_if)
962  {
963  assign(lhs, to_if_expr(rhs).true_case(), ns);
964  assign(lhs, to_if_expr(rhs).false_case(), ns);
965  return;
966  }
967 
968  const typet &type=ns.follow(lhs.type());
969 
970  if(type.id()==ID_struct ||
971  type.id()==ID_union)
972  {
973  const struct_union_typet &struct_type=to_struct_union_type(type);
974 
975  std::size_t no=0;
976 
977  for(struct_typet::componentst::const_iterator
978  c_it=struct_type.components().begin();
979  c_it!=struct_type.components().end();
980  c_it++, no++)
981  {
982  const typet &subtype=c_it->type();
983  const irep_idt &name = c_it->get_name();
984 
985  // ignore methods
986  if(subtype.id()==ID_code)
987  continue;
988 
989  member_exprt lhs_member(lhs, name, subtype);
990 
991  exprt rhs_member;
992 
993  if(rhs.id()==ID_unknown ||
994  rhs.id()==ID_invalid)
995  {
996  rhs_member=exprt(rhs.id(), subtype);
997  }
998  else
999  {
1000  if(rhs.type() != lhs.type())
1001  throw "value_set_fit::assign type mismatch: "
1002  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1003  "type:\n"+lhs.type().pretty();
1004 
1005  if(rhs.id()==ID_struct ||
1006  rhs.id()==ID_constant)
1007  {
1008  assert(no<rhs.operands().size());
1009  rhs_member=rhs.operands()[no];
1010  }
1011  else if(rhs.id()==ID_with)
1012  {
1013  // see if this is the member we want
1014  const auto &rhs_with = to_with_expr(rhs);
1015  const exprt &member_operand = rhs_with.where();
1016 
1017  const irep_idt &component_name=
1018  member_operand.get(ID_component_name);
1019 
1020  if(component_name==name)
1021  {
1022  // yes! just take op2
1023  rhs_member = rhs_with.new_value();
1024  }
1025  else
1026  {
1027  // no! do op0
1028  rhs_member=exprt(ID_member, subtype);
1029  rhs_member.copy_to_operands(rhs_with.old());
1030  rhs_member.set(ID_component_name, name);
1031  }
1032  }
1033  else
1034  {
1035  rhs_member=exprt(ID_member, subtype);
1036  rhs_member.copy_to_operands(rhs);
1037  rhs_member.set(ID_component_name, name);
1038  }
1039 
1040  assign(lhs_member, rhs_member, ns);
1041  }
1042  }
1043  }
1044  else if(type.id()==ID_array)
1045  {
1046  const index_exprt lhs_index(
1047  lhs, exprt(ID_unknown, index_type()), type.subtype());
1048 
1049  if(rhs.id()==ID_unknown ||
1050  rhs.id()==ID_invalid)
1051  {
1052  assign(lhs_index, exprt(rhs.id(), type.subtype()), ns);
1053  }
1054  else if(rhs.is_nil())
1055  {
1056  // do nothing
1057  }
1058  else
1059  {
1060  if(rhs.type() != type)
1061  throw "value_set_fit::assign type mismatch: "
1062  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1063  "type:\n"+type.pretty();
1064 
1065  if(rhs.id()==ID_array_of)
1066  {
1067  assign(lhs_index, to_array_of_expr(rhs).what(), ns);
1068  }
1069  else if(rhs.id()==ID_array ||
1070  rhs.id()==ID_constant)
1071  {
1072  forall_operands(o_it, rhs)
1073  {
1074  assign(lhs_index, *o_it, ns);
1075  }
1076  }
1077  else if(rhs.id()==ID_with)
1078  {
1079  const index_exprt op0_index(
1080  to_with_expr(rhs).old(),
1081  exprt(ID_unknown, index_type()),
1082  type.subtype());
1083 
1084  assign(lhs_index, op0_index, ns);
1085  assign(lhs_index, to_with_expr(rhs).new_value(), ns);
1086  }
1087  else
1088  {
1089  const index_exprt rhs_index(
1090  rhs, exprt(ID_unknown, index_type()), type.subtype());
1091  assign(lhs_index, rhs_index, ns);
1092  }
1093  }
1094  }
1095  else
1096  {
1097  // basic type
1098  object_mapt values_rhs;
1099 
1100  get_value_set(rhs, values_rhs, ns);
1101 
1102  assign_recursion_sett recset;
1103  assign_rec(lhs, values_rhs, "", ns, recset);
1104  }
1105 }
1106 
1108  const exprt &lhs,
1109  const object_mapt &values_rhs,
1110  const std::string &suffix,
1111  const namespacet &ns,
1112  assign_recursion_sett &recursion_set)
1113 {
1114  #if 0
1115  std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
1116  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1117 
1118  for(object_map_dt::const_iterator it=values_rhs.read().begin();
1119  it!=values_rhs.read().end(); it++)
1120  std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1121  #endif
1122 
1123  if(lhs.type().id()=="#REF#")
1124  {
1125  const irep_idt &ident = lhs.get(ID_identifier);
1126  object_mapt temp;
1127  gvs_recursion_sett recset;
1128  get_value_set_rec(lhs, temp, "", lhs.type().subtype(), ns, recset);
1129 
1130  if(recursion_set.find(ident)!=recursion_set.end())
1131  {
1132  recursion_set.insert(ident);
1133 
1134  for(const auto &object_entry : temp.read())
1135  {
1136  const exprt &object = object_numbering[object_entry.first];
1137 
1138  if(object.id() != ID_unknown)
1139  assign_rec(object, values_rhs, suffix, ns, recursion_set);
1140  }
1141 
1142  recursion_set.erase(ident);
1143  }
1144  }
1145  else if(lhs.id()==ID_symbol)
1146  {
1147  const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
1148 
1149  if(has_prefix(id2string(identifier),
1150  "value_set::dynamic_object") ||
1151  has_prefix(id2string(identifier),
1152  "value_set::return_value") ||
1153  values.find(id2string(identifier)+suffix)!=values.end())
1154  // otherwise we don't track this value
1155  {
1156  entryt &entry = get_entry(identifier, suffix);
1157 
1158  if(make_union(entry.object_map, values_rhs))
1159  changed = true;
1160  }
1161  }
1162  else if(lhs.id()==ID_dynamic_object)
1163  {
1166 
1167  const std::string name=
1168  "value_set::dynamic_object"+
1169  std::to_string(dynamic_object.get_instance());
1170 
1171  if(make_union(get_entry(name, suffix).object_map, values_rhs))
1172  changed = true;
1173  }
1174  else if(lhs.id()==ID_dereference)
1175  {
1176  if(lhs.operands().size()!=1)
1177  throw lhs.id_string()+" expected to have one operand";
1178 
1179  object_mapt reference_set;
1180  get_reference_set_sharing(lhs, reference_set, ns);
1181 
1182  for(const auto &object_entry : reference_set.read())
1183  {
1184  const exprt &object = object_numbering[object_entry.first];
1185 
1186  if(object.id()!=ID_unknown)
1187  assign_rec(object, values_rhs, suffix, ns, recursion_set);
1188  }
1189  }
1190  else if(lhs.id()==ID_index)
1191  {
1192  const typet &type = to_index_expr(lhs).array().type();
1193 
1194  DATA_INVARIANT(type.id()==ID_array ||
1195  type.id()=="#REF#",
1196  "operand 0 of index expression must be an array");
1197 
1198  assign_rec(
1199  to_index_expr(lhs).array(), values_rhs, "[]" + suffix, ns, recursion_set);
1200  }
1201  else if(lhs.id()==ID_member)
1202  {
1203  if(to_member_expr(lhs).compound().is_nil())
1204  return;
1205 
1206  const std::string &component_name=lhs.get_string(ID_component_name);
1207 
1208  const typet &type = ns.follow(to_member_expr(lhs).compound().type());
1209 
1211  type.id() == ID_struct || type.id() == ID_union,
1212  "operand 0 of member expression must be struct or union");
1213 
1214  assign_rec(
1215  to_member_expr(lhs).compound(),
1216  values_rhs,
1217  "." + component_name + suffix,
1218  ns,
1219  recursion_set);
1220  }
1221  else if(lhs.id()=="valid_object" ||
1222  lhs.id()=="dynamic_size" ||
1223  lhs.id()=="dynamic_type")
1224  {
1225  // we ignore this here
1226  }
1227  else if(lhs.id()==ID_string_constant)
1228  {
1229  // someone writes into a string-constant
1230  // evil guy
1231  }
1232  else if(lhs.id() == ID_null_object)
1233  {
1234  // evil as well
1235  }
1236  else if(lhs.id()==ID_typecast)
1237  {
1238  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1239 
1240  assign_rec(typecast_expr.op(), values_rhs, suffix, ns, recursion_set);
1241  }
1242  else if(lhs.id()=="zero_string" ||
1243  lhs.id()=="is_zero_string" ||
1244  lhs.id()=="zero_string_length")
1245  {
1246  // ignore
1247  }
1248  else if(lhs.id()==ID_byte_extract_little_endian ||
1249  lhs.id()==ID_byte_extract_big_endian)
1250  {
1251  assign_rec(
1252  to_byte_extract_expr(lhs).op(), values_rhs, suffix, ns, recursion_set);
1253  }
1254  else
1255  throw "assign NYI: '" + lhs.id_string() + "'";
1256 }
1257 
1259  const irep_idt &function,
1260  const exprt::operandst &arguments,
1261  const namespacet &ns)
1262 {
1263  const symbolt &symbol=ns.lookup(function);
1264 
1265  const code_typet &type=to_code_type(symbol.type);
1266  const code_typet::parameterst &parameter_types=type.parameters();
1267 
1268  // these first need to be assigned to dummy, temporary arguments
1269  // and only thereafter to the actuals, in order
1270  // to avoid overwriting actuals that are needed for recursive
1271  // calls
1272 
1273  for(std::size_t i=0; i<arguments.size(); i++)
1274  {
1275  const std::string identifier="value_set::" + id2string(function) + "::" +
1276  "argument$"+std::to_string(i);
1277  add_var(identifier);
1278  const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1279  assign(dummy_lhs, arguments[i], ns);
1280  }
1281 
1282  // now assign to 'actual actuals'
1283 
1284  std::size_t i=0;
1285 
1286  for(code_typet::parameterst::const_iterator
1287  it=parameter_types.begin();
1288  it!=parameter_types.end();
1289  it++)
1290  {
1291  const irep_idt &identifier=it->get_identifier();
1292  if(identifier.empty())
1293  continue;
1294 
1295  add_var(identifier);
1296 
1297  const exprt v_expr=
1298  symbol_exprt("value_set::" + id2string(function) + "::" +
1299  "argument$"+std::to_string(i), it->type());
1300 
1301  const symbol_exprt actual_lhs(identifier, it->type());
1302  assign(actual_lhs, v_expr, ns);
1303  i++;
1304  }
1305 }
1306 
1308  const exprt &lhs,
1309  const namespacet &ns)
1310 {
1311  if(lhs.is_nil())
1312  return;
1313 
1314  std::string rvs = "value_set::return_value" + std::to_string(from_function);
1315  symbol_exprt rhs(rvs, lhs.type());
1316 
1317  assign(lhs, rhs, ns);
1318 }
1319 
1320 void value_set_fit::apply_code(const codet &code, const namespacet &ns)
1321 {
1322  const irep_idt &statement=code.get(ID_statement);
1323 
1324  if(statement==ID_block)
1325  {
1326  for(const auto &stmt : to_code_block(code).statements())
1327  apply_code(stmt, ns);
1328  }
1329  else if(statement==ID_function_call)
1330  {
1331  // shouldn't be here
1332  UNREACHABLE;
1333  }
1334  else if(statement==ID_assign)
1335  {
1336  if(code.operands().size()!=2)
1337  throw "assignment expected to have two operands";
1338 
1339  assign(code.op0(), code.op1(), ns);
1340  }
1341  else if(statement==ID_decl)
1342  {
1343  if(code.operands().size()!=1)
1344  throw "decl expected to have one operand";
1345 
1346  const exprt &lhs=code.op0();
1347 
1348  if(lhs.id()!=ID_symbol)
1349  throw "decl expected to have symbol on lhs";
1350 
1351  assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1352  }
1353  else if(statement==ID_expression)
1354  {
1355  // can be ignored, we don't expect side effects here
1356  }
1357  else if(statement==ID_cpp_delete ||
1358  statement==ID_cpp_delete_array)
1359  {
1360  // does nothing
1361  }
1362  else if(statement=="lock" || statement=="unlock")
1363  {
1364  // ignore for now
1365  }
1366  else if(statement==ID_asm)
1367  {
1368  // ignore for now, probably not safe
1369  }
1370  else if(statement==ID_nondet)
1371  {
1372  // doesn't do anything
1373  }
1374  else if(statement==ID_printf)
1375  {
1376  // doesn't do anything
1377  }
1378  else if(statement==ID_return)
1379  {
1380  const code_returnt &code_return = to_code_return(code);
1381  // this is turned into an assignment
1382  if(code_return.has_return_value())
1383  {
1384  std::string rvs="value_set::return_value"+std::to_string(from_function);
1385  symbol_exprt lhs(rvs, code_return.return_value().type());
1386  assign(lhs, code_return.return_value(), ns);
1387  }
1388  }
1389  else if(statement==ID_fence)
1390  {
1391  }
1392  else if(statement==ID_array_copy ||
1393  statement==ID_array_replace ||
1394  statement==ID_array_set)
1395  {
1396  }
1398  {
1399  // doesn't do anything
1400  }
1401  else
1402  throw
1403  code.pretty()+"\n"+
1404  "value_set_fit: unexpected statement: "+id2string(statement);
1405 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:133
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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
value_set_fit::get_entry
entryt & get_entry(const idt &id, const std::string &suffix)
Definition: value_set_fi.h:230
alloc_adapter_prefix
static const char * alloc_adapter_prefix
Definition: value_set_fi.cpp:34
value_set_fit::assign_recursion_sett
std::unordered_set< idt, string_hash > assign_recursion_sett
Definition: value_set_fi.h:205
format
static format_containert< T > format(const T &o)
Definition: format.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
can_cast_expr< code_inputt >
bool can_cast_expr< code_inputt >(const exprt &base)
Definition: std_code.h:705
value_set_fit::object_map_dt::begin
iterator begin()
Definition: value_set_fi.h:79
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:103
value_set_fit::valuest
std::unordered_map< idt, entryt, string_hash > valuest
Definition: value_set_fi.h:201
value_set_fit::offset_is_zero
bool offset_is_zero(const offsett &offset) const
Definition: value_set_fi.h:61
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
value_set_fi.h
Value Set (Flow Insensitive, Sharing)
value_set_fit::object_map_dt::iterator
data_typet::iterator iterator
Definition: value_set_fi.h:73
symbolt::display_name
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
value_set_fit::values
valuest values
Definition: value_set_fi.h:258
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:746
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
value_set_fit::assign
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
Definition: value_set_fi.cpp:951
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
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
value_set_fit::get_reference_set_sharing_rec
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set_fi.cpp:755
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
dynamic_object_exprt
Representation of heap-allocated objects.
Definition: pointer_expr.h:108
value_set_fit::flatten_seent
std::unordered_set< idt, string_hash > flatten_seent
Definition: value_set_fi.h:202
numberingt< exprt, irep_hash >
value_set_fit::expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: value_set_fi.h:190
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:21
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
value_set_fit::do_function_call
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition: value_set_fi.cpp:1258
value_set_fit::entryt
Definition: value_set_fi.h:174
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1362
value_set_fit::from_function
unsigned from_function
Definition: value_set_fi.h:39
exprt
Base class for all expressions.
Definition: expr.h:54
from_type
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition: language_util.cpp:33
value_set_fit::gvs_recursion_sett
std::unordered_set< idt, string_hash > gvs_recursion_sett
Definition: value_set_fi.h:203
value_set_fit::dereference_rec
void dereference_rec(const exprt &src, exprt &dest) const
Definition: value_set_fi.cpp:680
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:71
value_set_fit::from_target_index
unsigned from_target_index
Definition: value_set_fi.h:40
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
value_set_fit::flatten
void flatten(const entryt &e, object_mapt &dest) const
Definition: value_set_fi.cpp:133
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
value_set_fit::flatten_rec
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
Definition: value_set_fi.cpp:149
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
value_set_fit::entryt::suffix
std::string suffix
Definition: value_set_fi.h:177
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_set_fit::entryt::identifier
idt identifier
Definition: value_set_fi.h:176
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
value_set_fit::apply_code
void apply_code(const codet &code, const namespacet &ns)
Definition: value_set_fi.cpp:1320
byte_operators.h
Expression classes for byte-level operators.
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
value_set_fit::changed
bool changed
Definition: value_set_fi.h:260
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
value_set_fit::object_map_dt::end
iterator end()
Definition: value_set_fi.h:83
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2569
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
value_set_fit::object_map_dt::const_iterator
data_typet::const_iterator const_iterator
Definition: value_set_fi.h:75
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
value_set_fit::get_value_set
std::vector< exprt > get_value_set(const exprt &expr, const namespacet &ns) const
Definition: value_set_fi.cpp:291
pointer_expr.h
API to expression classes for Pointers.
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2524
index_exprt::index
exprt & index()
Definition: std_expr.h:1269
value_set_fit::assign_rec
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
Definition: value_set_fi.cpp:1107
index_exprt::array
exprt & array()
Definition: std_expr.h:1259
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
code_typet
Base type of functions.
Definition: std_types.h:744
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
value_set_fit::entryt::object_map
object_mapt object_map
Definition: value_set_fi.h:175
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1391
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
to_dynamic_object_expr
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:151
reference_counting< object_map_dt >
std_code.h
value_set_fit::object_map_dt::blank
static const object_map_dt blank
Definition: value_set_fi.h:100
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2235
dstringt::clear
void clear()
Definition: dstring.h:142
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1920
simplify_expr.h
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
value_set_fit::make_union
bool make_union(object_mapt &dest, const object_mapt &src) const
Definition: value_set_fi.cpp:277
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
code_returnt::has_return_value
bool has_return_value() const
Definition: std_code.h:1362
value_set_fit::output
void output(const namespacet &ns, std::ostream &out) const
Definition: value_set_fi.cpp:36
can_cast_expr< code_outputt >
bool can_cast_expr< code_outputt >(const exprt &base)
Definition: std_code.h:751
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
value_set_fit::to_expr
exprt to_expr(const object_map_dt::value_type &it) const
Definition: value_set_fi.cpp:218
value_set_fit::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition: value_set_fi.cpp:1307
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
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
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
value_set_fit::object_numbering
static object_numberingt object_numbering
Definition: value_set_fi.h:41
reference_counting::read
const T & read() const
Definition: reference_counting.h:69
reference_counting::write
T & write()
Definition: reference_counting.h:76
value_set_fit::function_numbering
static numberingt< irep_idt > function_numbering
Definition: value_set_fi.h:42
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
value_set_fit::get_reference_set_sharing
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
Definition: value_set_fi.cpp:743
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
exprt::operands
operandst & operands()
Definition: expr.h:96
value_set_fit::offsett
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
Definition: value_set_fi.h:60
codet::op1
exprt & op1()
Definition: expr.h:106
index_exprt
Array index operator.
Definition: std_expr.h:1243
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
value_set_fit::object_map_dt::value_type
data_typet::value_type value_type
Definition: value_set_fi.h:77
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1352
object_descriptor_exprt::object
exprt & object()
Definition: pointer_expr.h:47
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
std_expr.h
API to expression classes.
c_types.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
value_set_fit::get_reference_set
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
Definition: value_set_fi.cpp:695
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
value_set_fit::object_map_dt
Definition: value_set_fi.h:67
value_set_fit::add_var
void add_var(const idt &id)
Definition: value_set_fi.h:220
value_set_fit::insert
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Definition: value_set_fi.h:115
value_set_fit::get_value_set_rec
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
Definition: value_set_fi.cpp:364
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
object_descriptor_exprt::offset
exprt & offset()
Definition: pointer_expr.h:59
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106