cprover
value_set_fivr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set (Flow Insensitive, Sharing, Validity Regions)
4 
5 Author: Daniel Kroening, kroening@kroening.com,
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
13 #include "value_set_fivr.h"
14 
15 #include <cassert>
16 #include <ostream>
17 
18 #include <util/symbol_table.h>
19 #include <util/simplify_expr.h>
20 #include <util/base_type.h>
21 #include <util/std_expr.h>
22 #include <util/prefix.h>
23 #include <util/std_code.h>
24 #include <util/arith_tools.h>
25 
26 #include <langapi/language_util.h>
27 #include <util/c_types.h>
28 
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_valid_objects(it, map) \
41  for(object_map_dt::const_iterator (it)=(map).begin(); \
42  (it)!=(map).end(); \
43  (it)++) \
44  if((map).is_valid_at((it)->first, from_function, from_target_index))
45 
46 #define Forall_objects(it, map) \
47  for(object_map_dt::iterator (it)=(map).begin(); \
48  (it)!=(map).end(); \
49  (it)++)
50 
51 #define Forall_valid_objects(it, map) \
52  for(object_map_dt::iterator (it)=(map).begin(); \
53  (it)!=(map).end(); \
54  (it)++) \
55  if((map).is_valid_at((it)->first, from_function, from_target_index)) /* NOLINT(*) */
56 
58  const namespacet &ns,
59  std::ostream &out) const
60 {
61  for(valuest::const_iterator
62  v_it=values.begin();
63  v_it!=values.end();
64  v_it++)
65  {
66  irep_idt identifier, display_name;
67 
68  const entryt &e=v_it->second;
69 
70  // do we need to output at all?
71 // bool yes=false;
72 // for (object_map_dt::const_iterator it=e.object_map.read().begin();
73 // it!=e.object_map.read().end();
74 // it++)
75 // if (e.object_map.read().is_valid_at(it->first,
76 // from_function,
77 // from_target_index)) yes=true;
78 // if (!yes) continue;
79 
80 // const object_mapt &object_map=e.object_map;
81  object_mapt object_map;
82  flatten(e, object_map);
83 
84 // if(has_prefix(id2string(e.identifier), "value_set::dynamic_object"))
85 // {
86 // display_name=id2string(e.identifier)+e.suffix;
87 // identifier="";
88 // }
89 // else if(e.identifier=="value_set::return_value")
90 // {
91 // display_name="RETURN_VALUE"+e.suffix;
92 // identifier="";
93 // }
94 // else
95  {
96  #if 0
97  const symbolt &symbol=ns.lookup(id2string(e.identifier));
98  display_name=symbol.display_name()+e.suffix;
99  identifier=symbol.name;
100  #else
101  identifier=id2string(e.identifier);
102  display_name=id2string(identifier)+e.suffix;
103  #endif
104  }
105 
106  out << display_name << "={ ";
107  if(!object_map.read().empty())
108  out << "\n ";
109 
110  std::size_t width=0;
111 
112  forall_objects(o_it, object_map.read())
113  {
114  const exprt &o=object_numbering[o_it->first];
115 
116  std::string result="<"; // +std::to_string(o_it->first) + ",";
117 
118  if(o.id()==ID_invalid)
119  {
120  result+='#';
121  result+=", *, "; // offset unknown
122  if(o.type().id()==ID_unknown)
123  result+='*';
124  else if(o.type().id()==ID_invalid)
125  result+='#';
126  else
127  result+=from_type(ns, identifier, o.type());
128  result+='>';
129  }
130  else if(o.id()==ID_unknown)
131  {
132  result+='*';
133  result+=", *, "; // offset unknown
134  if(o.type().id()==ID_unknown)
135  result+='*';
136  else if(o.type().id()==ID_invalid)
137  result+='#';
138  else
139  result+=from_type(ns, identifier, o.type());
140  result+='>';
141  }
142  else
143  {
144  result+=from_expr(ns, identifier, o)+", ";
145 
146  if(o_it->second.offset_is_set)
147  result+=integer2string(o_it->second.offset)+"";
148  else
149  result+='*';
150 
151  result+=", ";
152 
153  if(o.type().id()==ID_unknown)
154  result+='*';
155  else
156  {
157  if(o.type().id()=="#REF#")
158  result += "#REF#";
159  else
160  result+=from_type(ns, identifier, o.type());
161  }
162 
163 
164  result+='>';
165  }
166 
167  out << result << '\n';
168 
169  #if 0
170  object_map_dt::validity_rangest::const_iterator vr =
171  object_map.read().validity_ranges.find(o_it->first);
172 
173  if(vr != object_map.read().validity_ranges.end())
174  {
175  if(vr->second.empty())
176  std::cout << " Empty validity record\n";
177  else
178  {
179  for(object_map_dt::vrange_listt::const_iterator vit =
180  vr->second.begin();
181  vit!=vr->second.end();
182  vit++)
183  {
184  out << " valid at " << function_numbering[vit->function] <<
185  " [" << vit->from << "," << vit->to << "]";
186  if(from_function==vit->function &&
187  from_target_index>=vit->from &&
188  from_target_index<=vit->to)
189  out << " (*)";
190  out << '\n';
191  }
192  }
193  }
194  else
195  {
196  out << " No validity information\n";
197  }
198  #endif
199 
200  width+=result.size();
201 
203  next++;
204 
205  if(next!=object_map.read().end())
206  {
207  out << "\n ";
208  }
209  }
210 
211  out << " } \n";
212  }
213 }
214 
216  const entryt &e,
217  object_mapt &dest) const
218 {
219  #if 0
220  std::cout << "FLATTEN: " << e.identifier << e.suffix << '\n';
221  #endif
222 
223  flatten_seent seen;
225 
226  #if 0
227  std::cout << "FLATTEN: Done.\n";
228  #endif
229 }
230 
232  const entryt &e,
233  object_mapt &dest,
234  flatten_seent &seen,
235  unsigned at_function,
236  unsigned at_index) const
237 {
238  #if 0
239  std::cout << "FLATTEN_REC: " << e.identifier << e.suffix << '\n';
240  #endif
241 
242  std::string identifier=id2string(e.identifier);
243  assert(seen.find(identifier + e.suffix)==seen.end());
244 
245  bool generalize_index=false;
246  std::list<const object_map_dt::vrange_listt*> add_ranges;
247 
248  seen.insert(identifier + e.suffix);
249 
251  {
252  const exprt &o=object_numbering[it->first];
253 
254  if(o.type().id()=="#REF#")
255  {
256  if(seen.find(o.get(ID_identifier))!=seen.end())
257  {
258  generalize_index=true;
259 
260  object_map_dt::validity_rangest::const_iterator vit=
261  e.object_map.read().validity_ranges.find(it->first);
262 
263  if(vit!=e.object_map.read().validity_ranges.end())
264  {
265  const object_map_dt::vrange_listt &vl=vit->second;
266  add_ranges.push_back(&vl);
267  }
268  continue;
269  }
270 
271  valuest::const_iterator fi=values.find(o.get(ID_identifier));
272  if(fi==values.end())
273  {
274  // this is some static object, keep it in.
275  exprt se(ID_symbol, o.type().subtype());
276  se.set(ID_identifier, o.get(ID_identifier));
277  insert_from(dest, se, 0);
278  }
279  else
280  {
281  // we need to flatten_rec wherever the entry
282  // _started_ to become valid
283 
284  object_map_dt::validity_rangest::const_iterator ranges_it =
285  e.object_map.read().validity_ranges.find(it->first);
286  if(ranges_it!=e.object_map.read().validity_ranges.end())
287  {
288  for(object_map_dt::vrange_listt::const_iterator r_it =
289  ranges_it->second.begin();
290  r_it!=ranges_it->second.end();
291  r_it++)
292  {
293  // we only need to check the current function;
294  // the entry must have been valid within that function
295  if(r_it->function==at_function)
296  {
297  object_mapt temp;
298  flatten_rec(fi->second, temp, seen, r_it->function, r_it->from);
299 
300  for(object_map_dt::iterator t_it=temp.write().begin();
301  t_it!=temp.write().end();
302  t_it++)
303  {
304  if(t_it->second.offset_is_set &&
305  it->second.offset_is_set)
306  {
307  t_it->second.offset += it->second.offset;
308  }
309  else
310  t_it->second.offset_is_set=false;
311  }
312 
313  forall_objects(oit, temp.read())
314  insert_from(dest, oit);
315  }
316  }
317  }
318  }
319  }
320  else
321  insert_from(dest, it);
322  }
323 
324  if(generalize_index) // this means we had recursive symbols in there
325  {
326  Forall_objects(it, dest.write())
327  {
328  it->second.offset_is_set=false;
329  for(std::list<const object_map_dt::vrange_listt*>::const_iterator vit =
330  add_ranges.begin();
331  vit!=add_ranges.end();
332  vit++)
333  {
334  for(object_map_dt::vrange_listt::const_iterator lit =
335  (*vit)->begin();
336  lit!=(*vit)->end();
337  lit++)
338  dest.write().set_valid_at(it->first, *lit);
339  }
340  }
341  }
342 
343  seen.erase(identifier + e.suffix);
344 }
345 
347 {
348  const exprt &object=object_numbering[it->first];
349 
350  if(object.id()==ID_invalid ||
351  object.id()==ID_unknown)
352  return object;
353 
355 
356  od.object()=object;
357 
358  if(it->second.offset_is_set)
359  od.offset()=from_integer(it->second.offset, index_type());
360 
361  od.type()=od.object().type();
362 
363  return od;
364 }
365 
367  object_mapt &dest,
368  const object_mapt &src) const
369 {
370  bool result=false;
371 
372  forall_objects(it, src.read())
373  {
374  if(insert_to(dest, it))
375  result=true;
376  }
377 
378  return result;
379 }
380 
382  object_mapt &dest,
383  const object_mapt &src) const
384 {
385  bool result=false;
386 
387  forall_valid_objects(it, src.read())
388  {
389  if(insert_to(dest, it))
390  result=true;
391  }
392 
393  return result;
394 }
395 
397  object_mapt &dest,
398  const object_mapt &src) const
399 {
400  forall_valid_objects(it, src.read())
401  {
402  dest.write()[it->first]=it->second;
403  dest.write().validity_ranges[it->first].push_back(
407  }
408 }
409 
411  const exprt &expr,
412  std::list<exprt> &value_set,
413  const namespacet &ns) const
414 {
415  object_mapt object_map;
416  get_value_set(expr, object_map, ns);
417 
418  object_mapt flat_map;
419 
420  forall_objects(it, object_map.read())
421  {
422  const exprt &object=object_numbering[it->first];
423  if(object.type().id()=="#REF#")
424  {
425  assert(object.id()==ID_symbol);
426 
427  const irep_idt &ident=object.get(ID_identifier);
428  valuest::const_iterator v_it=values.find(ident);
429 
430  if(v_it!=values.end())
431  {
432  object_mapt temp;
433  flatten(v_it->second, temp);
434 
435  for(object_map_dt::iterator t_it=temp.write().begin();
436  t_it!=temp.write().end();
437  t_it++)
438  {
439  if(t_it->second.offset_is_set &&
440  it->second.offset_is_set)
441  {
442  t_it->second.offset += it->second.offset;
443  }
444  else
445  t_it->second.offset_is_set=false;
446 
447  flat_map.write()[t_it->first]=t_it->second;
448  }
449  }
450  }
451  else
452  flat_map.write()[it->first]=it->second;
453  }
454 
455  forall_objects(fit, flat_map.read())
456  value_set.push_back(to_expr(fit));
457 
458  #if 0
459  // Sanity check!
460  for(std::list<exprt>::const_iterator it=value_set.begin();
461  it!=value_set.end();
462  it++)
463  assert(it->type().id()!="#REF");
464  #endif
465 
466  #if 0
467  for(std::list<exprt>::const_iterator it=value_set.begin();
468  it!=value_set.end();
469  it++)
470  std::cout << "GET_VALUE_SET: " << from_expr(ns, "", *it) << '\n';
471  #endif
472 }
473 
475  const exprt &expr,
476  object_mapt &dest,
477  const namespacet &ns) const
478 {
479  exprt tmp(expr);
480  simplify(tmp, ns);
481 
482  gvs_recursion_sett recset;
483  get_value_set_rec(tmp, dest, "", tmp.type(), ns, recset);
484 }
485 
487  const exprt &expr,
488  object_mapt &dest,
489  const std::string &suffix,
490  const typet &original_type,
491  const namespacet &ns,
492  gvs_recursion_sett &recursion_set) const
493 {
494  #if 0
495  std::cout << "GET_VALUE_SET_REC EXPR: " << expr << '\n';
496  std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
497  std::cout << '\n';
498  #endif
499 
500  if(expr.type().id()=="#REF#")
501  {
502  valuest::const_iterator fi=values.find(expr.get(ID_identifier));
503 
504  if(fi!=values.end())
505  {
506  forall_valid_objects(it, fi->second.object_map.read())
507  get_value_set_rec(object_numbering[it->first], dest, suffix,
508  original_type, ns, recursion_set);
509  return;
510  }
511  else
512  {
513  insert_from(dest, exprt(ID_unknown, original_type));
514  return;
515  }
516  }
517  else if(expr.id()==ID_unknown || expr.id()==ID_invalid)
518  {
519  insert_from(dest, exprt(ID_unknown, original_type));
520  return;
521  }
522  else if(expr.id()==ID_index)
523  {
524  assert(expr.operands().size()==2);
525 
526  const typet &type=ns.follow(expr.op0().type());
527 
528  assert(type.id()==ID_array ||
529  type.id()==ID_incomplete_array ||
530  type.id()=="#REF#");
531 
532  get_value_set_rec(expr.op0(), dest, "[]"+suffix,
533  original_type, ns, recursion_set);
534 
535  return;
536  }
537  else if(expr.id()==ID_member)
538  {
539  assert(expr.operands().size()==1);
540 
541  if(expr.op0().is_not_nil())
542  {
543  const typet &type=ns.follow(expr.op0().type());
544 
545  assert(type.id()==ID_struct ||
546  type.id()==ID_union ||
547  type.id()==ID_incomplete_struct ||
548  type.id()==ID_incomplete_union);
549 
550  const std::string &component_name=
551  expr.get_string(ID_component_name);
552 
553  get_value_set_rec(expr.op0(), dest, "."+component_name+suffix,
554  original_type, ns, recursion_set);
555 
556  return;
557  }
558  }
559  else if(expr.id()==ID_symbol)
560  {
561  // just keep a reference to the ident in the set
562  // (if it exists)
563  irep_idt ident=expr.get_string(ID_identifier)+suffix;
564 
566  {
567  insert_from(dest, expr, 0);
568  return;
569  }
570  else
571  {
572  valuest::const_iterator v_it=values.find(ident);
573 
574  if(v_it!=values.end())
575  {
576  typet t("#REF#");
577  t.subtype()=expr.type();
578  symbol_exprt sym(ident, t);
579  insert_from(dest, sym, 0);
580  return;
581  }
582  }
583  }
584  else if(expr.id()==ID_if)
585  {
586  if(expr.operands().size()!=3)
587  throw "if takes three operands";
588 
589  get_value_set_rec(expr.op1(), dest, suffix,
590  original_type, ns, recursion_set);
591  get_value_set_rec(expr.op2(), dest, suffix,
592  original_type, ns, recursion_set);
593 
594  return;
595  }
596  else if(expr.id()==ID_address_of)
597  {
598  if(expr.operands().size()!=1)
599  throw expr.id_string()+" expected to have one operand";
600 
601  get_reference_set_sharing(expr.op0(), dest, ns);
602 
603  return;
604  }
605  else if(expr.id()==ID_dereference)
606  {
607  object_mapt reference_set;
608  get_reference_set_sharing(expr, reference_set, ns);
609  const object_map_dt &object_map=reference_set.read();
610 
611  if(object_map.begin()!=object_map.end())
612  {
613  forall_objects(it1, object_map)
614  {
615  const exprt &object=object_numbering[it1->first];
616  get_value_set_rec(object, dest, suffix,
617  original_type, ns, recursion_set);
618  }
619 
620  return;
621  }
622  }
623  else if(expr.id()=="reference_to")
624  {
625  object_mapt reference_set;
626 
627  get_reference_set_sharing(expr, reference_set, ns);
628 
629  const object_map_dt &object_map=reference_set.read();
630 
631  if(object_map.begin()!=object_map.end())
632  {
633  forall_objects(it, object_map)
634  {
635  const exprt &object=object_numbering[it->first];
636  get_value_set_rec(object, dest, suffix,
637  original_type, ns, recursion_set);
638  }
639 
640  return;
641  }
642  }
643  else if(expr.is_constant())
644  {
645  // check if NULL
646  if(expr.get(ID_value)==ID_NULL &&
647  expr.type().id()==ID_pointer)
648  {
649  insert_from(dest, exprt("NULL-object", expr.type().subtype()), 0);
650  return;
651  }
652  }
653  else if(expr.id()==ID_typecast)
654  {
655  if(expr.operands().size()!=1)
656  throw "typecast takes one operand";
657 
658  get_value_set_rec(expr.op0(), dest, suffix,
659  original_type, ns, recursion_set);
660 
661  return;
662  }
663  else if(expr.id()==ID_plus || expr.id()==ID_minus)
664  {
665  if(expr.operands().size()<2)
666  throw expr.id_string()+" expected to have at least two operands";
667 
668  if(expr.type().id()==ID_pointer)
669  {
670  // find the pointer operand
671  const exprt *ptr_operand=nullptr;
672 
673  forall_operands(it, expr)
674  if(it->type().id()==ID_pointer)
675  {
676  if(ptr_operand==nullptr)
677  ptr_operand=&(*it);
678  else
679  throw "more than one pointer operand in pointer arithmetic";
680  }
681 
682  if(ptr_operand==nullptr)
683  throw "pointer type sum expected to have pointer operand";
684 
685  object_mapt pointer_expr_set;
686  get_value_set_rec(*ptr_operand, pointer_expr_set, "",
687  ptr_operand->type(), ns, recursion_set);
688 
689  forall_objects(it, pointer_expr_set.read())
690  {
691  objectt object=it->second;
692 
693  if(object.offset_is_zero() &&
694  expr.operands().size()==2)
695  {
696  if(expr.op0().type().id()!=ID_pointer)
697  {
698  mp_integer i;
699  if(to_integer(expr.op0(), i))
700  object.offset_is_set=false;
701  else
702  object.offset=(expr.id()==ID_plus)? i : -i;
703  }
704  else
705  {
706  mp_integer i;
707  if(to_integer(expr.op1(), i))
708  object.offset_is_set=false;
709  else
710  object.offset=(expr.id()==ID_plus)? i : -i;
711  }
712  }
713  else
714  object.offset_is_set=false;
715 
716  insert_from(dest, it->first, object);
717  }
718 
719  return;
720  }
721  }
722  else if(expr.id()==ID_side_effect)
723  {
724  const irep_idt &statement=expr.get(ID_statement);
725 
726  if(statement==ID_function_call)
727  {
728  // these should be gone
729  throw "unexpected function_call sideeffect";
730  }
731  else if(statement==ID_malloc)
732  {
733  if(expr.type().id()!=ID_pointer)
734  throw "malloc expected to return pointer type";
735 
736  assert(suffix=="");
737 
738  const typet &dynamic_type=
739  static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
740 
741  dynamic_object_exprt dynamic_object(dynamic_type);
742  // let's make up a `unique' number for this object...
743  dynamic_object.set_instance(
744  (from_function << 16) | from_target_index);
745  dynamic_object.valid()=true_exprt();
746 
747  insert_from(dest, dynamic_object, 0);
748  return;
749  }
750  else if(statement==ID_cpp_new ||
751  statement==ID_cpp_new_array)
752  {
753  assert(suffix=="");
754  assert(expr.type().id()==ID_pointer);
755 
756  dynamic_object_exprt dynamic_object(expr.type().subtype());
757  // let's make up a unique number for this object...
758  dynamic_object.set_instance(
759  (from_function << 16) | from_target_index);
760  dynamic_object.valid()=true_exprt();
761 
762  insert_from(dest, dynamic_object, 0);
763  return;
764  }
765  }
766  else if(expr.id()==ID_struct)
767  {
768  // this is like a static struct object
769  insert_from(dest, address_of_exprt(expr), 0);
770  return;
771  }
772  else if(expr.id()==ID_with ||
773  expr.id()==ID_array_of ||
774  expr.id()==ID_array)
775  {
776  // these are supposed to be done by assign()
777  throw "unexpected value in get_value_set: "+expr.id_string();
778  }
779  else if(expr.id()==ID_dynamic_object)
780  {
783 
784  const std::string name=
785  "value_set::dynamic_object"+
786  std::to_string(dynamic_object.get_instance())+
787  suffix;
788 
789  // look it up
790  valuest::const_iterator v_it=values.find(name);
791 
792  if(v_it!=values.end())
793  {
794  copy_objects(dest, v_it->second.object_map);
795  return;
796  }
797  }
798 
799  insert_from(dest, exprt(ID_unknown, original_type));
800 }
801 
803  const exprt &src,
804  exprt &dest) const
805 {
806  // remove pointer typecasts
807  if(src.id()==ID_typecast)
808  {
809  assert(src.type().id()==ID_pointer);
810 
811  if(src.operands().size()!=1)
812  throw "typecast expects one operand";
813 
814  dereference_rec(src.op0(), dest);
815  }
816  else
817  dest=src;
818 }
819 
821  const exprt &expr,
822  expr_sett &dest,
823  const namespacet &ns) const
824 {
825  object_mapt object_map;
826  get_reference_set_sharing(expr, object_map, ns);
827 
828  forall_objects(it, object_map.read())
829  {
830  const exprt &expr=object_numbering[it->first];
831 
832  if(expr.type().id()=="#REF#")
833  {
834  const irep_idt &ident=expr.get(ID_identifier);
835  valuest::const_iterator vit=values.find(ident);
836  if(vit==values.end())
837  {
838  // Assume the variable never was assigned,
839  // so assume it's reference set is unknown.
840  dest.insert(exprt(ID_unknown, expr.type()));
841  }
842  else
843  {
844  object_mapt omt;
845  flatten(vit->second, omt);
846 
847  for(object_map_dt::iterator t_it=omt.write().begin();
848  t_it!=omt.write().end();
849  t_it++)
850  {
851  if(t_it->second.offset_is_set &&
852  it->second.offset_is_set)
853  {
854  t_it->second.offset += it->second.offset;
855  }
856  else
857  t_it->second.offset_is_set=false;
858  }
859 
860  forall_objects(it, omt.read())
861  dest.insert(to_expr(it));
862  }
863  }
864  else
865  dest.insert(to_expr(it));
866  }
867 }
868 
870  const exprt &expr,
871  expr_sett &dest,
872  const namespacet &ns) const
873 {
874  object_mapt object_map;
875  get_reference_set_sharing(expr, object_map, ns);
876 
877  forall_objects(it, object_map.read())
878  dest.insert(to_expr(it));
879 }
880 
882  const exprt &expr,
883  object_mapt &dest,
884  const namespacet &ns) const
885 {
886  #if 0
887  std::cout << "GET_REFERENCE_SET_REC EXPR: " << from_expr(ns, "", expr)
888  << '\n';
889  #endif
890 
891  if(expr.type().id()=="#REF#")
892  {
893  valuest::const_iterator fi=values.find(expr.get(ID_identifier));
894  if(fi!=values.end())
895  {
896  forall_valid_objects(it, fi->second.object_map.read())
897  get_reference_set_sharing_rec(object_numbering[it->first], dest, ns);
898  return;
899  }
900  }
901  else if(expr.id()==ID_symbol ||
902  expr.id()==ID_dynamic_object ||
903  expr.id()==ID_string_constant)
904  {
905  if(expr.type().id()==ID_array &&
906  expr.type().subtype().id()==ID_array)
907  insert_from(dest, expr);
908  else
909  insert_from(dest, expr, 0);
910 
911  return;
912  }
913  else if(expr.id()==ID_dereference)
914  {
915  if(expr.operands().size()!=1)
916  throw expr.id_string()+" expected to have one operand";
917 
918  gvs_recursion_sett recset;
919  object_mapt temp;
920  get_value_set_rec(expr.op0(), temp, "", expr.op0().type(), ns, recset);
921 
922  // REF's need to be dereferenced manually!
923  forall_objects(it, temp.read())
924  {
925  const exprt &obj=object_numbering[it->first];
926  if(obj.type().id()=="#REF#")
927  {
928  const irep_idt &ident=obj.get(ID_identifier);
929  valuest::const_iterator v_it=values.find(ident);
930 
931  if(v_it!=values.end())
932  {
933  object_mapt t2;
934  flatten(v_it->second, t2);
935 
936  for(object_map_dt::iterator t_it=t2.write().begin();
937  t_it!=t2.write().end();
938  t_it++)
939  {
940  if(t_it->second.offset_is_set &&
941  it->second.offset_is_set)
942  {
943  t_it->second.offset += it->second.offset;
944  }
945  else
946  t_it->second.offset_is_set=false;
947  }
948 
949  forall_objects(it2, t2.read())
950  insert_from(dest, it2);
951  }
952  else
953  insert_from(dest, exprt(ID_unknown, obj.type().subtype()));
954  }
955  else
956  insert_from(dest, it);
957  }
958 
959  #if 0
960  for(expr_sett::const_iterator it=value_set.begin();
961  it!=value_set.end();
962  it++)
963  std::cout << "VALUE_SET: " << from_expr(ns, "", *it) << '\n';
964  #endif
965 
966  return;
967  }
968  else if(expr.id()==ID_index)
969  {
970  if(expr.operands().size()!=2)
971  throw "index expected to have two operands";
972 
973  const exprt &array=expr.op0();
974  const exprt &offset=expr.op1();
975  const typet &array_type=ns.follow(array.type());
976 
977  assert(array_type.id()==ID_array ||
978  array_type.id()==ID_incomplete_array);
979 
980  object_mapt array_references;
981  get_reference_set_sharing(array, array_references, ns);
982 
983  const object_map_dt &object_map=array_references.read();
984 
985  forall_objects(a_it, object_map)
986  {
987  const exprt &object=object_numbering[a_it->first];
988 
989  if(object.id()==ID_unknown)
990  insert_from(dest, exprt(ID_unknown, expr.type()));
991  else
992  {
993  exprt index_expr(ID_index, expr.type());
994  index_expr.operands().resize(2);
995  index_expr.op0()=object;
996  index_expr.op1()=from_integer(0, index_type());
997 
998  // adjust type?
999  if(object.type().id()!="#REF#" &&
1000  ns.follow(object.type())!=array_type)
1001  index_expr.make_typecast(array.type());
1002 
1003  objectt o=a_it->second;
1004  mp_integer i;
1005 
1006  if(offset.is_zero())
1007  {
1008  }
1009  else if(!to_integer(offset, i) &&
1010  o.offset_is_zero())
1011  o.offset=i;
1012  else
1013  o.offset_is_set=false;
1014 
1015  insert_from(dest, index_expr, o);
1016  }
1017  }
1018 
1019  return;
1020  }
1021  else if(expr.id()==ID_member)
1022  {
1023  const irep_idt &component_name=expr.get(ID_component_name);
1024 
1025  if(expr.operands().size()!=1)
1026  throw "member expected to have one operand";
1027 
1028  const exprt &struct_op=expr.op0();
1029 
1030  object_mapt struct_references;
1031  get_reference_set_sharing(struct_op, struct_references, ns);
1032 
1033  const object_map_dt &object_map=struct_references.read();
1034 
1035  forall_objects(it, object_map)
1036  {
1037  const exprt &object=object_numbering[it->first];
1038  const typet &obj_type=ns.follow(object.type());
1039 
1040  if(object.id()==ID_unknown)
1041  insert_from(dest, exprt(ID_unknown, expr.type()));
1042  else if(object.id()==ID_dynamic_object &&
1043  obj_type.id()!=ID_struct &&
1044  obj_type.id()!=ID_union)
1045  {
1046  // we catch dynamic objects of the wrong type,
1047  // to avoid non-integral typecasts.
1048  insert_from(dest, exprt(ID_unknown, expr.type()));
1049  }
1050  else
1051  {
1052  objectt o=it->second;
1053 
1054  exprt member_expr(ID_member, expr.type());
1055  member_expr.copy_to_operands(object);
1056  member_expr.set(ID_component_name, component_name);
1057 
1058  // adjust type?
1059  if(ns.follow(struct_op.type())!=ns.follow(object.type()))
1060  member_expr.op0().make_typecast(struct_op.type());
1061 
1062  insert_from(dest, member_expr, o);
1063  }
1064  }
1065 
1066  return;
1067  }
1068  else if(expr.id()==ID_if)
1069  {
1070  if(expr.operands().size()!=3)
1071  throw "if takes three operands";
1072 
1073  get_reference_set_sharing_rec(expr.op1(), dest, ns);
1074  get_reference_set_sharing_rec(expr.op2(), dest, ns);
1075  return;
1076  }
1077 
1078  insert_from(dest, exprt(ID_unknown, expr.type()));
1079 }
1080 
1082  const exprt &lhs,
1083  const exprt &rhs,
1084  const namespacet &ns,
1085  bool add_to_sets)
1086 {
1087  #if 0
1088  std::cout << "ASSIGN LHS: " << lhs << '\n';
1089  std::cout << "ASSIGN LTYPE: " << ns.follow(lhs.type()) << '\n';
1090  std::cout << "ASSIGN RHS: " << from_expr(ns, "", rhs) << '\n';
1091  #endif
1092 
1093  if(rhs.id()==ID_if)
1094  {
1095  if(rhs.operands().size()!=3)
1096  throw "if takes three operands";
1097 
1098  assign(lhs, rhs.op1(), ns, add_to_sets);
1099  assign(lhs, rhs.op2(), ns, true);
1100  return;
1101  }
1102 
1103  const typet &type=ns.follow(lhs.type());
1104 
1105  if(type.id()==ID_struct ||
1106  type.id()==ID_union)
1107  {
1108  const struct_typet &struct_type=to_struct_type(type);
1109 
1110  unsigned no=0;
1111 
1112  for(struct_typet::componentst::const_iterator
1113  c_it=struct_type.components().begin();
1114  c_it!=struct_type.components().end();
1115  c_it++, no++)
1116  {
1117  const typet &subtype=c_it->type();
1118  const irep_idt &name=c_it->get(ID_name);
1119 
1120  // ignore methods
1121  if(subtype.id()==ID_code)
1122  continue;
1123 
1124  exprt lhs_member(ID_member, subtype);
1125  lhs_member.set(ID_component_name, name);
1126  lhs_member.copy_to_operands(lhs);
1127 
1128  exprt rhs_member;
1129 
1130  if(rhs.id()==ID_unknown ||
1131  rhs.id()==ID_invalid)
1132  {
1133  rhs_member=exprt(rhs.id(), subtype);
1134  }
1135  else
1136  {
1137  if(!base_type_eq(rhs.type(), type, ns))
1138  throw
1139  "type mismatch:\nRHS: "+rhs.type().pretty()+"\n"+
1140  "LHS: "+type.pretty();
1141 
1142  if(rhs.id()==ID_struct ||
1143  rhs.id()==ID_constant)
1144  {
1145  assert(no<rhs.operands().size());
1146  rhs_member=rhs.operands()[no];
1147  }
1148  else if(rhs.id()==ID_with)
1149  {
1150  assert(rhs.operands().size()==3);
1151 
1152  // see if op1 is the member we want
1153  const exprt &member_operand=rhs.op1();
1154 
1155  const irep_idt &component_name=
1156  member_operand.get(ID_component_name);
1157 
1158  if(component_name==name)
1159  {
1160  // yes! just take op2
1161  rhs_member=rhs.op2();
1162  }
1163  else
1164  {
1165  // no! do op0
1166  rhs_member=exprt(ID_member, subtype);
1167  rhs_member.copy_to_operands(rhs.op0());
1168  rhs_member.set(ID_component_name, name);
1169  }
1170  }
1171  else
1172  {
1173  rhs_member=exprt(ID_member, subtype);
1174  rhs_member.copy_to_operands(rhs);
1175  rhs_member.set(ID_component_name, name);
1176  }
1177 
1178  assign(lhs_member, rhs_member, ns, add_to_sets);
1179  }
1180  }
1181  }
1182  else if(type.id()==ID_array)
1183  {
1184  exprt lhs_index(ID_index, type.subtype());
1185  lhs_index.copy_to_operands(lhs, exprt(ID_unknown, index_type()));
1186 
1187  if(rhs.id()==ID_unknown ||
1188  rhs.id()==ID_invalid)
1189  {
1190  assign(lhs_index, exprt(rhs.id(), type.subtype()), ns, add_to_sets);
1191  }
1192  else
1193  {
1194  assert(base_type_eq(rhs.type(), type, ns));
1195 
1196  if(rhs.id()==ID_array_of)
1197  {
1198  assert(rhs.operands().size()==1);
1199 // std::cout << "AOF: " << rhs.op0() << '\n';
1200  assign(lhs_index, rhs.op0(), ns, add_to_sets);
1201  }
1202  else if(rhs.id()==ID_array ||
1203  rhs.id()==ID_constant)
1204  {
1205  forall_operands(o_it, rhs)
1206  {
1207  assign(lhs_index, *o_it, ns, add_to_sets);
1208  }
1209  }
1210  else if(rhs.id()==ID_with)
1211  {
1212  assert(rhs.operands().size()==3);
1213 
1214  exprt op0_index(ID_index, type.subtype());
1215  op0_index.copy_to_operands(rhs.op0(), exprt(ID_unknown, index_type()));
1216 
1217  assign(lhs_index, op0_index, ns, add_to_sets);
1218  assign(lhs_index, rhs.op2(), ns, true);
1219  }
1220  else
1221  {
1222  exprt rhs_index(ID_index, type.subtype());
1223  rhs_index.copy_to_operands(rhs, exprt(ID_unknown, index_type()));
1224  assign(lhs_index, rhs_index, ns, true);
1225  }
1226  }
1227  }
1228  else
1229  {
1230  // basic type
1231  object_mapt values_rhs;
1232 
1233  get_value_set(rhs, values_rhs, ns);
1234 
1235  assign_recursion_sett recset;
1236  assign_rec(lhs, values_rhs, "", ns, recset, add_to_sets);
1237  }
1238 }
1239 
1241  const exprt &op,
1242  const namespacet &ns)
1243 {
1244  // op must be a pointer
1245  if(op.type().id()!=ID_pointer)
1246  throw "free expected to have pointer-type operand";
1247 
1248  // find out what it points to
1249  object_mapt value_set;
1250  get_value_set(op, value_set, ns);
1251  entryt e; e.identifier="VP:TEMP";
1252  e.object_map=value_set;
1253  flatten(e, value_set);
1254 
1255  const object_map_dt &object_map=value_set.read();
1256 
1257  // find out which *instances* interest us
1258  dynamic_object_id_sett to_mark;
1259 
1260  forall_objects(it, object_map)
1261  {
1262  const exprt &object=object_numbering[it->first];
1263 
1264  if(object.id()==ID_dynamic_object)
1265  {
1267  to_dynamic_object_expr(object);
1268 
1269  if(dynamic_object.valid().is_true())
1270  to_mark.insert(dynamic_object.get_instance());
1271  }
1272  }
1273 
1274  // mark these as 'may be invalid'
1275  // this, unfortunately, destroys the sharing
1276  for(valuest::iterator v_it=values.begin();
1277  v_it!=values.end();
1278  v_it++)
1279  {
1280  object_mapt new_object_map;
1281 
1282  const object_map_dt &old_object_map=
1283  v_it->second.object_map.read();
1284 
1285  bool changed=false;
1286 
1287  forall_objects(o_it, old_object_map)
1288  {
1289  const exprt &object=object_numbering[o_it->first];
1290 
1291  if(object.id()==ID_dynamic_object)
1292  {
1294  to_dynamic_object_expr(object);
1295 
1296  if(to_mark.count(dynamic_object.get_instance())==0)
1297  set(new_object_map, o_it);
1298  else
1299  {
1300  // adjust
1301  objectt o=o_it->second;
1302  exprt tmp(object);
1303  to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
1304  insert_to(new_object_map, tmp, o);
1305  changed=true;
1306  }
1307  }
1308  else
1309  set(new_object_map, o_it);
1310  }
1311 
1312  if(changed)
1313  {
1314  entryt &temp_entry=get_temporary_entry(v_it->second.identifier,
1315  v_it->second.suffix);
1316  temp_entry.object_map=new_object_map;
1317  }
1318  }
1319 }
1320 
1322  const exprt &lhs,
1323  const object_mapt &values_rhs,
1324  const std::string &suffix,
1325  const namespacet &ns,
1326  assign_recursion_sett &recursion_set,
1327  bool add_to_sets)
1328 {
1329  #if 0
1330  std::cout << "ASSIGN_REC LHS: " << lhs << '\n';
1331  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1332 
1333  for(object_map_dt::const_iterator it=values_rhs.read().begin();
1334  it!=values_rhs.read().end(); it++)
1335  std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1336  #endif
1337 
1338  if(lhs.type().id()=="#REF#")
1339  {
1340  const irep_idt &ident=lhs.get(ID_identifier);
1341  object_mapt temp;
1342  gvs_recursion_sett recset;
1343  get_value_set_rec(lhs, temp, "", lhs.type().subtype(), ns, recset);
1344 
1345  if(recursion_set.find(ident)!=recursion_set.end())
1346  {
1347  recursion_set.insert(ident);
1348 
1349  forall_objects(it, temp.read())
1350  assign_rec(object_numbering[it->first], values_rhs,
1351  suffix, ns, recursion_set, add_to_sets);
1352 
1353  recursion_set.erase(ident);
1354  }
1355  }
1356  else if(lhs.id()==ID_symbol)
1357  {
1358  const irep_idt &identifier=lhs.get(ID_identifier);
1359 
1360  if(has_prefix(id2string(identifier),
1361  "value_set::dynamic_object") ||
1362  has_prefix(id2string(identifier),
1363  "value_set::return_value") ||
1364  values.find(id2string(identifier)+suffix)!=values.end())
1365  // otherwise we don't track this value
1366  {
1367  entryt &temp_entry=get_temporary_entry(identifier, suffix);
1368 
1369  // check if the right hand side contains a reference to ourselves,
1370  // in that case we need to include all old values!
1371 
1372  recfind_recursion_sett recset;
1373  if(add_to_sets ||
1374  recursive_find(identifier, values_rhs, recset))
1375  {
1376  entryt &state_entry=get_entry(identifier, suffix);
1377  make_valid_union(temp_entry.object_map, state_entry.object_map);
1378  }
1379 
1380  make_union(temp_entry.object_map, values_rhs);
1381  }
1382  }
1383  else if(lhs.id()==ID_dynamic_object)
1384  {
1387 
1388  const std::string name=
1389  "value_set::dynamic_object"+
1390  std::to_string(dynamic_object.get_instance());
1391 
1392  entryt &temp_entry=get_temporary_entry(name, suffix);
1393 
1394  // check if the right hand side contains a reference to ourselves,
1395  // in that case we need to include all old values!
1396 
1397  recfind_recursion_sett recset;
1398  if(add_to_sets ||
1399  recursive_find(name, values_rhs, recset))
1400  {
1401  entryt &state_entry=get_entry(name, suffix);
1402  make_valid_union(temp_entry.object_map, state_entry.object_map);
1403  }
1404 
1405  make_union(temp_entry.object_map, values_rhs);
1406  }
1407  else if(lhs.id()==ID_dereference)
1408  {
1409  if(lhs.operands().size()!=1)
1410  throw lhs.id_string()+" expected to have one operand";
1411 
1412  object_mapt reference_set;
1413  get_reference_set_sharing(lhs, reference_set, ns);
1414 
1415  forall_objects(it, reference_set.read())
1416  {
1417  const exprt &object=object_numbering[it->first];
1418 
1419  if(object.id()!=ID_unknown)
1420  assign_rec(object, values_rhs, suffix, ns, recursion_set, add_to_sets);
1421  }
1422  }
1423  else if(lhs.id()==ID_index)
1424  {
1425  if(lhs.operands().size()!=2)
1426  throw "index expected to have two operands";
1427 
1428  const typet &type=ns.follow(lhs.op0().type());
1429 
1430  assert(type.id()==ID_array ||
1431  type.id()==ID_incomplete_array ||
1432  type.id()=="#REF#");
1433 
1434  assign_rec(
1435  lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set, add_to_sets);
1436  }
1437  else if(lhs.id()==ID_member)
1438  {
1439  if(lhs.operands().size()!=1)
1440  throw "member expected to have one operand";
1441 
1442  if(lhs.op0().is_nil())
1443  return;
1444 
1445  const std::string &component_name=lhs.get_string(ID_component_name);
1446 
1447  const typet &type=ns.follow(lhs.op0().type());
1448 
1449  assert(type.id()==ID_struct ||
1450  type.id()==ID_union ||
1451  type.id()==ID_incomplete_struct ||
1452  type.id()==ID_incomplete_union);
1453 
1454  assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
1455  ns, recursion_set, add_to_sets);
1456  }
1457  else if(lhs.id()=="valid_object" ||
1458  lhs.id()=="dynamic_size" ||
1459  lhs.id()=="dynamic_type")
1460  {
1461  // we ignore this here
1462  }
1463  else if(lhs.id()==ID_string_constant)
1464  {
1465  // someone writes into a string-constant
1466  // evil guy
1467  }
1468  else if(lhs.id()=="NULL-object")
1469  {
1470  // evil as well
1471  }
1472  else if(lhs.id()==ID_typecast)
1473  {
1474  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1475 
1476  assign_rec(typecast_expr.op(), values_rhs, suffix,
1477  ns, recursion_set, add_to_sets);
1478  }
1479  else if(lhs.id()=="zero_string" ||
1480  lhs.id()=="is_zero_string" ||
1481  lhs.id()=="zero_string_length")
1482  {
1483  // ignore
1484  }
1485  else if(lhs.id()==ID_byte_extract_little_endian ||
1486  lhs.id()==ID_byte_extract_big_endian)
1487  {
1488  assert(lhs.operands().size()==2);
1489  assign_rec(lhs.op0(), values_rhs, suffix, ns, recursion_set, true);
1490  }
1491  else
1492  throw "assign NYI: `"+lhs.id_string()+"'";
1493 }
1494 
1496  const irep_idt &function,
1497  const exprt::operandst &arguments,
1498  const namespacet &ns)
1499 {
1500  const symbolt &symbol=ns.lookup(function);
1501 
1502  const code_typet &type=to_code_type(symbol.type);
1503  const code_typet::parameterst &parameter_types=type.parameters();
1504 
1505  // these first need to be assigned to dummy, temporary arguments
1506  // and only thereafter to the actuals, in order
1507  // to avoid overwriting actuals that are needed for recursive
1508  // calls
1509 
1510  // the assigned data must be valid on from!
1511  unsigned old_to_function=to_function;
1512  unsigned old_to_target_index=to_target_index;
1513 
1516 
1517  for(unsigned i=0; i<arguments.size(); i++)
1518  {
1519  const std::string identifier="value_set::" + id2string(function) + "::" +
1520  "argument$"+std::to_string(i);
1521  add_var(identifier, "");
1522  exprt dummy_lhs=symbol_exprt(identifier, arguments[i].type());
1523 // std::cout << arguments[i] << '\n';
1524 
1525  assign(dummy_lhs, arguments[i], ns, true);
1526 
1527  // merge it immediately, the actual assignment needs the data visible!
1528  // does this break the purpose of the dummies?
1529  make_union(values[identifier].object_map,
1530  temporary_values[identifier].object_map);
1531  }
1532 
1533  // restore
1534  to_function=old_to_function;
1535  to_target_index=old_to_target_index;
1536 
1537  // now assign to 'actual actuals'
1538 
1539  unsigned i=0;
1540 
1541  for(code_typet::parameterst::const_iterator
1542  it=parameter_types.begin();
1543  it!=parameter_types.end();
1544  it++)
1545  {
1546  const irep_idt &identifier=it->get_identifier();
1547  if(identifier=="")
1548  continue;
1549 
1550  add_var(identifier, "");
1551 
1552  const exprt v_expr=
1553  symbol_exprt("value_set::" + id2string(function) + "::" +
1554  "argument$"+std::to_string(i), it->type());
1555 
1556  exprt actual_lhs=symbol_exprt(identifier, it->type());
1557  assign(actual_lhs, v_expr, ns, true);
1558  i++;
1559  }
1560 }
1561 
1563  const exprt &lhs,
1564  const namespacet &ns)
1565 {
1566  if(lhs.is_nil())
1567  return;
1568 
1569  std::string rvs="value_set::return_value" + std::to_string(from_function);
1570  symbol_exprt rhs(rvs, lhs.type());
1571 
1572  assign(lhs, rhs, ns);
1573 }
1574 
1576  const exprt &code,
1577  const namespacet &ns)
1578 {
1579  const irep_idt &statement=code.get(ID_statement);
1580 
1581  if(statement==ID_block)
1582  {
1583  forall_operands(it, code)
1584  apply_code(*it, ns);
1585  }
1586  else if(statement==ID_function_call)
1587  {
1588  // shouldn't be here
1589  assert(false);
1590  }
1591  else if(statement==ID_assign ||
1592  statement==ID_init)
1593  {
1594  if(code.operands().size()!=2)
1595  throw "assignment expected to have two operands";
1596 
1597  assign(code.op0(), code.op1(), ns);
1598  }
1599  else if(statement==ID_decl)
1600  {
1601  if(code.operands().size()!=1)
1602  throw "decl expected to have one operand";
1603 
1604  const exprt &lhs=code.op0();
1605 
1606  if(lhs.id()!=ID_symbol)
1607  throw "decl expected to have symbol on lhs";
1608 
1609  assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1610  }
1611  else if(statement==ID_specc_notify ||
1612  statement==ID_specc_wait)
1613  {
1614  // ignore, does not change variables
1615  }
1616  else if(statement==ID_expression)
1617  {
1618  // can be ignored, we don't expect side effects here
1619  }
1620  else if(statement==ID_cpp_delete ||
1621  statement==ID_cpp_delete_array)
1622  {
1623  // does nothing
1624  }
1625  else if(statement==ID_free)
1626  {
1627  // this may kill a valid bit
1628 
1629  if(code.operands().size()!=1)
1630  throw "free expected to have one operand";
1631 
1632  do_free(code.op0(), ns);
1633  }
1634  else if(statement=="lock" || statement=="unlock")
1635  {
1636  // ignore for now
1637  }
1638  else if(statement==ID_asm)
1639  {
1640  // ignore for now, probably not safe
1641  }
1642  else if(statement==ID_nondet)
1643  {
1644  // doesn't do anything
1645  }
1646  else if(statement==ID_printf)
1647  {
1648  // doesn't do anything
1649  }
1650  else if(statement==ID_return)
1651  {
1652  // this is turned into an assignment
1653  if(code.operands().size()==1)
1654  {
1655  std::string rvs="value_set::return_value" + std::to_string(from_function);
1656  symbol_exprt lhs(rvs, code.op0().type());
1657  assign(lhs, code.op0(), ns);
1658  }
1659  }
1660  else if(statement==ID_input || statement==ID_output)
1661  {
1662  // doesn't do anything
1663  }
1664 
1665  else
1666  throw
1667  code.pretty()+"\n"+
1668  "value_set_fivrt: unexpected statement: "+id2string(statement);
1669 }
1670 
1672  object_mapt &dest,
1673  unsigned n,
1674  const objectt &object) const
1675 {
1676  object_map_dt &map=dest.write();
1677  if(map.find(n)==map.end())
1678  {
1679 // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1680  // new
1681  map[n]=object;
1683  return true;
1684  }
1685  else
1686  {
1687 // std::cout << "UPD " << n << '\n';
1688  objectt &old=map[n];
1689 
1690  bool res=map.set_valid_at(n, to_function, to_target_index);
1691 
1692  if(old.offset_is_set && object.offset_is_set)
1693  {
1694  if(old.offset==object.offset)
1695  return res;
1696  else
1697  {
1698  old.offset_is_set=false;
1699  return true;
1700  }
1701  }
1702  else if(!old.offset_is_set)
1703  return res;
1704  else
1705  {
1706  old.offset_is_set=false;
1707  return true;
1708  }
1709  }
1710 }
1711 
1713  object_mapt &dest,
1714  unsigned n,
1715  const objectt &object) const
1716 {
1717  object_map_dt &map=dest.write();
1718  if(map.find(n)==map.end())
1719  {
1720 // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1721  // new
1722  map[n]=object;
1724  return true;
1725  }
1726  else
1727  {
1728 // std::cout << "UPD " << n << '\n';
1729  objectt &old=map[n];
1730 
1731  bool res=map.set_valid_at(n, from_function, from_target_index);
1732 
1733  if(old.offset_is_set && object.offset_is_set)
1734  {
1735  if(old.offset==object.offset)
1736  return res;
1737  else
1738  {
1739  old.offset_is_set=false;
1740  return true;
1741  }
1742  }
1743  else if(!old.offset_is_set)
1744  return res;
1745  else
1746  {
1747  old.offset_is_set=false;
1748  return true;
1749  }
1750  }
1751 }
1752 
1754  unsigned inx,
1755  const validity_ranget &vr)
1756 {
1757  bool res=false;
1758 
1759  for(unsigned i=vr.from; i<=vr.to; i++)
1760  if(set_valid_at(inx, vr.function, i))
1761  res=true;
1762 
1763  return res;
1764 }
1765 
1767  unsigned inx,
1768  unsigned f,
1769  unsigned line)
1770 {
1771  if(is_valid_at(inx, f, line))
1772  return false;
1773 
1774  vrange_listt &ranges=validity_ranges[inx];
1775  vrange_listt::iterator it=ranges.begin();
1776 
1777  while(it->function!=f && it!=ranges.end()) it++; // ffw to function block
1778 
1779  for(;
1780  it!=ranges.end() && it->function==f && it->from <= line;
1781  it++)
1782  {
1783  if(it->function==f)
1784  {
1785  if( line == it->to+1)
1786  {
1787  it->to++;
1788 
1789  // by any chance: does the next one connect to this one?
1790  vrange_listt::iterator n_it=it; n_it++;
1791  if(n_it!=ranges.end() &&
1792  it->function == n_it->function &&
1793  it->to+1 == n_it->from)
1794  {
1795  n_it->from=it->from; // connected!
1796  it=ranges.erase(it);
1797  }
1798  return true;
1799  }
1800  }
1801  }
1802 
1803  // it now points to either the end,
1804  // the first of a new function block,or
1805  // the first one that has from > line
1806  if(it!=ranges.end())
1807  {
1808  if(it->function==f)
1809  {
1810  if( line == it->from - 1)
1811  {
1812  it->from--;
1813 
1814  // by any chance: does the previous one connect to this one?
1815  if(it!=ranges.begin())
1816  {
1817  vrange_listt::iterator p_it=it; p_it--;
1818  if(p_it->function == it->function &&
1819  p_it->to+1 == it->from)
1820  {
1821  p_it->to=it->to; // connected!
1822  it=ranges.erase(it);
1823  }
1824  }
1825  return true;
1826  }
1827  }
1828  }
1829 
1830  // none matched
1831  validity_ranget insr(f, line, line);
1832  ranges.insert(it, insr);
1833 
1834  return true;
1835 }
1836 
1838  unsigned inx,
1839  unsigned f,
1840  unsigned line) const
1841 {
1842  #if 0
1843  std::cout << "IS_VALID_AT: " << inx << ", " << f << ", line " << line <<
1844  '\n';
1845  #endif
1846 
1847  validity_rangest::const_iterator vrs=validity_ranges.find(inx);
1848  if(vrs!=validity_ranges.end())
1849  {
1850  const vrange_listt &ranges=vrs->second;
1851 
1852  object_map_dt::vrange_listt::const_iterator it=ranges.begin();
1853 
1854  while(it->function!=f &&
1855  it!=ranges.end())
1856  it++; // ffw to function block
1857 
1858  for( ;
1859  it!=ranges.end() && it->function==f && it->from<=line;
1860  it++)
1861  if(it->contains(f, line))
1862  return true;
1863  }
1864  return false;
1865 }
1866 
1868  const irep_idt &ident,
1869  const object_mapt &rhs,
1870  recfind_recursion_sett &recursion_set) const
1871 {
1872  forall_objects(it, rhs.read())
1873  {
1874  const exprt &o=object_numbering[it->first];
1875 
1876  if(o.id()==ID_symbol && o.get(ID_identifier)==ident)
1877  return true;
1878  else if(o.type().id()=="#REF#")
1879  {
1880  const irep_idt oid=o.get(ID_identifier);
1881 
1882  if(recursion_set.find(oid)!=recursion_set.end())
1883  return false; // we hit some other cycle on the way down
1884 
1885  if(oid==ident)
1886  return true;
1887  else
1888  {
1889  valuest::const_iterator vit=values.find(oid);
1890  if(vit!=values.end())
1891  {
1892  const entryt &e=vit->second;
1893 
1894  recursion_set.insert(oid);
1895  if(recursive_find(ident, e.object_map, recursion_set))
1896  return true;
1897  recursion_set.erase(oid);
1898  }
1899  }
1900  }
1901  }
1902 
1903  return false;
1904 }
1905 
1907 {
1908  bool changed=false;
1909 
1910  for(valuest::iterator it=values.begin();
1911  it!=values.end();
1912  it++)
1913  {
1914  object_mapt &state_map=it->second.object_map;
1915 
1916  irep_idt ident=id2string(it->second.identifier)+it->second.suffix;
1917 
1918  valuest::const_iterator t_it=temporary_values.find(ident);
1919 
1920  if(t_it==temporary_values.end())
1921  {
1922 // std::cout << "OLD VALUES FOR: " << ident << '\n';
1923  Forall_valid_objects(o_it, state_map.write())
1924  {
1925  if(state_map.write().set_valid_at(o_it->first,
1927  changed=true;
1928  }
1929  }
1930  else
1931  {
1932 // std::cout << "NEW VALUES FOR: " << ident << '\n';
1933  if(make_union(state_map, t_it->second.object_map))
1934  changed=true;
1935  }
1936  }
1937 
1938  temporary_values.clear();
1939 
1940  return changed;
1941 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
BigInt mp_integer
Definition: mp_arith.h:19
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
void dereference_rec(const exprt &src, exprt &dest) const
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
Definition: std_expr.h:1701
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
#define forall_objects(it, map)
void do_end_function(const exprt &lhs, const namespacet &ns)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
unsigned from_function
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
Definition: std_types.h:829
bool recursive_find(const irep_idt &ident, const object_mapt &rhs, recfind_recursion_sett &recursion_set) const
const componentst & components() const
Definition: std_types.h:242
unsigned to_target_index
#define Forall_objects(it, map)
bool make_union(object_mapt &dest, const object_mapt &src) const
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
void copy_objects(object_mapt &dest, const object_mapt &src) const
void output(const namespacet &ns, std::ostream &out) const
std::unordered_set< exprt, irep_hash > expr_sett
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
Structure type.
Definition: std_types.h:296
exprt & op()
Definition: std_expr.h:1739
unsigned to_function
unsigned from_target_index
#define Forall_valid_objects(it, map)
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
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
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &, unsigned from_function, unsigned from_index) const
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void apply_code(const exprt &code, const namespacet &ns)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::list< validity_ranget > vrange_listt
valuest temporary_values
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1578
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
#define forall_operands(it, expr)
Definition: expr.h:17
std::unordered_set< idt, string_hash > gvs_recursion_sett
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
bitvector_typet index_type()
Definition: c_types.cpp:15
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
Symbol table.
entryt & get_entry(const idt &id, const std::string &suffix)
static object_numberingt object_numbering
Operator to return the address of an object.
Definition: std_expr.h:2593
void flatten(const entryt &e, object_mapt &dest) const
static const object_map_dt blank
std::unordered_set< unsigned int > dynamic_object_id_sett
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
const irep_idt & display_name() const
Definition: symbol.h:60
static const char * alloc_adapter_prefix
typet type
Type of symbol.
Definition: symbol.h:37
exprt to_expr(object_map_dt::const_iterator it) const
objmapt::const_iterator const_iterator
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set, bool add_to_sets)
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
#define forall_valid_objects(it, map)
Value Set (Flow Insensitive, Sharing, Validity Regions)
static hash_numbering< irep_idt, irep_id_hash > function_numbering
std::unordered_set< idt, string_hash > flatten_seent
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const T & read() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
const std::string & id_string() const
Definition: irep.h:192
bool is_zero() const
Definition: expr.cpp:236
void add_var(const idt &id, const std::string &suffix)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
exprt dynamic_object(const exprt &pointer)
std::unordered_set< idt, string_hash > assign_recursion_sett
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
TO_BE_DOCUMENTED.
Definition: std_expr.h:1658
void do_free(const exprt &op, const namespacet &ns)
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::unordered_set< idt, string_hash > recfind_recursion_sett
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
const_iterator find(unsigned k)
bool simplify(exprt &expr, const namespacet &ns)