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