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 <ostream>
16 
17 #include <util/symbol_table.h>
18 #include <util/simplify_expr.h>
19 #include <util/base_type.h>
20 #include <util/std_expr.h>
21 #include <util/prefix.h>
22 #include <util/std_code.h>
23 #include <util/arith_tools.h>
24 
25 #include <langapi/language_util.h>
26 #include <util/c_types.h>
27 
31 
32 static const char *alloc_adapter_prefix="alloc_adaptor::";
33 
34 #define forall_objects(it, map) \
35  for(object_map_dt::const_iterator (it) = (map).begin(); \
36  (it)!=(map).end(); \
37  (it)++)
38 
39 #define Forall_objects(it, map) \
40  for(object_map_dt::iterator (it) = (map).begin(); \
41  (it)!=(map).end(); \
42  (it)++)
43 
45  const namespacet &ns,
46  std::ostream &out) const
47 {
48  for(valuest::const_iterator
49  v_it=values.begin();
50  v_it!=values.end();
51  v_it++)
52  {
53  irep_idt identifier, display_name;
54 
55  const entryt &e=v_it->second;
56 
57  if(has_prefix(id2string(e.identifier), "value_set::dynamic_object"))
58  {
59  display_name=id2string(e.identifier)+e.suffix;
60  identifier="";
61  }
62  else
63  {
64  #if 0
65  const symbolt &symbol=ns.lookup(id2string(e.identifier));
66  display_name=symbol.display_name()+e.suffix;
67  identifier=symbol.name;
68  #else
69  identifier=id2string(e.identifier);
70  display_name=id2string(identifier)+e.suffix;
71  #endif
72  }
73 
74  out << display_name;
75 
76  out << " = { ";
77 
78  object_mapt object_map;
79  flatten(e, object_map);
80 
81  std::size_t width=0;
82 
83  forall_objects(o_it, object_map.read())
84  {
85  const exprt &o=object_numbering[o_it->first];
86 
87  std::string result;
88 
89  if(o.id()==ID_invalid || o.id()==ID_unknown)
90  {
91  result="<";
92  result+=from_expr(ns, identifier, o);
93  result+=", *, "; // offset unknown
94  if(o.type().id()==ID_unknown)
95  result+='*';
96  else
97  result+=from_type(ns, identifier, o.type());
98  result+='>';
99  }
100  else
101  {
102  result="<"+from_expr(ns, identifier, o)+", ";
103 
104  if(o_it->second.offset_is_set)
105  result+=integer2string(o_it->second.offset)+"";
106  else
107  result+='*';
108 
109  result+=", ";
110 
111  if(o.type().id()==ID_unknown)
112  result+='*';
113  else
114  result+=from_type(ns, identifier, o.type());
115 
116  result+='>';
117  }
118 
119  out << result;
120 
121  width+=result.size();
122 
123  object_map_dt::const_iterator next(o_it);
124  next++;
125 
126  if(next!=object_map.read().end())
127  {
128  out << ", ";
129  if(width>=40)
130  out << "\n ";
131  }
132  }
133 
134  out << " } \n";
135  }
136 }
137 
139  const entryt &e,
140  object_mapt &dest) const
141 {
142  #if 0
143  std::cout << "FLATTEN: " << e.identifier << e.suffix << '\n';
144  #endif
145 
146  flatten_seent seen;
147  flatten_rec(e, dest, seen);
148 
149  #if 0
150  std::cout << "FLATTEN: Done.\n";
151  #endif
152 }
153 
155  const entryt &e,
156  object_mapt &dest,
157  flatten_seent &seen) const
158 {
159  #if 0
160  std::cout << "FLATTEN_REC: " << e.identifier << e.suffix << '\n';
161  #endif
162 
163  std::string identifier = id2string(e.identifier);
164  assert(seen.find(identifier + e.suffix)==seen.end());
165 
166  bool generalize_index = false;
167 
168  seen.insert(identifier + e.suffix);
169 
171  {
172  const exprt &o=object_numbering[it->first];
173 
174  if(o.type().id()=="#REF#")
175  {
176  if(seen.find(o.get(ID_identifier))!=seen.end())
177  {
178  generalize_index = true;
179  continue;
180  }
181 
182  valuest::const_iterator fi = values.find(o.get(ID_identifier));
183  if(fi==values.end())
184  {
185  // this is some static object, keep it in.
186  exprt se(ID_symbol, o.type().subtype());
187  se.set(ID_identifier, o.get(ID_identifier));
188  insert(dest, se, 0);
189  }
190  else
191  {
192  object_mapt temp;
193  flatten_rec(fi->second, temp, seen);
194 
195  for(object_map_dt::iterator t_it=temp.write().begin();
196  t_it!=temp.write().end();
197  t_it++)
198  {
199  if(t_it->second.offset_is_set &&
200  it->second.offset_is_set)
201  {
202  t_it->second.offset += it->second.offset;
203  }
204  else
205  t_it->second.offset_is_set=false;
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.offset_is_set = false;
220  }
221 
222  seen.erase(identifier + e.suffix);
223 }
224 
225 exprt value_set_fit::to_expr(object_map_dt::const_iterator it) const
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.offset_is_set)
238  od.offset()=from_integer(it->second.offset, index_type());
239 
240  od.type()=od.object().type();
241 
242  return od;
243 }
244 
246 {
247  assert(0);
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  object_mapt object_map;
303  get_value_set(expr, object_map, ns);
304 
305  object_mapt flat_map;
306 
307  forall_objects(it, object_map.read())
308  {
309  const exprt &object=object_numbering[it->first];
310  if(object.type().id()=="#REF#")
311  {
312  assert(object.id()==ID_symbol);
313 
314  const irep_idt &ident = object.get(ID_identifier);
315  valuest::const_iterator v_it = values.find(ident);
316 
317  if(v_it!=values.end())
318  {
319  object_mapt temp;
320  flatten(v_it->second, temp);
321 
322  for(object_map_dt::iterator t_it=temp.write().begin();
323  t_it!=temp.write().end();
324  t_it++)
325  {
326  if(t_it->second.offset_is_set &&
327  it->second.offset_is_set)
328  {
329  t_it->second.offset += it->second.offset;
330  }
331  else
332  t_it->second.offset_is_set=false;
333 
334  flat_map.write()[t_it->first]=t_it->second;
335  }
336  }
337  }
338  else
339  flat_map.write()[it->first]=it->second;
340  }
341 
342  forall_objects(fit, flat_map.read())
343  value_set.push_back(to_expr(fit));
344 
345  #if 0
346  // Sanity check!
347  for(std::list<exprt>::const_iterator it=value_set.begin();
348  it!=value_set.end();
349  it++)
350  assert(it->type().id()!="#REF");
351  #endif
352 
353  #if 0
354  for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
355  std::cout << "GET_VALUE_SET: " << from_expr(ns, "", *it) << '\n';
356  #endif
357 }
358 
360  const exprt &expr,
361  object_mapt &dest,
362  const namespacet &ns) const
363 {
364  exprt tmp(expr);
365  simplify(tmp, ns);
366 
367  gvs_recursion_sett recset;
368  get_value_set_rec(tmp, dest, "", tmp.type(), ns, recset);
369 }
370 
372  const exprt &expr,
373  object_mapt &dest,
374  const std::string &suffix,
375  const typet &original_type,
376  const namespacet &ns,
377  gvs_recursion_sett &recursion_set) const
378 {
379  #if 0
380  std::cout << "GET_VALUE_SET_REC EXPR: " << from_expr(ns, "", expr)
381  << '\n';
382  std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
383  std::cout << '\n';
384  #endif
385 
386  if(expr.type().id()=="#REF#")
387  {
388  valuest::const_iterator fi = values.find(expr.get(ID_identifier));
389 
390  if(fi!=values.end())
391  {
392  forall_objects(it, fi->second.object_map.read())
393  get_value_set_rec(object_numbering[it->first], dest, suffix,
394  original_type, ns, recursion_set);
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  assert(expr.operands().size()==2);
411 
412  const typet &type=ns.follow(expr.op0().type());
413 
414  assert(type.id()==ID_array ||
415  type.id()==ID_incomplete_array ||
416  type.id()=="#REF#");
417 
418  get_value_set_rec(expr.op0(), dest, "[]"+suffix,
419  original_type, ns, recursion_set);
420 
421  return;
422  }
423  else if(expr.id()==ID_member)
424  {
425  assert(expr.operands().size()==1);
426 
427  if(expr.op0().is_not_nil())
428  {
429  const typet &type=ns.follow(expr.op0().type());
430 
431  assert(type.id()==ID_struct ||
432  type.id()==ID_union ||
433  type.id()==ID_incomplete_struct ||
434  type.id()==ID_incomplete_union);
435 
436  const std::string &component_name=
437  expr.get_string(ID_component_name);
438 
439  get_value_set_rec(expr.op0(), dest, "."+component_name+suffix,
440  original_type, ns, recursion_set);
441 
442  return;
443  }
444  }
445  else if(expr.id()==ID_symbol)
446  {
447  // just keep a reference to the ident in the set
448  // (if it exists)
449  irep_idt ident = expr.get_string(ID_identifier)+suffix;
450  valuest::const_iterator v_it=values.find(ident);
451 
453  {
454  insert(dest, expr, 0);
455  return;
456  }
457  else if(v_it!=values.end())
458  {
459  typet t("#REF#");
460  t.subtype() = expr.type();
461  symbol_exprt sym(ident, t);
462  insert(dest, sym, 0);
463  return;
464  }
465  }
466  else if(expr.id()==ID_if)
467  {
468  if(expr.operands().size()!=3)
469  throw "if takes three operands";
470 
471  get_value_set_rec(expr.op1(), dest, suffix,
472  original_type, ns, recursion_set);
473  get_value_set_rec(expr.op2(), dest, suffix,
474  original_type, ns, recursion_set);
475 
476  return;
477  }
478  else if(expr.id()==ID_address_of)
479  {
480  if(expr.operands().size()!=1)
481  throw expr.id_string()+" expected to have one operand";
482 
483  get_reference_set_sharing(expr.op0(), dest, ns);
484 
485  return;
486  }
487  else if(expr.id()==ID_dereference)
488  {
489  object_mapt reference_set;
490  get_reference_set_sharing(expr, reference_set, ns);
491  const object_map_dt &object_map=reference_set.read();
492 
493  if(object_map.begin()!=object_map.end())
494  {
495  forall_objects(it1, object_map)
496  {
497  const exprt &object=object_numbering[it1->first];
498  get_value_set_rec(object, dest, suffix,
499  original_type, ns, recursion_set);
500  }
501 
502  return;
503  }
504  }
505  else if(expr.id()=="reference_to")
506  {
507  object_mapt reference_set;
508 
509  get_reference_set_sharing(expr, reference_set, ns);
510 
511  const object_map_dt &object_map=reference_set.read();
512 
513  if(object_map.begin()!=object_map.end())
514  {
515  forall_objects(it, object_map)
516  {
517  const exprt &object=object_numbering[it->first];
518  get_value_set_rec(object, dest, suffix,
519  original_type, ns, recursion_set);
520  }
521 
522  return;
523  }
524  }
525  else if(expr.is_constant())
526  {
527  // check if NULL
528  if(expr.get(ID_value)==ID_NULL &&
529  expr.type().id()==ID_pointer)
530  {
531  insert(dest, exprt("NULL-object", expr.type().subtype()), 0);
532  return;
533  }
534  }
535  else if(expr.id()==ID_typecast)
536  {
537  if(expr.operands().size()!=1)
538  throw "typecast takes one operand";
539 
540  get_value_set_rec(expr.op0(), dest, suffix,
541  original_type, ns, recursion_set);
542 
543  return;
544  }
545  else if(expr.id()==ID_plus || expr.id()==ID_minus)
546  {
547  if(expr.operands().size()<2)
548  throw expr.id_string()+" expected to have at least two operands";
549 
550  if(expr.type().id()==ID_pointer)
551  {
552  // find the pointer operand
553  const exprt *ptr_operand=nullptr;
554 
555  forall_operands(it, expr)
556  if(it->type().id()==ID_pointer)
557  {
558  if(ptr_operand==nullptr)
559  ptr_operand=&(*it);
560  else
561  throw "more than one pointer operand in pointer arithmetic";
562  }
563 
564  if(ptr_operand==nullptr)
565  throw "pointer type sum expected to have pointer operand";
566 
567  object_mapt pointer_expr_set;
568  get_value_set_rec(*ptr_operand, pointer_expr_set, "",
569  ptr_operand->type(), ns, recursion_set);
570 
571  forall_objects(it, pointer_expr_set.read())
572  {
573  objectt object=it->second;
574 
575  if(object.offset_is_zero() &&
576  expr.operands().size()==2)
577  {
578  if(expr.op0().type().id()!=ID_pointer)
579  {
580  mp_integer i;
581  if(to_integer(expr.op0(), i))
582  object.offset_is_set=false;
583  else
584  object.offset=(expr.id()==ID_plus)? i : -i;
585  }
586  else
587  {
588  mp_integer i;
589  if(to_integer(expr.op1(), i))
590  object.offset_is_set=false;
591  else
592  object.offset=(expr.id()==ID_plus)? i : -i;
593  }
594  }
595  else
596  object.offset_is_set=false;
597 
598  insert(dest, it->first, object);
599  }
600 
601  return;
602  }
603  }
604  else if(expr.id()==ID_side_effect)
605  {
606  const irep_idt &statement=expr.get(ID_statement);
607 
608  if(statement==ID_function_call)
609  {
610  // these should be gone
611  throw "unexpected function_call sideeffect";
612  }
613  else if(statement==ID_malloc)
614  {
615  if(expr.type().id()!=ID_pointer)
616  throw "malloc expected to return pointer type";
617 
618  assert(suffix=="");
619 
620  const typet &dynamic_type=
621  static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
622 
623  dynamic_object_exprt dynamic_object(dynamic_type);
624  // let's make up a `unique' number for this object...
625  dynamic_object.set_instance(
626  (from_function << 16) | from_target_index);
627  dynamic_object.valid()=true_exprt();
628 
629  insert(dest, dynamic_object, 0);
630  return;
631  }
632  else if(statement==ID_cpp_new ||
633  statement==ID_cpp_new_array)
634  {
635  assert(suffix=="");
636  assert(expr.type().id()==ID_pointer);
637 
639  dynamic_object.set_instance(
640  (from_function << 16) | from_target_index);
641  dynamic_object.valid()=true_exprt();
642 
643  insert(dest, dynamic_object, 0);
644  return;
645  }
646  }
647  else if(expr.id()==ID_struct)
648  {
649  // this is like a static struct object
650  insert(dest, address_of_exprt(expr), 0);
651  return;
652  }
653  else if(expr.id()==ID_with)
654  {
655  // these are supposed to be done by assign()
656  throw "unexpected value in get_value_set: "+expr.id_string();
657  }
658  else if(expr.id()==ID_array_of ||
659  expr.id()==ID_array)
660  {
661  // an array constructor, possibly containing addresses
662  forall_operands(it, expr)
663  get_value_set_rec(*it, dest, suffix, original_type, ns, recursion_set);
664  }
665  else if(expr.id()==ID_dynamic_object)
666  {
669 
670  const std::string name=
671  "value_set::dynamic_object"+
672  std::to_string(dynamic_object.get_instance())+
673  suffix;
674 
675  // look it up
676  valuest::const_iterator v_it=values.find(name);
677 
678  if(v_it!=values.end())
679  {
680  make_union(dest, v_it->second.object_map);
681  return;
682  }
683  }
684 
685  insert(dest, exprt(ID_unknown, original_type));
686 }
687 
689  const exprt &src,
690  exprt &dest) const
691 {
692  // remove pointer typecasts
693  if(src.id()==ID_typecast)
694  {
695  assert(src.type().id()==ID_pointer);
696 
697  if(src.operands().size()!=1)
698  throw "typecast expects one operand";
699 
700  dereference_rec(src.op0(), dest);
701  }
702  else
703  dest=src;
704 }
705 
707  const exprt &expr,
708  expr_sett &dest,
709  const namespacet &ns) const
710 {
711  object_mapt object_map;
712  get_reference_set_sharing(expr, object_map, ns);
713 
714  forall_objects(it, object_map.read())
715  {
716  const exprt &expr = object_numbering[it->first];
717 
718  if(expr.type().id()=="#REF#")
719  {
720  const irep_idt &ident = expr.get(ID_identifier);
721  valuest::const_iterator vit = values.find(ident);
722  if(vit==values.end())
723  {
724  // Assume the variable never was assigned,
725  // so assume it's reference set is unknown.
726  dest.insert(exprt(ID_unknown, expr.type()));
727  }
728  else
729  {
730  object_mapt omt;
731  flatten(vit->second, omt);
732 
733  for(object_map_dt::iterator t_it=omt.write().begin();
734  t_it!=omt.write().end();
735  t_it++)
736  {
737  if(t_it->second.offset_is_set &&
738  it->second.offset_is_set)
739  {
740  t_it->second.offset += it->second.offset;
741  }
742  else
743  t_it->second.offset_is_set=false;
744  }
745 
746  forall_objects(it, omt.read())
747  dest.insert(to_expr(it));
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: " << from_expr(ns, "", 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  if(expr.operands().size()!=1)
802  throw expr.id_string()+" expected to have one operand";
803 
804  gvs_recursion_sett recset;
805  object_mapt temp;
806  get_value_set_rec(expr.op0(), temp, "", expr.op0().type(), ns, recset);
807 
808  // REF's need to be dereferenced manually!
809  forall_objects(it, temp.read())
810  {
811  const exprt &obj = object_numbering[it->first];
812  if(obj.type().id()=="#REF#")
813  {
814  const irep_idt &ident = obj.get(ID_identifier);
815  valuest::const_iterator v_it = values.find(ident);
816 
817  if(v_it!=values.end())
818  {
819  object_mapt t2;
820  flatten(v_it->second, t2);
821 
822  for(object_map_dt::iterator t_it=t2.write().begin();
823  t_it!=t2.write().end();
824  t_it++)
825  {
826  if(t_it->second.offset_is_set &&
827  it->second.offset_is_set)
828  {
829  t_it->second.offset += it->second.offset;
830  }
831  else
832  t_it->second.offset_is_set=false;
833  }
834 
835  forall_objects(it2, t2.read())
836  insert(dest, it2);
837  }
838  else
839  insert(dest, exprt(ID_unknown, obj.type().subtype()));
840  }
841  else
842  insert(dest, it);
843  }
844 
845  #if 0
846  for(expr_sett::const_iterator it=value_set.begin();
847  it!=value_set.end();
848  it++)
849  std::cout << "VALUE_SET: " << from_expr(ns, "", *it) << '\n';
850  #endif
851 
852  return;
853  }
854  else if(expr.id()==ID_index)
855  {
856  if(expr.operands().size()!=2)
857  throw "index expected to have two operands";
858 
859  const exprt &array=expr.op0();
860  const exprt &offset=expr.op1();
861  const typet &array_type=ns.follow(array.type());
862 
863  assert(array_type.id()==ID_array ||
864  array_type.id()==ID_incomplete_array);
865 
866  object_mapt array_references;
867  get_reference_set_sharing(array, array_references, ns);
868 
869  const object_map_dt &object_map=array_references.read();
870 
871  forall_objects(a_it, object_map)
872  {
873  const exprt &object=object_numbering[a_it->first];
874 
875  if(object.id()==ID_unknown)
876  insert(dest, exprt(ID_unknown, expr.type()));
877  else
878  {
879  exprt index_expr(ID_index, expr.type());
880  index_expr.operands().resize(2);
881  index_expr.op0()=object;
882  index_expr.op1()=from_integer(0, index_type());
883 
884  // adjust type?
885  if(object.type().id()!="#REF#" &&
886  ns.follow(object.type())!=array_type)
887  index_expr.make_typecast(array.type());
888 
889  objectt o=a_it->second;
890  mp_integer i;
891 
892  if(offset.is_zero())
893  {
894  }
895  else if(!to_integer(offset, i) &&
896  o.offset_is_zero())
897  o.offset=i;
898  else
899  o.offset_is_set=false;
900 
901  insert(dest, index_expr, o);
902  }
903  }
904 
905  return;
906  }
907  else if(expr.id()==ID_member)
908  {
909  const irep_idt &component_name=expr.get(ID_component_name);
910 
911  if(expr.operands().size()!=1)
912  throw "member expected to have one operand";
913 
914  const exprt &struct_op=expr.op0();
915 
916  object_mapt struct_references;
917  get_reference_set_sharing(struct_op, struct_references, ns);
918 
919  forall_objects(it, struct_references.read())
920  {
921  const exprt &object=object_numbering[it->first];
922  const typet &obj_type=ns.follow(object.type());
923 
924  if(object.id()==ID_unknown)
925  insert(dest, exprt(ID_unknown, expr.type()));
926  else if(object.id()==ID_dynamic_object &&
927  obj_type.id()!=ID_struct &&
928  obj_type.id()!=ID_union)
929  {
930  // we catch dynamic objects of the wrong type,
931  // to avoid non-integral typecasts.
932  insert(dest, exprt(ID_unknown, expr.type()));
933  }
934  else
935  {
936  objectt o=it->second;
937 
938  exprt member_expr(ID_member, expr.type());
939  member_expr.copy_to_operands(object);
940  member_expr.set(ID_component_name, component_name);
941 
942  // adjust type?
943  if(ns.follow(struct_op.type())!=ns.follow(object.type()))
944  member_expr.op0().make_typecast(struct_op.type());
945 
946  insert(dest, member_expr, o);
947  }
948  }
949 
950  return;
951  }
952  else if(expr.id()==ID_if)
953  {
954  if(expr.operands().size()!=3)
955  throw "if takes three operands";
956 
957  get_reference_set_sharing_rec(expr.op1(), dest, ns);
958  get_reference_set_sharing_rec(expr.op2(), dest, ns);
959  return;
960  }
961 
962  insert(dest, exprt(ID_unknown, expr.type()));
963 }
964 
966  const exprt &lhs,
967  const exprt &rhs,
968  const namespacet &ns)
969 {
970  #if 0
971  std::cout << "ASSIGN LHS: " << from_expr(ns, "", lhs) << '\n';
972  std::cout << "ASSIGN RHS: " << from_expr(ns, "", rhs) << '\n';
973  #endif
974 
975  if(rhs.id()==ID_if)
976  {
977  if(rhs.operands().size()!=3)
978  throw "if takes three operands";
979 
980  assign(lhs, rhs.op1(), ns);
981  assign(lhs, rhs.op2(), ns);
982  return;
983  }
984 
985  const typet &type=ns.follow(lhs.type());
986 
987  if(type.id()==ID_struct ||
988  type.id()==ID_union)
989  {
990  const struct_union_typet &struct_type=to_struct_union_type(type);
991 
992  unsigned no=0;
993 
994  for(struct_typet::componentst::const_iterator
995  c_it=struct_type.components().begin();
996  c_it!=struct_type.components().end();
997  c_it++, no++)
998  {
999  const typet &subtype=c_it->type();
1000  const irep_idt &name=c_it->get(ID_name);
1001 
1002  // ignore methods
1003  if(subtype.id()==ID_code)
1004  continue;
1005 
1006  exprt lhs_member(ID_member, subtype);
1007  lhs_member.set(ID_component_name, name);
1008  lhs_member.copy_to_operands(lhs);
1009 
1010  exprt rhs_member;
1011 
1012  if(rhs.id()==ID_unknown ||
1013  rhs.id()==ID_invalid)
1014  {
1015  rhs_member=exprt(rhs.id(), subtype);
1016  }
1017  else
1018  {
1019  if(!base_type_eq(rhs.type(), type, ns))
1020  throw "value_set_fit::assign type mismatch: "
1021  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1022  "type:\n"+type.pretty();
1023 
1024  if(rhs.id()==ID_struct ||
1025  rhs.id()==ID_constant)
1026  {
1027  assert(no<rhs.operands().size());
1028  rhs_member=rhs.operands()[no];
1029  }
1030  else if(rhs.id()==ID_with)
1031  {
1032  assert(rhs.operands().size()==3);
1033 
1034  // see if op1 is the member we want
1035  const exprt &member_operand=rhs.op1();
1036 
1037  const irep_idt &component_name=
1038  member_operand.get(ID_component_name);
1039 
1040  if(component_name==name)
1041  {
1042  // yes! just take op2
1043  rhs_member=rhs.op2();
1044  }
1045  else
1046  {
1047  // no! do op0
1048  rhs_member=exprt(ID_member, subtype);
1049  rhs_member.copy_to_operands(rhs.op0());
1050  rhs_member.set(ID_component_name, name);
1051  }
1052  }
1053  else
1054  {
1055  rhs_member=exprt(ID_member, subtype);
1056  rhs_member.copy_to_operands(rhs);
1057  rhs_member.set(ID_component_name, name);
1058  }
1059 
1060  assign(lhs_member, rhs_member, ns);
1061  }
1062  }
1063  }
1064  else if(type.id()==ID_array)
1065  {
1066  exprt lhs_index(ID_index, type.subtype());
1067  lhs_index.copy_to_operands(lhs, exprt(ID_unknown, index_type()));
1068 
1069  if(rhs.id()==ID_unknown ||
1070  rhs.id()==ID_invalid)
1071  {
1072  assign(lhs_index, exprt(rhs.id(), type.subtype()), ns);
1073  }
1074  else if(rhs.is_nil())
1075  {
1076  // do nothing
1077  }
1078  else
1079  {
1080  if(!base_type_eq(rhs.type(), type, ns))
1081  throw "value_set_fit::assign type mismatch: "
1082  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1083  "type:\n"+type.pretty();
1084 
1085  if(rhs.id()==ID_array_of)
1086  {
1087  assert(rhs.operands().size()==1);
1088  assign(lhs_index, rhs.op0(), ns);
1089  }
1090  else if(rhs.id()==ID_array ||
1091  rhs.id()==ID_constant)
1092  {
1093  forall_operands(o_it, rhs)
1094  {
1095  assign(lhs_index, *o_it, ns);
1096  }
1097  }
1098  else if(rhs.id()==ID_with)
1099  {
1100  assert(rhs.operands().size()==3);
1101 
1102  exprt op0_index(ID_index, type.subtype());
1103  op0_index.copy_to_operands(rhs.op0(), exprt(ID_unknown, index_type()));
1104 
1105  assign(lhs_index, op0_index, ns);
1106  assign(lhs_index, rhs.op2(), ns);
1107  }
1108  else
1109  {
1110  exprt rhs_index(ID_index, type.subtype());
1111  rhs_index.copy_to_operands(rhs, exprt(ID_unknown, index_type()));
1112  assign(lhs_index, rhs_index, ns);
1113  }
1114  }
1115  }
1116  else
1117  {
1118  // basic type
1119  object_mapt values_rhs;
1120 
1121  get_value_set(rhs, values_rhs, ns);
1122 
1123  assign_recursion_sett recset;
1124  assign_rec(lhs, values_rhs, "", ns, recset);
1125  }
1126 }
1127 
1129  const exprt &op,
1130  const namespacet &ns)
1131 {
1132  // op must be a pointer
1133  if(op.type().id()!=ID_pointer)
1134  throw "free expected to have pointer-type operand";
1135 
1136  // find out what it points to
1137  object_mapt value_set;
1138  get_value_set(op, value_set, ns);
1139  entryt e; e.identifier="VP:TEMP";
1140  e.object_map = value_set;
1141  flatten(e, value_set);
1142 
1143  const object_map_dt &object_map=value_set.read();
1144 
1145  // find out which *instances* interest us
1146  dynamic_object_id_sett to_mark;
1147 
1148  forall_objects(it, object_map)
1149  {
1150  const exprt &object=object_numbering[it->first];
1151 
1152  if(object.id()==ID_dynamic_object)
1153  {
1155  to_dynamic_object_expr(object);
1156 
1157  if(dynamic_object.valid().is_true())
1158  to_mark.insert(dynamic_object.get_instance());
1159  }
1160  }
1161 
1162  // mark these as 'may be invalid'
1163  // this, unfortunately, destroys the sharing
1164  for(valuest::iterator v_it=values.begin();
1165  v_it!=values.end();
1166  v_it++)
1167  {
1168  object_mapt new_object_map;
1169 
1170  const object_map_dt &old_object_map=
1171  v_it->second.object_map.read();
1172 
1173  bool changed=false;
1174 
1175  forall_objects(o_it, old_object_map)
1176  {
1177  const exprt &object=object_numbering[o_it->first];
1178 
1179  if(object.id()==ID_dynamic_object)
1180  {
1182  to_dynamic_object_expr(object);
1183 
1184  if(to_mark.count(dynamic_object.get_instance())==0)
1185  set(new_object_map, o_it);
1186  else
1187  {
1188  // adjust
1189  objectt o=o_it->second;
1190  exprt tmp(object);
1191  to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
1192  insert(new_object_map, tmp, o);
1193  changed=true;
1194  }
1195  }
1196  else
1197  set(new_object_map, o_it);
1198  }
1199 
1200  if(changed)
1201  v_it->second.object_map=new_object_map;
1202  }
1203 }
1204 
1206  const exprt &lhs,
1207  const object_mapt &values_rhs,
1208  const std::string &suffix,
1209  const namespacet &ns,
1210  assign_recursion_sett &recursion_set)
1211 {
1212  #if 0
1213  std::cout << "ASSIGN_REC LHS: " << from_expr(ns, "", lhs) << '\n';
1214  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1215 
1216  for(object_map_dt::const_iterator it=values_rhs.read().begin();
1217  it!=values_rhs.read().end(); it++)
1218  std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1219  #endif
1220 
1221  if(lhs.type().id()=="#REF#")
1222  {
1223  const irep_idt &ident = lhs.get(ID_identifier);
1224  object_mapt temp;
1225  gvs_recursion_sett recset;
1226  get_value_set_rec(lhs, temp, "", lhs.type().subtype(), ns, recset);
1227 
1228  if(recursion_set.find(ident)!=recursion_set.end())
1229  {
1230  recursion_set.insert(ident);
1231 
1232  forall_objects(it, temp.read())
1233  if(object_numbering[it->first].id()!=ID_unknown)
1234  assign_rec(object_numbering[it->first], values_rhs,
1235  suffix, ns, recursion_set);
1236 
1237  recursion_set.erase(ident);
1238  }
1239  }
1240  else if(lhs.id()==ID_symbol)
1241  {
1242  const irep_idt &identifier=lhs.get(ID_identifier);
1243 
1244  if(has_prefix(id2string(identifier),
1245  "value_set::dynamic_object") ||
1246  has_prefix(id2string(identifier),
1247  "value_set::return_value") ||
1248  values.find(id2string(identifier)+suffix)!=values.end())
1249  // otherwise we don't track this value
1250  {
1251  entryt &entry = get_entry(identifier, suffix);
1252 
1253  if(make_union(entry.object_map, values_rhs))
1254  changed = true;
1255  }
1256  }
1257  else if(lhs.id()==ID_dynamic_object)
1258  {
1261 
1262  const std::string name=
1263  "value_set::dynamic_object"+
1264  std::to_string(dynamic_object.get_instance());
1265 
1266  if(make_union(get_entry(name, suffix).object_map, values_rhs))
1267  changed = true;
1268  }
1269  else if(lhs.id()==ID_dereference)
1270  {
1271  if(lhs.operands().size()!=1)
1272  throw lhs.id_string()+" expected to have one operand";
1273 
1274  object_mapt reference_set;
1275  get_reference_set_sharing(lhs, reference_set, ns);
1276 
1277  forall_objects(it, reference_set.read())
1278  {
1279  const exprt &object=object_numbering[it->first];
1280 
1281  if(object.id()!=ID_unknown)
1282  assign_rec(object, values_rhs, suffix, ns, recursion_set);
1283  }
1284  }
1285  else if(lhs.id()==ID_index)
1286  {
1287  if(lhs.operands().size()!=2)
1288  throw "index expected to have two operands";
1289 
1290  const typet &type=ns.follow(lhs.op0().type());
1291 
1292  assert(type.id()==ID_array ||
1293  type.id()==ID_incomplete_array ||
1294  type.id()=="#REF#");
1295 
1296  assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set);
1297  }
1298  else if(lhs.id()==ID_member)
1299  {
1300  if(lhs.operands().size()!=1)
1301  throw "member expected to have one operand";
1302 
1303  if(lhs.op0().is_nil())
1304  return;
1305 
1306  const std::string &component_name=lhs.get_string(ID_component_name);
1307 
1308  const typet &type=ns.follow(lhs.op0().type());
1309 
1310  assert(type.id()==ID_struct ||
1311  type.id()==ID_union ||
1312  type.id()==ID_incomplete_struct ||
1313  type.id()==ID_incomplete_union);
1314 
1315  assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
1316  ns, recursion_set);
1317  }
1318  else if(lhs.id()=="valid_object" ||
1319  lhs.id()=="dynamic_size" ||
1320  lhs.id()=="dynamic_type")
1321  {
1322  // we ignore this here
1323  }
1324  else if(lhs.id()==ID_string_constant)
1325  {
1326  // someone writes into a string-constant
1327  // evil guy
1328  }
1329  else if(lhs.id()=="NULL-object")
1330  {
1331  // evil as well
1332  }
1333  else if(lhs.id()==ID_typecast)
1334  {
1335  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1336 
1337  assign_rec(typecast_expr.op(), values_rhs, suffix, ns, recursion_set);
1338  }
1339  else if(lhs.id()=="zero_string" ||
1340  lhs.id()=="is_zero_string" ||
1341  lhs.id()=="zero_string_length")
1342  {
1343  // ignore
1344  }
1345  else if(lhs.id()==ID_byte_extract_little_endian ||
1346  lhs.id()==ID_byte_extract_big_endian)
1347  {
1348  assert(lhs.operands().size()==2);
1349  assign_rec(lhs.op0(), values_rhs, suffix, ns, recursion_set);
1350  }
1351  else
1352  throw "assign NYI: `"+lhs.id_string()+"'";
1353 }
1354 
1356  const irep_idt &function,
1357  const exprt::operandst &arguments,
1358  const namespacet &ns)
1359 {
1360  const symbolt &symbol=ns.lookup(function);
1361 
1362  const code_typet &type=to_code_type(symbol.type);
1363  const code_typet::parameterst &parameter_types=type.parameters();
1364 
1365  // these first need to be assigned to dummy, temporary arguments
1366  // and only thereafter to the actuals, in order
1367  // to avoid overwriting actuals that are needed for recursive
1368  // calls
1369 
1370  for(unsigned i=0; i<arguments.size(); i++)
1371  {
1372  const std::string identifier="value_set::" + id2string(function) + "::" +
1373  "argument$"+std::to_string(i);
1374  add_var(identifier, "");
1375  exprt dummy_lhs=symbol_exprt(identifier, arguments[i].type());
1376  assign(dummy_lhs, arguments[i], ns);
1377  }
1378 
1379  // now assign to 'actual actuals'
1380 
1381  unsigned i=0;
1382 
1383  for(code_typet::parameterst::const_iterator
1384  it=parameter_types.begin();
1385  it!=parameter_types.end();
1386  it++)
1387  {
1388  const irep_idt &identifier=it->get_identifier();
1389  if(identifier.empty())
1390  continue;
1391 
1392  add_var(identifier, "");
1393 
1394  const exprt v_expr=
1395  symbol_exprt("value_set::" + id2string(function) + "::" +
1396  "argument$"+std::to_string(i), it->type());
1397 
1398  exprt actual_lhs=symbol_exprt(identifier, it->type());
1399  assign(actual_lhs, v_expr, ns);
1400  i++;
1401  }
1402 }
1403 
1405  const exprt &lhs,
1406  const namespacet &ns)
1407 {
1408  if(lhs.is_nil())
1409  return;
1410 
1411  std::string rvs = "value_set::return_value" + std::to_string(from_function);
1412  symbol_exprt rhs(rvs, lhs.type());
1413 
1414  assign(lhs, rhs, ns);
1415 }
1416 
1418  const exprt &code,
1419  const namespacet &ns)
1420 {
1421  const irep_idt &statement=code.get(ID_statement);
1422 
1423  if(statement==ID_block)
1424  {
1425  forall_operands(it, code)
1426  apply_code(*it, ns);
1427  }
1428  else if(statement==ID_function_call)
1429  {
1430  // shouldn't be here
1431  assert(false);
1432  }
1433  else if(statement==ID_assign ||
1434  statement==ID_init)
1435  {
1436  if(code.operands().size()!=2)
1437  throw "assignment expected to have two operands";
1438 
1439  assign(code.op0(), code.op1(), ns);
1440  }
1441  else if(statement==ID_decl)
1442  {
1443  if(code.operands().size()!=1)
1444  throw "decl expected to have one operand";
1445 
1446  const exprt &lhs=code.op0();
1447 
1448  if(lhs.id()!=ID_symbol)
1449  throw "decl expected to have symbol on lhs";
1450 
1451  assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1452  }
1453  else if(statement==ID_specc_notify ||
1454  statement==ID_specc_wait)
1455  {
1456  // ignore, does not change variables
1457  }
1458  else if(statement==ID_expression)
1459  {
1460  // can be ignored, we don't expect side effects here
1461  }
1462  else if(statement==ID_cpp_delete ||
1463  statement==ID_cpp_delete_array)
1464  {
1465  // does nothing
1466  }
1467  else if(statement==ID_free)
1468  {
1469  // this may kill a valid bit
1470 
1471  if(code.operands().size()!=1)
1472  throw "free expected to have one operand";
1473 
1474  do_free(code.op0(), ns);
1475  }
1476  else if(statement=="lock" || statement=="unlock")
1477  {
1478  // ignore for now
1479  }
1480  else if(statement==ID_asm)
1481  {
1482  // ignore for now, probably not safe
1483  }
1484  else if(statement==ID_nondet)
1485  {
1486  // doesn't do anything
1487  }
1488  else if(statement==ID_printf)
1489  {
1490  // doesn't do anything
1491  }
1492  else if(statement==ID_return)
1493  {
1494  // this is turned into an assignment
1495  if(code.operands().size()==1)
1496  {
1497  std::string rvs="value_set::return_value"+std::to_string(from_function);
1498  symbol_exprt lhs(rvs, code.op0().type());
1499  assign(lhs, code.op0(), ns);
1500  }
1501  }
1502  else if(statement==ID_fence)
1503  {
1504  }
1505  else if(statement==ID_array_copy ||
1506  statement==ID_array_replace ||
1507  statement==ID_array_set)
1508  {
1509  }
1510  else if(statement==ID_input || statement==ID_output)
1511  {
1512  // doesn't do anything
1513  }
1514  else
1515  throw
1516  code.pretty()+"\n"+
1517  "value_set_fit: unexpected statement: "+id2string(statement);
1518 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
void output(const namespacet &ns, std::ostream &out) const
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
std::unordered_set< unsigned int > dynamic_object_id_sett
Definition: value_set_fi.h:161
BigInt mp_integer
Definition: mp_arith.h:19
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
std::unordered_set< idt, string_hash > flatten_seent
Definition: value_set_fi.h:171
std::unordered_set< exprt, irep_hash > expr_sett
Definition: value_set_fi.h:159
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
Definition: std_expr.h:1701
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
unsigned int get_instance() const
Definition: std_expr.cpp:45
void do_free(const exprt &op, const namespacet &ns)
std::unordered_map< idt, entryt, string_hash > valuest
Definition: value_set_fi.h:170
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
Definition: std_types.h:829
exprt to_expr(object_map_dt::const_iterator it) const
const componentst & components() const
Definition: std_types.h:242
static const char * alloc_adapter_prefix
bool is_true() const
Definition: expr.cpp:133
Value Set (Flow Insensitive, Sharing)
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static const object_map_dt blank
Definition: value_set_fi.h:75
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
exprt & op()
Definition: std_expr.h:1739
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
void apply_code(const exprt &code, const namespacet &ns)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
std::unordered_set< idt, string_hash > gvs_recursion_sett
Definition: value_set_fi.h:172
unsigned from_function
Definition: value_set_fi.h:33
const irep_idt & id() const
Definition: irep.h:189
bool make_union(object_mapt &dest, const object_mapt &src) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
The boolean constant true.
Definition: std_expr.h:3742
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
#define Forall_objects(it, map)
static object_numberingt object_numbering
Definition: value_set_fi.h:35
API to expression classes.
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
entryt & get_entry(const idt &id, const std::string &suffix)
Definition: value_set_fi.h:206
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1578
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
#define forall_operands(it, expr)
Definition: expr.h:17
bitvector_typet index_type()
Definition: c_types.cpp:15
Symbol table.
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
Operator to return the address of an object.
Definition: std_expr.h:2593
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void flatten(const entryt &e, object_mapt &dest) const
bool is_constant() const
Definition: expr.cpp:128
valuest values
Definition: value_set_fi.h:234
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const irep_idt & display_name() const
Definition: symbol.h:60
void do_end_function(const exprt &lhs, const namespacet &ns)
typet type
Type of symbol.
Definition: symbol.h:37
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
std::unordered_set< idt, string_hash > assign_recursion_sett
Definition: value_set_fi.h:174
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
void dereference_rec(const exprt &src, exprt &dest) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fi.h:36
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const T & read() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
const std::string & id_string() const
Definition: irep.h:192
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
bool is_zero() const
Definition: expr.cpp:236
void add_var(const idt &id, const std::string &suffix)
Definition: value_set_fi.h:196
bool offset_is_zero() const
Definition: value_set_fi.h:67
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
exprt dynamic_object(const exprt &pointer)
object_mapt object_map
Definition: value_set_fi.h:144
bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set_fi.h:87
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
TO_BE_DOCUMENTED.
Definition: std_expr.h:1658
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
unsigned from_target_index
Definition: value_set_fi.h:34
#define forall_objects(it, map)
bool simplify(exprt &expr, const namespacet &ns)