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