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 std::move(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 &object = object_numbering[it->first];
828 
829  if(object.type().id() == "#REF#")
830  {
831  const irep_idt &ident = object.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, object.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(it2, omt.read())
857  dest.insert(to_expr(it2));
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_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 &lhs,
1229  const object_mapt &values_rhs,
1230  const std::string &suffix,
1231  const namespacet &ns,
1232  assign_recursion_sett &recursion_set,
1233  bool add_to_sets)
1234 {
1235  #if 0
1236  std::cout << "ASSIGN_REC LHS: " << lhs << '\n';
1237  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1238 
1239  for(object_map_dt::const_iterator it=values_rhs.read().begin();
1240  it!=values_rhs.read().end(); it++)
1241  std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1242  #endif
1243 
1244  if(lhs.type().id()=="#REF#")
1245  {
1246  const irep_idt &ident=lhs.get(ID_identifier);
1247  object_mapt temp;
1248  gvs_recursion_sett recset;
1249  get_value_set_rec(lhs, temp, "", lhs.type().subtype(), ns, recset);
1250 
1251  if(recursion_set.find(ident)!=recursion_set.end())
1252  {
1253  recursion_set.insert(ident);
1254 
1255  forall_objects(it, temp.read())
1256  assign_rec(object_numbering[it->first], values_rhs,
1257  suffix, ns, recursion_set, add_to_sets);
1258 
1259  recursion_set.erase(ident);
1260  }
1261  }
1262  else if(lhs.id()==ID_symbol)
1263  {
1264  const irep_idt &identifier=lhs.get(ID_identifier);
1265 
1266  if(has_prefix(id2string(identifier),
1267  "value_set::dynamic_object") ||
1268  has_prefix(id2string(identifier),
1269  "value_set::return_value") ||
1270  values.find(id2string(identifier)+suffix)!=values.end())
1271  // otherwise we don't track this value
1272  {
1273  entryt &temp_entry=get_temporary_entry(identifier, suffix);
1274 
1275  // check if the right hand side contains a reference to ourselves,
1276  // in that case we need to include all old values!
1277 
1278  recfind_recursion_sett recset;
1279  if(add_to_sets ||
1280  recursive_find(identifier, values_rhs, recset))
1281  {
1282  entryt &state_entry=get_entry(identifier, suffix);
1283  make_valid_union(temp_entry.object_map, state_entry.object_map);
1284  }
1285 
1286  make_union(temp_entry.object_map, values_rhs);
1287  }
1288  }
1289  else if(lhs.id()==ID_dynamic_object)
1290  {
1293 
1294  const std::string name=
1295  "value_set::dynamic_object"+
1296  std::to_string(dynamic_object.get_instance());
1297 
1298  entryt &temp_entry=get_temporary_entry(name, suffix);
1299 
1300  // check if the right hand side contains a reference to ourselves,
1301  // in that case we need to include all old values!
1302 
1303  recfind_recursion_sett recset;
1304  if(add_to_sets ||
1305  recursive_find(name, values_rhs, recset))
1306  {
1307  entryt &state_entry=get_entry(name, suffix);
1308  make_valid_union(temp_entry.object_map, state_entry.object_map);
1309  }
1310 
1311  make_union(temp_entry.object_map, values_rhs);
1312  }
1313  else if(lhs.id()==ID_dereference)
1314  {
1315  if(lhs.operands().size()!=1)
1316  throw lhs.id_string()+" expected to have one operand";
1317 
1318  object_mapt reference_set;
1319  get_reference_set_sharing(lhs, reference_set, ns);
1320 
1321  forall_objects(it, reference_set.read())
1322  {
1323  const exprt &object=object_numbering[it->first];
1324 
1325  if(object.id()!=ID_unknown)
1326  assign_rec(object, values_rhs, suffix, ns, recursion_set, add_to_sets);
1327  }
1328  }
1329  else if(lhs.id()==ID_index)
1330  {
1331  if(lhs.operands().size()!=2)
1332  throw "index expected to have two operands";
1333 
1334  const typet &type=ns.follow(lhs.op0().type());
1335 
1336  DATA_INVARIANT(type.id()==ID_array ||
1337  type.id()==ID_incomplete_array ||
1338  type.id()=="#REF#",
1339  "operand 0 of index expression must be an array");
1340 
1341  assign_rec(
1342  lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set, add_to_sets);
1343  }
1344  else if(lhs.id()==ID_member)
1345  {
1346  if(lhs.operands().size()!=1)
1347  throw "member expected to have one operand";
1348 
1349  if(lhs.op0().is_nil())
1350  return;
1351 
1352  const std::string &component_name=lhs.get_string(ID_component_name);
1353 
1354  const typet &type=ns.follow(lhs.op0().type());
1355 
1356  DATA_INVARIANT(type.id()==ID_struct ||
1357  type.id()==ID_union ||
1358  type.id()==ID_incomplete_struct ||
1359  type.id()==ID_incomplete_union,
1360  "operand 0 of member expression must be struct or union");
1361 
1362  assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
1363  ns, recursion_set, add_to_sets);
1364  }
1365  else if(lhs.id()=="valid_object" ||
1366  lhs.id()=="dynamic_size" ||
1367  lhs.id()=="dynamic_type")
1368  {
1369  // we ignore this here
1370  }
1371  else if(lhs.id()==ID_string_constant)
1372  {
1373  // someone writes into a string-constant
1374  // evil guy
1375  }
1376  else if(lhs.id() == ID_null_object)
1377  {
1378  // evil as well
1379  }
1380  else if(lhs.id()==ID_typecast)
1381  {
1382  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1383 
1384  assign_rec(typecast_expr.op(), values_rhs, suffix,
1385  ns, recursion_set, add_to_sets);
1386  }
1387  else if(lhs.id()=="zero_string" ||
1388  lhs.id()=="is_zero_string" ||
1389  lhs.id()=="zero_string_length")
1390  {
1391  // ignore
1392  }
1393  else if(lhs.id()==ID_byte_extract_little_endian ||
1394  lhs.id()==ID_byte_extract_big_endian)
1395  {
1396  assert(lhs.operands().size()==2);
1397  assign_rec(lhs.op0(), values_rhs, suffix, ns, recursion_set, true);
1398  }
1399  else
1400  throw "assign NYI: `"+lhs.id_string()+"'";
1401 }
1402 
1404  const irep_idt &function,
1405  const exprt::operandst &arguments,
1406  const namespacet &ns)
1407 {
1408  const symbolt &symbol=ns.lookup(function);
1409 
1410  const code_typet &type=to_code_type(symbol.type);
1411  const code_typet::parameterst &parameter_types=type.parameters();
1412 
1413  // these first need to be assigned to dummy, temporary arguments
1414  // and only thereafter to the actuals, in order
1415  // to avoid overwriting actuals that are needed for recursive
1416  // calls
1417 
1418  // the assigned data must be valid on from!
1419  unsigned old_to_function=to_function;
1420  unsigned old_to_target_index=to_target_index;
1421 
1424 
1425  for(std::size_t i=0; i<arguments.size(); i++)
1426  {
1427  const std::string identifier="value_set::" + id2string(function) + "::" +
1428  "argument$"+std::to_string(i);
1429  add_var(identifier, "");
1430  const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1431 
1432  assign(dummy_lhs, arguments[i], ns, true);
1433 
1434  // merge it immediately, the actual assignment needs the data visible!
1435  // does this break the purpose of the dummies?
1436  make_union(values[identifier].object_map,
1437  temporary_values[identifier].object_map);
1438  }
1439 
1440  // restore
1441  to_function=old_to_function;
1442  to_target_index=old_to_target_index;
1443 
1444  // now assign to 'actual actuals'
1445 
1446  std::size_t i=0;
1447 
1448  for(code_typet::parameterst::const_iterator
1449  it=parameter_types.begin();
1450  it!=parameter_types.end();
1451  it++)
1452  {
1453  const irep_idt &identifier=it->get_identifier();
1454  if(identifier=="")
1455  continue;
1456 
1457  add_var(identifier, "");
1458 
1459  const exprt v_expr=
1460  symbol_exprt("value_set::" + id2string(function) + "::" +
1461  "argument$"+std::to_string(i), it->type());
1462 
1463  const symbol_exprt actual_lhs(identifier, it->type());
1464  assign(actual_lhs, v_expr, ns, true);
1465  i++;
1466  }
1467 }
1468 
1470  const exprt &lhs,
1471  const namespacet &ns)
1472 {
1473  if(lhs.is_nil())
1474  return;
1475 
1476  std::string rvs="value_set::return_value" + std::to_string(from_function);
1477  symbol_exprt rhs(rvs, lhs.type());
1478 
1479  assign(lhs, rhs, ns);
1480 }
1481 
1483  const exprt &code,
1484  const namespacet &ns)
1485 {
1486  const irep_idt &statement=code.get(ID_statement);
1487 
1488  if(statement==ID_block)
1489  {
1490  forall_operands(it, code)
1491  apply_code(*it, ns);
1492  }
1493  else if(statement==ID_function_call)
1494  {
1495  // shouldn't be here
1496  UNREACHABLE;
1497  }
1498  else if(statement==ID_assign)
1499  {
1500  if(code.operands().size()!=2)
1501  throw "assignment expected to have two operands";
1502 
1503  assign(code.op0(), code.op1(), ns);
1504  }
1505  else if(statement==ID_decl)
1506  {
1507  if(code.operands().size()!=1)
1508  throw "decl expected to have one operand";
1509 
1510  const exprt &lhs=code.op0();
1511 
1512  if(lhs.id()!=ID_symbol)
1513  throw "decl expected to have symbol on lhs";
1514 
1515  assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1516  }
1517  else if(statement==ID_expression)
1518  {
1519  // can be ignored, we don't expect side effects here
1520  }
1521  else if(statement==ID_cpp_delete ||
1522  statement==ID_cpp_delete_array)
1523  {
1524  // does nothing
1525  }
1526  else if(statement=="lock" || statement=="unlock")
1527  {
1528  // ignore for now
1529  }
1530  else if(statement==ID_asm)
1531  {
1532  // ignore for now, probably not safe
1533  }
1534  else if(statement==ID_nondet)
1535  {
1536  // doesn't do anything
1537  }
1538  else if(statement==ID_printf)
1539  {
1540  // doesn't do anything
1541  }
1542  else if(statement==ID_return)
1543  {
1544  // this is turned into an assignment
1545  if(code.operands().size()==1)
1546  {
1547  std::string rvs="value_set::return_value" + std::to_string(from_function);
1548  symbol_exprt lhs(rvs, code.op0().type());
1549  assign(lhs, code.op0(), ns);
1550  }
1551  }
1552  else if(statement==ID_input || statement==ID_output)
1553  {
1554  // doesn't do anything
1555  }
1556 
1557  else
1558  throw
1559  code.pretty()+"\n"+
1560  "value_set_fivrt: unexpected statement: "+id2string(statement);
1561 }
1562 
1564  object_mapt &dest,
1566  const offsett &offset) const
1567 {
1568  object_map_dt &map=dest.write();
1569  if(map.find(n)==map.end())
1570  {
1571  // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1572  // new
1573  map[n] = offset;
1575  return true;
1576  }
1577  else
1578  {
1579  // std::cout << "UPD " << n << '\n';
1580  offsett &old_offset = map[n];
1581 
1582  bool res = map.set_valid_at(n, to_function, to_target_index);
1583 
1584  if(old_offset && offset)
1585  {
1586  if(*old_offset == *offset)
1587  return res;
1588  else
1589  {
1590  old_offset.reset();
1591  return true;
1592  }
1593  }
1594  else if(!old_offset)
1595  return res;
1596  else
1597  {
1598  old_offset.reset();
1599  return true;
1600  }
1601  }
1602 }
1603 
1605  object_mapt &dest,
1607  const offsett &offset) const
1608 {
1609  object_map_dt &map=dest.write();
1610  if(map.find(n)==map.end())
1611  {
1612  // std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
1613  // new
1614  map[n] = offset;
1616  return true;
1617  }
1618  else
1619  {
1620  // std::cout << "UPD " << n << '\n';
1621  offsett &old_offset = map[n];
1622 
1623  bool res = map.set_valid_at(n, from_function, from_target_index);
1624 
1625  if(old_offset && offset)
1626  {
1627  if(*old_offset == *offset)
1628  return res;
1629  else
1630  {
1631  old_offset.reset();
1632  return true;
1633  }
1634  }
1635  else if(!old_offset)
1636  return res;
1637  else
1638  {
1639  old_offset.reset();
1640  return true;
1641  }
1642  }
1643 }
1644 
1646  unsigned inx,
1647  const validity_ranget &vr)
1648 {
1649  bool res=false;
1650 
1651  for(unsigned i=vr.from; i<=vr.to; i++)
1652  if(set_valid_at(inx, vr.function, i))
1653  res=true;
1654 
1655  return res;
1656 }
1657 
1659  unsigned inx,
1660  unsigned f,
1661  unsigned line)
1662 {
1663  if(is_valid_at(inx, f, line))
1664  return false;
1665 
1666  vrange_listt &ranges=validity_ranges[inx];
1667  vrange_listt::iterator it=ranges.begin();
1668 
1669  while(it->function!=f && it!=ranges.end()) it++; // ffw to function block
1670 
1671  for(;
1672  it!=ranges.end() && it->function==f && it->from <= line;
1673  it++)
1674  {
1675  if(it->function==f)
1676  {
1677  if( line == it->to+1)
1678  {
1679  it->to++;
1680 
1681  // by any chance: does the next one connect to this one?
1682  vrange_listt::iterator n_it=it; n_it++;
1683  if(n_it!=ranges.end() &&
1684  it->function == n_it->function &&
1685  it->to+1 == n_it->from)
1686  {
1687  n_it->from=it->from; // connected!
1688  it=ranges.erase(it);
1689  }
1690  return true;
1691  }
1692  }
1693  }
1694 
1695  // it now points to either the end,
1696  // the first of a new function block,or
1697  // the first one that has from > line
1698  if(it!=ranges.end())
1699  {
1700  if(it->function==f)
1701  {
1702  if( line == it->from - 1)
1703  {
1704  it->from--;
1705 
1706  // by any chance: does the previous one connect to this one?
1707  if(it!=ranges.begin())
1708  {
1709  vrange_listt::iterator p_it=it; p_it--;
1710  if(p_it->function == it->function &&
1711  p_it->to+1 == it->from)
1712  {
1713  p_it->to=it->to; // connected!
1714  it=ranges.erase(it);
1715  }
1716  }
1717  return true;
1718  }
1719  }
1720  }
1721 
1722  // none matched
1723  validity_ranget insr(f, line, line);
1724  ranges.insert(it, insr);
1725 
1726  return true;
1727 }
1728 
1730  unsigned inx,
1731  unsigned f,
1732  unsigned line) const
1733 {
1734  #if 0
1735  std::cout << "IS_VALID_AT: " << inx << ", " << f << ", line " << line <<
1736  '\n';
1737  #endif
1738 
1739  validity_rangest::const_iterator vrs=validity_ranges.find(inx);
1740  if(vrs!=validity_ranges.end())
1741  {
1742  const vrange_listt &ranges=vrs->second;
1743 
1744  object_map_dt::vrange_listt::const_iterator it=ranges.begin();
1745 
1746  while(it->function!=f &&
1747  it!=ranges.end())
1748  it++; // ffw to function block
1749 
1750  for( ;
1751  it!=ranges.end() && it->function==f && it->from<=line;
1752  it++)
1753  if(it->contains(f, line))
1754  return true;
1755  }
1756  return false;
1757 }
1758 
1760  const irep_idt &ident,
1761  const object_mapt &rhs,
1762  recfind_recursion_sett &recursion_set) const
1763 {
1764  forall_objects(it, rhs.read())
1765  {
1766  const exprt &o=object_numbering[it->first];
1767 
1768  if(o.id()==ID_symbol && o.get(ID_identifier)==ident)
1769  return true;
1770  else if(o.type().id()=="#REF#")
1771  {
1772  const irep_idt oid=o.get(ID_identifier);
1773 
1774  if(recursion_set.find(oid)!=recursion_set.end())
1775  return false; // we hit some other cycle on the way down
1776 
1777  if(oid==ident)
1778  return true;
1779  else
1780  {
1781  valuest::const_iterator vit=values.find(oid);
1782  if(vit!=values.end())
1783  {
1784  const entryt &e=vit->second;
1785 
1786  recursion_set.insert(oid);
1787  if(recursive_find(ident, e.object_map, recursion_set))
1788  return true;
1789  recursion_set.erase(oid);
1790  }
1791  }
1792  }
1793  }
1794 
1795  return false;
1796 }
1797 
1799 {
1800  bool changed=false;
1801 
1802  for(valuest::iterator it=values.begin();
1803  it!=values.end();
1804  it++)
1805  {
1806  object_mapt &state_map=it->second.object_map;
1807 
1808  irep_idt ident=id2string(it->second.identifier)+it->second.suffix;
1809 
1810  valuest::const_iterator t_it=temporary_values.find(ident);
1811 
1812  if(t_it==temporary_values.end())
1813  {
1814 // std::cout << "OLD VALUES FOR: " << ident << '\n';
1815  Forall_valid_objects(o_it, state_map.write())
1816  {
1817  if(state_map.write().set_valid_at(o_it->first,
1819  changed=true;
1820  }
1821  }
1822  else
1823  {
1824 // std::cout << "NEW VALUES FOR: " << ident << '\n';
1825  if(make_union(state_map, t_it->second.object_map))
1826  changed=true;
1827  }
1828  }
1829 
1830  temporary_values.clear();
1831 
1832  return changed;
1833 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
Semantic type conversion.
Definition: std_expr.h:2277
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:751
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:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
#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 an exprt to a dynamic_object_exprt.
Definition: std_expr.h:2245
const exprt & op() const
Definition: std_expr.h:371
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
unsigned from_function
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
Definition: std_types.h:754
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:205
unsigned to_target_index
#define Forall_objects(it, map)
bool make_union(object_mapt &dest, const object_mapt &src) const
typet & type()
Return the type of the expression.
Definition: expr.h:68
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.
Definition: symbol.h:27
Structure type, corresponds to C style structs.
Definition: std_types.h:276
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:3890
#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:4443
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:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
void apply_code(const exprt &code, const namespacet &ns)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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:2136
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
#define forall_operands(it, expr)
Definition: expr.h:20
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
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
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:35
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:3255
void flatten(const entryt &e, object_mapt &dest) const
static const object_map_dt blank
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:57
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
static const char * alloc_adapter_prefix
typet type
Type of symbol.
Definition: symbol.h:31
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:54
const parameterst & parameters() const
Definition: std_types.h:893
#define forall_valid_objects(it, map)
Value Set (Flow Insensitive, Sharing, Validity Regions)
static hash_numbering< irep_idt, irep_id_hash > function_numbering
std::unordered_set< idt, string_hash > flatten_seent
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
const T & read() const
const std::string & id_string() const
Definition: irep.h:262
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
void add_var(const idt &id, const std::string &suffix)
Expression to hold a symbol (variable)
Definition: std_expr.h:143
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
exprt dynamic_object(const exprt &pointer)
std::unordered_set< idt, string_hash > assign_recursion_sett
Base Type Computation.
const typet & subtype() const
Definition: type.h:38
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
Representation of heap-allocated objects.
Definition: std_expr.h:2208
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
std::unordered_set< idt, string_hash > recfind_recursion_sett
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
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:1595
static format_containert< T > format(const T &o)
Definition: format.h:35