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