cprover
value_set.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set
4
5Author: 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
43bool 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 {
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
111 }
112 else if(!entry->second)
114 else if(offset && *entry->second == *offset)
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
138void 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
217exprt 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
287bool 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
353std::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
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
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
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,
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),
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
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
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
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_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
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:542
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 & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
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
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
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
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
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 & new_value()
Definition: std_expr.h:2342
exprt & where()
Definition: std_expr.h:2332
exprt & old()
Definition: std_expr.h:2322
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
bool can_cast_expr< code_inputt >(const exprt &base)
bool can_cast_expr< code_outputt >(const exprt &base)
const code_returnt & to_code_return(const codet &code)
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:301
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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.
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 array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1456
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3097
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1657
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
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
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.