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