cprover
Loading...
Searching...
No Matches
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/ssa_expr.h>
27#include <util/std_code.h>
28#include <util/symbol.h>
29#include <util/xml.h>
30
31#ifdef DEBUG
32# include <iostream>
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(
47 id.starts_with("value_set::dynamic_object") ||
48 id == "value_set::return_value" || id == "value_set::memory")
49 return true;
50
51 // otherwise it has to be a struct
52 return type.id() == ID_struct || type.id() == ID_struct_tag;
53}
54
56{
57 auto found = values.find(id);
58 return !found.has_value() ? nullptr : &(found->get());
59}
60
62 const entryt &e,
63 const typet &type,
64 const object_mapt &new_values,
65 bool add_to_sets)
66{
67 irep_idt index;
68
69 if(field_sensitive(e.identifier, type))
70 index=id2string(e.identifier)+e.suffix;
71 else
72 index=e.identifier;
73
74 auto existing_entry = values.find(index);
75 if(existing_entry.has_value())
76 {
77 if(add_to_sets)
78 {
79 if(make_union_would_change(existing_entry->get().object_map, new_values))
80 {
81 values.update(index, [&new_values, this](entryt &entry) {
82 make_union(entry.object_map, new_values);
83 });
84 }
85 }
86 else
87 {
88 values.update(
89 index, [&new_values](entryt &entry) { entry.object_map = new_values; });
90 }
91 }
92 else
93 {
94 entryt new_entry = e;
95 new_entry.object_map = new_values;
96 values.insert(index, std::move(new_entry));
97 }
98}
99
101 const object_mapt &dest,
103 const offsett &offset) const
104{
105 auto entry=dest.read().find(n);
106
107 if(entry==dest.read().end())
108 {
109 // new
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(e.identifier.starts_with("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 << format(*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
218{
219 xmlt output;
220
222 this->values.get_view(view);
223
224 for(const auto &values_entry : view)
225 {
226 xmlt &var = output.new_element("variable");
227 var.new_element("identifier").data = id2string(values_entry.first);
228
229#if 0
230 const value_sett::expr_sett &expr_set=
231 value_entries.expr_set();
232
233 for(value_sett::expr_sett::const_iterator
234 e_it=expr_set.begin();
235 e_it!=expr_set.end();
236 e_it++)
237 {
238 std::string value_str=
239 from_expr(ns, identifier, *e_it);
240
241 var.new_element("value").data=
242 xmlt::escape(value_str);
243 }
244#endif
245 }
246
247 return output;
248}
249
250exprt value_sett::to_expr(const object_map_dt::value_type &it) const
251{
252 const exprt &object=object_numbering[it.first];
253
254 if(object.id()==ID_invalid ||
255 object.id()==ID_unknown)
256 return object;
257
259
260 od.object()=object;
261
262 if(it.second)
263 od.offset() = *it.second;
264
265 od.type()=od.object().type();
266
267 return std::move(od);
268}
269
271{
272 bool result=false;
273
275
276 new_values.get_delta_view(values, delta_view, false);
277
278 for(const auto &delta_entry : delta_view)
279 {
280 if(delta_entry.is_in_both_maps())
281 {
283 delta_entry.get_other_map_value().object_map,
284 delta_entry.m.object_map))
285 {
286 values.update(delta_entry.k, [&](entryt &existing_entry) {
287 make_union(existing_entry.object_map, delta_entry.m.object_map);
288 });
289 result = true;
290 }
291 }
292 else
293 {
294 values.insert(delta_entry.k, delta_entry.m);
295 result = true;
296 }
297 }
298
299 return result;
300}
301
303 const object_mapt &dest,
304 const object_mapt &src) const
305{
306 for(const auto &number_and_offset : src.read())
307 {
308 if(
310 dest, number_and_offset.first, number_and_offset.second) !=
312 {
313 return true;
314 }
315 }
316
317 return false;
318}
319
320bool value_sett::make_union(object_mapt &dest, const object_mapt &src) const
321{
322 bool result=false;
323
324 for(object_map_dt::const_iterator it=src.read().begin();
325 it!=src.read().end();
326 it++)
327 {
328 if(insert(dest, *it))
329 result=true;
330 }
331
332 return result;
333}
334
336 exprt &expr,
337 const namespacet &ns) const
338{
339 bool mod=false;
340
341 if(expr.id()==ID_pointer_offset)
342 {
343 const object_mapt reference_set =
344 get_value_set(to_pointer_offset_expr(expr).pointer(), ns, true);
345
346 exprt new_expr;
347 mp_integer previous_offset=0;
348
349 const object_map_dt &object_map=reference_set.read();
350 for(object_map_dt::const_iterator
351 it=object_map.begin();
352 it!=object_map.end();
353 it++)
354 {
355 if(!it->second || !it->second->is_constant())
356 return false;
357 else
358 {
359 const exprt &object=object_numbering[it->first];
360 auto ptr_offset = compute_pointer_offset(object, ns);
361
362 if(!ptr_offset.has_value())
363 return false;
364
365 *ptr_offset +=
367
368 if(mod && *ptr_offset != previous_offset)
369 return false;
370
371 new_expr = from_integer(*ptr_offset, expr.type());
372 previous_offset = *ptr_offset;
373 mod=true;
374 }
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(
446 suffix_starts_with_field(suffix, field),
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 {
481 const struct_union_typet &struct_union_type =
482 to_struct_union_type(followed_type);
483
484 if(!struct_union_type.components().empty())
485 {
486 const irep_idt &first_component_name =
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,
508 bool &includes_nondet_pointer,
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 {
520 insert(dest, exprt(ID_unknown, original_type));
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,
532 includes_nondet_pointer,
533 "[]" + suffix,
534 original_type,
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=
549 expr.get_string(ID_component_name);
550
552 compound,
553 dest,
554 includes_nondet_pointer,
555 "." + component_name + suffix,
556 original_type,
557 ns);
558 }
559 else if(expr.id()==ID_symbol)
560 {
561 const symbol_exprt expr_l1 = is_ssa_expr(expr)
563 : to_symbol_expr(expr);
564 auto entry_index =
565 get_index_of_symbol(expr_l1.get_identifier(), expr.type(), suffix, ns);
566
567 if(entry_index.has_value())
568 make_union(dest, find_entry(*entry_index)->object_map);
569 else
570 insert(dest, exprt(ID_unknown, original_type));
571 }
572 else if(expr.id() == ID_nondet_symbol)
573 {
574 if(expr.type().id() == ID_pointer)
575 includes_nondet_pointer = true;
576 else
577 insert(dest, exprt(ID_unknown, original_type));
578 }
579 else if(expr.id()==ID_if)
580 {
582 to_if_expr(expr).true_case(),
583 dest,
584 includes_nondet_pointer,
585 suffix,
586 original_type,
587 ns);
589 to_if_expr(expr).false_case(),
590 dest,
591 includes_nondet_pointer,
592 suffix,
593 original_type,
594 ns);
595 }
596 else if(expr.id()==ID_address_of)
597 {
598 get_reference_set(to_address_of_expr(expr).object(), dest, ns);
599 }
600 else if(expr.id()==ID_dereference)
601 {
602 object_mapt reference_set;
603 get_reference_set(expr, reference_set, ns);
604 const object_map_dt &object_map=reference_set.read();
605
606 if(object_map.begin()==object_map.end())
607 insert(dest, exprt(ID_unknown, original_type));
608 else
609 {
610 for(object_map_dt::const_iterator
611 it1=object_map.begin();
612 it1!=object_map.end();
613 it1++)
614 {
617 const exprt object=object_numbering[it1->first];
619 object, dest, includes_nondet_pointer, suffix, original_type, ns);
620 }
621 }
622 }
623 else if(expr.is_constant())
624 {
625 // check if NULL
626 if(to_constant_expr(expr).is_null_pointer())
627 {
628 insert(
629 dest,
630 exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
632 }
633 else if(
634 expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv)
635 {
636 // an integer constant got turned into a pointer
637 insert(dest, exprt(ID_integer_address, unsigned_char_type()));
638 }
639 else
640 insert(dest, exprt(ID_unknown, original_type));
641 }
642 else if(expr.id()==ID_typecast)
643 {
644 // let's see what gets converted to what
645
646 const auto &op = to_typecast_expr(expr).op();
647 const typet &op_type = op.type();
648
649 if(op_type.id()==ID_pointer)
650 {
651 // pointer-to-something -- we just ignore the type cast
653 op, dest, includes_nondet_pointer, suffix, original_type, ns);
654 }
655 else if(
656 op_type.id() == ID_unsignedbv || op_type.id() == ID_signedbv ||
657 op_type.id() == ID_bv)
658 {
659 // integer-to-something
660
661 if(op.is_zero())
662 {
663 insert(
664 dest,
665 exprt(ID_null_object, empty_typet{}),
667 }
668 else
669 {
670 // see if we have something for the integer
671 object_mapt tmp;
672
674 op, tmp, includes_nondet_pointer, suffix, original_type, ns);
675
676 if(tmp.read().empty())
677 {
678 // if not, throw in integer
679 insert(dest, exprt(ID_integer_address, unsigned_char_type()));
680 }
681 else if(tmp.read().size()==1 &&
682 object_numbering[tmp.read().begin()->first].id()==ID_unknown)
683 {
684 // if not, throw in integer
685 insert(dest, exprt(ID_integer_address, unsigned_char_type()));
686 }
687 else
688 {
689 // use as is
690 dest.write().insert(tmp.read().begin(), tmp.read().end());
691 }
692 }
693 }
694 else
695 insert(dest, exprt(ID_unknown, original_type));
696 }
697 else if(
698 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_bitor ||
699 expr.id() == ID_bitand || expr.id() == ID_bitxor ||
700 expr.id() == ID_bitnand || expr.id() == ID_bitnor ||
701 expr.id() == ID_bitxnor)
702 {
704 expr.operands().size() >= 2,
705 expr.id_string() + " expected to have at least two operands");
706
707 object_mapt pointer_expr_set;
708 std::optional<exprt> additional_offset;
709
710 // special case for plus/minus and exactly one pointer
711 std::optional<exprt> ptr_operand;
712 if(
713 expr.type().id() == ID_pointer &&
714 (expr.id() == ID_plus || expr.id() == ID_minus))
715 {
716 for(const auto &op : expr.operands())
717 {
718 if(op.type().id() == ID_pointer)
719 {
720 if(ptr_operand.has_value())
721 {
722 ptr_operand.reset();
723 break;
724 }
725
726 ptr_operand = op;
727 }
728 else
729 {
730 if(!additional_offset.has_value())
731 additional_offset = op;
732 else
733 {
734 additional_offset = plus_exprt{
735 *additional_offset,
736 typecast_exprt::conditional_cast(op, additional_offset->type())};
737 }
738 }
739 }
740
741 if(ptr_operand.has_value() && additional_offset.has_value())
742 {
743 typet pointer_base_type =
744 to_pointer_type(ptr_operand->type()).base_type();
745 if(pointer_base_type.id() == ID_empty)
746 pointer_base_type = char_type();
747
748 auto size = pointer_offset_size(pointer_base_type, ns);
749
750 if(!size.has_value() || (*size) == 0)
751 {
752 additional_offset.reset();
753 }
754 else
755 {
756 additional_offset = mult_exprt{
757 *additional_offset, from_integer(*size, additional_offset->type())};
758
759 if(expr.id()==ID_minus)
760 {
762 to_minus_expr(expr).lhs() == *ptr_operand,
763 "unexpected subtraction of pointer from integer");
765 additional_offset->type().id() != ID_unsignedbv,
766 "offset type must support negation");
767 additional_offset = unary_minus_exprt{*additional_offset};
768 }
769 }
770 }
771 }
772
773 if(ptr_operand.has_value())
774 {
776 *ptr_operand,
777 pointer_expr_set,
778 includes_nondet_pointer,
779 "",
780 ptr_operand->type(),
781 ns);
782 }
783 else
784 {
785 // we get the points-to for all operands, even integers
786 for(const auto &op : expr.operands())
787 {
789 op, pointer_expr_set, includes_nondet_pointer, "", op.type(), ns);
790 }
791 }
792
793 for(object_map_dt::const_iterator
794 it=pointer_expr_set.read().begin();
795 it!=pointer_expr_set.read().end();
796 it++)
797 {
798 offsett offset = it->second;
799
800 // adjust by offset
801 if(offset && additional_offset.has_value())
802 {
803 offset = simplify_expr(
805 *offset,
807 *additional_offset, offset->type())},
808 ns);
809 }
810 else
811 offset.reset();
812
813 insert(dest, it->first, offset);
814 }
815 }
816 else if(expr.id()==ID_mult)
817 {
818 // this is to do stuff like
819 // (int*)((sel*(ulong)&a)+((sel^0x1)*(ulong)&b))
820
822 expr.operands().size() >= 2,
823 expr.id_string() + " expected to have at least two operands");
824
825 object_mapt pointer_expr_set;
826
827 // we get the points-to for all operands, even integers
828 for(const auto &op : expr.operands())
829 {
831 op, pointer_expr_set, includes_nondet_pointer, "", op.type(), ns);
832 }
833
834 for(object_map_dt::const_iterator
835 it=pointer_expr_set.read().begin();
836 it!=pointer_expr_set.read().end();
837 it++)
838 {
839 offsett offset = it->second;
840
841 // kill any offset
842 offset.reset();
843
844 insert(dest, it->first, offset);
845 }
846 }
847 else if(expr.id() == ID_lshr || expr.id() == ID_ashr || expr.id() == ID_shl)
848 {
849 const binary_exprt &binary_expr = to_binary_expr(expr);
850
851 object_mapt pointer_expr_set;
853 binary_expr.op0(),
854 pointer_expr_set,
855 includes_nondet_pointer,
856 "",
857 binary_expr.op0().type(),
858 ns);
859
860 for(const auto &object_map_entry : pointer_expr_set.read())
861 {
862 offsett offset = object_map_entry.second;
863
864 // kill any offset
865 offset.reset();
866
867 insert(dest, object_map_entry.first, offset);
868 }
869 }
870 else if(expr.id()==ID_side_effect)
871 {
872 const irep_idt &statement = to_side_effect_expr(expr).get_statement();
873
874 if(statement==ID_function_call)
875 {
876 // these should be gone
878 }
879 else if(statement==ID_allocate)
880 {
881 PRECONDITION(suffix.empty());
882
883 const typet &dynamic_type=
884 static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
885
886 dynamic_object_exprt dynamic_object(dynamic_type);
887 dynamic_object.set_instance(location_number);
888 dynamic_object.valid()=true_exprt();
889
890 insert(dest, dynamic_object, from_integer(0, c_index_type()));
891 }
892 else if(statement==ID_cpp_new ||
893 statement==ID_cpp_new_array)
894 {
895 // this is rewritten in the front-end, should be gone
897 PRECONDITION(suffix.empty());
898 PRECONDITION(expr.type().id() == ID_pointer);
899
900 dynamic_object_exprt dynamic_object(
901 to_pointer_type(expr.type()).base_type());
902 dynamic_object.set_instance(location_number);
903 dynamic_object.valid()=true_exprt();
904
905 insert(dest, dynamic_object, from_integer(0, c_index_type()));
906 }
907 else
908 insert(dest, exprt(ID_unknown, original_type));
909 }
910 else if(expr.id()==ID_struct)
911 {
912 const auto &struct_components =
913 expr.type().id() == ID_struct_tag
915 : to_struct_type(expr.type()).components();
916 INVARIANT(
917 struct_components.size() == expr.operands().size(),
918 "struct expression should have an operand per component");
919 auto component_iter = struct_components.begin();
920 bool found_component = false;
921
922 // a struct constructor, which may contain addresses
923
924 for(const auto &op : expr.operands())
925 {
926 const std::string &component_name =
927 id2string(component_iter->get_name());
928 if(suffix_starts_with_field(suffix, component_name))
929 {
930 std::string remaining_suffix =
931 strip_first_field_from_suffix(suffix, component_name);
933 op,
934 dest,
935 includes_nondet_pointer,
936 remaining_suffix,
937 original_type,
938 ns);
939 found_component = true;
940 }
941 ++component_iter;
942 }
943
944 if(!found_component)
945 {
946 // Struct field doesn't appear as expected -- this has probably been
947 // cast from an incompatible type. Conservatively assume all fields may
948 // be of interest.
949 for(const auto &op : expr.operands())
950 {
952 op, dest, includes_nondet_pointer, suffix, original_type, ns);
953 }
954 }
955 }
956 else if(expr.id() == ID_union)
957 {
959 to_union_expr(expr).op(),
960 dest,
961 includes_nondet_pointer,
962 suffix,
963 original_type,
964 ns);
965 }
966 else if(expr.id()==ID_with)
967 {
968 const with_exprt &with_expr = to_with_expr(expr);
969
970 // If the suffix is empty we're looking for the whole struct:
971 // default to combining both options as below.
972 if(
973 (expr.type().id() == ID_struct_tag || expr.type().id() == ID_struct) &&
974 !suffix.empty())
975 {
976 irep_idt component_name = with_expr.where().get(ID_component_name);
977 if(suffix_starts_with_field(suffix, id2string(component_name)))
978 {
979 // Looking for the member overwritten by this WITH expression
980 std::string remaining_suffix =
981 strip_first_field_from_suffix(suffix, id2string(component_name));
983 with_expr.new_value(),
984 dest,
985 includes_nondet_pointer,
986 remaining_suffix,
987 original_type,
988 ns);
989 }
990 else if(
991 (expr.type().id() == ID_struct &&
992 to_struct_type(expr.type()).has_component(component_name)) ||
993 (expr.type().id() == ID_struct_tag &&
995 .has_component(component_name)))
996 {
997 // Looking for a non-overwritten member, look through this expression
999 with_expr.old(),
1000 dest,
1001 includes_nondet_pointer,
1002 suffix,
1003 original_type,
1004 ns);
1005 }
1006 else
1007 {
1008 // Member we're looking for is not defined in this struct -- this
1009 // must be a reinterpret cast of some sort. Default to conservatively
1010 // assuming either operand might be involved.
1012 with_expr.old(),
1013 dest,
1014 includes_nondet_pointer,
1015 suffix,
1016 original_type,
1017 ns);
1019 with_expr.new_value(),
1020 dest,
1021 includes_nondet_pointer,
1022 "",
1023 original_type,
1024 ns);
1025 }
1026 }
1027 else if(expr.type().id() == ID_array && !suffix.empty())
1028 {
1029 std::string new_value_suffix;
1030 if(has_prefix(suffix, "[]"))
1031 new_value_suffix = suffix.substr(2);
1032
1033 // Otherwise use a blank suffix on the assumption anything involved with
1034 // the new value might be interesting.
1035
1037 with_expr.old(),
1038 dest,
1039 includes_nondet_pointer,
1040 suffix,
1041 original_type,
1042 ns);
1044 with_expr.new_value(),
1045 dest,
1046 includes_nondet_pointer,
1047 new_value_suffix,
1048 original_type,
1049 ns);
1050 }
1051 else
1052 {
1053 // Something else-- the suffixes used here are a rough guess at best,
1054 // so this is imprecise.
1056 with_expr.old(),
1057 dest,
1058 includes_nondet_pointer,
1059 suffix,
1060 original_type,
1061 ns);
1063 with_expr.new_value(),
1064 dest,
1065 includes_nondet_pointer,
1066 "",
1067 original_type,
1068 ns);
1069 }
1070 }
1071 else if(expr.id()==ID_array)
1072 {
1073 // an array constructor, possibly containing addresses
1074 std::string new_suffix = suffix;
1075 if(has_prefix(suffix, "[]"))
1076 new_suffix = suffix.substr(2);
1077 // Otherwise we're probably reinterpreting some other type -- try persisting
1078 // with the current suffix for want of a better idea.
1079
1080 for(const auto &op : expr.operands())
1081 {
1083 op, dest, includes_nondet_pointer, new_suffix, original_type, ns);
1084 }
1085 }
1086 else if(expr.id()==ID_array_of)
1087 {
1088 // an array constructor, possibly containing an address
1089 std::string new_suffix = suffix;
1090 if(has_prefix(suffix, "[]"))
1091 new_suffix = suffix.substr(2);
1092 // Otherwise we're probably reinterpreting some other type -- try persisting
1093 // with the current suffix for want of a better idea.
1094
1096 to_array_of_expr(expr).what(),
1097 dest,
1098 includes_nondet_pointer,
1099 new_suffix,
1100 original_type,
1101 ns);
1102 }
1103 else if(expr.id()==ID_dynamic_object)
1104 {
1105 const dynamic_object_exprt &dynamic_object=
1107
1108 const std::string prefix=
1109 "value_set::dynamic_object"+
1110 std::to_string(dynamic_object.get_instance());
1111
1112 // first try with suffix
1113 const std::string full_name=prefix+suffix;
1114
1115 // look it up
1116 const entryt *entry = find_entry(full_name);
1117
1118 // not found? try without suffix
1119 if(!entry)
1120 entry = find_entry(prefix);
1121
1122 if(!entry)
1123 insert(dest, exprt(ID_unknown, original_type));
1124 else
1125 make_union(dest, entry->object_map);
1126 }
1127 else if(expr.id()==ID_byte_extract_little_endian ||
1128 expr.id()==ID_byte_extract_big_endian)
1129 {
1130 const auto &byte_extract_expr = to_byte_extract_expr(expr);
1131
1132 bool found=false;
1133
1134 if(
1135 byte_extract_expr.op().type().id() == ID_struct ||
1136 byte_extract_expr.op().type().id() == ID_struct_tag)
1137 {
1138 exprt offset = byte_extract_expr.offset();
1139 if(eval_pointer_offset(offset, ns))
1140 simplify(offset, ns);
1141
1142 const auto offset_int = numeric_cast<mp_integer>(offset);
1143 const auto type_size = pointer_offset_size(expr.type(), ns);
1144
1145 const struct_typet &struct_type =
1146 byte_extract_expr.op().type().id() == ID_struct_tag
1147 ? ns.follow_tag(to_struct_tag_type(byte_extract_expr.op().type()))
1148 : to_struct_type(byte_extract_expr.op().type());
1149
1150 for(const auto &c : struct_type.components())
1151 {
1152 const irep_idt &name = c.get_name();
1153
1154 if(offset_int.has_value())
1155 {
1156 auto comp_offset = member_offset(struct_type, name, ns);
1157 if(comp_offset.has_value())
1158 {
1159 if(
1160 type_size.has_value() && *offset_int + *type_size <= *comp_offset)
1161 {
1162 break;
1163 }
1164
1165 auto member_size = pointer_offset_size(c.type(), ns);
1166 if(
1167 member_size.has_value() &&
1168 *offset_int >= *comp_offset + *member_size)
1169 {
1170 continue;
1171 }
1172 }
1173 }
1174
1175 found=true;
1176
1177 member_exprt member(byte_extract_expr.op(), c);
1179 member, dest, includes_nondet_pointer, suffix, original_type, ns);
1180 }
1181 }
1182
1183 if(
1184 byte_extract_expr.op().type().id() == ID_union ||
1185 byte_extract_expr.op().type().id() == ID_union_tag)
1186 {
1187 // just collect them all
1188 const auto &components =
1189 byte_extract_expr.op().type().id() == ID_union_tag
1190 ? ns.follow_tag(to_union_tag_type(byte_extract_expr.op().type()))
1191 .components()
1192 : to_union_type(byte_extract_expr.op().type()).components();
1193 for(const auto &c : components)
1194 {
1195 const irep_idt &name = c.get_name();
1196 member_exprt member(byte_extract_expr.op(), name, c.type());
1198 member, dest, includes_nondet_pointer, suffix, original_type, ns);
1199 }
1200 }
1201
1202 if(!found)
1203 // we just pass through
1205 byte_extract_expr.op(),
1206 dest,
1207 includes_nondet_pointer,
1208 suffix,
1209 original_type,
1210 ns);
1211 }
1212 else if(expr.id()==ID_byte_update_little_endian ||
1213 expr.id()==ID_byte_update_big_endian)
1214 {
1215 const auto &byte_update_expr = to_byte_update_expr(expr);
1216
1217 // we just pass through
1219 byte_update_expr.op(),
1220 dest,
1221 includes_nondet_pointer,
1222 suffix,
1223 original_type,
1224 ns);
1226 byte_update_expr.value(),
1227 dest,
1228 includes_nondet_pointer,
1229 suffix,
1230 original_type,
1231 ns);
1232
1233 // we could have checked object size to be more precise
1234 }
1235 else if(expr.id() == ID_let)
1236 {
1237 const auto &let_expr = to_let_expr(expr);
1238 // This depends on copying `value_sett` being cheap -- which it is, because
1239 // our backing store is sharing_mapt.
1240 value_sett value_set_with_local_definition = *this;
1241 value_set_with_local_definition.assign(
1242 let_expr.symbol(), let_expr.value(), ns, false, false);
1243
1244 value_set_with_local_definition.get_value_set_rec(
1245 let_expr.where(),
1246 dest,
1247 includes_nondet_pointer,
1248 suffix,
1249 original_type,
1250 ns);
1251 }
1252 else if(auto eb = expr_try_dynamic_cast<extractbits_exprt>(expr))
1253 {
1254 object_mapt pointer_expr_set;
1256 eb->src(),
1257 pointer_expr_set,
1258 includes_nondet_pointer,
1259 "",
1260 eb->src().type(),
1261 ns);
1262
1263 for(const auto &object_map_entry : pointer_expr_set.read())
1264 {
1265 offsett offset = object_map_entry.second;
1266
1267 // kill any offset
1268 offset.reset();
1269
1270 insert(dest, object_map_entry.first, offset);
1271 }
1272 }
1273 else
1274 {
1275 object_mapt pointer_expr_set;
1276 for(const auto &op : expr.operands())
1277 {
1279 op, pointer_expr_set, includes_nondet_pointer, "", original_type, ns);
1280 }
1281
1282 for(const auto &object_map_entry : pointer_expr_set.read())
1283 {
1284 offsett offset = object_map_entry.second;
1285
1286 // kill any offset
1287 offset.reset();
1288
1289 insert(dest, object_map_entry.first, offset);
1290 }
1291
1292 if(pointer_expr_set.read().empty())
1293 insert(dest, exprt(ID_unknown, original_type));
1294 }
1295
1296 #ifdef DEBUG
1297 std::cout << "GET_VALUE_SET_REC RESULT:\n";
1298 for(const auto &obj : dest.read())
1299 {
1300 const exprt &e=to_expr(obj);
1301 std::cout << " " << format(e) << "\n";
1302 }
1303 std::cout << "\n";
1304 #endif
1305}
1306
1308 const exprt &src,
1309 exprt &dest) const
1310{
1311 // remove pointer typecasts
1312 if(src.id()==ID_typecast)
1313 {
1314 PRECONDITION(src.type().id() == ID_pointer);
1315
1316 dereference_rec(to_typecast_expr(src).op(), dest);
1317 }
1318 else
1319 dest=src;
1320}
1321
1323 const exprt &expr,
1325 const namespacet &ns) const
1326{
1327 object_mapt object_map;
1328 get_reference_set(expr, object_map, ns);
1329
1330 for(object_map_dt::const_iterator
1331 it=object_map.read().begin();
1332 it!=object_map.read().end();
1333 it++)
1334 dest.push_back(to_expr(*it));
1335}
1336
1338 const exprt &expr,
1339 object_mapt &dest,
1340 const namespacet &ns) const
1341{
1342#ifdef DEBUG
1343 std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
1344 << '\n';
1345#endif
1346
1347 if(expr.id()==ID_symbol ||
1348 expr.id()==ID_dynamic_object ||
1349 expr.id()==ID_string_constant ||
1350 expr.id()==ID_array)
1351 {
1352 exprt l1_expr =
1353 is_ssa_expr(expr) ? remove_level_2(to_ssa_expr(expr)) : expr;
1354
1355 if(
1356 expr.type().id() == ID_array &&
1357 to_array_type(expr.type()).element_type().id() == ID_array)
1358 {
1359 insert(dest, l1_expr);
1360 }
1361 else
1362 insert(dest, l1_expr, from_integer(0, c_index_type()));
1363
1364 return;
1365 }
1366 else if(expr.id()==ID_dereference)
1367 {
1368 const auto &pointer = to_dereference_expr(expr).pointer();
1369
1370 bool includes_nondet_pointer = false;
1372 pointer, dest, includes_nondet_pointer, "", pointer.type(), ns);
1373
1374#ifdef DEBUG
1375 for(const auto &map_entry : dest.read())
1376 {
1377 std::cout << "VALUE_SET: " << format(object_numbering[map_entry.first])
1378 << '\n';
1379 }
1380#endif
1381
1382 return;
1383 }
1384 else if(expr.id()==ID_index)
1385 {
1386 const index_exprt &index_expr=to_index_expr(expr);
1387 const exprt &array=index_expr.array();
1388 const exprt &index = index_expr.index();
1389
1391 array.type().id() == ID_array, "index takes array-typed operand");
1392
1393 const auto &array_type = to_array_type(array.type());
1394
1395 object_mapt array_references;
1396 get_reference_set(array, array_references, ns);
1397
1398 const object_map_dt &object_map=array_references.read();
1399
1400 for(object_map_dt::const_iterator
1401 a_it=object_map.begin();
1402 a_it!=object_map.end();
1403 a_it++)
1404 {
1405 const exprt &object=object_numbering[a_it->first];
1406
1407 if(object.id()==ID_unknown)
1408 insert(dest, exprt(ID_unknown, expr.type()));
1409 else
1410 {
1411 const index_exprt deref_index_expr(
1412 typecast_exprt::conditional_cast(object, array_type),
1414
1415 offsett o = a_it->second;
1416
1417 if(!index.is_zero() && o.has_value())
1418 {
1419 auto size = pointer_offset_size(array_type.element_type(), ns);
1420
1421 if(!size.has_value() || *size == 0)
1422 o.reset();
1423 else
1424 {
1425 o = simplify_expr(
1426 plus_exprt{
1427 *o,
1429 mult_exprt{index, from_integer(*size, index.type())},
1430 o->type())},
1431 ns);
1432 }
1433 }
1434
1435 insert(dest, deref_index_expr, o);
1436 }
1437 }
1438
1439 return;
1440 }
1441 else if(expr.id()==ID_member)
1442 {
1443 const irep_idt &component_name=expr.get(ID_component_name);
1444
1445 const exprt &struct_op = to_member_expr(expr).compound();
1446
1447 object_mapt struct_references;
1448 get_reference_set(struct_op, struct_references, ns);
1449
1450 const object_map_dt &object_map=struct_references.read();
1451
1452 for(object_map_dt::const_iterator
1453 it=object_map.begin();
1454 it!=object_map.end();
1455 it++)
1456 {
1457 const exprt &object=object_numbering[it->first];
1458
1459 if(object.id()==ID_unknown)
1460 insert(dest, exprt(ID_unknown, expr.type()));
1461 else if(
1462 object.type().id() == ID_struct ||
1463 object.type().id() == ID_struct_tag || object.type().id() == ID_union ||
1464 object.type().id() == ID_union_tag)
1465 {
1466 offsett o = it->second;
1467
1468 member_exprt member_expr(object, component_name, expr.type());
1469
1470 // We cannot introduce a cast from scalar to non-scalar,
1471 // thus, we can only adjust the types of structs and unions.
1472
1473 if(
1474 object.type().id() == ID_struct ||
1475 object.type().id() == ID_struct_tag ||
1476 object.type().id() == ID_union || object.type().id() == ID_union_tag)
1477 {
1478 // adjust type?
1479 if(struct_op.type() != object.type())
1480 {
1481 member_expr.compound() =
1482 typecast_exprt(member_expr.compound(), struct_op.type());
1483 }
1484
1485 insert(dest, member_expr, o);
1486 }
1487 else
1488 insert(dest, exprt(ID_unknown, expr.type()));
1489 }
1490 else
1491 insert(dest, exprt(ID_unknown, expr.type()));
1492 }
1493
1494 return;
1495 }
1496 else if(expr.id()==ID_if)
1497 {
1498 get_reference_set_rec(to_if_expr(expr).true_case(), dest, ns);
1499 get_reference_set_rec(to_if_expr(expr).false_case(), dest, ns);
1500 return;
1501 }
1502
1503 insert(dest, exprt(ID_unknown, expr.type()));
1504}
1505
1507 const exprt &lhs,
1508 const exprt &rhs,
1509 const namespacet &ns,
1510 bool is_simplified,
1511 bool add_to_sets)
1512{
1513#ifdef DEBUG
1514 std::cout << "ASSIGN LHS: " << format(lhs) << " : "
1515 << format(lhs.type()) << '\n';
1516 std::cout << "ASSIGN RHS: " << format(rhs) << " : "
1517 << format(rhs.type()) << '\n';
1518 std::cout << "--------------------------------------------\n";
1519 output(std::cout);
1520#endif
1521
1522 if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
1523 {
1524 const auto &components =
1525 lhs.type().id() == ID_struct_tag
1527 : to_struct_type(lhs.type()).components();
1528
1529 for(const auto &c : components)
1530 {
1531 const typet &subtype = c.type();
1532 const irep_idt &name = c.get_name();
1533
1534 // ignore padding
1536 subtype.id() != ID_code, "struct member must not be of code type");
1537 if(c.get_is_padding())
1538 continue;
1539
1540 member_exprt lhs_member(lhs, name, subtype);
1541
1542 exprt rhs_member;
1543
1544 if(rhs.id()==ID_unknown ||
1545 rhs.id()==ID_invalid)
1546 {
1547 // this branch is deemed dead as otherwise we'd be missing assignments
1548 // that never happened in this branch
1550 rhs_member=exprt(rhs.id(), subtype);
1551 }
1552 else
1553 {
1555 rhs.type() == lhs.type(),
1556 "value_sett::assign types should match, got: "
1557 "rhs.type():\n" +
1558 rhs.type().pretty() + "\n" + "lhs.type():\n" + lhs.type().pretty());
1559
1560 if(rhs.type().id() == ID_struct_tag || rhs.type().id() == ID_union_tag)
1561 {
1562 const struct_union_typet &rhs_struct_union_type =
1564
1565 const typet &rhs_subtype = rhs_struct_union_type.component_type(name);
1566 rhs_member = simplify_expr(member_exprt{rhs, name, rhs_subtype}, ns);
1567
1568 assign(lhs_member, rhs_member, ns, true, add_to_sets);
1569 }
1570 else if(rhs.type().id() == ID_struct || rhs.type().id() == ID_union)
1571 {
1572 const struct_union_typet &rhs_struct_union_type =
1574
1575 const typet &rhs_subtype = rhs_struct_union_type.component_type(name);
1576 rhs_member = simplify_expr(member_exprt{rhs, name, rhs_subtype}, ns);
1577
1578 assign(lhs_member, rhs_member, ns, true, add_to_sets);
1579 }
1580 }
1581 }
1582 }
1583 else if(lhs.type().id() == ID_array)
1584 {
1585 const index_exprt lhs_index(
1586 lhs,
1587 exprt(ID_unknown, c_index_type()),
1589
1590 if(rhs.id()==ID_unknown ||
1591 rhs.id()==ID_invalid)
1592 {
1593 assign(
1594 lhs_index,
1595 exprt(rhs.id(), to_array_type(lhs.type()).element_type()),
1596 ns,
1597 is_simplified,
1598 add_to_sets);
1599 }
1600 else
1601 {
1603 rhs.type() == lhs.type(),
1604 "value_sett::assign types should match, got: "
1605 "rhs.type():\n" +
1606 rhs.type().pretty() + "\n" + "type:\n" + lhs.type().pretty());
1607
1608 if(rhs.id()==ID_array_of)
1609 {
1610 assign(
1611 lhs_index,
1612 to_array_of_expr(rhs).what(),
1613 ns,
1614 is_simplified,
1615 add_to_sets);
1616 }
1617 else if(rhs.id() == ID_array || rhs.is_constant())
1618 {
1619 for(const auto &op : rhs.operands())
1620 {
1621 assign(lhs_index, op, ns, is_simplified, add_to_sets);
1622 add_to_sets=true;
1623 }
1624 }
1625 else if(rhs.id()==ID_with)
1626 {
1627 const index_exprt op0_index(
1628 to_with_expr(rhs).old(),
1629 exprt(ID_unknown, c_index_type()),
1631
1632 assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1633 assign(
1634 lhs_index, to_with_expr(rhs).new_value(), ns, is_simplified, true);
1635 }
1636 else
1637 {
1638 const index_exprt rhs_index(
1639 rhs,
1640 exprt(ID_unknown, c_index_type()),
1642 assign(lhs_index, rhs_index, ns, is_simplified, true);
1643 }
1644 }
1645 }
1646 else
1647 {
1648 // basic type or union
1649 object_mapt values_rhs = get_value_set(rhs, ns, is_simplified);
1650
1651 // Permit custom subclass to alter the read values prior to write:
1652 adjust_assign_rhs_values(rhs, ns, values_rhs);
1653
1654 // Permit custom subclass to perform global side-effects prior to write:
1655 apply_assign_side_effects(lhs, rhs, ns);
1656
1657 assign_rec(lhs, values_rhs, "", ns, add_to_sets);
1658 }
1659}
1660
1662 const exprt &lhs,
1663 const object_mapt &values_rhs,
1664 const std::string &suffix,
1665 const namespacet &ns,
1666 bool add_to_sets)
1667{
1668#ifdef DEBUG
1669 std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
1670 std::cout << "ASSIGN_REC LHS ID: " << lhs.id() << '\n';
1671 std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1672
1673 for(object_map_dt::const_iterator it=values_rhs.read().begin();
1674 it!=values_rhs.read().end();
1675 it++)
1676 std::cout << "ASSIGN_REC RHS: " <<
1677 format(object_numbering[it->first]) << '\n';
1678 std::cout << '\n';
1679#endif
1680
1681 if(lhs.id()==ID_symbol)
1682 {
1683 const symbol_exprt lhs_l1 =
1685 const irep_idt &identifier = lhs_l1.get_identifier();
1686
1688 entryt{identifier, suffix}, lhs.type(), values_rhs, add_to_sets);
1689 }
1690 else if(lhs.id()==ID_dynamic_object)
1691 {
1692 const dynamic_object_exprt &dynamic_object=
1694
1695 const std::string name=
1696 "value_set::dynamic_object"+
1697 std::to_string(dynamic_object.get_instance());
1698
1699 update_entry(entryt{name, suffix}, lhs.type(), values_rhs, true);
1700 }
1701 else if(lhs.id()==ID_dereference)
1702 {
1704 lhs.operands().size() == 1,
1705 lhs.id_string() + " expected to have one operand");
1706
1707 object_mapt reference_set;
1708 get_reference_set(lhs, reference_set, ns);
1709
1710 if(reference_set.read().size()!=1)
1711 add_to_sets=true;
1712
1713 for(object_map_dt::const_iterator
1714 it=reference_set.read().begin();
1715 it!=reference_set.read().end();
1716 it++)
1717 {
1720 const exprt object=object_numbering[it->first];
1721
1722 if(object.id()!=ID_unknown)
1723 assign_rec(object, values_rhs, suffix, ns, add_to_sets);
1724 }
1725 }
1726 else if(lhs.id()==ID_index)
1727 {
1728 const auto &array = to_index_expr(lhs).array();
1729
1730 const typet &type = array.type();
1731
1733 type.id() == ID_array, "operand 0 of index expression must be an array");
1734
1735 assign_rec(array, values_rhs, "[]" + suffix, ns, true);
1736 }
1737 else if(lhs.id()==ID_member)
1738 {
1739 const auto &lhs_member_expr = to_member_expr(lhs);
1740 const auto &component_name = lhs_member_expr.get_component_name();
1741 const exprt &compound = lhs_member_expr.compound();
1742
1744 compound.type().id() == ID_struct ||
1745 compound.type().id() == ID_struct_tag ||
1746 compound.type().id() == ID_union ||
1747 compound.type().id() == ID_union_tag,
1748 "operand 0 of member expression must be struct or union");
1749
1750 assign_rec(
1751 compound,
1752 values_rhs,
1753 "." + id2string(component_name) + suffix,
1754 ns,
1755 add_to_sets);
1756 }
1757 else if(lhs.id()=="valid_object" ||
1758 lhs.id()=="dynamic_type" ||
1759 lhs.id()=="is_zero_string" ||
1760 lhs.id()=="zero_string" ||
1761 lhs.id()=="zero_string_length")
1762 {
1763 // we ignore this here
1764 }
1765 else if(lhs.id()==ID_string_constant)
1766 {
1767 // someone writes into a string-constant
1768 // evil guy
1769 }
1770 else if(lhs.id() == ID_null_object)
1771 {
1772 // evil as well
1773 }
1774 else if(lhs.id()==ID_typecast)
1775 {
1776 const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1777
1778 assign_rec(typecast_expr.op(), values_rhs, suffix, ns, add_to_sets);
1779 }
1780 else if(lhs.id()==ID_byte_extract_little_endian ||
1781 lhs.id()==ID_byte_extract_big_endian)
1782 {
1783 assign_rec(to_byte_extract_expr(lhs).op(), values_rhs, suffix, ns, true);
1784 }
1785 else if(lhs.id()==ID_integer_address)
1786 {
1787 // that's like assigning into __CPROVER_memory[...],
1788 // which we don't track
1789 }
1790 else
1791 UNIMPLEMENTED_FEATURE("assign NYI: '" + lhs.id_string() + "'");
1792}
1793
1795 const irep_idt &function,
1796 const exprt::operandst &arguments,
1797 const namespacet &ns)
1798{
1799 const symbolt &symbol=ns.lookup(function);
1800
1801 const code_typet &type=to_code_type(symbol.type);
1802 const code_typet::parameterst &parameter_types=type.parameters();
1803
1804 // these first need to be assigned to dummy, temporary arguments
1805 // and only thereafter to the actuals, in order
1806 // to avoid overwriting actuals that are needed for recursive
1807 // calls
1808
1809 for(std::size_t i=0; i<arguments.size(); i++)
1810 {
1811 const std::string identifier="value_set::dummy_arg_"+std::to_string(i);
1812 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1813 assign(dummy_lhs, arguments[i], ns, false, false);
1814 }
1815
1816 // now assign to 'actual actuals'
1817
1818 unsigned i=0;
1819
1820 for(code_typet::parameterst::const_iterator
1821 it=parameter_types.begin();
1822 it!=parameter_types.end();
1823 it++)
1824 {
1825 const irep_idt &identifier=it->get_identifier();
1826 if(identifier.empty())
1827 continue;
1828
1829 const exprt v_expr=
1830 symbol_exprt("value_set::dummy_arg_"+std::to_string(i), it->type());
1831
1832 const symbol_exprt actual_lhs(identifier, it->type());
1833 assign(actual_lhs, v_expr, ns, true, true);
1834 i++;
1835 }
1836
1837 // we could delete the dummy_arg_* now.
1838}
1839
1841 const exprt &lhs,
1842 const namespacet &ns)
1843{
1844 if(lhs.is_nil())
1845 return;
1846
1847 symbol_exprt rhs("value_set::return_value", lhs.type());
1848
1849 assign(lhs, rhs, ns, false, false);
1850}
1851
1853 const codet &code,
1854 const namespacet &ns)
1855{
1856 const irep_idt &statement=code.get_statement();
1857
1858 if(statement==ID_block)
1859 {
1860 for(const auto &op : code.operands())
1861 apply_code_rec(to_code(op), ns);
1862 }
1863 else if(statement==ID_function_call)
1864 {
1865 // shouldn't be here
1867 }
1868 else if(statement==ID_assign)
1869 {
1870 const code_assignt &a = to_code_assign(code);
1871 assign(a.lhs(), a.rhs(), ns, false, false);
1872 }
1873 else if(statement==ID_decl)
1874 {
1875 const code_declt &decl = to_code_decl(code);
1876 const symbol_exprt &symbol = decl.symbol();
1877 const typet &symbol_type = symbol.type();
1878
1879 if(
1880 symbol_type.id() == ID_pointer ||
1881 (symbol_type.id() == ID_array &&
1882 to_array_type(symbol_type).element_type().id() == ID_pointer))
1883 {
1884 const symbol_exprt symbol_l1 = is_ssa_expr(symbol)
1885 ? remove_level_2(to_ssa_expr(symbol))
1886 : to_symbol_expr(symbol);
1887 // assign the address of the failed object
1888 if(auto failed = get_failed_symbol(symbol_l1, ns))
1889 {
1890 address_of_exprt address_of_expr(*failed, to_pointer_type(symbol_type));
1891 assign(symbol, address_of_expr, ns, false, false);
1892 }
1893 else
1894 assign(symbol, exprt(ID_invalid), ns, false, false);
1895 }
1896 }
1897 else if(statement==ID_expression)
1898 {
1899 // can be ignored, we don't expect side effects here
1900 }
1901 else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array)
1902 {
1903 // does nothing
1904 }
1905 else if(statement=="lock" || statement=="unlock")
1906 {
1907 // ignore for now
1908 }
1909 else if(statement==ID_asm)
1910 {
1911 // ignore for now, probably not safe
1912 }
1913 else if(statement==ID_nondet)
1914 {
1915 // doesn't do anything
1916 }
1917 else if(statement==ID_printf)
1918 {
1919 // doesn't do anything
1920 }
1921 else if(statement==ID_return)
1922 {
1923 const code_returnt &code_return = to_code_return(code);
1924 // this is turned into an assignment
1925 symbol_exprt lhs(
1926 "value_set::return_value", code_return.return_value().type());
1927 assign(lhs, code_return.return_value(), ns, false, false);
1928 }
1929 else if(statement==ID_array_set)
1930 {
1931 }
1932 else if(statement==ID_array_copy)
1933 {
1934 }
1935 else if(statement==ID_array_replace)
1936 {
1937 }
1938 else if(statement == ID_array_equal)
1939 {
1940 }
1941 else if(statement==ID_assume)
1942 {
1943 guard(to_code_assume(code).assumption(), ns);
1944 }
1945 else if(statement==ID_user_specified_predicate ||
1946 statement==ID_user_specified_parameter_predicates ||
1947 statement==ID_user_specified_return_predicates)
1948 {
1949 // doesn't do anything
1950 }
1951 else if(statement==ID_fence)
1952 {
1953 }
1955 {
1956 // doesn't do anything
1957 }
1958 else if(statement==ID_dead)
1959 {
1960 // Ignore by default; could prune the value set.
1961 }
1962 else if(statement == ID_havoc_object)
1963 {
1964 }
1965 else
1966 {
1968 "value_sett: unexpected statement: " + id2string(statement));
1969 }
1970}
1971
1973 const exprt &expr,
1974 const namespacet &ns)
1975{
1976 if(expr.id()==ID_and)
1977 {
1978 for(const auto &op : expr.operands())
1979 guard(op, ns);
1980 }
1981 else if(expr.id()==ID_equal)
1982 {
1983 }
1984 else if(expr.id()==ID_notequal)
1985 {
1986 }
1987 else if(expr.id()==ID_not)
1988 {
1989 }
1990 else if(expr.id()==ID_dynamic_object)
1991 {
1992 dynamic_object_exprt dynamic_object(unsigned_char_type());
1993 // dynamic_object.instance()=
1994 // from_integer(location_number, typet(ID_natural));
1995 dynamic_object.valid()=true_exprt();
1996
1997 address_of_exprt address_of(dynamic_object);
1998 address_of.type() = to_dynamic_object_expr(expr).op0().type();
1999
2000 assign(to_dynamic_object_expr(expr).op0(), address_of, ns, false, false);
2001 }
2002}
2003
2005 const irep_idt &index,
2006 const std::unordered_set<exprt, irep_hash> &values_to_erase)
2007{
2008 if(values_to_erase.empty())
2009 return;
2010
2011 auto entry = find_entry(index);
2012 if(!entry)
2013 return;
2014
2015 std::vector<object_map_dt::key_type> keys_to_erase;
2016
2017 for(auto &key_value : entry->object_map.read())
2018 {
2019 const auto &rhs_object = to_expr(key_value);
2020 if(values_to_erase.count(rhs_object))
2021 {
2022 keys_to_erase.emplace_back(key_value.first);
2023 }
2024 }
2025
2027 keys_to_erase.size() == values_to_erase.size(),
2028 "value_sett::erase_value_from_entry() should erase exactly one value for "
2029 "each element in the set it is given");
2030
2031 entryt replacement = *entry;
2032 for(const auto &key_to_erase : keys_to_erase)
2033 {
2034 replacement.object_map.write().erase(key_to_erase);
2035 }
2036 values.replace(index, std::move(replacement));
2037}
2038
2040 const struct_union_typet &struct_union_type,
2041 const std::string &erase_prefix,
2042 const namespacet &ns)
2043{
2044 for(const auto &c : struct_union_type.components())
2045 {
2046 const typet &subtype = c.type();
2047 const irep_idt &name = c.get_name();
2048
2049 // ignore padding
2051 subtype.id() != ID_code, "struct/union member must not be of code type");
2052 if(c.get_is_padding())
2053 continue;
2054
2055 erase_symbol_rec(subtype, erase_prefix + "." + id2string(name), ns);
2056 }
2057}
2058
2060 const typet &type,
2061 const std::string &erase_prefix,
2062 const namespacet &ns)
2063{
2064 if(type.id() == ID_struct_tag)
2066 ns.follow_tag(to_struct_tag_type(type)), erase_prefix, ns);
2067 else if(type.id() == ID_union_tag)
2069 ns.follow_tag(to_union_tag_type(type)), erase_prefix, ns);
2070 else if(type.id() == ID_array)
2072 to_array_type(type).element_type(), erase_prefix + "[]", ns);
2073 else if(values.has_key(erase_prefix))
2074 values.erase(erase_prefix);
2075}
2076
2078 const symbol_exprt &symbol_expr,
2079 const namespacet &ns)
2080{
2082 symbol_expr.type(), id2string(symbol_expr.get_identifier()), ns);
2083}
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)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral 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.
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
A base class for binary expressions.
Definition std_expr.h:638
exprt & op0()
Definition expr.h:133
A goto_instruction_codet representing an assignment in the program.
A goto_instruction_codet representing the declaration of a local variable.
symbol_exprt & symbol()
goto_instruction_codet representation of a "return from afunction" statement.
const exprt & return_value() const
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.
const irep_idt & get_statement() const
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
void clear()
Definition dstring.h:159
Representation of heap-allocated objects.
unsigned int get_instance() const
void set_instance(unsigned int instance)
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
exprt & index()
Definition std_expr.h:1510
exprt & array()
Definition std_expr.h:1500
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:2972
const exprt & compound() const
Definition std_expr.h:3021
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
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.
The plus expression Associativity is not specified.
Definition std_expr.h:1002
const typet & base_type() const
The type of the data what we point to.
const T & read() const
std::vector< view_itemt > viewt
std::vector< delta_view_itemt > delta_viewt
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.
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:77
const componentst & components() const
Definition std_types.h:147
bool has_component(const irep_idt &component_name) const
Definition std_types.h:157
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
irep_idt name
The unique identifier.
Definition symbol.h:40
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
The Boolean constant true.
Definition std_expr.h:3191
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
const exprt & op() const
Definition std_expr.h:391
The unary minus expression.
Definition std_expr.h:484
std::list< exprt > valuest
Definition value_sets.h:28
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
sharing_mapt< irep_idt, entryt > valuest
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets.
Definition value_set.h:230
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: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.
std::optional< exprt > offsett
Represents the offset into an object: either some (possibly constant) expression, or an unknown value...
Definition value_set.h:80
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:281
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)
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: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.
reference_counting< object_map_dt, empty_object_map > object_mapt
Reference-counts instances of object_map_dt, such that multiple instructions' value_sett instances ca...
Definition value_set.h:109
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:43
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:40
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:513
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:499
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:2603
exprt & new_value()
Definition std_expr.h:2633
exprt & where()
Definition std_expr.h:2623
exprt & old()
Definition std_expr.h:2613
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 can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
static format_containert< T > format(const T &o)
Definition format.h:37
const code_assignt & to_code_assign(const goto_instruction_codet &code)
const code_declt & to_code_decl(const goto_instruction_codet &code)
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)
numberingt< exprt, irep_hash > object_numberingt
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)
BigInt mp_integer
Definition smt_terms.h:17
#define UNIMPLEMENTED_FEATURE(FEATURE)
Definition invariant.h:549
#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
ssa_exprt remove_level_2(ssa_exprt ssa)
Definition ssa_expr.cpp:219
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
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:3456
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
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:3173
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:2661
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:188
irep_idt identifier
Definition value_set.h:190
std::string suffix
Definition value_set.h:191
object_mapt object_map
Definition value_set.h:189
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.
dstringt irep_idt