cprover
value_set.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "value_set.h"
13 
14 #include <cassert>
15 #include <ostream>
16 
17 #include <util/arith_tools.h>
18 #include <util/base_type.h>
19 #include <util/c_types.h>
21 #include <util/simplify_expr.h>
22 
23 #include <langapi/language_util.h>
24 
25 #ifdef DEBUG
26 #include <iostream>
27 #include <util/format_expr.h>
28 #include <util/format_type.h>
29 #endif
30 
31 #include "add_failed_symbols.h"
32 
33 // Due to a large number of functions defined inline, `value_sett` and
34 // associated types are documented in its header file, `value_set.h`.
35 
38 
40  const irep_idt &id,
41  const typet &type,
42  const namespacet &ns)
43 {
44  // we always track fields on these
45  if(has_prefix(id2string(id), "value_set::dynamic_object") ||
46  id=="value_set::return_value" ||
47  id=="value_set::memory")
48  return true;
49 
50  // otherwise it has to be a struct
51  return ns.follow(type).id()==ID_struct;
52 }
53 
55  const entryt &e,
56  const typet &type,
57  const namespacet &ns)
58 {
59  irep_idt index;
60 
61  if(field_sensitive(e.identifier, type, ns))
62  index=id2string(e.identifier)+e.suffix;
63  else
64  index=e.identifier;
65 
66  std::pair<valuest::iterator, bool> r=
67  values.insert(std::pair<idt, entryt>(index, e));
68 
69  return r.first->second;
70 }
71 
73  object_mapt &dest,
75  const offsett &offset) const
76 {
77  auto entry=dest.read().find(n);
78 
79  if(entry==dest.read().end())
80  {
81  // new
82  dest.write()[n] = offset;
83  return true;
84  }
85  else if(!entry->second)
86  return false; // no change
87  else if(offset && *entry->second == *offset)
88  return false; // no change
89  else
90  {
91  dest.write()[n].reset();
92  return true;
93  }
94 }
95 
97  const namespacet &ns,
98  std::ostream &out) const
99 {
100  for(valuest::const_iterator
101  v_it=values.begin();
102  v_it!=values.end();
103  v_it++)
104  {
105  irep_idt identifier, display_name;
106 
107  const entryt &e=v_it->second;
108 
109  if(has_prefix(id2string(e.identifier), "value_set::dynamic_object"))
110  {
111  display_name=id2string(e.identifier)+e.suffix;
112  identifier="";
113  }
114  else if(e.identifier=="value_set::return_value")
115  {
116  display_name="RETURN_VALUE"+e.suffix;
117  identifier="";
118  }
119  else
120  {
121  #if 0
122  const symbolt &symbol=ns.lookup(e.identifier);
123  display_name=id2string(symbol.display_name())+e.suffix;
124  identifier=symbol.name;
125  #else
126  identifier=id2string(e.identifier);
127  display_name=id2string(identifier)+e.suffix;
128  #endif
129  }
130 
131  out << display_name;
132 
133  out << " = { ";
134 
135  const object_map_dt &object_map=e.object_map.read();
136 
137  std::size_t width=0;
138 
140  o_it=object_map.begin();
141  o_it!=object_map.end();
142  o_it++)
143  {
144  const exprt &o=object_numbering[o_it->first];
145 
146  std::string result;
147 
148  if(o.id()==ID_invalid || o.id()==ID_unknown)
149  result=from_expr(ns, identifier, o);
150  else
151  {
152  result="<"+from_expr(ns, identifier, o)+", ";
153 
154  if(o_it->second)
155  result += integer2string(*o_it->second) + "";
156  else
157  result+='*';
158 
159  if(o.type().is_nil())
160  result+=", ?";
161  else
162  result+=", "+from_type(ns, identifier, o.type());
163 
164  result+='>';
165  }
166 
167  out << result;
168 
169  width+=result.size();
170 
172  next++;
173 
174  if(next!=object_map.end())
175  {
176  out << ", ";
177  if(width>=40)
178  out << "\n ";
179  }
180  }
181 
182  out << " } \n";
183  }
184 }
185 
187 {
188  const exprt &object=object_numbering[it.first];
189 
190  if(object.id()==ID_invalid ||
191  object.id()==ID_unknown)
192  return object;
193 
195 
196  od.object()=object;
197 
198  if(it.second)
199  od.offset() = from_integer(*it.second, index_type());
200 
201  od.type()=od.object().type();
202 
203  return od;
204 }
205 
207 {
208  bool result=false;
209 
210  valuest::iterator v_it=values.begin();
211 
212  for(valuest::const_iterator
213  it=new_values.begin();
214  it!=new_values.end();
215  ) // no it++
216  {
217  if(v_it==values.end() || it->first<v_it->first)
218  {
219  values.insert(v_it, *it);
220  result=true;
221  it++;
222  continue;
223  }
224  else if(v_it->first<it->first)
225  {
226  v_it++;
227  continue;
228  }
229 
230  assert(v_it->first==it->first);
231 
232  entryt &e=v_it->second;
233  const entryt &new_e=it->second;
234 
235  if(make_union(e.object_map, new_e.object_map))
236  result=true;
237 
238  v_it++;
239  it++;
240  }
241 
242  return result;
243 }
244 
245 bool value_sett::make_union(object_mapt &dest, const object_mapt &src) const
246 {
247  bool result=false;
248 
250  it!=src.read().end();
251  it++)
252  {
253  if(insert(dest, *it))
254  result=true;
255  }
256 
257  return result;
258 }
259 
261  exprt &expr,
262  const namespacet &ns) const
263 {
264  bool mod=false;
265 
266  if(expr.id()==ID_pointer_offset)
267  {
268  assert(expr.operands().size()==1);
269 
270  object_mapt reference_set;
271  get_value_set(expr.op0(), reference_set, ns, true);
272 
273  exprt new_expr;
274  mp_integer previous_offset=0;
275 
276  const object_map_dt &object_map=reference_set.read();
278  it=object_map.begin();
279  it!=object_map.end();
280  it++)
281  if(!it->second)
282  return false;
283  else
284  {
285  const exprt &object=object_numbering[it->first];
286  mp_integer ptr_offset=compute_pointer_offset(object, ns);
287 
288  if(ptr_offset<0)
289  return false;
290 
291  ptr_offset += *it->second;
292 
293  if(mod && ptr_offset!=previous_offset)
294  return false;
295 
296  new_expr=from_integer(ptr_offset, expr.type());
297  previous_offset=ptr_offset;
298  mod=true;
299  }
300 
301  if(mod)
302  expr.swap(new_expr);
303  }
304  else
305  {
306  Forall_operands(it, expr)
307  mod=eval_pointer_offset(*it, ns) || mod;
308  }
309 
310  return mod;
311 }
312 
314  const exprt &expr,
315  value_setst::valuest &dest,
316  const namespacet &ns) const
317 {
318  object_mapt object_map;
319  get_value_set(expr, object_map, ns, false);
320 
322  it=object_map.read().begin();
323  it!=object_map.read().end();
324  it++)
325  dest.push_back(to_expr(*it));
326 
327  #if 0
328  for(value_setst::valuest::const_iterator it=dest.begin();
329  it!=dest.end(); it++)
330  std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
331  #endif
332 }
333 
335  const exprt &expr,
336  object_mapt &dest,
337  const namespacet &ns,
338  bool is_simplified) const
339 {
340  exprt tmp(expr);
341  if(!is_simplified)
342  simplify(tmp, ns);
343 
344  get_value_set_rec(tmp, dest, "", tmp.type(), ns);
345 }
346 
348  const exprt &expr,
349  object_mapt &dest,
350  const std::string &suffix,
351  const typet &original_type,
352  const namespacet &ns) const
353 {
354  #if 0
355  std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr) << "\n";
356  std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
357  #endif
358 
359  const typet &expr_type=ns.follow(expr.type());
360 
361  if(expr.id()==ID_unknown || expr.id()==ID_invalid)
362  {
363  insert(dest, exprt(ID_unknown, original_type));
364  }
365  else if(expr.id()==ID_index)
366  {
367  assert(expr.operands().size()==2);
368 
369  const typet &type=ns.follow(expr.op0().type());
370 
371  DATA_INVARIANT(type.id()==ID_array ||
372  type.id()==ID_incomplete_array,
373  "operand 0 of index expression must be an array");
374 
375  get_value_set_rec(expr.op0(), dest, "[]"+suffix, original_type, ns);
376  }
377  else if(expr.id()==ID_member)
378  {
379  assert(expr.operands().size()==1);
380 
381  const typet &type=ns.follow(expr.op0().type());
382 
383  DATA_INVARIANT(type.id()==ID_struct ||
384  type.id()==ID_union ||
385  type.id()==ID_incomplete_struct ||
386  type.id()==ID_incomplete_union,
387  "operand 0 of member expression must be struct or union");
388 
389  const std::string &component_name=
390  expr.get_string(ID_component_name);
391 
392  get_value_set_rec(expr.op0(), dest,
393  "."+component_name+suffix, original_type, ns);
394  }
395  else if(expr.id()==ID_symbol)
396  {
397  irep_idt identifier=to_symbol_expr(expr).get_identifier();
398 
399  // is it a pointer, integer, array or struct?
400  if(expr_type.id()==ID_pointer ||
401  expr_type.id()==ID_signedbv ||
402  expr_type.id()==ID_unsignedbv ||
403  expr_type.id()==ID_struct ||
404  expr_type.id()==ID_union ||
405  expr_type.id()==ID_array)
406  {
407  // look it up
408  valuest::const_iterator v_it=
409  values.find(id2string(identifier)+suffix);
410 
411  // try first component name as suffix if not yet found
412  if(v_it==values.end() &&
413  (expr_type.id()==ID_struct ||
414  expr_type.id()==ID_union))
415  {
416  const struct_union_typet &struct_union_type=
417  to_struct_union_type(expr_type);
418 
419  const std::string first_component_name=
420  struct_union_type.components().front().get_string(ID_name);
421 
422  v_it=values.find(
423  id2string(identifier)+"."+first_component_name+suffix);
424  }
425 
426  // not found? try without suffix
427  if(v_it==values.end())
428  v_it=values.find(identifier);
429 
430  if(v_it!=values.end())
431  make_union(dest, v_it->second.object_map);
432  else
433  insert(dest, exprt(ID_unknown, original_type));
434  }
435  else
436  insert(dest, exprt(ID_unknown, original_type));
437  }
438  else if(expr.id()==ID_if)
439  {
440  if(expr.operands().size()!=3)
441  throw "if takes three operands";
442 
443  get_value_set_rec(expr.op1(), dest, suffix, original_type, ns);
444  get_value_set_rec(expr.op2(), dest, suffix, original_type, ns);
445  }
446  else if(expr.id()==ID_address_of)
447  {
448  if(expr.operands().size()!=1)
449  throw expr.id_string()+" expected to have one operand";
450 
451  get_reference_set(expr.op0(), dest, ns);
452  }
453  else if(expr.id()==ID_dereference)
454  {
455  object_mapt reference_set;
456  get_reference_set(expr, reference_set, ns);
457  const object_map_dt &object_map=reference_set.read();
458 
459  if(object_map.begin()==object_map.end())
460  insert(dest, exprt(ID_unknown, original_type));
461  else
462  {
464  it1=object_map.begin();
465  it1!=object_map.end();
466  it1++)
467  {
470  const exprt object=object_numbering[it1->first];
471  get_value_set_rec(object, dest, suffix, original_type, ns);
472  }
473  }
474  }
475  else if(expr.id()=="reference_to")
476  {
477  // old stuff, will go away
478  object_mapt reference_set;
479 
480  get_reference_set(expr, reference_set, ns);
481 
482  const object_map_dt &object_map=reference_set.read();
483 
484  if(object_map.begin()==object_map.end())
485  insert(dest, exprt(ID_unknown, original_type));
486  else
487  {
489  it=object_map.begin();
490  it!=object_map.end();
491  it++)
492  {
495  const exprt object=object_numbering[it->first];
496  get_value_set_rec(object, dest, suffix, original_type, ns);
497  }
498  }
499  }
500  else if(expr.is_constant())
501  {
502  // check if NULL
503  if(expr.get(ID_value)==ID_NULL &&
504  expr_type.id()==ID_pointer)
505  {
506  insert(dest, exprt(ID_null_object, expr_type.subtype()), 0);
507  }
508  else if(expr_type.id()==ID_unsignedbv ||
509  expr_type.id()==ID_signedbv)
510  {
511  // an integer constant got turned into a pointer
512  insert(dest, exprt(ID_integer_address, unsigned_char_type()));
513  }
514  else
515  insert(dest, exprt(ID_unknown, original_type));
516  }
517  else if(expr.id()==ID_typecast)
518  {
519  if(expr.operands().size()!=1)
520  throw "typecast takes one operand";
521 
522  // let's see what gets converted to what
523 
524  const typet &op_type=ns.follow(expr.op0().type());
525 
526  if(op_type.id()==ID_pointer)
527  {
528  // pointer-to-pointer -- we just ignore these
529  get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
530  }
531  else if(op_type.id()==ID_unsignedbv ||
532  op_type.id()==ID_signedbv)
533  {
534  // integer-to-pointer
535 
536  if(expr.op0().is_zero())
537  insert(dest, exprt(ID_null_object, expr_type.subtype()), 0);
538  else
539  {
540  // see if we have something for the integer
541  object_mapt tmp;
542 
543  get_value_set_rec(expr.op0(), tmp, suffix, original_type, ns);
544 
545  if(tmp.read().empty())
546  {
547  // if not, throw in integer
548  insert(dest, exprt(ID_integer_address, unsigned_char_type()));
549  }
550  else if(tmp.read().size()==1 &&
551  object_numbering[tmp.read().begin()->first].id()==ID_unknown)
552  {
553  // if not, throw in integer
554  insert(dest, exprt(ID_integer_address, unsigned_char_type()));
555  }
556  else
557  {
558  // use as is
559  dest.write().insert(tmp.read().begin(), tmp.read().end());
560  }
561  }
562  }
563  else
564  insert(dest, exprt(ID_unknown, original_type));
565  }
566  else if(expr.id()==ID_plus ||
567  expr.id()==ID_minus)
568  {
569  if(expr.operands().size()<2)
570  throw expr.id_string()+" expected to have at least two operands";
571 
572  object_mapt pointer_expr_set;
573  mp_integer i;
574  bool i_is_set=false;
575 
576  // special case for pointer+integer
577 
578  if(expr.operands().size()==2 &&
579  expr_type.id()==ID_pointer)
580  {
581  exprt ptr_operand;
582 
583  if(expr.op0().type().id()!=ID_pointer &&
584  expr.op0().is_constant())
585  {
586  i_is_set=!to_integer(expr.op0(), i);
587  ptr_operand=expr.op1();
588  }
589  else
590  {
591  i_is_set=!to_integer(expr.op1(), i);
592  ptr_operand=expr.op0();
593  }
594 
595  if(i_is_set)
596  {
597  typet pointer_sub_type=ptr_operand.type().subtype();
598  if(pointer_sub_type.id()==ID_empty)
599  pointer_sub_type=char_type();
600 
601  mp_integer size=pointer_offset_size(pointer_sub_type, ns);
602 
603  if(size<=0)
604  {
605  i_is_set=false;
606  }
607  else
608  {
609  i*=size;
610 
611  if(expr.id()==ID_minus)
612  i.negate();
613  }
614  }
615 
617  ptr_operand, pointer_expr_set, "", ptr_operand.type(), ns);
618  }
619  else
620  {
621  // we get the points-to for all operands, even integers
622  forall_operands(it, expr)
623  {
625  *it, pointer_expr_set, "", it->type(), ns);
626  }
627  }
628 
630  it=pointer_expr_set.read().begin();
631  it!=pointer_expr_set.read().end();
632  it++)
633  {
634  offsett offset = it->second;
635 
636  // adjust by offset
637  if(offset && i_is_set)
638  *offset += i;
639  else
640  offset.reset();
641 
642  insert(dest, it->first, offset);
643  }
644  }
645  else if(expr.id()==ID_mult)
646  {
647  // this is to do stuff like
648  // (int*)((sel*(ulong)&a)+((sel^0x1)*(ulong)&b))
649 
650  if(expr.operands().size()<2)
651  throw expr.id_string()+" expected to have at least two operands";
652 
653  object_mapt pointer_expr_set;
654 
655  // we get the points-to for all operands, even integers
656  forall_operands(it, expr)
657  {
659  *it, pointer_expr_set, "", it->type(), ns);
660  }
661 
663  it=pointer_expr_set.read().begin();
664  it!=pointer_expr_set.read().end();
665  it++)
666  {
667  offsett offset = it->second;
668 
669  // kill any offset
670  offset.reset();
671 
672  insert(dest, it->first, offset);
673  }
674  }
675  else if(expr.id()==ID_side_effect)
676  {
677  const irep_idt &statement=expr.get(ID_statement);
678 
679  if(statement==ID_function_call)
680  {
681  // these should be gone
682  throw "unexpected function_call sideeffect";
683  }
684  else if(statement==ID_allocate)
685  {
686  assert(suffix=="");
687 
688  const typet &dynamic_type=
689  static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
690 
691  dynamic_object_exprt dynamic_object(dynamic_type);
692  dynamic_object.set_instance(location_number);
693  dynamic_object.valid()=true_exprt();
694 
695  insert(dest, dynamic_object, 0);
696  }
697  else if(statement==ID_cpp_new ||
698  statement==ID_cpp_new_array)
699  {
700  assert(suffix=="");
701  assert(expr_type.id()==ID_pointer);
702 
704  dynamic_object.set_instance(location_number);
705  dynamic_object.valid()=true_exprt();
706 
707  insert(dest, dynamic_object, 0);
708  }
709  else
710  insert(dest, exprt(ID_unknown, original_type));
711  }
712  else if(expr.id()==ID_struct)
713  {
714  // a struct constructor, which may contain addresses
715  forall_operands(it, expr)
716  get_value_set_rec(*it, dest, suffix, original_type, ns);
717  }
718  else if(expr.id()==ID_with)
719  {
720  assert(expr.operands().size()==3);
721 
722  // this is the array/struct
723  object_mapt tmp_map0;
724  get_value_set_rec(expr.op0(), tmp_map0, suffix, original_type, ns);
725 
726  // this is the update value -- note NO SUFFIX
727  object_mapt tmp_map2;
728  get_value_set_rec(expr.op2(), tmp_map2, "", original_type, ns);
729 
730  if(expr_type.id()==ID_struct)
731  {
732  #if 0
733  const object_map_dt &object_map0=tmp_map0.read();
734  irep_idt component_name=expr.op1().get(ID_component_name);
735 
736  bool insert=true;
737 
739  it=object_map0.begin();
740  it!=object_map0.end();
741  it++)
742  {
743  const exprt &e=to_expr(it);
744 
745  if(e.id()==ID_member &&
746  e.get(ID_component_name)==component_name)
747  {
748  if(insert)
749  {
750  dest.write().insert(tmp_map2.read().begin(), tmp_map2.read().end());
751  insert=false;
752  }
753  }
754  else
755  dest.write().insert(*it);
756  }
757  #else
758  // Should be more precise! We only want "suffix"
759  make_union(dest, tmp_map0);
760  make_union(dest, tmp_map2);
761  #endif
762  }
763  else
764  {
765  make_union(dest, tmp_map0);
766  make_union(dest, tmp_map2);
767  }
768  }
769  else if(expr.id()==ID_array)
770  {
771  // an array constructor, possibly containing addresses
772  forall_operands(it, expr)
773  get_value_set_rec(*it, dest, suffix, original_type, ns);
774  }
775  else if(expr.id()==ID_array_of)
776  {
777  // an array constructor, possibly containing an address
778  assert(expr.operands().size()==1);
779  get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
780  }
781  else if(expr.id()==ID_dynamic_object)
782  {
785 
786  const std::string prefix=
787  "value_set::dynamic_object"+
788  std::to_string(dynamic_object.get_instance());
789 
790  // first try with suffix
791  const std::string full_name=prefix+suffix;
792 
793  // look it up
794  valuest::const_iterator v_it=values.find(full_name);
795 
796  // not found? try without suffix
797  if(v_it==values.end())
798  v_it=values.find(prefix);
799 
800  if(v_it==values.end())
801  insert(dest, exprt(ID_unknown, original_type));
802  else
803  make_union(dest, v_it->second.object_map);
804  }
805  else if(expr.id()==ID_byte_extract_little_endian ||
806  expr.id()==ID_byte_extract_big_endian)
807  {
808  if(expr.operands().size()!=2)
809  throw "byte_extract takes two operands";
810 
811  bool found=false;
812 
813  exprt op1=expr.op1();
814  if(eval_pointer_offset(op1, ns))
815  simplify(op1, ns);
816 
817  mp_integer op1_offset;
818  const typet &op0_type=ns.follow(expr.op0().type());
819  if(!to_integer(op1, op1_offset) && op0_type.id()==ID_struct)
820  {
821  const struct_typet &struct_type=to_struct_type(op0_type);
822 
823  for(struct_union_typet::componentst::const_iterator
824  c_it=struct_type.components().begin();
825  !found && c_it!=struct_type.components().end();
826  c_it++)
827  {
828  const irep_idt &name=c_it->get_name();
829 
830  mp_integer comp_offset=member_offset(struct_type, name, ns);
831 
832  if(comp_offset>op1_offset)
833  break;
834  else if(comp_offset!=op1_offset)
835  continue;
836 
837  found=true;
838 
839  member_exprt member(expr.op0(), *c_it);
840  get_value_set_rec(member, dest, suffix, original_type, ns);
841  }
842  }
843 
844  if(op0_type.id()==ID_union)
845  {
846  const union_typet &union_type=to_union_type(op0_type);
847 
848  // just collect them all
849  for(union_typet::componentst::const_iterator
850  c_it=union_type.components().begin();
851  c_it!=union_type.components().end(); c_it++)
852  {
853  const irep_idt &name=c_it->get_name();
854  member_exprt member(expr.op0(), name, c_it->type());
855  get_value_set_rec(member, dest, suffix, original_type, ns);
856  }
857  }
858 
859  if(!found)
860  // we just pass through
861  get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
862  }
863  else if(expr.id()==ID_byte_update_little_endian ||
864  expr.id()==ID_byte_update_big_endian)
865  {
866  if(expr.operands().size()!=3)
867  throw "byte_update takes three operands";
868 
869  // we just pass through
870  get_value_set_rec(expr.op0(), dest, suffix, original_type, ns);
871  get_value_set_rec(expr.op2(), dest, suffix, original_type, ns);
872 
873  // we could have checked object size to be more precise
874  }
875  else
876  {
877  #if 0
878  std::cout << "WARNING: not doing " << expr.id() << '\n';
879  #endif
880  }
881 
882  #ifdef DEBUG
883  std::cout << "GET_VALUE_SET_REC RESULT:\n";
884  for(const auto &obj : dest.read())
885  {
886  const exprt &e=to_expr(obj);
887  std::cout << " " << format(e) << "\n";
888  }
889  std::cout << "\n";
890  #endif
891 }
892 
894  const exprt &src,
895  exprt &dest) const
896 {
897  // remove pointer typecasts
898  if(src.id()==ID_typecast)
899  {
900  assert(src.type().id()==ID_pointer);
901 
902  if(src.operands().size()!=1)
903  throw "typecast expects one operand";
904 
905  dereference_rec(src.op0(), dest);
906  }
907  else
908  dest=src;
909 }
910 
912  const exprt &expr,
913  value_setst::valuest &dest,
914  const namespacet &ns) const
915 {
916  object_mapt object_map;
917  get_reference_set(expr, object_map, ns);
918 
920  it=object_map.read().begin();
921  it!=object_map.read().end();
922  it++)
923  dest.push_back(to_expr(*it));
924 }
925 
927  const exprt &expr,
928  object_mapt &dest,
929  const namespacet &ns) const
930 {
931  #if 0
932  std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
933  << '\n';
934  #endif
935 
936  if(expr.id()==ID_symbol ||
937  expr.id()==ID_dynamic_object ||
938  expr.id()==ID_string_constant ||
939  expr.id()==ID_array)
940  {
941  if(expr.type().id()==ID_array &&
942  expr.type().subtype().id()==ID_array)
943  insert(dest, expr);
944  else
945  insert(dest, expr, 0);
946 
947  return;
948  }
949  else if(expr.id()==ID_dereference)
950  {
951  if(expr.operands().size()!=1)
952  throw expr.id_string()+" expected to have one operand";
953 
954  get_value_set_rec(expr.op0(), dest, "", expr.op0().type(), ns);
955 
956  #if 0
957  for(expr_sett::const_iterator it=value_set.begin();
958  it!=value_set.end(); it++)
959  std::cout << "VALUE_SET: " << format(*it) << '\n';
960  #endif
961 
962  return;
963  }
964  else if(expr.id()==ID_index)
965  {
966  if(expr.operands().size()!=2)
967  throw "index expected to have two operands";
968 
969  const index_exprt &index_expr=to_index_expr(expr);
970  const exprt &array=index_expr.array();
971  const exprt &offset=index_expr.index();
972  const typet &array_type=ns.follow(array.type());
973 
974  assert(array_type.id()==ID_array ||
975  array_type.id()==ID_incomplete_array);
976 
977  object_mapt array_references;
978  get_reference_set(array, array_references, ns);
979 
980  const object_map_dt &object_map=array_references.read();
981 
983  a_it=object_map.begin();
984  a_it!=object_map.end();
985  a_it++)
986  {
987  const exprt &object=object_numbering[a_it->first];
988 
989  if(object.id()==ID_unknown)
990  insert(dest, exprt(ID_unknown, expr.type()));
991  else
992  {
993  index_exprt index_expr(expr.type());
994  index_expr.array()=object;
995  index_expr.index()=from_integer(0, index_type());
996 
997  // adjust type?
998  if(ns.follow(object.type())!=array_type)
999  index_expr.make_typecast(array.type());
1000 
1001  offsett o = a_it->second;
1002  mp_integer i;
1003 
1004  if(offset.is_zero())
1005  {
1006  }
1007  else if(!to_integer(offset, i) && o)
1008  {
1009  mp_integer size=pointer_offset_size(array_type.subtype(), ns);
1010 
1011  if(size<=0)
1012  o.reset();
1013  else
1014  *o = i * size;
1015  }
1016  else
1017  o.reset();
1018 
1019  insert(dest, index_expr, o);
1020  }
1021  }
1022 
1023  return;
1024  }
1025  else if(expr.id()==ID_member)
1026  {
1027  const irep_idt &component_name=expr.get(ID_component_name);
1028 
1029  if(expr.operands().size()!=1)
1030  throw "member expected to have one operand";
1031 
1032  const exprt &struct_op=expr.op0();
1033 
1034  object_mapt struct_references;
1035  get_reference_set(struct_op, struct_references, ns);
1036 
1037  const object_map_dt &object_map=struct_references.read();
1038 
1040  it=object_map.begin();
1041  it!=object_map.end();
1042  it++)
1043  {
1044  const exprt &object=object_numbering[it->first];
1045 
1046  if(object.id()==ID_unknown)
1047  insert(dest, exprt(ID_unknown, expr.type()));
1048  else
1049  {
1050  offsett o = it->second;
1051 
1052  member_exprt member_expr(object, component_name, expr.type());
1053 
1054  // We cannot introduce a cast from scalar to non-scalar,
1055  // thus, we can only adjust the types of structs and unions.
1056 
1057  const typet &final_object_type = ns.follow(object.type());
1058 
1059  if(final_object_type.id()==ID_struct ||
1060  final_object_type.id()==ID_union)
1061  {
1062  // adjust type?
1063  if(ns.follow(struct_op.type())!=final_object_type)
1064  member_expr.op0().make_typecast(struct_op.type());
1065 
1066  insert(dest, member_expr, o);
1067  }
1068  else
1069  insert(dest, exprt(ID_unknown, expr.type()));
1070  }
1071  }
1072 
1073  return;
1074  }
1075  else if(expr.id()==ID_if)
1076  {
1077  if(expr.operands().size()!=3)
1078  throw "if takes three operands";
1079 
1080  get_reference_set_rec(expr.op1(), dest, ns);
1081  get_reference_set_rec(expr.op2(), dest, ns);
1082  return;
1083  }
1084 
1085  insert(dest, exprt(ID_unknown, expr.type()));
1086 }
1087 
1089  const exprt &lhs,
1090  const exprt &rhs,
1091  const namespacet &ns,
1092  bool is_simplified,
1093  bool add_to_sets)
1094 {
1095 #if 0
1096  std::cout << "ASSIGN LHS: " << format(lhs) << " : "
1097  << format(lhs.type()) << '\n';
1098  std::cout << "ASSIGN RHS: " << format(rhs) << " : "
1099  << format(rhs.type()) << '\n';
1100  std::cout << "--------------------------------------------\n";
1101  output(ns, std::cout);
1102 #endif
1103 
1104  const typet &type=ns.follow(lhs.type());
1105 
1106  if(type.id()==ID_struct ||
1107  type.id()==ID_union)
1108  {
1109  const struct_union_typet &struct_union_type=
1110  to_struct_union_type(type);
1111 
1112  for(struct_union_typet::componentst::const_iterator
1113  c_it=struct_union_type.components().begin();
1114  c_it!=struct_union_type.components().end();
1115  c_it++)
1116  {
1117  const typet &subtype=c_it->type();
1118  const irep_idt &name=c_it->get(ID_name);
1119 
1120  // ignore methods and padding
1121  if(subtype.id()==ID_code ||
1122  c_it->get_is_padding()) continue;
1123 
1124  member_exprt lhs_member(lhs, name, subtype);
1125 
1126  exprt rhs_member;
1127 
1128  if(rhs.id()==ID_unknown ||
1129  rhs.id()==ID_invalid)
1130  {
1131  rhs_member=exprt(rhs.id(), subtype);
1132  }
1133  else
1134  {
1135  if(!base_type_eq(rhs.type(), type, ns))
1136  throw "value_sett::assign type mismatch: "
1137  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1138  "type:\n"+type.pretty();
1139 
1140  rhs_member=make_member(rhs, name, ns);
1141 
1142  assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
1143  }
1144  }
1145  }
1146  else if(type.id()==ID_array)
1147  {
1148  const index_exprt lhs_index(
1149  lhs, exprt(ID_unknown, index_type()), type.subtype());
1150 
1151  if(rhs.id()==ID_unknown ||
1152  rhs.id()==ID_invalid)
1153  {
1154  assign(
1155  lhs_index,
1156  exprt(rhs.id(), type.subtype()),
1157  ns,
1158  is_simplified,
1159  add_to_sets);
1160  }
1161  else
1162  {
1163  if(!base_type_eq(rhs.type(), type, ns))
1164  throw "value_sett::assign type mismatch: "
1165  "rhs.type():\n"+rhs.type().pretty()+"\n"+
1166  "type:\n"+type.pretty();
1167 
1168  if(rhs.id()==ID_array_of)
1169  {
1170  assert(rhs.operands().size()==1);
1171  assign(lhs_index, rhs.op0(), ns, is_simplified, add_to_sets);
1172  }
1173  else if(rhs.id()==ID_array ||
1174  rhs.id()==ID_constant)
1175  {
1176  forall_operands(o_it, rhs)
1177  {
1178  assign(lhs_index, *o_it, ns, is_simplified, add_to_sets);
1179  add_to_sets=true;
1180  }
1181  }
1182  else if(rhs.id()==ID_with)
1183  {
1184  assert(rhs.operands().size()==3);
1185 
1186  const index_exprt op0_index(
1187  rhs.op0(), exprt(ID_unknown, index_type()), type.subtype());
1188 
1189  assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1190  assign(lhs_index, rhs.op2(), ns, is_simplified, true);
1191  }
1192  else
1193  {
1194  const index_exprt rhs_index(
1195  rhs, exprt(ID_unknown, index_type()), type.subtype());
1196  assign(lhs_index, rhs_index, ns, is_simplified, true);
1197  }
1198  }
1199  }
1200  else
1201  {
1202  // basic type
1203  object_mapt values_rhs;
1204  get_value_set(rhs, values_rhs, ns, is_simplified);
1205 
1206  // Permit custom subclass to alter the read values prior to write:
1207  adjust_assign_rhs_values(rhs, ns, values_rhs);
1208 
1209  // Permit custom subclass to perform global side-effects prior to write:
1210  apply_assign_side_effects(lhs, rhs, ns);
1211 
1212  assign_rec(lhs, values_rhs, "", ns, add_to_sets);
1213  }
1214 }
1215 
1217  const exprt &op,
1218  const namespacet &ns)
1219 {
1220  // op must be a pointer
1221  if(op.type().id()!=ID_pointer)
1222  throw "free expected to have pointer-type operand";
1223 
1224  // find out what it points to
1225  object_mapt value_set;
1226  get_value_set(op, value_set, ns, false);
1227 
1228  const object_map_dt &object_map=value_set.read();
1229 
1230  // find out which *instances* interest us
1231  dynamic_object_id_sett to_mark;
1232 
1234  it=object_map.begin();
1235  it!=object_map.end();
1236  it++)
1237  {
1238  const exprt &object=object_numbering[it->first];
1239 
1240  if(object.id()==ID_dynamic_object)
1241  {
1243  to_dynamic_object_expr(object);
1244 
1245  if(dynamic_object.valid().is_true())
1246  to_mark.insert(dynamic_object.get_instance());
1247  }
1248  }
1249 
1250  // mark these as 'may be invalid'
1251  // this, unfortunately, destroys the sharing
1252  for(valuest::iterator v_it=values.begin();
1253  v_it!=values.end();
1254  v_it++)
1255  {
1256  object_mapt new_object_map;
1257 
1258  const object_map_dt &old_object_map=
1259  v_it->second.object_map.read();
1260 
1261  bool changed=false;
1262 
1264  o_it=old_object_map.begin();
1265  o_it!=old_object_map.end();
1266  o_it++)
1267  {
1268  const exprt &object=object_numbering[o_it->first];
1269 
1270  if(object.id()==ID_dynamic_object)
1271  {
1273  to_dynamic_object_expr(object);
1274 
1275  if(to_mark.count(dynamic_object.get_instance())==0)
1276  set(new_object_map, *o_it);
1277  else
1278  {
1279  // adjust
1280  offsett o = o_it->second;
1281  exprt tmp(object);
1282  to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
1283  insert(new_object_map, tmp, o);
1284  changed=true;
1285  }
1286  }
1287  else
1288  set(new_object_map, *o_it);
1289  }
1290 
1291  if(changed)
1292  v_it->second.object_map=new_object_map;
1293  }
1294 }
1295 
1297  const exprt &lhs,
1298  const object_mapt &values_rhs,
1299  const std::string &suffix,
1300  const namespacet &ns,
1301  bool add_to_sets)
1302 {
1303  #if 0
1304  std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
1305  std::cout << "ASSIGN_REC LHS ID: " << lhs.id() << '\n';
1306  std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1307 
1308  for(object_map_dt::const_iterator it=values_rhs.read().begin();
1309  it!=values_rhs.read().end();
1310  it++)
1311  std::cout << "ASSIGN_REC RHS: " <<
1312  format(object_numbering[it->first]) << '\n';
1313  std::cout << '\n';
1314  #endif
1315 
1316  if(lhs.id()==ID_symbol)
1317  {
1318  const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
1319 
1320  entryt &e=get_entry(entryt(identifier, suffix), lhs.type(), ns);
1321 
1322  if(add_to_sets)
1323  make_union(e.object_map, values_rhs);
1324  else
1325  e.object_map=values_rhs;
1326  }
1327  else if(lhs.id()==ID_dynamic_object)
1328  {
1331 
1332  const std::string name=
1333  "value_set::dynamic_object"+
1334  std::to_string(dynamic_object.get_instance());
1335 
1336  entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns);
1337 
1338  make_union(e.object_map, values_rhs);
1339  }
1340  else if(lhs.id()==ID_dereference)
1341  {
1342  if(lhs.operands().size()!=1)
1343  throw lhs.id_string()+" expected to have one operand";
1344 
1345  object_mapt reference_set;
1346  get_reference_set(lhs, reference_set, ns);
1347 
1348  if(reference_set.read().size()!=1)
1349  add_to_sets=true;
1350 
1352  it=reference_set.read().begin();
1353  it!=reference_set.read().end();
1354  it++)
1355  {
1358  const exprt object=object_numbering[it->first];
1359 
1360  if(object.id()!=ID_unknown)
1361  assign_rec(object, values_rhs, suffix, ns, add_to_sets);
1362  }
1363  }
1364  else if(lhs.id()==ID_index)
1365  {
1366  if(lhs.operands().size()!=2)
1367  throw "index expected to have two operands";
1368 
1369  const typet &type=ns.follow(lhs.op0().type());
1370 
1371  DATA_INVARIANT(type.id()==ID_array || type.id()==ID_incomplete_array,
1372  "operand 0 of index expression must be an array");
1373 
1374  assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, true);
1375  }
1376  else if(lhs.id()==ID_member)
1377  {
1378  if(lhs.operands().size()!=1)
1379  throw "member expected to have one operand";
1380 
1381  const std::string &component_name=lhs.get_string(ID_component_name);
1382 
1383  const typet &type=ns.follow(lhs.op0().type());
1384 
1385  DATA_INVARIANT(type.id()==ID_struct ||
1386  type.id()==ID_union ||
1387  type.id()==ID_incomplete_struct ||
1388  type.id()==ID_incomplete_union,
1389  "operand 0 of member expression must be struct or union");
1390 
1391  assign_rec(
1392  lhs.op0(), values_rhs, "."+component_name+suffix, ns, add_to_sets);
1393  }
1394  else if(lhs.id()=="valid_object" ||
1395  lhs.id()=="dynamic_size" ||
1396  lhs.id()=="dynamic_type" ||
1397  lhs.id()=="is_zero_string" ||
1398  lhs.id()=="zero_string" ||
1399  lhs.id()=="zero_string_length")
1400  {
1401  // we ignore this here
1402  }
1403  else if(lhs.id()==ID_string_constant)
1404  {
1405  // someone writes into a string-constant
1406  // evil guy
1407  }
1408  else if(lhs.id() == ID_null_object)
1409  {
1410  // evil as well
1411  }
1412  else if(lhs.id()==ID_typecast)
1413  {
1414  const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1415 
1416  assign_rec(typecast_expr.op(), values_rhs, suffix, ns, add_to_sets);
1417  }
1418  else if(lhs.id()==ID_byte_extract_little_endian ||
1419  lhs.id()==ID_byte_extract_big_endian)
1420  {
1421  assert(lhs.operands().size()==2);
1422  assign_rec(lhs.op0(), values_rhs, suffix, ns, true);
1423  }
1424  else if(lhs.id()==ID_integer_address)
1425  {
1426  // that's like assigning into __CPROVER_memory[...],
1427  // which we don't track
1428  }
1429  else
1430  throw "assign NYI: `"+lhs.id_string()+"'";
1431 }
1432 
1434  const irep_idt &function,
1435  const exprt::operandst &arguments,
1436  const namespacet &ns)
1437 {
1438  const symbolt &symbol=ns.lookup(function);
1439 
1440  const code_typet &type=to_code_type(symbol.type);
1441  const code_typet::parameterst &parameter_types=type.parameters();
1442 
1443  // these first need to be assigned to dummy, temporary arguments
1444  // and only thereafter to the actuals, in order
1445  // to avoid overwriting actuals that are needed for recursive
1446  // calls
1447 
1448  for(std::size_t i=0; i<arguments.size(); i++)
1449  {
1450  const std::string identifier="value_set::dummy_arg_"+std::to_string(i);
1451  const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1452  assign(dummy_lhs, arguments[i], ns, false, false);
1453  }
1454 
1455  // now assign to 'actual actuals'
1456 
1457  unsigned i=0;
1458 
1459  for(code_typet::parameterst::const_iterator
1460  it=parameter_types.begin();
1461  it!=parameter_types.end();
1462  it++)
1463  {
1464  const irep_idt &identifier=it->get_identifier();
1465  if(identifier=="")
1466  continue;
1467 
1468  const exprt v_expr=
1469  symbol_exprt("value_set::dummy_arg_"+std::to_string(i), it->type());
1470 
1471  const symbol_exprt actual_lhs(identifier, it->type());
1472  assign(actual_lhs, v_expr, ns, true, true);
1473  i++;
1474  }
1475 
1476  // we could delete the dummy_arg_* now.
1477 }
1478 
1480  const exprt &lhs,
1481  const namespacet &ns)
1482 {
1483  if(lhs.is_nil())
1484  return;
1485 
1486  symbol_exprt rhs("value_set::return_value", lhs.type());
1487 
1488  assign(lhs, rhs, ns, false, false);
1489 }
1490 
1492  const codet &code,
1493  const namespacet &ns)
1494 {
1495  const irep_idt &statement=code.get_statement();
1496 
1497  if(statement==ID_block)
1498  {
1499  forall_operands(it, code)
1500  apply_code_rec(to_code(*it), ns);
1501  }
1502  else if(statement==ID_function_call)
1503  {
1504  // shouldn't be here
1505  UNREACHABLE;
1506  }
1507  else if(statement==ID_assign ||
1508  statement==ID_init)
1509  {
1510  if(code.operands().size()!=2)
1511  throw "assignment expected to have two operands";
1512 
1513  assign(code.op0(), code.op1(), ns, false, false);
1514  }
1515  else if(statement==ID_decl)
1516  {
1517  if(code.operands().size()!=1)
1518  throw "decl expected to have one operand";
1519 
1520  const exprt &lhs=code.op0();
1521 
1522  if(lhs.id()!=ID_symbol)
1523  throw "decl expected to have symbol on lhs";
1524 
1525  const typet &lhs_type=ns.follow(lhs.type());
1526 
1527  if(lhs_type.id()==ID_pointer ||
1528  (lhs_type.id()==ID_array &&
1529  ns.follow(lhs_type.subtype()).id()==ID_pointer))
1530  {
1531  // assign the address of the failed object
1532  exprt failed=get_failed_symbol(to_symbol_expr(lhs), ns);
1533 
1534  if(failed.is_not_nil())
1535  {
1536  address_of_exprt address_of_expr(
1537  failed, to_pointer_type(lhs.type()));
1538  assign(lhs, address_of_expr, ns, false, false);
1539  }
1540  else
1541  assign(lhs, exprt(ID_invalid), ns, false, false);
1542  }
1543  }
1544  else if(statement==ID_expression)
1545  {
1546  // can be ignored, we don't expect side effects here
1547  }
1548  else if(statement=="cpp_delete" ||
1549  statement=="cpp_delete[]")
1550  {
1551  // does nothing
1552  }
1553  else if(statement==ID_free)
1554  {
1555  // this may kill a valid bit
1556 
1557  if(code.operands().size()!=1)
1558  throw "free expected to have one operand";
1559 
1560  do_free(code.op0(), ns);
1561  }
1562  else if(statement=="lock" || statement=="unlock")
1563  {
1564  // ignore for now
1565  }
1566  else if(statement==ID_asm)
1567  {
1568  // ignore for now, probably not safe
1569  }
1570  else if(statement==ID_nondet)
1571  {
1572  // doesn't do anything
1573  }
1574  else if(statement==ID_printf)
1575  {
1576  // doesn't do anything
1577  }
1578  else if(statement==ID_return)
1579  {
1580  // this is turned into an assignment
1581  if(code.operands().size()==1)
1582  {
1583  symbol_exprt lhs("value_set::return_value", code.op0().type());
1584  assign(lhs, code.op0(), ns, false, false);
1585  }
1586  }
1587  else if(statement==ID_array_set)
1588  {
1589  }
1590  else if(statement==ID_array_copy)
1591  {
1592  }
1593  else if(statement==ID_array_replace)
1594  {
1595  }
1596  else if(statement==ID_assume)
1597  {
1598  guard(to_code_assume(code).op0(), ns);
1599  }
1600  else if(statement==ID_user_specified_predicate ||
1601  statement==ID_user_specified_parameter_predicates ||
1602  statement==ID_user_specified_return_predicates)
1603  {
1604  // doesn't do anything
1605  }
1606  else if(statement==ID_fence)
1607  {
1608  }
1609  else if(statement==ID_input || statement==ID_output)
1610  {
1611  // doesn't do anything
1612  }
1613  else if(statement==ID_dead)
1614  {
1615  // Ignore by default; could prune the value set.
1616  }
1617  else
1618  {
1619  // std::cerr << code.pretty() << '\n';
1620  throw "value_sett: unexpected statement: "+id2string(statement);
1621  }
1622 }
1623 
1625  const exprt &expr,
1626  const namespacet &ns)
1627 {
1628  if(expr.id()==ID_and)
1629  {
1630  forall_operands(it, expr)
1631  guard(*it, ns);
1632  }
1633  else if(expr.id()==ID_equal)
1634  {
1635  }
1636  else if(expr.id()==ID_notequal)
1637  {
1638  }
1639  else if(expr.id()==ID_not)
1640  {
1641  }
1642  else if(expr.id()==ID_dynamic_object)
1643  {
1644  assert(expr.operands().size()==1);
1645 
1647  // dynamic_object.instance()=
1648  // from_integer(location_number, typet(ID_natural));
1649  dynamic_object.valid()=true_exprt();
1650 
1651  address_of_exprt address_of(dynamic_object);
1652  address_of.type()=expr.op0().type();
1653 
1654  assign(expr.op0(), address_of, ns, false, false);
1655  }
1656 }
1657 
1659  const exprt &src,
1660  const irep_idt &component_name,
1661  const namespacet &ns)
1662 {
1663  const struct_union_typet &struct_union_type=
1664  to_struct_union_type(ns.follow(src.type()));
1665 
1666  if(src.id()==ID_struct ||
1667  src.id()==ID_constant)
1668  {
1669  std::size_t no=struct_union_type.component_number(component_name);
1670  assert(no<src.operands().size());
1671  return src.operands()[no];
1672  }
1673  else if(src.id()==ID_with)
1674  {
1675  assert(src.operands().size()==3);
1676 
1677  // see if op1 is the member we want
1678  const exprt &member_operand=src.op1();
1679 
1680  if(component_name==member_operand.get(ID_component_name))
1681  // yes! just take op2
1682  return src.op2();
1683  else
1684  // no! do this recursively
1685  return make_member(src.op0(), component_name, ns);
1686  }
1687  else if(src.id()==ID_typecast)
1688  {
1689  // push through typecast
1690  assert(src.operands().size()==1);
1691  return make_member(src.op0(), component_name, ns);
1692  }
1693 
1694  // give up
1695  typet subtype=struct_union_type.component_type(component_name);
1696  member_exprt member_expr(src, component_name, subtype);
1697 
1698  return member_expr;
1699 }
const irep_idt & get_statement() const
Definition: std_code.h:39
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
static int8_t r
Definition: irep_hash.h:59
BigInt mp_integer
Definition: mp_arith.h:22
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
Represents a row of a value_sett.
Definition: value_set.h:235
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:386
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
object_mapt object_map
Definition: value_set.h:237
const exprt & op() const
Definition: std_expr.h:340
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
const irep_idt & get_identifier() const
Definition: std_expr.h:128
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it...
Definition: value_set.cpp:1088
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
Definition: value_set.cpp:245
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
Definition: value_set.cpp:1491
std::vector< parametert > parameterst
Definition: std_types.h:767
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
Definition: value_set.cpp:926
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:313
const componentst & components() const
Definition: std_types.h:245
Value Set.
static const object_map_dt blank
Definition: value_set.h:126
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
Definition: value_set.h:59
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void insert(It b, It e)
Definition: value_set.h:121
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
Definition: value_set.cpp:893
Pointer Dereferencing.
Structure type.
Definition: std_types.h:297
virtual void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Subclass customisation point for recursion over LHS expression:
Definition: value_set.cpp:1296
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
virtual void apply_assign_side_effects(const exprt &lhs, const exprt &rhs, const namespacet &ns)
Subclass customisation point to apply global side-effects to this domain, after RHS values are read b...
Definition: value_set.h:543
Extract member of struct or union.
Definition: std_expr.h:3871
static bool field_sensitive(const irep_idt &id, const typet &type, const namespacet &)
Definition: value_set.cpp:39
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:4488
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-s...
Definition: value_set.cpp:260
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
data_typet::value_type value_type
Definition: value_set.h:89
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Transforms this value-set by executing the actual -> formal parameter assignments for a particular ca...
Definition: value_set.cpp:1433
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
data_typet::const_iterator const_iterator
Definition: value_set.h:87
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
Definition: value_set.h:65
virtual void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Subclass customisation point for recursion over RHS expression:
Definition: value_set.cpp:347
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
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
typename Map::mapped_type number_type
Definition: numbering.h:24
typet component_type(const irep_idt &component_name) const
Definition: std_types.cpp:68
Operator to return the address of an object.
Definition: std_expr.h:3170
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool is_constant() const
Definition: expr.cpp:119
virtual void adjust_assign_rhs_values(const exprt &rhs, const namespacet &ns, object_mapt &rhs_values) const
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set b...
Definition: value_set.h:532
std::vector< exprt > operandst
Definition: expr.h:45
Pointer Logic.
const irep_idt & display_name() const
Definition: symbol.h:57
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
const_iterator find(T &&t) const
Definition: value_set.h:124
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Merges an existing entry into an object map.
Definition: value_set.h:179
std::unordered_map< idt, entryt, string_hash > valuest
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets...
Definition: value_set.h:289
typet type
Type of symbol.
Definition: symbol.h:34
void do_end_function(const exprt &lhs, const namespacet &ns)
Transforms this value-set by assigning this function&#39;s return value to a given LHS expression...
Definition: value_set.cpp:1479
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
exprt & index()
Definition: std_expr.h:1496
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets the set of expressions that expr may refer to, according to this value set.
Definition: value_set.cpp:911
Base class for all expressions.
Definition: expr.h:42
The union type.
Definition: std_types.h:458
const parameterst & parameters() const
Definition: std_types.h:905
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
#define UNREACHABLE
Definition: invariant.h:250
std::set< unsigned int > dynamic_object_id_sett
Set of dynamic object numbers, equivalent to a set of dynamic_object_exprts with corresponding IDs...
Definition: value_set.h:271
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances)...
Definition: value_set.h:78
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const T & read() const
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_zero() const
Definition: expr.cpp:161
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
Definition: value_set.cpp:96
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
exprt dynamic_object(const exprt &pointer)
A statement in a programming language.
Definition: std_code.h:21
exprt to_expr(const object_map_dt::value_type &it) const
Converts an object_map_dt entry object_number -> offset into an object_descriptor_exprt with ...
Definition: value_set.cpp:186
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
entryt & get_entry(const entryt &e, const typet &type, const namespacet &ns)
Gets or inserts an entry in this value-set.
Definition: value_set.cpp:54
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
TO_BE_DOCUMENTED.
Definition: std_expr.h:2035
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
Definition: value_set.cpp:1624
operandst & operands()
Definition: expr.h:66
void do_free(const exprt &op, const namespacet &ns)
Marks objects that may be pointed to by op as maybe-invalid.
Definition: value_set.cpp:1216
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::list< exprt > valuest
Definition: value_sets.h:28
std::string suffix
Definition: value_set.h:239
exprt & array()
Definition: std_expr.h:1486
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:341
bitvector_typet char_type()
Definition: c_types.cpp:114
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
size_t size() const
Definition: value_set.h:101
bool simplify(exprt &expr, const namespacet &ns)
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
Definition: value_set.h:55
exprt make_member(const exprt &src, const irep_idt &component_name, const namespacet &ns)
Extracts a member from a struct- or union-typed expression.
Definition: value_set.cpp:1658
array index operator
Definition: std_expr.h:1462
static format_containert< T > format(const T &o)
Definition: format.h:35