cprover
Loading...
Searching...
No Matches
shadow_memory_util.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symex Shadow Memory Instrumentation
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "shadow_memory_util.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/config.h>
19#include <util/format_expr.h>
20#include <util/invariant.h>
21#include <util/namespace.h>
23#include <util/ssa_expr.h>
24#include <util/std_expr.h>
26
27#include <langapi/language_util.h> // IWYU pragma: keep
30
32 const namespacet &ns,
33 const messaget &log,
34 const irep_idt &field_name,
35 const exprt &expr,
36 const exprt &value)
37{
38#ifdef DEBUG_SHADOW_MEMORY
40 log.debug(), [field_name, ns, expr, value](messaget::mstreamt &mstream) {
41 mstream << "Shadow memory: set_field: " << id2string(field_name)
42 << " for " << format(expr) << " to " << format(value)
43 << messaget::eom;
44 });
45#endif
46}
47
49 const namespacet &ns,
50 const messaget &log,
51 const irep_idt &field_name,
52 const exprt &expr)
53{
54#ifdef DEBUG_SHADOW_MEMORY
56 log.debug(), [ns, field_name, expr](messaget::mstreamt &mstream) {
57 mstream << "Shadow memory: get_field: " << id2string(field_name)
58 << " for " << format(expr) << messaget::eom;
59 });
60#endif
61}
62
64 const namespacet &ns,
65 const messaget &log,
66 const std::vector<exprt> &value_set)
67{
68#ifdef DEBUG_SHADOW_MEMORY
70 log.debug(), [ns, value_set](messaget::mstreamt &mstream) {
71 for(const auto &e : value_set)
72 {
73 mstream << "Shadow memory: value_set: " << format(e) << messaget::eom;
74 }
75 });
76#endif
77}
78
80 const namespacet &ns,
81 const messaget &log,
82 const exprt &address,
83 const exprt &expr)
84{
85 // Leave guards rename to DEBUG_SHADOW_MEMORY
86#ifdef DEBUG_SHADOW_MEMORY
88 log.debug(), [ns, address, expr](messaget::mstreamt &mstream) {
89 mstream << "Shadow memory: value_set_match: " << format(address)
90 << " <-- " << format(expr) << messaget::eom;
91 });
92#endif
93}
94
96 const namespacet &ns,
97 const messaget &log,
98 const char *text,
99 const exprt &expr)
100{
101#ifdef DEBUG_SHADOW_MEMORY
103 log.debug(), [ns, text, expr](messaget::mstreamt &mstream) {
104 mstream << "Shadow memory: " << text << ": " << format(expr)
105 << messaget::eom;
106 });
107#endif
108}
109
114 const namespacet &ns,
115 const messaget &log,
119 const exprt &expr,
121{
122#ifdef DEBUG_SHADOW_MEMORY
124 log.debug(),
125 [ns,
127 expr,
131 mstream << "Shadow memory: value_set_match: " << messaget::eom;
132 mstream << "Shadow memory: base: " << format(shadowed_address.address)
133 << " <-- " << format(matched_base_address) << messaget::eom;
134 mstream << "Shadow memory: cell: " << format(dereference.pointer)
135 << " <-- " << format(expr) << messaget::eom;
136 mstream << "Shadow memory: shadow_ptr: "
137 << format(shadow_dereference.pointer) << messaget::eom;
138 mstream << "Shadow memory: shadow_val: "
139 << format(shadow_dereference.value) << messaget::eom;
140 });
141#endif
142}
143
146 const namespacet &ns,
147 const messaget &log,
149{
150#ifdef DEBUG_SHADOW_MEMORY
152 log.debug(), [ns, shadowed_address](messaget::mstreamt &mstream) {
153 mstream << "Shadow memory: trying shadowed address: "
154 << format(shadowed_address.address) << messaget::eom;
155 });
156#endif
157}
158
160static void log_shadow_memory_message(const messaget &log, const char *text)
161{
162#ifdef DEBUG_SHADOW_MEMORY
163 log.debug() << text << messaget::eom;
164#endif
165}
166
168 const namespacet &ns,
169 const exprt &expr,
171 const messaget &log)
172{
173#ifdef DEBUG_SHADOW_MEMORY
174 log.debug() << "Shadow memory: incompatible types "
175 << from_type(ns, "", expr.type()) << ", "
176 << from_type(ns, "", shadowed_address.address.type())
177 << messaget::eom;
178#endif
179}
180
182 const messaget &log,
183 const namespacet &ns,
184 const exprt &expr,
185 const exprt &null_pointer)
186{
187#ifdef DEBUG_SHADOW_MEMORY
189 log.debug(), [ns, null_pointer, expr](messaget::mstreamt &mstream) {
190 mstream << "Shadow memory: value set match: " << format(null_pointer)
191 << " <-- " << format(expr) << messaget::eom;
192 mstream << "Shadow memory: ignoring set field on NULL object"
193 << messaget::eom;
194 });
195#endif
196}
197
199 const messaget &log,
200 const namespacet &ns,
201 const exprt &expr,
203{
204#ifdef DEBUG_SHADOW_MEMORY
205 log.debug() << "Shadow memory: incompatible types "
206 << from_type(ns, "", expr.type()) << ", "
207 << from_type(ns, "", shadowed_address.address.type())
208 << messaget::eom;
209#endif
210}
211
213{
221 {
222 return string_expr.get(ID_value);
223 }
224 else
225 {
226 UNREACHABLE_BECAUSE("Failed to extract shadow memory field name.");
227 }
228}
229
233static void remove_array_type_l2(typet &type)
234{
235 if(to_array_type(type).size().id() != ID_symbol)
236 return;
237
238 ssa_exprt &size = to_ssa_expr(to_array_type(type).size());
239 size.remove_level_2();
240}
241
243{
245 {
246 return to_address_of_expr(expr).object();
247 }
248
249 return dereference_exprt(expr);
250}
251
252void clean_pointer_expr(exprt &expr, const typet &type)
253{
254 if(
256 to_array_type(type).size().get_bool(ID_C_SSA_symbol))
257 {
259 exprt original_expr = to_ssa_expr(expr).get_original_expr();
261 to_ssa_expr(expr).set_expression(original_expr);
262 }
263 if(expr.id() == ID_string_constant)
264 {
265 expr = address_of_exprt(expr);
266 expr.type() = pointer_type(char_type());
267 }
269 {
270 expr = to_dereference_expr(expr).pointer();
271 }
272 else
273 {
274 expr = address_of_exprt(expr);
275 }
277}
278
280{
281 if(
282 expr.id() == ID_symbol && expr.type().id() == ID_pointer &&
283 (id2string(to_symbol_expr(expr).get_identifier()).rfind("invalid_object") !=
284 std::string::npos ||
285 id2string(to_symbol_expr(expr).get_identifier()).rfind("$object") !=
286 std::string::npos))
287 {
289 return;
290 }
291 Forall_operands(it, expr)
292 {
294 }
295}
296
297const exprt &
299{
302 {
303 return field_type_it->second;
304 }
307 return field_type_it->second;
308}
309
310const typet &
312{
314 return field_init_expr.type();
315}
316
318 const std::vector<exprt> &value_set,
319 const exprt &address)
320{
321 if(
322 address.id() == ID_constant && address.type().id() == ID_pointer &&
323 to_constant_expr(address).is_zero())
324 {
325 for(const auto &e : value_set)
326 {
327 if(e.id() != ID_object_descriptor)
328 continue;
329
330 const exprt &expr = to_object_descriptor_expr(e).object();
331 if(expr.id() == ID_null_object)
332 return true;
333 }
334 return false;
335 }
336
337 for(const auto &e : value_set)
338 {
339 if(e.id() == ID_unknown || e.id() == ID_object_descriptor)
340 return true;
341 }
342 return false;
343}
344
349{
350 if(value.type().id() != ID_floatbv)
351 {
352 return value;
353 }
354 return make_byte_extract(
355 value,
357 unsignedbv_typet(to_bitvector_type(value.type()).get_width()));
358}
359
368 const exprt &value,
369 const typet &type,
370 const typet &field_type,
371 exprt::operandst &values)
372{
373 INVARIANT(
375 "Cannot combine with *or* elements of a non-bitvector type.");
376 const size_t size =
377 to_bitvector_type(type).get_width() / config.ansi_c.char_width;
378 values.push_back(typecast_exprt::conditional_cast(value, field_type));
379 for(size_t i = 1; i < size; ++i)
380 {
381 values.push_back(typecast_exprt::conditional_cast(
382 lshr_exprt(value, from_integer(8 * i, size_type())), field_type));
383 }
384}
385
397 exprt element,
398 const typet &field_type,
399 const namespacet &ns,
400 const messaget &log,
401 const bool is_union,
402 exprt::operandst &values)
403{
405 if(element.type().id() == ID_unsignedbv || element.type().id() == ID_signedbv)
406 {
407 exprt value = element;
408 if(is_union)
409 {
410 extract_bytes_of_bv(value, element.type(), field_type, values);
411 }
412 else
413 {
414 values.push_back(typecast_exprt::conditional_cast(value, field_type));
415 }
416 }
417 else
418 {
419 exprt value = compute_or_over_bytes(element, field_type, ns, log, is_union);
420 values.push_back(typecast_exprt::conditional_cast(value, field_type));
421 }
422}
423
431static exprt or_values(const exprt::operandst &values, const typet &field_type)
432{
433 if(values.size() == 1)
434 {
435 return values[0];
436 }
437 return multi_ary_exprt(ID_bitor, values, field_type);
438}
439
441 const exprt &expr,
442 const typet &field_type,
443 const namespacet &ns,
444 const messaget &log,
445 const bool is_union)
446{
447 INVARIANT(
448 can_cast_type<c_bool_typet>(field_type) ||
449 can_cast_type<bool_typet>(field_type),
450 "Can aggregate bytes with *or* only if the shadow memory type is _Bool.");
451 const typet type = ns.follow(expr.type());
452
453 if(type.id() == ID_struct || type.id() == ID_union)
454 {
455 exprt::operandst values;
456 for(const auto &component : to_struct_union_type(type).components())
457 {
458 if(component.get_is_padding())
459 {
460 continue;
461 }
463 member_exprt(expr, component), field_type, ns, log, is_union, values);
464 }
465 return or_values(values, field_type);
466 }
467 else if(type.id() == ID_array)
468 {
469 const array_typet &array_type = to_array_type(type);
470 if(array_type.size().is_constant())
471 {
472 exprt::operandst values;
473 const mp_integer size =
475 for(mp_integer index = 0; index < size; ++index)
476 {
478 index_exprt(expr, from_integer(index, index_type())),
479 field_type,
480 ns,
481 log,
482 is_union,
483 values);
484 }
485 return or_values(values, field_type);
486 }
487 else
488 {
489 log.warning()
490 << "Shadow memory: cannot compute or over variable-size array "
491 << format(expr) << messaget::eom;
492 }
493 }
494 exprt::operandst values;
495 if(is_union)
496 {
498 conditional_cast_floatbv_to_unsignedbv(expr), type, field_type, values);
499 }
500 else
501 {
502 values.push_back(typecast_exprt::conditional_cast(
503 conditional_cast_floatbv_to_unsignedbv(expr), field_type));
504 }
505 return or_values(values, field_type);
506}
507
516std::pair<exprt, exprt> compare_to_collection(
517 const std::vector<exprt>::const_iterator &expr_iterator,
518 const std::vector<exprt>::const_iterator &end)
519{
520 // We need at least an element in the collection
521 INVARIANT(expr_iterator != end, "Cannot compute max of an empty collection");
523
524 // Iterator for the other elements in the collection in the interval denoted
525 // by `expr_iterator` and `end`.
526 std::vector<exprt>::const_iterator expr_to_compare_to =
527 std::next(expr_iterator);
528 if(expr_to_compare_to == end)
529 {
530 return {nil_exprt{}, current_expr};
531 }
532
533 std::vector<exprt> comparisons;
535 {
536 // Compare the current element with the n-th following it
537 comparisons.emplace_back(
539 }
540
542}
543
550 const std::vector<std::pair<exprt, exprt>> &conditions_and_values)
551{
552 // We need at least one element
553 INVARIANT(
554 conditions_and_values.size() > 0,
555 "Cannot compute max of an empty collection");
556
557 // We use reverse-iterator, so the last element is the one in the last else
558 // case.
559 auto reverse_ite = conditions_and_values.rbegin();
560
561 // The last element must have `nil_exprt` as condition
562 INVARIANT(
563 reverse_ite->first == nil_exprt{},
564 "Last element of condition-value list must have nil_exprt condition.");
565
566 exprt res = std::move(reverse_ite->second);
567
569 {
570 res = if_exprt(reverse_ite->first, reverse_ite->second, res);
571 }
572
573 return res;
574}
575
579static exprt create_max_expr(const std::vector<exprt> &values)
580{
581 std::vector<std::pair<exprt, exprt>> rows;
582 rows.reserve(values.size());
583 for(auto byte_it = values.begin(); byte_it != values.end(); ++byte_it)
584 {
585 // Create a pair condition-element where the condition is the comparison of
586 // the element with all the ones contained in the rest of the collection.
587 rows.emplace_back(compare_to_collection(byte_it, values.end()));
588 }
589
591}
592
594 const exprt &expr,
595 const typet &field_type,
596 const namespacet &ns)
597{
598 // Compute the bit-width of the type of `expr`.
599 std::size_t size = boolbv_widtht{ns}(expr.type());
600
601 // Compute how many bytes are in `expr`
602 std::size_t byte_count = size / config.ansi_c.char_width;
603
604 // Extract each byte of `expr` by using byte_extract.
605 std::vector<exprt> extracted_bytes;
607 for(std::size_t i = 0; i < byte_count; ++i)
608 {
610 expr, from_integer(i, unsigned_long_int_type()), field_type));
611 }
612
613 // Compute the max of the bytes extracted from `expr`.
615
616 INVARIANT(
617 max_expr.type() == field_type,
618 "Aggregated max value type must be the same as shadow memory field's "
619 "type.");
620
621 return max_expr;
622}
623
625 const std::vector<std::pair<exprt, exprt>> &conds_values)
626{
628 !conds_values.empty(), "build_if_else_expr requires non-empty argument");
629 exprt result = nil_exprt();
630 for(const auto &cond_value : conds_values)
631 {
632 if(result.is_nil())
633 {
634 result = cond_value.second;
635 }
636 else
637 {
638 result = if_exprt(cond_value.first, cond_value.second, result);
639 }
640 }
641 return result;
642}
643
650static bool
652{
653 if(expr_type.id() != ID_pointer || shadow_type.id() != ID_pointer)
654 return true;
655
656 // We filter out the particularly annoying case of char ** being definitely
657 // incompatible with char[].
658 const typet &expr_subtype = to_pointer_type(expr_type).base_type();
659 const typet &shadow_subtype = to_pointer_type(shadow_type).base_type();
660
661 if(
662 expr_subtype.id() == ID_pointer &&
663 to_pointer_type(expr_subtype).base_type().id() != ID_pointer &&
664 shadow_subtype.id() == ID_array &&
665 to_array_type(shadow_subtype).element_type().id() != ID_pointer)
666 {
667 return false;
668 }
669 if(
670 shadow_subtype.id() == ID_pointer &&
671 to_pointer_type(shadow_subtype).base_type().id() != ID_pointer &&
672 expr_subtype.id() != ID_pointer)
673 {
674 return false;
675 }
676 return true;
677}
678
682static void clean_string_constant(exprt &expr)
683{
685 if(
686 index_expr && index_expr->index().is_zero() &&
688 {
689 expr = index_expr->array();
690 }
691}
692
697static void adjust_array_types(typet &type)
698{
700 if(!pointer_type)
701 {
702 return;
703 }
704 if(
705 const auto *array_type =
707 {
708 pointer_type->base_type() = array_type->element_type();
709 }
711 {
713 }
714}
715
723 const exprt &shadowed_address,
725 const namespacet &ns,
726 const messaget &log)
727{
730 exprt lhs =
734 exprt base_cond = simplify_expr(equal_exprt(lhs, rhs), ns);
735 if(
736 base_cond.id() == ID_equal &&
738 {
739 return true_exprt();
740 }
741 if(base_cond.id() == ID_equal)
742 {
744 const bool equality_types_match =
745 equal_expr.lhs().type() == equal_expr.rhs().type();
748 "types of expressions on each side of equality should match",
751 }
752
753 return base_cond;
754}
755
763 const exprt &expr,
764 const namespacet &ns,
765 const messaget &log)
766{
767 typet expr_type = expr.type();
773 ns);
774 if(
775 expr_cond.id() == ID_equal &&
777 {
778 return true_exprt();
779 }
780 if(expr_cond.id() == ID_equal)
781 {
783 const bool equality_types_match =
784 equal_expr.lhs().type() == equal_expr.rhs().type();
787 "types of expressions on each side of equality should match",
790 }
791 return expr_cond;
792}
793
805 const exprt &shadow,
807 const exprt &expr,
808 const namespacet &ns,
809 const messaget &log)
810{
812 shadowed_object.object() = shadow;
815#ifdef DEBUG_SHADOW_MEMORY
816 log.debug() << "Shadow memory: shadow-deref: "
818#endif
819 return shadow_dereference;
820}
821
822/* foreach shadowed_address in SM:
823 * if(incompatible(shadow.object, object)) continue; // Type incompatibility
824 * base_match = object == shadow_object; // Do the base obj match the SM obj
825 * if(!base_match) continue;
826 * if(object is null) continue; // Done in the caller
827 * if(type_of(dereference object is void)
828 * // we terminate as we don't know how big is the memory at that location
829 * shadowed_dereference.pointer = deref(shadow.shadowed_object, expr);
830 * aggregate the object depending on the type
831 * expr_match = shadowed_dereference == expr
832 * if(!expr_match)
833 * continue;
834 * shadow_dereference = deref(shadow.object, expr);
835 * if(expr_match)
836 * result = shadow_dereference.value [exact match]
837 * break;
838 * if(base_match) [shadow memory matches]
839 * result += (expr_match, shadow_dereference.value)
840 * break;
841 * result += (base_match & expr_match, shadow_dereference.value)
842*/
843std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
844 const namespacet &ns,
845 const messaget &log,
846 const exprt &matched_object,
847 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
848 const typet &field_type,
849 const exprt &expr,
850 const typet &lhs_type,
851 bool &exact_match)
852{
853 std::vector<std::pair<exprt, exprt>> result;
854
855 for(const auto &shadowed_address : addresses)
856 {
858 if(!are_types_compatible(expr.type(), shadowed_address.address.type()))
859 {
861 continue;
862 }
868
869 // NULL has already been handled in the caller; skip.
870 if(matched_base_descriptor.object().id() == ID_null_object)
871 {
872 continue;
873 }
874
875 // Used only to check if the pointer is `void`
878
879 if(is_void_pointer(dereference.pointer.type()))
880 {
881 std::stringstream s;
882 s << "Shadow memory: cannot get shadow memory via type void* for "
883 << format(expr)
884 << ". Insert a cast to the type that you want to access.";
885 throw invalid_input_exceptiont(s.str());
886 }
887
888 // Replace original memory with the shadow object (symbolic dereferencing is
889 // performed during symex later on).
892 shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
894 ns,
895 log,
899 expr,
901
902 const bool is_union = matched_base_descriptor.type().id() == ID_union ||
904
905 exprt value;
906 // Aggregate the value depending on the type
907 if(field_type.id() == ID_c_bool || field_type.id() == ID_bool)
908 {
909 // Value is of bool type, so aggregate with or.
912 shadow_dereference.value, field_type, ns, log, is_union),
913 lhs_type);
914 }
915 else
916 {
917 // Value is of other (bitvector) type, so aggregate with max
918 value = compute_max_over_bytes(shadow_dereference.value, field_type, ns);
919 }
920
922 shadowed_address.address, matched_base_address, ns, log);
923 shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
924 if(base_cond.is_false())
925 {
926 continue;
927 }
928
929 const exprt expr_cond =
930 get_matched_expr_cond(dereference.pointer, expr, ns, log);
931 if(expr_cond.is_false())
932 {
933 continue;
934 }
935
936 if(base_cond.is_true() && expr_cond.is_true())
937 {
938#ifdef DEBUG_SHADOW_MEMORY
939 log.debug() << "exact match" << messaget::eom;
940#endif
941 exact_match = true;
942 result.clear();
943 result.emplace_back(base_cond, value);
944 break;
945 }
946
947 if(base_cond.is_true())
948 {
949 // No point looking at further shadow addresses
950 // as only one of them can match.
951#ifdef DEBUG_SHADOW_MEMORY
952 log.debug() << "base match" << messaget::eom;
953#endif
954 result.clear();
955 result.emplace_back(expr_cond, value);
956 break;
957 }
958 else
959 {
960#ifdef DEBUG_SHADOW_MEMORY
961 log.debug() << "conditional match" << messaget::eom;
962#endif
963 result.emplace_back(and_exprt(base_cond, expr_cond), value);
964 }
965 }
966 return result;
967}
968
969// Unfortunately.
972{
973 if(expr.object().id() == ID_symbol)
974 {
975 return expr;
976 }
977 if(expr.offset().id() == ID_unknown)
978 {
979 return expr;
980 }
981
982 object_descriptor_exprt result = expr;
983 mp_integer offset =
985 exprt object = expr.object();
986
987 while(true)
988 {
989 if(object.id() == ID_index)
990 {
991 const index_exprt &index_expr = to_index_expr(object);
992 mp_integer index =
994
995 offset += *pointer_offset_size(index_expr.type(), ns) * index;
996 object = index_expr.array();
997 }
998 else if(object.id() == ID_member)
999 {
1000 const member_exprt &member_expr = to_member_expr(object);
1001 const struct_typet &struct_type =
1002 to_struct_type(ns.follow(member_expr.struct_op().type()));
1003 offset +=
1004 *member_offset(struct_type, member_expr.get_component_name(), ns);
1005 object = member_expr.struct_op();
1006 }
1007 else
1008 {
1009 break;
1010 }
1011 }
1012 result.object() = object;
1013 result.offset() = from_integer(offset, expr.offset().type());
1014 return result;
1015}
1016
1018 const namespacet &ns,
1019 const messaget &log,
1020 const std::vector<exprt> &value_set,
1021 const exprt &expr)
1022{
1023 INVARIANT(
1025 "Cannot check if value_set contains only NULL as `expr` type is not a "
1026 "pointer.");
1028 if(value_set.size() == 1 && contains_null_or_invalid(value_set, null_pointer))
1029 {
1031 return true;
1032 }
1033 return false;
1034}
1035
1037static std::vector<std::pair<exprt, exprt>>
1039 const exprt &expr,
1040 const exprt &matched_object,
1041 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1042 const namespacet &ns,
1043 const messaget &log,
1044 bool &exact_match)
1045{
1046 std::vector<std::pair<exprt, exprt>> result;
1047 for(const auto &shadowed_address : addresses)
1048 {
1050
1051 if(!are_types_compatible(expr.type(), shadowed_address.address.type()))
1052 {
1054 continue;
1055 }
1056
1059
1062 matched_base_descriptor, expr, ns);
1063
1067
1068 // NULL has already been handled in the caller; skip.
1069 if(matched_base_descriptor.object().id() == ID_null_object)
1070 {
1071 continue;
1072 }
1075 shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
1077 ns,
1078 log,
1082 expr,
1084
1086 shadowed_address.address, matched_base_address, ns, log);
1087 shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
1088 if(base_cond.is_false())
1089 {
1090 continue;
1091 }
1092
1093 const exprt expr_cond =
1094 get_matched_expr_cond(dereference.pointer, expr, ns, log);
1095 if(expr_cond.is_false())
1096 {
1097 continue;
1098 }
1099
1100 if(base_cond.is_true() && expr_cond.is_true())
1101 {
1102 log_shadow_memory_message(log, "exact match");
1103
1104 exact_match = true;
1105 result.clear();
1106 result.push_back({base_cond, shadow_dereference.pointer});
1107 break;
1108 }
1109
1110 if(base_cond.is_true())
1111 {
1112 // No point looking at further shadow addresses
1113 // as only one of them can match.
1114 log_shadow_memory_message(log, "base match");
1115
1116 result.clear();
1117 result.emplace_back(expr_cond, shadow_dereference.pointer);
1118 break;
1119 }
1120 else
1121 {
1122 log_shadow_memory_message(log, "conditional match");
1123 result.emplace_back(
1125 }
1126 }
1127 return result;
1128}
1129
1131 const exprt &expr,
1132 const std::vector<exprt> &value_set,
1133 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1134 const namespacet &ns,
1135 const messaget &log,
1136 size_t &mux_size)
1137{
1138 std::vector<std::pair<exprt, exprt>> conds_values;
1139 for(const auto &matched_object : value_set)
1140 {
1142 {
1143 log.warning() << "Shadow memory: value set contains unknown for "
1144 << format(expr) << messaget::eom;
1145 continue;
1146 }
1147 if(
1148 to_object_descriptor_expr(matched_object).root_object().id() ==
1150 {
1151 log.warning() << "Shadow memory: value set contains integer_address for "
1152 << format(expr) << messaget::eom;
1153 continue;
1154 }
1155 if(matched_object.type().get_bool(ID_C_is_failed_symbol))
1156 {
1157 log.warning() << "Shadow memory: value set contains failed symbol for "
1158 << format(expr) << messaget::eom;
1159 continue;
1160 }
1161
1162 bool exact_match = false;
1164 expr, matched_object, addresses, ns, log, exact_match);
1165
1166 if(!per_value_set_conds_values.empty())
1167 {
1168 if(exact_match)
1169 {
1171 }
1172 conds_values.insert(
1173 conds_values.begin(),
1176 mux_size += conds_values.size() - 1;
1177 if(exact_match)
1178 {
1179 break;
1180 }
1181 }
1182 }
1183 if(!conds_values.empty())
1184 {
1186 }
1187 return {};
1188}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes for bitvectors.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
bitvector_typet index_type()
Definition c_types.cpp:22
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:41
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:91
unsignedbv_typet size_type()
Definition c_types.cpp:55
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
bitvector_typet char_type()
Definition c_types.cpp:111
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
Arrays with given size.
Definition std_types.h:763
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:676
struct configt::ansi_ct ansi_c
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
Central data structure: state.
shadow_memory_statet shadow_memory
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
Thrown when user-provided input cannot be processed.
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
Logical right shift.
Extract member of struct or union.
Definition std_expr.h:2794
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & debug() const
Definition message.h:429
mstreamt & warning() const
Definition message.h:404
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition message.cpp:139
static eomt eom
Definition message.h:297
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:857
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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
The NIL expression.
Definition std_expr.h:3026
The null pointer constant.
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.
field_definitiont global_fields
Field definitions for global-scope fields.
field_definitiont local_fields
Field definitions for local-scope fields.
shadow_memory_field_definitionst fields
The available shadow memory field definitions.
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
void remove_level_2()
Definition ssa_expr.cpp:198
Structure type, corresponds to C style structs.
Definition std_types.h:231
The Boolean constant true.
Definition std_expr.h:3008
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
Return value for build_reference_to; see that method for documentation.
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
#define Forall_operands(it, expr)
Definition expr.h:27
static format_containert< T > format(const T &o)
Definition format.h:37
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
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.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
void replace_invalid_object_by_null(exprt &expr)
Replace an invalid object by a null pointer.
static object_descriptor_exprt normalize(const object_descriptor_exprt &expr, const namespacet &ns)
void shadow_memory_log_value_set_match(const namespacet &ns, const messaget &log, const exprt &address, const exprt &expr)
Logs a successful match between an address and a value within the value set.
static void clean_string_constant(exprt &expr)
Simplify &string_constant[0] to &string_constant to facilitate expression equality for exact matching...
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
bool contains_null_or_invalid(const std::vector< exprt > &value_set, const exprt &address)
Given a pointer expression check to see if it can be a null pointer or an invalid object within value...
const exprt & get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state)
Retrieve the expression that a field was initialised with within a given symex state.
static exprt or_values(const exprt::operandst &values, const typet &field_type)
Translate a list of values into an or expression.
exprt compute_or_over_bytes(const exprt &expr, const typet &field_type, const namespacet &ns, const messaget &log, const bool is_union)
Performs aggregation of the shadow memory field value over multiple bytes for fields whose type is _B...
static bool are_types_compatible(const typet &expr_type, const typet &shadow_type)
Checks given types (object type and shadow memory field type) for equality.
static void extract_bytes_of_expr(exprt element, const typet &field_type, const namespacet &ns, const messaget &log, const bool is_union, exprt::operandst &values)
Extract the components from the input expression value and places them into the array values.
static void adjust_array_types(typet &type)
Flattens type of the form pointer_type(array_type(element_type)) to pointer_type(element_type) and po...
bool check_value_set_contains_only_null_ptr(const namespacet &ns, const messaget &log, const std::vector< exprt > &value_set, const exprt &expr)
Checks if value_set contains only a NULL pointer expression of the same type of expr.
const typet & get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state)
Retrieves the type of the shadow memory by returning the type of the shadow memory initializer value.
static void log_value_set_match(const namespacet &ns, const messaget &log, const shadow_memory_statet::shadowed_addresst &shadowed_address, const exprt &matched_base_address, const value_set_dereferencet::valuet &dereference, const exprt &expr, const value_set_dereferencet::valuet &shadow_dereference)
Log a match between an address and the value set.
void shadow_memory_log_set_field(const namespacet &ns, const messaget &log, const irep_idt &field_name, const exprt &expr, const exprt &value)
Logs setting a value to a given shadow field.
static exprt combine_condition_and_max_values(const std::vector< std::pair< exprt, exprt > > &conditions_and_values)
Combine each (condition, value) element in the input collection into a if-then-else expression such a...
static exprt get_matched_expr_cond(const exprt &dereference_pointer, const exprt &expr, const namespacet &ns, const messaget &log)
Function that compares the two arguments dereference_pointer and expr, simplifies the comparison expr...
std::vector< std::pair< exprt, exprt > > get_shadow_dereference_candidates(const namespacet &ns, const messaget &log, const exprt &matched_object, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const typet &field_type, const exprt &expr, const typet &lhs_type, bool &exact_match)
Get a list of (condition, value) pairs for a certain pointer from the shadow memory,...
static void log_try_shadow_address(const namespacet &ns, const messaget &log, const shadow_memory_statet::shadowed_addresst &shadowed_address)
Log trying out a match between an object and a (target) shadow address.
static void log_value_set_contains_only_null(const messaget &log, const namespacet &ns, const exprt &expr, const exprt &null_pointer)
static void log_are_types_incompatible(const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address, const messaget &log)
exprt compute_max_over_bytes(const exprt &expr, const typet &field_type, const namespacet &ns)
Performs aggregation of the shadow memory field value over multiple cells for fields whose type is a ...
static void log_shadow_memory_incompatible_types(const messaget &log, const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address)
exprt build_if_else_expr(const std::vector< std::pair< exprt, exprt > > &conds_values)
Build an if-then-else chain from a vector containing pairs of expressions.
static void log_shadow_memory_message(const messaget &log, const char *text)
Generic logging function to log a text if DEBUG_SHADOW_MEMORY is defined.
void shadow_memory_log_get_field(const namespacet &ns, const messaget &log, const irep_idt &field_name, const exprt &expr)
Logs getting a value corresponding to a shadow memory field.
irep_idt extract_field_name(const exprt &string_expr)
Extracts the field name identifier from a string expression, e.g.
static exprt create_max_expr(const std::vector< exprt > &values)
Create an expression encoding the max operation over the collection values
static void remove_array_type_l2(typet &type)
If the given type is an array type, then remove the L2 level renaming from its size.
void shadow_memory_log_value_set(const namespacet &ns, const messaget &log, const std::vector< exprt > &value_set)
Logs the retrieval of the value associated with a given shadow memory field.
void clean_pointer_expr(exprt &expr, const typet &type)
Clean the given pointer expression so that it has the right shape for being used for identifying shad...
void shadow_memory_log_text_and_expr(const namespacet &ns, const messaget &log, const char *text, const exprt &expr)
Generic logging function that will log depending on the configured verbosity.
std::pair< exprt, exprt > compare_to_collection(const std::vector< exprt >::const_iterator &expr_iterator, const std::vector< exprt >::const_iterator &end)
Create an expression comparing the element at expr_iterator with the following elements of the collec...
static value_set_dereferencet::valuet get_shadow_dereference(const exprt &shadow, const object_descriptor_exprt &matched_base_descriptor, const exprt &expr, const namespacet &ns, const messaget &log)
Retrieve the shadow value a pointer expression may point to.
optionalt< exprt > get_shadow_memory(const exprt &expr, const std::vector< exprt > &value_set, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const namespacet &ns, const messaget &log, size_t &mux_size)
Get shadow memory values for a given expression within a specified value set.
static exprt conditional_cast_floatbv_to_unsignedbv(const exprt &value)
Casts a given (float) bitvector expression to an unsigned bitvector.
static std::vector< std::pair< exprt, exprt > > get_shadow_memory_for_matched_object(const exprt &expr, const exprt &matched_object, const std::vector< shadow_memory_statet::shadowed_addresst > &addresses, const namespacet &ns, const messaget &log, bool &exact_match)
Used for set_field and shadow memory copy.
static void extract_bytes_of_bv(const exprt &value, const typet &type, const typet &field_type, exprt::operandst &values)
Extract byte-sized elements from the input bitvector-typed expression value and places them into the ...
static exprt get_matched_base_cond(const exprt &shadowed_address, const exprt &matched_base_address, const namespacet &ns, const messaget &log)
Function that compares the two arguments shadowed_address and matched_base_address,...
Symex Shadow Memory Instrumentation Utilities.
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:535
#define POSTCONDITION(CONDITION)
Definition invariant.h:479
#define UNREACHABLE_BECAUSE(REASON)
Definition invariant.h:526
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:77
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1347
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
Pointer Dereferencing.