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