CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 <util/arith_tools.h>
15#include <util/bitvector_expr.h>
16#include <util/byte_operators.h>
17#include <util/c_types.h>
18#include <util/format_expr.h>
19#include <util/format_type.h>
20#include <util/namespace.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.h>
28#include <util/xml.h>
29
30#include <ostream>
31
32#ifdef DEBUG
33#include <iostream>
34#include <util/format_expr.h>
35#include <util/format_type.h>
36#endif
37
38#include "add_failed_symbols.h"
39
40// Due to a large number of functions defined inline, `value_sett` and
41// associated types are documented in its header file, `value_set.h`.
42
45
46bool value_sett::field_sensitive(const irep_idt &id, const typet &type)
47{
48 // we always track fields on these
49 if(
50 id.starts_with("value_set::dynamic_object") ||
51 id == "value_set::return_value" || id == "value_set::memory")
52 return true;
53
54 // otherwise it has to be a struct
55 return type.id() == ID_struct || type.id() == ID_struct_tag;
56}
57
59{
60 auto found = values.find(id);
61 return !found.has_value() ? nullptr : &(found->get());
62}
63
65 const entryt &e,
66 const typet &type,
68 bool add_to_sets)
69{
70 irep_idt index;
71
72 if(field_sensitive(e.identifier, type))
73 index=id2string(e.identifier)+e.suffix;
74 else
75 index=e.identifier;
76
77 auto existing_entry = values.find(index);
78 if(existing_entry.has_value())
79 {
80 if(add_to_sets)
81 {
83 {
84 values.update(index, [&new_values, this](entryt &entry) {
86 });
87 }
88 }
89 else
90 {
92 index, [&new_values](entryt &entry) { entry.object_map = new_values; });
93 }
94 }
95 else
96 {
97 entryt new_entry = e;
98 new_entry.object_map = new_values;
99 values.insert(index, std::move(new_entry));
100 }
101}
102
104 const object_mapt &dest,
106 const offsett &offset) const
107{
108 auto entry=dest.read().find(n);
109
110 if(entry==dest.read().end())
111 {
112 // new
114 }
115 else if(!entry->second)
117 else if(offset && *entry->second == *offset)
119 else
121}
122
124 object_mapt &dest,
126 const offsett &offset) const
127{
128 auto insert_action = get_insert_action(dest, n, offset);
130 return false;
131
132 auto &new_offset = dest.write()[n];
134 new_offset = offset;
135 else
136 new_offset.reset();
137
138 return true;
139}
140
141void value_sett::output(std::ostream &out, const std::string &indent) const
142{
143 values.iterate([&](const irep_idt &, const entryt &e) {
144 irep_idt identifier, display_name;
145
146 if(e.identifier.starts_with("value_set::dynamic_object"))
147 {
148 display_name = id2string(e.identifier) + e.suffix;
149 identifier.clear();
150 }
151 else if(e.identifier == "value_set::return_value")
152 {
153 display_name = "RETURN_VALUE" + e.suffix;
154 identifier.clear();
155 }
156 else
157 {
158#if 0
159 const symbolt &symbol=ns.lookup(e.identifier);
160 display_name=id2string(symbol.display_name())+e.suffix;
161 identifier=symbol.name;
162#else
163 identifier = id2string(e.identifier);
164 display_name = id2string(identifier) + e.suffix;
165#endif
166 }
167
168 out << indent << display_name << " = { ";
169
170 const object_map_dt &object_map = e.object_map.read();
171
172 std::size_t width = 0;
173
174 for(object_map_dt::const_iterator o_it = object_map.begin();
175 o_it != object_map.end();
176 o_it++)
177 {
178 const exprt &o = object_numbering[o_it->first];
179
180 std::ostringstream stream;
181
182 if(o.id() == ID_invalid || o.id() == ID_unknown)
183 stream << format(o);
184 else
185 {
186 stream << "<" << format(o) << ", ";
187
188 if(o_it->second)
189 stream << *o_it->second;
190 else
191 stream << '*';
192
193 if(o.type().is_nil())
194 stream << ", ?";
195 else
196 stream << ", " << format(o.type());
197
198 stream << '>';
199 }
200
201 const std::string result = stream.str();
202 out << result;
203 width += result.size();
204
205 object_map_dt::const_iterator next(o_it);
206 next++;
207
208 if(next != object_map.end())
209 {
210 out << ", ";
211 if(width >= 40)
212 out << "\n" << std::string(indent.size(), ' ') << " ";
213 }
214 }
215
216 out << " } \n";
217 });
218}
219
221{
222 xmlt output;
223
225 this->values.get_view(view);
226
227 for(const auto &values_entry : view)
228 {
229 xmlt &var = output.new_element("variable");
230 var.new_element("identifier").data = id2string(values_entry.first);
231
232#if 0
233 const value_sett::expr_sett &expr_set=
234 value_entries.expr_set();
235
236 for(value_sett::expr_sett::const_iterator
237 e_it=expr_set.begin();
238 e_it!=expr_set.end();
239 e_it++)
240 {
241 std::string value_str=
242 from_expr(ns, identifier, *e_it);
243
244 var.new_element("value").data=
246 }
247#endif
248 }
249
250 return output;
251}
252
253exprt value_sett::to_expr(const object_map_dt::value_type &it) const
254{
255 const exprt &object=object_numbering[it.first];
256
257 if(object.id()==ID_invalid ||
258 object.id()==ID_unknown)
259 return object;
260
262
263 od.object()=object;
264
265 if(it.second)
266 od.offset() = from_integer(*it.second, c_index_type());
267
268 od.type()=od.object().type();
269
270 return std::move(od);
271}
272
274{
275 bool result=false;
276
278
279 new_values.get_delta_view(values, delta_view, false);
280
281 for(const auto &delta_entry : delta_view)
282 {
283 if(delta_entry.is_in_both_maps())
284 {
286 delta_entry.get_other_map_value().object_map,
287 delta_entry.m.object_map))
288 {
290 make_union(existing_entry.object_map, delta_entry.m.object_map);
291 });
292 result = true;
293 }
294 }
295 else
296 {
298 result = true;
299 }
300 }
301
302 return result;
303}
304
306 const object_mapt &dest,
307 const object_mapt &src) const
308{
309 for(const auto &number_and_offset : src.read())
310 {
311 if(
313 dest, number_and_offset.first, number_and_offset.second) !=
315 {
316 return true;
317 }
318 }
319
320 return false;
321}
322
323bool value_sett::make_union(object_mapt &dest, const object_mapt &src) const
324{
325 bool result=false;
326
327 for(object_map_dt::const_iterator it=src.read().begin();
328 it!=src.read().end();
329 it++)
330 {
331 if(insert(dest, *it))
332 result=true;
333 }
334
335 return result;
336}
337
339 exprt &expr,
340 const namespacet &ns) const
341{
342 bool mod=false;
343
344 if(expr.id()==ID_pointer_offset)
345 {
347 get_value_set(to_pointer_offset_expr(expr).pointer(), ns, true);
348
351
352 const object_map_dt &object_map=reference_set.read();
353 for(object_map_dt::const_iterator
354 it=object_map.begin();
355 it!=object_map.end();
356 it++)
357 if(!it->second)
358 return false;
359 else
360 {
361 const exprt &object=object_numbering[it->first];
362 auto ptr_offset = compute_pointer_offset(object, ns);
363
364 if(!ptr_offset.has_value())
365 return false;
366
367 *ptr_offset += *it->second;
368
370 return false;
371
374 mod=true;
375 }
376
377 if(mod)
378 expr.swap(new_expr);
379 }
380 else
381 {
382 Forall_operands(it, expr)
383 mod=eval_pointer_offset(*it, ns) || mod;
384 }
385
386 return mod;
387}
388
389std::vector<exprt>
391{
392 const object_mapt object_map = get_value_set(std::move(expr), ns, false);
393 return make_range(object_map.read())
394 .map([&](const object_map_dt::value_type &pair) { return to_expr(pair); });
395}
396
398 exprt expr,
399 const namespacet &ns,
400 bool is_simplified) const
401{
402 if(!is_simplified)
403 simplify(expr, ns);
404
405 object_mapt dest;
406 bool includes_nondet_pointer = false;
407 get_value_set_rec(expr, dest, includes_nondet_pointer, "", expr.type(), ns);
408
409 if(includes_nondet_pointer && expr.type().id() == ID_pointer)
410 {
411 // we'll take the union of all objects we see, with unspecified offsets
412 values.iterate([this, &dest](const irep_idt &key, const entryt &value) {
413 for(const auto &object : value.object_map.read())
414 insert(dest, object.first, offsett());
415 });
416
417 // we'll add null, in case it's not there yet
418 insert(
419 dest,
420 exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
421 offsett());
422 }
423
424 return dest;
425}
426
431 const std::string &suffix, const std::string &field)
432{
433 return
434 !suffix.empty() &&
435 suffix[0] == '.' &&
436 suffix.compare(1, field.length(), field) == 0 &&
437 (suffix.length() == field.length() + 1 ||
438 suffix[field.length() + 1] == '.' ||
439 suffix[field.length() + 1] == '[');
440}
441
443 const std::string &suffix, const std::string &field)
444{
445 INVARIANT(
447 "suffix should start with " + field);
448 return suffix.substr(field.length() + 1);
449}
450
451std::optional<irep_idt> value_sett::get_index_of_symbol(
452 irep_idt identifier,
453 const typet &type,
454 const std::string &suffix,
455 const namespacet &ns) const
456{
457 if(
458 type.id() != ID_pointer && type.id() != ID_signedbv &&
459 type.id() != ID_unsignedbv && type.id() != ID_array &&
460 type.id() != ID_struct && type.id() != ID_struct_tag &&
461 type.id() != ID_union && type.id() != ID_union_tag)
462 {
463 return {};
464 }
465
466 // look it up
467 irep_idt index = id2string(identifier) + suffix;
468 auto *entry = find_entry(index);
469 if(entry)
470 return std::move(index);
471
472 const typet &followed_type = type.id() == ID_struct_tag
474 : type.id() == ID_union_tag
475 ? ns.follow_tag(to_union_tag_type(type))
476 : type;
477
478 // try first component name as suffix if not yet found
479 if(followed_type.id() == ID_struct || followed_type.id() == ID_union)
480 {
483
484 if(!struct_union_type.components().empty())
485 {
487 struct_union_type.components().front().get_name();
488
489 index =
490 id2string(identifier) + "." + id2string(first_component_name) + suffix;
491 entry = find_entry(index);
492 if(entry)
493 return std::move(index);
494 }
495 }
496
497 // not found? try without suffix
498 entry = find_entry(identifier);
499 if(entry)
500 return std::move(identifier);
501
502 return {};
503}
504
506 const exprt &expr,
507 object_mapt &dest,
509 const std::string &suffix,
510 const typet &original_type,
511 const namespacet &ns) const
512{
513#ifdef DEBUG
514 std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr) << "\n";
515 std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
516#endif
517
518 if(expr.id()==ID_unknown || expr.id()==ID_invalid)
519 {
521 }
522 else if(expr.id()==ID_index)
523 {
524 const typet &type = to_index_expr(expr).array().type();
525
527 type.id() == ID_array, "operand 0 of index expression must be an array");
528
530 to_index_expr(expr).array(),
531 dest,
533 "[]" + suffix,
535 ns);
536 }
537 else if(expr.id()==ID_member)
538 {
539 const exprt &compound = to_member_expr(expr).compound();
540
542 compound.type().id() == ID_struct ||
543 compound.type().id() == ID_struct_tag ||
544 compound.type().id() == ID_union ||
545 compound.type().id() == ID_union_tag,
546 "compound of member expression must be struct or union");
547
548 const std::string &component_name=
550
552 compound,
553 dest,
555 "." + component_name + suffix,
557 ns);
558 }
559 else if(expr.id()==ID_symbol)
560 {
562 to_symbol_expr(expr).get_identifier(), expr.type(), suffix, ns);
563
564 if(entry_index.has_value())
565 make_union(dest, find_entry(*entry_index)->object_map);
566 else
568 }
569 else if(expr.id() == ID_nondet_symbol)
570 {
571 if(expr.type().id() == ID_pointer)
573 else
575 }
576 else if(expr.id()==ID_if)
577 {
579 to_if_expr(expr).true_case(),
580 dest,
582 suffix,
584 ns);
586 to_if_expr(expr).false_case(),
587 dest,
589 suffix,
591 ns);
592 }
593 else if(expr.id()==ID_address_of)
594 {
595 get_reference_set(to_address_of_expr(expr).object(), dest, ns);
596 }
597 else if(expr.id()==ID_dereference)
598 {
601 const object_map_dt &object_map=reference_set.read();
602
603 if(object_map.begin()==object_map.end())
605 else
606 {
607 for(object_map_dt::const_iterator
608 it1=object_map.begin();
609 it1!=object_map.end();
610 it1++)
611 {
614 const exprt object=object_numbering[it1->first];
616 object, dest, includes_nondet_pointer, suffix, original_type, ns);
617 }
618 }
619 }
620 else if(expr.is_constant())
621 {
622 // check if NULL
624 {
625 insert(
626 dest,
627 exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
628 mp_integer{0});
629 }
630 else if(
631 expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv)
632 {
633 // an integer constant got turned into a pointer
635 }
636 else
638 }
639 else if(expr.id()==ID_typecast)
640 {
641 // let's see what gets converted to what
642
643 const auto &op = to_typecast_expr(expr).op();
644 const typet &op_type = op.type();
645
646 if(op_type.id()==ID_pointer)
647 {
648 // pointer-to-something -- we just ignore the type cast
650 op, dest, includes_nondet_pointer, suffix, original_type, ns);
651 }
652 else if(
653 op_type.id() == ID_unsignedbv || op_type.id() == ID_signedbv ||
654 op_type.id() == ID_bv)
655 {
656 // integer-to-something
657
658 if(op.is_zero())
659 {
661 }
662 else
663 {
664 // see if we have something for the integer
666
668 op, tmp, includes_nondet_pointer, suffix, original_type, ns);
669
670 if(tmp.read().empty())
671 {
672 // if not, throw in integer
674 }
675 else if(tmp.read().size()==1 &&
676 object_numbering[tmp.read().begin()->first].id()==ID_unknown)
677 {
678 // if not, throw in integer
680 }
681 else
682 {
683 // use as is
684 dest.write().insert(tmp.read().begin(), tmp.read().end());
685 }
686 }
687 }
688 else
690 }
691 else if(
692 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_bitor ||
693 expr.id() == ID_bitand || expr.id() == ID_bitxor ||
694 expr.id() == ID_bitnand || expr.id() == ID_bitnor ||
695 expr.id() == ID_bitxnor)
696 {
697 if(expr.operands().size()<2)
698 throw expr.id_string()+" expected to have at least two operands";
699
701 std::optional<mp_integer> i;
702
703 // special case for plus/minus and exactly one pointer
704 std::optional<exprt> ptr_operand;
705 if(
706 expr.type().id() == ID_pointer &&
707 (expr.id() == ID_plus || expr.id() == ID_minus))
708 {
709 bool non_const_offset = false;
710 for(const auto &op : expr.operands())
711 {
712 if(op.type().id() == ID_pointer)
713 {
714 if(ptr_operand.has_value())
715 {
716 ptr_operand.reset();
717 break;
718 }
719
720 ptr_operand = op;
721 }
722 else if(!non_const_offset)
723 {
724 auto offset = numeric_cast<mp_integer>(op);
725 if(!offset.has_value())
726 {
727 i.reset();
728 non_const_offset = true;
729 }
730 else
731 {
732 if(!i.has_value())
733 i = mp_integer{0};
734 i = *i + *offset;
735 }
736 }
737 }
738
739 if(ptr_operand.has_value() && i.has_value())
740 {
742 to_pointer_type(ptr_operand->type()).base_type();
743 if(pointer_base_type.id() == ID_empty)
745
746 auto size = pointer_offset_size(pointer_base_type, ns);
747
748 if(!size.has_value() || (*size) == 0)
749 {
750 i.reset();
751 }
752 else
753 {
754 *i *= *size;
755
756 if(expr.id()==ID_minus)
757 {
759 to_minus_expr(expr).lhs() == *ptr_operand,
760 "unexpected subtraction of pointer from integer");
761 i->negate();
762 }
763 }
764 }
765 }
766
767 if(ptr_operand.has_value())
768 {
773 "",
774 ptr_operand->type(),
775 ns);
776 }
777 else
778 {
779 // we get the points-to for all operands, even integers
780 for(const auto &op : expr.operands())
781 {
783 op, pointer_expr_set, includes_nondet_pointer, "", op.type(), ns);
784 }
785 }
786
787 for(object_map_dt::const_iterator
788 it=pointer_expr_set.read().begin();
789 it!=pointer_expr_set.read().end();
790 it++)
791 {
792 offsett offset = it->second;
793
794 // adjust by offset
795 if(offset && i.has_value())
796 *offset += *i;
797 else
798 offset.reset();
799
800 insert(dest, it->first, offset);
801 }
802 }
803 else if(expr.id()==ID_mult)
804 {
805 // this is to do stuff like
806 // (int*)((sel*(ulong)&a)+((sel^0x1)*(ulong)&b))
807
808 if(expr.operands().size()<2)
809 throw expr.id_string()+" expected to have at least two operands";
810
812
813 // we get the points-to for all operands, even integers
814 for(const auto &op : expr.operands())
815 {
817 op, pointer_expr_set, includes_nondet_pointer, "", op.type(), ns);
818 }
819
820 for(object_map_dt::const_iterator
821 it=pointer_expr_set.read().begin();
822 it!=pointer_expr_set.read().end();
823 it++)
824 {
825 offsett offset = it->second;
826
827 // kill any offset
828 offset.reset();
829
830 insert(dest, it->first, offset);
831 }
832 }
833 else if(expr.id() == ID_lshr || expr.id() == ID_ashr || expr.id() == ID_shl)
834 {
836
839 binary_expr.op0(),
842 "",
843 binary_expr.op0().type(),
844 ns);
845
846 for(const auto &object_map_entry : pointer_expr_set.read())
847 {
848 offsett offset = object_map_entry.second;
849
850 // kill any offset
851 offset.reset();
852
853 insert(dest, object_map_entry.first, offset);
854 }
855 }
856 else if(expr.id()==ID_side_effect)
857 {
858 const irep_idt &statement = to_side_effect_expr(expr).get_statement();
859
860 if(statement==ID_function_call)
861 {
862 // these should be gone
863 throw "unexpected function_call sideeffect";
864 }
865 else if(statement==ID_allocate)
866 {
867 PRECONDITION(suffix.empty());
868
869 const typet &dynamic_type=
870 static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
871
873 dynamic_object.set_instance(location_number);
874 dynamic_object.valid()=true_exprt();
875
877 }
878 else if(statement==ID_cpp_new ||
879 statement==ID_cpp_new_array)
880 {
881 PRECONDITION(suffix.empty());
882 PRECONDITION(expr.type().id() == ID_pointer);
883
885 to_pointer_type(expr.type()).base_type());
886 dynamic_object.set_instance(location_number);
887 dynamic_object.valid()=true_exprt();
888
890 }
891 else
893 }
894 else if(expr.id()==ID_struct)
895 {
896 const auto &struct_components =
897 expr.type().id() == ID_struct_tag
898 ? ns.follow_tag(to_struct_tag_type(expr.type())).components()
899 : to_struct_type(expr.type()).components();
900 INVARIANT(
901 struct_components.size() == expr.operands().size(),
902 "struct expression should have an operand per component");
903 auto component_iter = struct_components.begin();
904 bool found_component = false;
905
906 // a struct constructor, which may contain addresses
907
908 for(const auto &op : expr.operands())
909 {
910 const std::string &component_name =
911 id2string(component_iter->get_name());
912 if(suffix_starts_with_field(suffix, component_name))
913 {
914 std::string remaining_suffix =
915 strip_first_field_from_suffix(suffix, component_name);
917 op,
918 dest,
922 ns);
923 found_component = true;
924 }
926 }
927
928 if(!found_component)
929 {
930 // Struct field doesn't appear as expected -- this has probably been
931 // cast from an incompatible type. Conservatively assume all fields may
932 // be of interest.
933 for(const auto &op : expr.operands())
934 {
936 op, dest, includes_nondet_pointer, suffix, original_type, ns);
937 }
938 }
939 }
940 else if(expr.id() == ID_union)
941 {
943 to_union_expr(expr).op(),
944 dest,
946 suffix,
948 ns);
949 }
950 else if(expr.id()==ID_with)
951 {
952 const with_exprt &with_expr = to_with_expr(expr);
953
954 // If the suffix is empty we're looking for the whole struct:
955 // default to combining both options as below.
956 if(
957 (expr.type().id() == ID_struct_tag || expr.type().id() == ID_struct) &&
958 !suffix.empty())
959 {
960 irep_idt component_name = with_expr.where().get(ID_component_name);
961 if(suffix_starts_with_field(suffix, id2string(component_name)))
962 {
963 // Looking for the member overwritten by this WITH expression
964 std::string remaining_suffix =
965 strip_first_field_from_suffix(suffix, id2string(component_name));
967 with_expr.new_value(),
968 dest,
972 ns);
973 }
974 else if(
975 (expr.type().id() == ID_struct &&
976 to_struct_type(expr.type()).has_component(component_name)) ||
977 (expr.type().id() == ID_struct_tag &&
979 .has_component(component_name)))
980 {
981 // Looking for a non-overwritten member, look through this expression
983 with_expr.old(),
984 dest,
986 suffix,
988 ns);
989 }
990 else
991 {
992 // Member we're looking for is not defined in this struct -- this
993 // must be a reinterpret cast of some sort. Default to conservatively
994 // assuming either operand might be involved.
996 with_expr.old(),
997 dest,
999 suffix,
1001 ns);
1003 with_expr.new_value(),
1004 dest,
1006 "",
1008 ns);
1009 }
1010 }
1011 else if(expr.type().id() == ID_array && !suffix.empty())
1012 {
1013 std::string new_value_suffix;
1014 if(has_prefix(suffix, "[]"))
1015 new_value_suffix = suffix.substr(2);
1016
1017 // Otherwise use a blank suffix on the assumption anything involved with
1018 // the new value might be interesting.
1019
1021 with_expr.old(),
1022 dest,
1024 suffix,
1026 ns);
1028 with_expr.new_value(),
1029 dest,
1033 ns);
1034 }
1035 else
1036 {
1037 // Something else-- the suffixes used here are a rough guess at best,
1038 // so this is imprecise.
1040 with_expr.old(),
1041 dest,
1043 suffix,
1045 ns);
1047 with_expr.new_value(),
1048 dest,
1050 "",
1052 ns);
1053 }
1054 }
1055 else if(expr.id()==ID_array)
1056 {
1057 // an array constructor, possibly containing addresses
1058 std::string new_suffix = suffix;
1059 if(has_prefix(suffix, "[]"))
1060 new_suffix = suffix.substr(2);
1061 // Otherwise we're probably reinterpreting some other type -- try persisting
1062 // with the current suffix for want of a better idea.
1063
1064 for(const auto &op : expr.operands())
1065 {
1068 }
1069 }
1070 else if(expr.id()==ID_array_of)
1071 {
1072 // an array constructor, possibly containing an address
1073 std::string new_suffix = suffix;
1074 if(has_prefix(suffix, "[]"))
1075 new_suffix = suffix.substr(2);
1076 // Otherwise we're probably reinterpreting some other type -- try persisting
1077 // with the current suffix for want of a better idea.
1078
1080 to_array_of_expr(expr).what(),
1081 dest,
1083 new_suffix,
1085 ns);
1086 }
1087 else if(expr.id()==ID_dynamic_object)
1088 {
1091
1092 const std::string prefix=
1093 "value_set::dynamic_object"+
1094 std::to_string(dynamic_object.get_instance());
1095
1096 // first try with suffix
1097 const std::string full_name=prefix+suffix;
1098
1099 // look it up
1100 const entryt *entry = find_entry(full_name);
1101
1102 // not found? try without suffix
1103 if(!entry)
1104 entry = find_entry(prefix);
1105
1106 if(!entry)
1108 else
1109 make_union(dest, entry->object_map);
1110 }
1111 else if(expr.id()==ID_byte_extract_little_endian ||
1113 {
1114 const auto &byte_extract_expr = to_byte_extract_expr(expr);
1115
1116 bool found=false;
1117
1118 if(
1119 byte_extract_expr.op().type().id() == ID_struct ||
1120 byte_extract_expr.op().type().id() == ID_struct_tag)
1121 {
1122 exprt offset = byte_extract_expr.offset();
1123 if(eval_pointer_offset(offset, ns))
1124 simplify(offset, ns);
1125
1126 const auto offset_int = numeric_cast<mp_integer>(offset);
1127 const auto type_size = pointer_offset_size(expr.type(), ns);
1128
1129 const struct_typet &struct_type =
1130 byte_extract_expr.op().type().id() == ID_struct_tag
1132 : to_struct_type(byte_extract_expr.op().type());
1133
1134 for(const auto &c : struct_type.components())
1135 {
1136 const irep_idt &name = c.get_name();
1137
1138 if(offset_int.has_value())
1139 {
1140 auto comp_offset = member_offset(struct_type, name, ns);
1141 if(comp_offset.has_value())
1142 {
1143 if(
1144 type_size.has_value() && *offset_int + *type_size <= *comp_offset)
1145 {
1146 break;
1147 }
1148
1149 auto member_size = pointer_offset_size(c.type(), ns);
1150 if(
1151 member_size.has_value() &&
1153 {
1154 continue;
1155 }
1156 }
1157 }
1158
1159 found=true;
1160
1161 member_exprt member(byte_extract_expr.op(), c);
1163 member, dest, includes_nondet_pointer, suffix, original_type, ns);
1164 }
1165 }
1166
1167 if(
1168 byte_extract_expr.op().type().id() == ID_union ||
1169 byte_extract_expr.op().type().id() == ID_union_tag)
1170 {
1171 // just collect them all
1172 const auto &components =
1173 byte_extract_expr.op().type().id() == ID_union_tag
1175 .components()
1176 : to_union_type(byte_extract_expr.op().type()).components();
1177 for(const auto &c : components)
1178 {
1179 const irep_idt &name = c.get_name();
1180 member_exprt member(byte_extract_expr.op(), name, c.type());
1182 member, dest, includes_nondet_pointer, suffix, original_type, ns);
1183 }
1184 }
1185
1186 if(!found)
1187 // we just pass through
1189 byte_extract_expr.op(),
1190 dest,
1192 suffix,
1194 ns);
1195 }
1196 else if(expr.id()==ID_byte_update_little_endian ||
1198 {
1199 const auto &byte_update_expr = to_byte_update_expr(expr);
1200
1201 // we just pass through
1203 byte_update_expr.op(),
1204 dest,
1206 suffix,
1208 ns);
1210 byte_update_expr.value(),
1211 dest,
1213 suffix,
1215 ns);
1216
1217 // we could have checked object size to be more precise
1218 }
1219 else if(expr.id() == ID_let)
1220 {
1221 const auto &let_expr = to_let_expr(expr);
1222 // This depends on copying `value_sett` being cheap -- which it is, because
1223 // our backing store is sharing_mapt.
1226 let_expr.symbol(), let_expr.value(), ns, false, false);
1227
1228 value_set_with_local_definition.get_value_set_rec(
1229 let_expr.where(),
1230 dest,
1232 suffix,
1234 ns);
1235 }
1236 else if(auto eb = expr_try_dynamic_cast<extractbits_exprt>(expr))
1237 {
1240 eb->src(),
1243 "",
1244 eb->src().type(),
1245 ns);
1246
1247 for(const auto &object_map_entry : pointer_expr_set.read())
1248 {
1249 offsett offset = object_map_entry.second;
1250
1251 // kill any offset
1252 offset.reset();
1253
1254 insert(dest, object_map_entry.first, offset);
1255 }
1256 }
1257 else
1258 {
1260 for(const auto &op : expr.operands())
1261 {
1264 }
1265
1266 for(const auto &object_map_entry : pointer_expr_set.read())
1267 {
1268 offsett offset = object_map_entry.second;
1269
1270 // kill any offset
1271 offset.reset();
1272
1273 insert(dest, object_map_entry.first, offset);
1274 }
1275
1276 if(pointer_expr_set.read().empty())
1278 }
1279
1280 #ifdef DEBUG
1281 std::cout << "GET_VALUE_SET_REC RESULT:\n";
1282 for(const auto &obj : dest.read())
1283 {
1284 const exprt &e=to_expr(obj);
1285 std::cout << " " << format(e) << "\n";
1286 }
1287 std::cout << "\n";
1288 #endif
1289}
1290
1292 const exprt &src,
1293 exprt &dest) const
1294{
1295 // remove pointer typecasts
1296 if(src.id()==ID_typecast)
1297 {
1298 PRECONDITION(src.type().id() == ID_pointer);
1299
1300 dereference_rec(to_typecast_expr(src).op(), dest);
1301 }
1302 else
1303 dest=src;
1304}
1305
1307 const exprt &expr,
1309 const namespacet &ns) const
1310{
1311 object_mapt object_map;
1312 get_reference_set(expr, object_map, ns);
1313
1314 for(object_map_dt::const_iterator
1315 it=object_map.read().begin();
1316 it!=object_map.read().end();
1317 it++)
1318 dest.push_back(to_expr(*it));
1319}
1320
1322 const exprt &expr,
1323 object_mapt &dest,
1324 const namespacet &ns) const
1325{
1326#ifdef DEBUG
1327 std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
1328 << '\n';
1329#endif
1330
1331 if(expr.id()==ID_symbol ||
1332 expr.id()==ID_dynamic_object ||
1333 expr.id()==ID_string_constant ||
1334 expr.id()==ID_array)
1335 {
1336 if(
1337 expr.type().id() == ID_array &&
1338 to_array_type(expr.type()).element_type().id() == ID_array)
1339 insert(dest, expr);
1340 else
1341 insert(dest, expr, mp_integer{0});
1342
1343 return;
1344 }
1345 else if(expr.id()==ID_dereference)
1346 {
1347 const auto &pointer = to_dereference_expr(expr).pointer();
1348
1349 bool includes_nondet_pointer = false;
1351 pointer, dest, includes_nondet_pointer, "", pointer.type(), ns);
1352
1353#ifdef DEBUG
1354 for(const auto &map_entry : dest.read())
1355 {
1356 std::cout << "VALUE_SET: " << format(object_numbering[map_entry.first])
1357 << '\n';
1358 }
1359#endif
1360
1361 return;
1362 }
1363 else if(expr.id()==ID_index)
1364 {
1365 if(expr.operands().size()!=2)
1366 throw "index expected to have two operands";
1367
1369 const exprt &array=index_expr.array();
1370 const exprt &offset=index_expr.index();
1371
1373 array.type().id() == ID_array, "index takes array-typed operand");
1374
1375 const auto &array_type = to_array_type(array.type());
1376
1379
1380 const object_map_dt &object_map=array_references.read();
1381
1382 for(object_map_dt::const_iterator
1383 a_it=object_map.begin();
1384 a_it!=object_map.end();
1385 a_it++)
1386 {
1387 const exprt &object=object_numbering[a_it->first];
1388
1389 if(object.id()==ID_unknown)
1390 insert(dest, exprt(ID_unknown, expr.type()));
1391 else
1392 {
1396
1397 offsett o = a_it->second;
1398 const auto i = numeric_cast<mp_integer>(offset);
1399
1400 if(offset.is_zero())
1401 {
1402 }
1403 else if(i.has_value() && o)
1404 {
1405 auto size = pointer_offset_size(array_type.element_type(), ns);
1406
1407 if(!size.has_value() || *size == 0)
1408 o.reset();
1409 else
1410 *o = *i * (*size);
1411 }
1412 else
1413 o.reset();
1414
1415 insert(dest, deref_index_expr, o);
1416 }
1417 }
1418
1419 return;
1420 }
1421 else if(expr.id()==ID_member)
1422 {
1423 const irep_idt &component_name=expr.get(ID_component_name);
1424
1425 const exprt &struct_op = to_member_expr(expr).compound();
1426
1428 get_reference_set(struct_op, struct_references, ns);
1429
1430 const object_map_dt &object_map=struct_references.read();
1431
1432 for(object_map_dt::const_iterator
1433 it=object_map.begin();
1434 it!=object_map.end();
1435 it++)
1436 {
1437 const exprt &object=object_numbering[it->first];
1438
1439 if(object.id()==ID_unknown)
1440 insert(dest, exprt(ID_unknown, expr.type()));
1441 else if(
1442 object.type().id() == ID_struct ||
1443 object.type().id() == ID_struct_tag || object.type().id() == ID_union ||
1444 object.type().id() == ID_union_tag)
1445 {
1446 offsett o = it->second;
1447
1448 member_exprt member_expr(object, component_name, expr.type());
1449
1450 // We cannot introduce a cast from scalar to non-scalar,
1451 // thus, we can only adjust the types of structs and unions.
1452
1453 if(
1454 object.type().id() == ID_struct ||
1455 object.type().id() == ID_struct_tag ||
1456 object.type().id() == ID_union || object.type().id() == ID_union_tag)
1457 {
1458 // adjust type?
1459 if(struct_op.type() != object.type())
1460 {
1461 member_expr.compound() =
1462 typecast_exprt(member_expr.compound(), struct_op.type());
1463 }
1464
1465 insert(dest, member_expr, o);
1466 }
1467 else
1468 insert(dest, exprt(ID_unknown, expr.type()));
1469 }
1470 else
1471 insert(dest, exprt(ID_unknown, expr.type()));
1472 }
1473
1474 return;
1475 }
1476 else if(expr.id()==ID_if)
1477 {
1478 get_reference_set_rec(to_if_expr(expr).true_case(), dest, ns);
1479 get_reference_set_rec(to_if_expr(expr).false_case(), dest, ns);
1480 return;
1481 }
1482
1483 insert(dest, exprt(ID_unknown, expr.type()));
1484}
1485
1487 const exprt &lhs,
1488 const exprt &rhs,
1489 const namespacet &ns,
1490 bool is_simplified,
1491 bool add_to_sets)
1492{
1493#ifdef DEBUG
1494 std::cout << "ASSIGN LHS: " << format(lhs) << " : "
1495 << format(lhs.type()) << '\n';
1496 std::cout << "ASSIGN RHS: " << format(rhs) << " : "
1497 << format(rhs.type()) << '\n';
1498 std::cout << "--------------------------------------------\n";
1499 output(std::cout);
1500#endif
1501
1502 if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
1503 {
1504 const auto &components =
1505 lhs.type().id() == ID_struct_tag
1506 ? ns.follow_tag(to_struct_tag_type(lhs.type())).components()
1507 : to_struct_type(lhs.type()).components();
1508
1509 for(const auto &c : components)
1510 {
1511 const typet &subtype = c.type();
1512 const irep_idt &name = c.get_name();
1513
1514 // ignore padding
1516 subtype.id() != ID_code, "struct member must not be of code type");
1517 if(c.get_is_padding())
1518 continue;
1519
1520 member_exprt lhs_member(lhs, name, subtype);
1521
1523
1524 if(rhs.id()==ID_unknown ||
1525 rhs.id()==ID_invalid)
1526 {
1527 // this branch is deemed dead as otherwise we'd be missing assignments
1528 // that never happened in this branch
1530 rhs_member=exprt(rhs.id(), subtype);
1531 }
1532 else
1533 {
1535 rhs.type() == lhs.type(),
1536 "value_sett::assign types should match, got: "
1537 "rhs.type():\n" +
1538 rhs.type().pretty() + "\n" + "lhs.type():\n" + lhs.type().pretty());
1539
1540 if(rhs.type().id() == ID_struct_tag || rhs.type().id() == ID_union_tag)
1541 {
1544
1545 const typet &rhs_subtype = rhs_struct_union_type.component_type(name);
1547
1549 }
1550 else if(rhs.type().id() == ID_struct || rhs.type().id() == ID_union)
1551 {
1554
1555 const typet &rhs_subtype = rhs_struct_union_type.component_type(name);
1557
1559 }
1560 }
1561 }
1562 }
1563 else if(lhs.type().id() == ID_array)
1564 {
1565 const index_exprt lhs_index(
1566 lhs,
1568 to_array_type(lhs.type()).element_type());
1569
1570 if(rhs.id()==ID_unknown ||
1571 rhs.id()==ID_invalid)
1572 {
1573 assign(
1574 lhs_index,
1575 exprt(rhs.id(), to_array_type(lhs.type()).element_type()),
1576 ns,
1578 add_to_sets);
1579 }
1580 else
1581 {
1583 rhs.type() == lhs.type(),
1584 "value_sett::assign types should match, got: "
1585 "rhs.type():\n" +
1586 rhs.type().pretty() + "\n" + "type:\n" + lhs.type().pretty());
1587
1588 if(rhs.id()==ID_array_of)
1589 {
1590 assign(
1591 lhs_index,
1592 to_array_of_expr(rhs).what(),
1593 ns,
1595 add_to_sets);
1596 }
1597 else if(rhs.id() == ID_array || rhs.is_constant())
1598 {
1599 for(const auto &op : rhs.operands())
1600 {
1602 add_to_sets=true;
1603 }
1604 }
1605 else if(rhs.id()==ID_with)
1606 {
1607 const index_exprt op0_index(
1608 to_with_expr(rhs).old(),
1610 to_array_type(lhs.type()).element_type());
1611
1613 assign(
1614 lhs_index, to_with_expr(rhs).new_value(), ns, is_simplified, true);
1615 }
1616 else
1617 {
1618 const index_exprt rhs_index(
1619 rhs,
1621 to_array_type(lhs.type()).element_type());
1623 }
1624 }
1625 }
1626 else
1627 {
1628 // basic type or union
1630
1631 // Permit custom subclass to alter the read values prior to write:
1633
1634 // Permit custom subclass to perform global side-effects prior to write:
1635 apply_assign_side_effects(lhs, rhs, ns);
1636
1637 assign_rec(lhs, values_rhs, "", ns, add_to_sets);
1638 }
1639}
1640
1642 const exprt &lhs,
1643 const object_mapt &values_rhs,
1644 const std::string &suffix,
1645 const namespacet &ns,
1646 bool add_to_sets)
1647{
1648#ifdef DEBUG
1649 std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
1650 std::cout << "ASSIGN_REC LHS ID: " << lhs.id() << '\n';
1651 std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1652
1653 for(object_map_dt::const_iterator it=values_rhs.read().begin();
1654 it!=values_rhs.read().end();
1655 it++)
1656 std::cout << "ASSIGN_REC RHS: " <<
1657 format(object_numbering[it->first]) << '\n';
1658 std::cout << '\n';
1659#endif
1660
1661 if(lhs.id()==ID_symbol)
1662 {
1663 const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
1664
1666 entryt{identifier, suffix}, lhs.type(), values_rhs, add_to_sets);
1667 }
1668 else if(lhs.id()==ID_dynamic_object)
1669 {
1672
1673 const std::string name=
1674 "value_set::dynamic_object"+
1675 std::to_string(dynamic_object.get_instance());
1676
1677 update_entry(entryt{name, suffix}, lhs.type(), values_rhs, true);
1678 }
1679 else if(lhs.id()==ID_dereference)
1680 {
1681 if(lhs.operands().size()!=1)
1682 throw lhs.id_string()+" expected to have one operand";
1683
1686
1687 if(reference_set.read().size()!=1)
1688 add_to_sets=true;
1689
1690 for(object_map_dt::const_iterator
1691 it=reference_set.read().begin();
1692 it!=reference_set.read().end();
1693 it++)
1694 {
1697 const exprt object=object_numbering[it->first];
1698
1699 if(object.id()!=ID_unknown)
1700 assign_rec(object, values_rhs, suffix, ns, add_to_sets);
1701 }
1702 }
1703 else if(lhs.id()==ID_index)
1704 {
1705 const auto &array = to_index_expr(lhs).array();
1706
1707 const typet &type = array.type();
1708
1710 type.id() == ID_array, "operand 0 of index expression must be an array");
1711
1712 assign_rec(array, values_rhs, "[]" + suffix, ns, true);
1713 }
1714 else if(lhs.id()==ID_member)
1715 {
1716 const auto &lhs_member_expr = to_member_expr(lhs);
1717 const auto &component_name = lhs_member_expr.get_component_name();
1718 const exprt &compound = lhs_member_expr.compound();
1719
1721 compound.type().id() == ID_struct ||
1722 compound.type().id() == ID_struct_tag ||
1723 compound.type().id() == ID_union ||
1724 compound.type().id() == ID_union_tag,
1725 "operand 0 of member expression must be struct or union");
1726
1727 assign_rec(
1728 compound,
1729 values_rhs,
1730 "." + id2string(component_name) + suffix,
1731 ns,
1732 add_to_sets);
1733 }
1734 else if(lhs.id()=="valid_object" ||
1735 lhs.id()=="dynamic_type" ||
1736 lhs.id()=="is_zero_string" ||
1737 lhs.id()=="zero_string" ||
1738 lhs.id()=="zero_string_length")
1739 {
1740 // we ignore this here
1741 }
1742 else if(lhs.id()==ID_string_constant)
1743 {
1744 // someone writes into a string-constant
1745 // evil guy
1746 }
1747 else if(lhs.id() == ID_null_object)
1748 {
1749 // evil as well
1750 }
1751 else if(lhs.id()==ID_typecast)
1752 {
1754
1755 assign_rec(typecast_expr.op(), values_rhs, suffix, ns, add_to_sets);
1756 }
1757 else if(lhs.id()==ID_byte_extract_little_endian ||
1759 {
1760 assign_rec(to_byte_extract_expr(lhs).op(), values_rhs, suffix, ns, true);
1761 }
1762 else if(lhs.id()==ID_integer_address)
1763 {
1764 // that's like assigning into __CPROVER_memory[...],
1765 // which we don't track
1766 }
1767 else
1768 throw "assign NYI: '" + lhs.id_string() + "'";
1769}
1770
1772 const irep_idt &function,
1773 const exprt::operandst &arguments,
1774 const namespacet &ns)
1775{
1776 const symbolt &symbol=ns.lookup(function);
1777
1778 const code_typet &type=to_code_type(symbol.type);
1780
1781 // these first need to be assigned to dummy, temporary arguments
1782 // and only thereafter to the actuals, in order
1783 // to avoid overwriting actuals that are needed for recursive
1784 // calls
1785
1786 for(std::size_t i=0; i<arguments.size(); i++)
1787 {
1788 const std::string identifier="value_set::dummy_arg_"+std::to_string(i);
1789 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1790 assign(dummy_lhs, arguments[i], ns, false, false);
1791 }
1792
1793 // now assign to 'actual actuals'
1794
1795 unsigned i=0;
1796
1797 for(code_typet::parameterst::const_iterator
1798 it=parameter_types.begin();
1799 it!=parameter_types.end();
1800 it++)
1801 {
1802 const irep_idt &identifier=it->get_identifier();
1803 if(identifier.empty())
1804 continue;
1805
1806 const exprt v_expr=
1807 symbol_exprt("value_set::dummy_arg_"+std::to_string(i), it->type());
1808
1809 const symbol_exprt actual_lhs(identifier, it->type());
1810 assign(actual_lhs, v_expr, ns, true, true);
1811 i++;
1812 }
1813
1814 // we could delete the dummy_arg_* now.
1815}
1816
1818 const exprt &lhs,
1819 const namespacet &ns)
1820{
1821 if(lhs.is_nil())
1822 return;
1823
1824 symbol_exprt rhs("value_set::return_value", lhs.type());
1825
1826 assign(lhs, rhs, ns, false, false);
1827}
1828
1830 const codet &code,
1831 const namespacet &ns)
1832{
1833 const irep_idt &statement=code.get_statement();
1834
1835 if(statement==ID_block)
1836 {
1837 for(const auto &op : code.operands())
1838 apply_code_rec(to_code(op), ns);
1839 }
1840 else if(statement==ID_function_call)
1841 {
1842 // shouldn't be here
1844 }
1845 else if(statement==ID_assign)
1846 {
1847 if(code.operands().size()!=2)
1848 throw "assignment expected to have two operands";
1849
1850 assign(code.op0(), code.op1(), ns, false, false);
1851 }
1852 else if(statement==ID_decl)
1853 {
1854 if(code.operands().size()!=1)
1855 throw "decl expected to have one operand";
1856
1857 const exprt &lhs=code.op0();
1858
1859 if(lhs.id()!=ID_symbol)
1860 throw "decl expected to have symbol on lhs";
1861
1862 const typet &lhs_type = lhs.type();
1863
1864 if(
1865 lhs_type.id() == ID_pointer ||
1866 (lhs_type.id() == ID_array &&
1867 to_array_type(lhs_type).element_type().id() == ID_pointer))
1868 {
1869 // assign the address of the failed object
1870 if(auto failed = get_failed_symbol(to_symbol_expr(lhs), ns))
1871 {
1873 assign(lhs, address_of_expr, ns, false, false);
1874 }
1875 else
1876 assign(lhs, exprt(ID_invalid), ns, false, false);
1877 }
1878 }
1879 else if(statement==ID_expression)
1880 {
1881 // can be ignored, we don't expect side effects here
1882 }
1883 else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array)
1884 {
1885 // does nothing
1886 }
1887 else if(statement=="lock" || statement=="unlock")
1888 {
1889 // ignore for now
1890 }
1891 else if(statement==ID_asm)
1892 {
1893 // ignore for now, probably not safe
1894 }
1895 else if(statement==ID_nondet)
1896 {
1897 // doesn't do anything
1898 }
1899 else if(statement==ID_printf)
1900 {
1901 // doesn't do anything
1902 }
1903 else if(statement==ID_return)
1904 {
1906 // this is turned into an assignment
1907 symbol_exprt lhs(
1908 "value_set::return_value", code_return.return_value().type());
1909 assign(lhs, code_return.return_value(), ns, false, false);
1910 }
1911 else if(statement==ID_array_set)
1912 {
1913 }
1914 else if(statement==ID_array_copy)
1915 {
1916 }
1917 else if(statement==ID_array_replace)
1918 {
1919 }
1920 else if(statement == ID_array_equal)
1921 {
1922 }
1923 else if(statement==ID_assume)
1924 {
1925 guard(to_code_assume(code).assumption(), ns);
1926 }
1927 else if(statement==ID_user_specified_predicate ||
1930 {
1931 // doesn't do anything
1932 }
1933 else if(statement==ID_fence)
1934 {
1935 }
1937 {
1938 // doesn't do anything
1939 }
1940 else if(statement==ID_dead)
1941 {
1942 // Ignore by default; could prune the value set.
1943 }
1944 else if(statement == ID_havoc_object)
1945 {
1946 }
1947 else
1948 {
1949 // std::cerr << code.pretty() << '\n';
1950 throw "value_sett: unexpected statement: "+id2string(statement);
1951 }
1952}
1953
1955 const exprt &expr,
1956 const namespacet &ns)
1957{
1958 if(expr.id()==ID_and)
1959 {
1960 for(const auto &op : expr.operands())
1961 guard(op, ns);
1962 }
1963 else if(expr.id()==ID_equal)
1964 {
1965 }
1966 else if(expr.id()==ID_notequal)
1967 {
1968 }
1969 else if(expr.id()==ID_not)
1970 {
1971 }
1972 else if(expr.id()==ID_dynamic_object)
1973 {
1975 // dynamic_object.instance()=
1976 // from_integer(location_number, typet(ID_natural));
1977 dynamic_object.valid()=true_exprt();
1978
1980 address_of.type() = to_dynamic_object_expr(expr).op0().type();
1981
1982 assign(to_dynamic_object_expr(expr).op0(), address_of, ns, false, false);
1983 }
1984}
1985
1987 const irep_idt &index,
1988 const std::unordered_set<exprt, irep_hash> &values_to_erase)
1989{
1990 if(values_to_erase.empty())
1991 return;
1992
1993 auto entry = find_entry(index);
1994 if(!entry)
1995 return;
1996
1997 std::vector<object_map_dt::key_type> keys_to_erase;
1998
1999 for(auto &key_value : entry->object_map.read())
2000 {
2001 const auto &rhs_object = to_expr(key_value);
2002 if(values_to_erase.count(rhs_object))
2003 {
2004 keys_to_erase.emplace_back(key_value.first);
2005 }
2006 }
2007
2009 keys_to_erase.size() == values_to_erase.size(),
2010 "value_sett::erase_value_from_entry() should erase exactly one value for "
2011 "each element in the set it is given");
2012
2013 entryt replacement = *entry;
2014 for(const auto &key_to_erase : keys_to_erase)
2015 {
2016 replacement.object_map.write().erase(key_to_erase);
2017 }
2018 values.replace(index, std::move(replacement));
2019}
2020
2023 const std::string &erase_prefix,
2024 const namespacet &ns)
2025{
2026 for(const auto &c : struct_union_type.components())
2027 {
2028 const typet &subtype = c.type();
2029 const irep_idt &name = c.get_name();
2030
2031 // ignore padding
2033 subtype.id() != ID_code, "struct/union member must not be of code type");
2034 if(c.get_is_padding())
2035 continue;
2036
2037 erase_symbol_rec(subtype, erase_prefix + "." + id2string(name), ns);
2038 }
2039}
2040
2042 const typet &type,
2043 const std::string &erase_prefix,
2044 const namespacet &ns)
2045{
2046 if(type.id() == ID_struct_tag)
2049 else if(type.id() == ID_union_tag)
2052 else if(type.id() == ID_array)
2054 to_array_type(type).element_type(), erase_prefix + "[]", ns);
2055 else if(values.has_key(erase_prefix))
2057}
2058
2060 const symbol_exprt &symbol_expr,
2061 const namespacet &ns)
2062{
2064 symbol_expr.type(), id2string(symbol_expr.get_identifier()), ns);
2065}
std::optional< 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)
API to expression classes for bitvectors.
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:127
bitvector_typet char_type()
Definition c_types.cpp:106
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:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A base class for binary expressions.
Definition std_expr.h:638
goto_instruction_codet representation of a "return from a function" statement.
Base type of functions.
Definition std_types.h:583
std::vector< parametert > parameterst
Definition std_types.h:586
const parameterst & parameters() const
Definition std_types.h:699
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
bool empty() const
Definition dstring.h:89
Representation of heap-allocated objects.
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
Array index operator.
Definition std_expr.h:1470
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const std::string & id_string() const
Definition irep.h:391
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
Extract member of struct or union.
Definition std_expr.h:2971
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
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().
Split an expression into a base object and a (byte) offset.
const T & read() const
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
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.
void erase(const key_type &k)
Erase element, element must exist in map.
bool has_key(const key_type &k) const
Check if key is in map.
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
std::optional< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
void update(const key_type &k, std::function< void(mapped_type &)> mutator)
Update an element in place; element must exist in map.
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
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
The Boolean constant true.
Definition std_expr.h:3190
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
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:44
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
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...
const entryt * find_entry(const irep_idt &id) const
Finds an entry in this value-set.
Definition value_set.cpp:58
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
virtual void get_value_set_rec(const exprt &expr, object_mapt &dest, bool &includes_nondet_pointer, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Subclass customisation point for recursion over RHS expression.
xmlt output_xml(void) const
Output the value set formatted as XML.
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
valuest values
Stores the LHS ID -> RHS expression set map.
Definition value_set.h:296
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
Definition value_set.h:73
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
Definition value_set.h:77
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:128
void erase_struct_union_symbol(const struct_union_typet &struct_union_type, const std::string &erase_prefix, const namespacet &ns)
std::optional< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
Definition value_set.h:81
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
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 ....
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.
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:64
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.
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:
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...
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
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:46
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
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.
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.
static const object_map_dt empty_object_map
Definition value_set.h:43
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...
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.
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:528
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:88
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:514
std::optional< 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.
void erase_symbol_rec(const typet &type, const std::string &erase_prefix, const namespacet &ns)
Operator to update elements in structs and arrays.
Definition std_expr.h:2598
Definition xml.h:21
xmlt & new_element(const std::string &key)
Definition xml.h:95
std::string data
Definition xml.h:39
static void escape(const std::string &s, std::ostream &out)
escaping for XML elements
Definition xml.cpp:79
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define Forall_operands(it, expr)
Definition expr.h:27
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
static format_containert< T > format(const T &o)
Definition format.h:37
const code_returnt & to_code_return(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Pointer Logic.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#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:1603
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3455
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1086
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1816
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2660
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
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:518
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition std_types.h:478
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
Represents a row of a value_sett.
Definition value_set.h:203
irep_idt identifier
Definition value_set.h:205
std::string suffix
Definition value_set.h:206
object_mapt object_map
Definition value_set.h:204
Symbol table entry.
static bool failed(bool error_indicator)
static std::string strip_first_field_from_suffix(const std::string &suffix, const std::string &field)
static bool suffix_starts_with_field(const std::string &suffix, const std::string &field)
Check if 'suffix' starts with 'field'.
Value Set.