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