CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
39 log.conditional_output(
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
55 log.conditional_output(
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
69 log.conditional_output(
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
87 log.conditional_output(
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
102 log.conditional_output(
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
123 log.conditional_output(
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
151 log.conditional_output(
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
188 log.conditional_output(
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
253{
254 if(
257 to_array_type(expr.type()).size().get_bool(ID_C_SSA_symbol))
258 {
260 exprt original_expr = to_ssa_expr(expr).get_original_expr();
262 to_ssa_expr(expr).set_expression(original_expr);
263 }
264 if(expr.id() == ID_string_constant)
265 {
266 expr = address_of_exprt(expr);
267 expr.type() = pointer_type(char_type());
268 }
270 {
271 expr = to_dereference_expr(expr).pointer();
272 }
273 else
274 {
275 expr = address_of_exprt(expr);
276 }
278}
279
281{
282 if(
283 expr.id() == ID_symbol && expr.type().id() == ID_pointer &&
284 (id2string(to_symbol_expr(expr).get_identifier()).rfind("invalid_object") !=
285 std::string::npos ||
286 id2string(to_symbol_expr(expr).get_identifier()).rfind("$object") !=
287 std::string::npos))
288 {
290 return;
291 }
292 Forall_operands(it, expr)
293 {
295 }
296}
297
298const exprt &
300{
303 {
304 return field_type_it->second;
305 }
308 return field_type_it->second;
309}
310
311const typet &
313{
315 return field_init_expr.type();
316}
317
319 const std::vector<exprt> &value_set,
320 const exprt &address)
321{
322 if(address.is_constant() && to_constant_expr(address).is_null_pointer())
323 {
324 for(const auto &e : value_set)
325 {
326 if(e.id() != ID_object_descriptor)
327 continue;
328
329 const exprt &expr = to_object_descriptor_expr(e).object();
330 if(expr.id() == ID_null_object)
331 return true;
332 }
333 return false;
334 }
335
336 for(const auto &e : value_set)
337 {
338 if(e.id() == ID_unknown || e.id() == ID_object_descriptor)
339 return true;
340 }
341 return false;
342}
343
348{
349 if(value.type().id() != ID_floatbv)
350 {
351 return value;
352 }
353 return make_byte_extract(
354 value,
356 unsignedbv_typet(to_bitvector_type(value.type()).get_width()));
357}
358
367 const exprt &value,
368 const typet &type,
369 const typet &field_type,
370 exprt::operandst &values)
371{
372 INVARIANT(
374 "Cannot combine with *or* elements of a non-bitvector type.");
375 const size_t size =
376 to_bitvector_type(type).get_width() / config.ansi_c.char_width;
377 values.push_back(typecast_exprt::conditional_cast(value, field_type));
378 for(size_t i = 1; i < size; ++i)
379 {
380 values.push_back(typecast_exprt::conditional_cast(
381 lshr_exprt(value, from_integer(8 * i, size_type())), field_type));
382 }
383}
384
396 exprt element,
397 const typet &field_type,
398 const namespacet &ns,
399 const messaget &log,
400 const bool is_union,
401 exprt::operandst &values)
402{
404 if(element.type().id() == ID_unsignedbv || element.type().id() == ID_signedbv)
405 {
406 exprt value = element;
407 if(is_union)
408 {
409 extract_bytes_of_bv(value, element.type(), field_type, values);
410 }
411 else
412 {
413 values.push_back(typecast_exprt::conditional_cast(value, field_type));
414 }
415 }
416 else
417 {
418 exprt value = compute_or_over_bytes(element, field_type, ns, log, is_union);
419 values.push_back(typecast_exprt::conditional_cast(value, field_type));
420 }
421}
422
430static exprt or_values(const exprt::operandst &values, const typet &field_type)
431{
432 if(values.size() == 1)
433 {
434 return values[0];
435 }
436 return multi_ary_exprt(ID_bitor, values, field_type);
437}
438
440 const exprt &expr,
441 const typet &field_type,
442 const namespacet &ns,
443 const messaget &log,
444 const bool is_union)
445{
446 INVARIANT(
447 can_cast_type<c_bool_typet>(field_type) ||
448 can_cast_type<bool_typet>(field_type),
449 "Can aggregate bytes with *or* only if the shadow memory type is _Bool.");
450
451 if(
452 expr.type().id() == ID_struct || expr.type().id() == ID_union ||
453 expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag)
454 {
455 const auto &components =
456 (expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag)
457 ? ns.follow_tag(to_struct_or_union_tag_type(expr.type())).components()
458 : to_struct_union_type(expr.type()).components();
459 exprt::operandst values;
460 for(const auto &component : components)
461 {
462 if(component.get_is_padding())
463 {
464 continue;
465 }
467 member_exprt(expr, component), field_type, ns, log, is_union, values);
468 }
469 return or_values(values, field_type);
470 }
471 else if(expr.type().id() == ID_array)
472 {
473 const array_typet &array_type = to_array_type(expr.type());
474 if(array_type.size().is_constant())
475 {
476 exprt::operandst values;
477 const mp_integer size =
479 for(mp_integer index = 0; index < size; ++index)
480 {
482 index_exprt(expr, from_integer(index, array_type.index_type())),
483 field_type,
484 ns,
485 log,
486 is_union,
487 values);
488 }
489 return or_values(values, field_type);
490 }
491 else
492 {
493 log.warning()
494 << "Shadow memory: cannot compute or over variable-size array "
495 << format(expr) << messaget::eom;
496 }
497 }
498 exprt::operandst values;
499 if(is_union)
500 {
503 expr.type(),
504 field_type,
505 values);
506 }
507 else
508 {
509 values.push_back(typecast_exprt::conditional_cast(
510 conditional_cast_floatbv_to_unsignedbv(expr), field_type));
511 }
512 return or_values(values, field_type);
513}
514
523std::pair<exprt, exprt> compare_to_collection(
524 const std::vector<exprt>::const_iterator &expr_iterator,
525 const std::vector<exprt>::const_iterator &end)
526{
527 // We need at least an element in the collection
528 INVARIANT(expr_iterator != end, "Cannot compute max of an empty collection");
530
531 // Iterator for the other elements in the collection in the interval denoted
532 // by `expr_iterator` and `end`.
533 std::vector<exprt>::const_iterator expr_to_compare_to =
534 std::next(expr_iterator);
535 if(expr_to_compare_to == end)
536 {
537 return {nil_exprt{}, current_expr};
538 }
539
540 std::vector<exprt> comparisons;
542 {
543 // Compare the current element with the n-th following it
544 comparisons.emplace_back(
546 }
547
549}
550
557 const std::vector<std::pair<exprt, exprt>> &conditions_and_values)
558{
559 // We need at least one element
560 INVARIANT(
561 conditions_and_values.size() > 0,
562 "Cannot compute max of an empty collection");
563
564 // We use reverse-iterator, so the last element is the one in the last else
565 // case.
566 auto reverse_ite = conditions_and_values.rbegin();
567
568 // The last element must have `nil_exprt` as condition
569 INVARIANT(
570 reverse_ite->first == nil_exprt{},
571 "Last element of condition-value list must have nil_exprt condition.");
572
573 exprt res = std::move(reverse_ite->second);
574
576 {
577 res = if_exprt(reverse_ite->first, reverse_ite->second, res);
578 }
579
580 return res;
581}
582
586static exprt create_max_expr(const std::vector<exprt> &values)
587{
588 std::vector<std::pair<exprt, exprt>> rows;
589 rows.reserve(values.size());
590 for(auto byte_it = values.begin(); byte_it != values.end(); ++byte_it)
591 {
592 // Create a pair condition-element where the condition is the comparison of
593 // the element with all the ones contained in the rest of the collection.
594 rows.emplace_back(compare_to_collection(byte_it, values.end()));
595 }
596
598}
599
601 const exprt &expr,
602 const typet &field_type,
603 const namespacet &ns)
604{
605 // Compute the bit-width of the type of `expr`.
606 std::size_t size = boolbv_widtht{ns}(expr.type());
607
608 // Compute how many bytes are in `expr`
609 std::size_t byte_count = size / config.ansi_c.char_width;
610
611 // Extract each byte of `expr` by using byte_extract.
612 std::vector<exprt> extracted_bytes;
614 for(std::size_t i = 0; i < byte_count; ++i)
615 {
617 expr, from_integer(i, unsigned_long_int_type()), field_type));
618 }
619
620 // Compute the max of the bytes extracted from `expr`.
622
623 INVARIANT(
624 max_expr.type() == field_type,
625 "Aggregated max value type must be the same as shadow memory field's "
626 "type.");
627
628 return max_expr;
629}
630
632 const std::vector<std::pair<exprt, exprt>> &conds_values)
633{
635 !conds_values.empty(), "build_if_else_expr requires non-empty argument");
636 exprt result = nil_exprt();
637 for(const auto &cond_value : conds_values)
638 {
639 if(result.is_nil())
640 {
641 result = cond_value.second;
642 }
643 else
644 {
645 result = if_exprt(cond_value.first, cond_value.second, result);
646 }
647 }
648 return result;
649}
650
657static bool
659{
660 if(expr_type.id() != ID_pointer || shadow_type.id() != ID_pointer)
661 return true;
662
663 // We filter out the particularly annoying case of char ** being definitely
664 // incompatible with char[].
665 const typet &expr_subtype = to_pointer_type(expr_type).base_type();
666 const typet &shadow_subtype = to_pointer_type(shadow_type).base_type();
667
668 if(
669 expr_subtype.id() == ID_pointer &&
670 to_pointer_type(expr_subtype).base_type().id() != ID_pointer &&
671 shadow_subtype.id() == ID_array &&
672 to_array_type(shadow_subtype).element_type().id() != ID_pointer)
673 {
674 return false;
675 }
676 if(
677 shadow_subtype.id() == ID_pointer &&
678 to_pointer_type(shadow_subtype).base_type().id() != ID_pointer &&
679 expr_subtype.id() != ID_pointer)
680 {
681 return false;
682 }
683 return true;
684}
685
689static void clean_string_constant(exprt &expr)
690{
692 if(
693 index_expr && index_expr->index().is_zero() &&
695 {
696 expr = index_expr->array();
697 }
698}
699
704static void adjust_array_types(typet &type)
705{
707 if(!pointer_type)
708 {
709 return;
710 }
711 if(
712 const auto *array_type =
714 {
715 pointer_type->base_type() = array_type->element_type();
716 }
718 {
720 }
721}
722
730 const exprt &shadowed_address,
732 const namespacet &ns,
733 const messaget &log)
734{
737 exprt lhs =
741 exprt base_cond = simplify_expr(equal_exprt(lhs, rhs), ns);
742 if(
743 base_cond.id() == ID_equal &&
745 {
746 return true_exprt();
747 }
748 if(base_cond.id() == ID_equal)
749 {
751 const bool equality_types_match =
752 equal_expr.lhs().type() == equal_expr.rhs().type();
755 "types of expressions on each side of equality should match",
758 }
759
760 return base_cond;
761}
762
770 const exprt &expr,
771 const namespacet &ns,
772 const messaget &log)
773{
774 typet expr_type = expr.type();
780 ns);
781 if(
782 expr_cond.id() == ID_equal &&
784 {
785 return true_exprt();
786 }
787 if(expr_cond.id() == ID_equal)
788 {
790 const bool equality_types_match =
791 equal_expr.lhs().type() == equal_expr.rhs().type();
794 "types of expressions on each side of equality should match",
797 }
798 return expr_cond;
799}
800
812 const exprt &shadow,
814 const exprt &expr,
815 const namespacet &ns,
816 const messaget &log)
817{
819 shadowed_object.object() = shadow;
822#ifdef DEBUG_SHADOW_MEMORY
823 log.debug() << "Shadow memory: shadow-deref: "
825#endif
826 return shadow_dereference;
827}
828
829/* foreach shadowed_address in SM:
830 * if(incompatible(shadow.object, object)) continue; // Type incompatibility
831 * base_match = object == shadow_object; // Do the base obj match the SM obj
832 * if(!base_match) continue;
833 * if(object is null) continue; // Done in the caller
834 * if(type_of(dereference object is void)
835 * // we terminate as we don't know how big is the memory at that location
836 * shadowed_dereference.pointer = deref(shadow.shadowed_object, expr);
837 * aggregate the object depending on the type
838 * expr_match = shadowed_dereference == expr
839 * if(!expr_match)
840 * continue;
841 * shadow_dereference = deref(shadow.object, expr);
842 * if(expr_match)
843 * result = shadow_dereference.value [exact match]
844 * break;
845 * if(base_match) [shadow memory matches]
846 * result += (expr_match, shadow_dereference.value)
847 * break;
848 * result += (base_match & expr_match, shadow_dereference.value)
849*/
850std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
851 const namespacet &ns,
852 const messaget &log,
853 const exprt &matched_object,
854 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
855 const typet &field_type,
856 const exprt &expr,
857 const typet &lhs_type,
858 bool &exact_match)
859{
860 std::vector<std::pair<exprt, exprt>> result;
861
862 for(const auto &shadowed_address : addresses)
863 {
865 if(!are_types_compatible(expr.type(), shadowed_address.address.type()))
866 {
868 continue;
869 }
875
876 // NULL has already been handled in the caller; skip.
877 if(matched_base_descriptor.object().id() == ID_null_object)
878 {
879 continue;
880 }
881
882 // Used only to check if the pointer is `void`
885
886 if(is_void_pointer(dereference.pointer.type()))
887 {
888 std::stringstream s;
889 s << "Shadow memory: cannot get shadow memory via type void* for "
890 << format(expr)
891 << ". Insert a cast to the type that you want to access.";
892 throw invalid_input_exceptiont(s.str());
893 }
894
895 // Replace original memory with the shadow object (symbolic dereferencing is
896 // performed during symex later on).
899 shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
901 ns,
902 log,
906 expr,
908
909 const bool is_union = matched_base_descriptor.type().id() == ID_union ||
911
912 exprt value;
913 // Aggregate the value depending on the type
914 if(field_type.id() == ID_c_bool || field_type.id() == ID_bool)
915 {
916 // Value is of bool type, so aggregate with or.
919 shadow_dereference.value, field_type, ns, log, is_union),
920 lhs_type);
921 }
922 else
923 {
924 // Value is of other (bitvector) type, so aggregate with max
925 value = compute_max_over_bytes(shadow_dereference.value, field_type, ns);
926 }
927
931 if(base_cond.is_false())
932 {
933 continue;
934 }
935
936 const exprt expr_cond =
937 get_matched_expr_cond(dereference.pointer, expr, ns, log);
938 if(expr_cond.is_false())
939 {
940 continue;
941 }
942
943 if(base_cond.is_true() && expr_cond.is_true())
944 {
945#ifdef DEBUG_SHADOW_MEMORY
946 log.debug() << "exact match" << messaget::eom;
947#endif
948 exact_match = true;
949 result.clear();
950 result.emplace_back(base_cond, value);
951 break;
952 }
953
954 if(base_cond.is_true())
955 {
956 // No point looking at further shadow addresses
957 // as only one of them can match.
958#ifdef DEBUG_SHADOW_MEMORY
959 log.debug() << "base match" << messaget::eom;
960#endif
961 result.clear();
962 result.emplace_back(expr_cond, value);
963 break;
964 }
965 else
966 {
967#ifdef DEBUG_SHADOW_MEMORY
968 log.debug() << "conditional match" << messaget::eom;
969#endif
970 result.emplace_back(and_exprt(base_cond, expr_cond), value);
971 }
972 }
973 return result;
974}
975
976// Unfortunately.
979{
980 if(expr.object().id() == ID_symbol)
981 {
982 return expr;
983 }
984 if(expr.offset().id() == ID_unknown)
985 {
986 return expr;
987 }
988
989 object_descriptor_exprt result = expr;
990 mp_integer offset =
992 exprt object = expr.object();
993
994 while(true)
995 {
996 if(object.id() == ID_index)
997 {
998 const index_exprt &index_expr = to_index_expr(object);
999 mp_integer index =
1001
1002 offset += *pointer_offset_size(index_expr.type(), ns) * index;
1003 object = index_expr.array();
1004 }
1005 else if(object.id() == ID_member)
1006 {
1007 const member_exprt &member_expr = to_member_expr(object);
1008 const auto &struct_op = member_expr.struct_op();
1009 const struct_typet &struct_type =
1010 struct_op.type().id() == ID_struct_tag
1011 ? ns.follow_tag(to_struct_tag_type(struct_op.type()))
1012 : to_struct_type(struct_op.type());
1013 offset +=
1014 *member_offset(struct_type, member_expr.get_component_name(), ns);
1015 object = struct_op;
1016 }
1017 else
1018 {
1019 break;
1020 }
1021 }
1022 result.object() = object;
1023 result.offset() = from_integer(offset, expr.offset().type());
1024 return result;
1025}
1026
1028 const namespacet &ns,
1029 const messaget &log,
1030 const std::vector<exprt> &value_set,
1031 const exprt &expr)
1032{
1033 INVARIANT(
1035 "Cannot check if value_set contains only NULL as `expr` type is not a "
1036 "pointer.");
1038 if(value_set.size() == 1 && contains_null_or_invalid(value_set, null_pointer))
1039 {
1041 return true;
1042 }
1043 return false;
1044}
1045
1047static std::vector<std::pair<exprt, exprt>>
1049 const exprt &expr,
1050 const exprt &matched_object,
1051 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1052 const namespacet &ns,
1053 const messaget &log,
1054 bool &exact_match)
1055{
1056 std::vector<std::pair<exprt, exprt>> result;
1057 for(const auto &shadowed_address : addresses)
1058 {
1060
1061 if(!are_types_compatible(expr.type(), shadowed_address.address.type()))
1062 {
1064 continue;
1065 }
1066
1069
1072 matched_base_descriptor, expr, ns);
1073
1077
1078 // NULL has already been handled in the caller; skip.
1079 if(matched_base_descriptor.object().id() == ID_null_object)
1080 {
1081 continue;
1082 }
1085 shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
1087 ns,
1088 log,
1092 expr,
1094
1098 if(base_cond.is_false())
1099 {
1100 continue;
1101 }
1102
1103 const exprt expr_cond =
1104 get_matched_expr_cond(dereference.pointer, expr, ns, log);
1105 if(expr_cond.is_false())
1106 {
1107 continue;
1108 }
1109
1110 if(base_cond.is_true() && expr_cond.is_true())
1111 {
1112 log_shadow_memory_message(log, "exact match");
1113
1114 exact_match = true;
1115 result.clear();
1116 result.push_back({base_cond, shadow_dereference.pointer});
1117 break;
1118 }
1119
1120 if(base_cond.is_true())
1121 {
1122 // No point looking at further shadow addresses
1123 // as only one of them can match.
1124 log_shadow_memory_message(log, "base match");
1125
1126 result.clear();
1127 result.emplace_back(expr_cond, shadow_dereference.pointer);
1128 break;
1129 }
1130 else
1131 {
1132 log_shadow_memory_message(log, "conditional match");
1133 result.emplace_back(
1135 }
1136 }
1137 return result;
1138}
1139
1140std::optional<exprt> get_shadow_memory(
1141 const exprt &expr,
1142 const std::vector<exprt> &value_set,
1143 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1144 const namespacet &ns,
1145 const messaget &log,
1146 size_t &mux_size)
1147{
1148 std::vector<std::pair<exprt, exprt>> conds_values;
1149 for(const auto &matched_object : value_set)
1150 {
1152 {
1153 log.warning() << "Shadow memory: value set contains unknown for "
1154 << format(expr) << messaget::eom;
1155 continue;
1156 }
1157 if(
1158 to_object_descriptor_expr(matched_object).root_object().id() ==
1160 {
1161 log.warning() << "Shadow memory: value set contains integer_address for "
1162 << format(expr) << messaget::eom;
1163 continue;
1164 }
1165 if(matched_object.type().get_bool(ID_C_is_failed_symbol))
1166 {
1167 log.warning() << "Shadow memory: value set contains failed symbol for "
1168 << format(expr) << messaget::eom;
1169 continue;
1170 }
1171
1172 bool exact_match = false;
1175
1176 if(!per_value_set_conds_values.empty())
1177 {
1178 if(exact_match)
1179 {
1181 }
1182 conds_values.insert(
1183 conds_values.begin(),
1186 mux_size += conds_values.size() - 1;
1187 if(exact_match)
1188 {
1189 break;
1190 }
1191 }
1192 }
1193 if(!conds_values.empty())
1194 {
1196 }
1197 return {};
1198}
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.
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:36
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:86
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
bitvector_typet char_type()
Definition c_types.cpp:106
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
Arrays with given size.
Definition std_types.h:807
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
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:38
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
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
Central data structure: state.
shadow_memory_statet shadow_memory
The trinary if-then-else operator.
Definition std_expr.h:2497
Array index operator.
Definition std_expr.h:1470
Thrown when user-provided input cannot be processed.
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Logical right shift.
Extract member of struct or union.
Definition std_expr.h:2971
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3208
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:199
Structure type, corresponds to C style structs.
Definition std_types.h:231
The Boolean constant true.
Definition std_expr.h:3190
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
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
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
static format_containert< T > format(const T &o)
Definition format.h:37
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets, message_handlert &message_handler)
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:44
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
double log(double x)
Definition math.c:2449
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.
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 > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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.
std::optional< 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 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.
void clean_pointer_expr(exprt &expr)
Clean the given pointer expression so that it has the right shape for being used for identifying shad...
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 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.
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)
BigInt mp_integer
Definition smt_terms.h:17
#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:97
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
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
#define size_type
Definition unistd.c:186
Pointer Dereferencing.