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