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