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