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