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