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