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,
116 const shadow_memory_statet::shadowed_addresst &shadowed_address,
117 const exprt &matched_base_address,
119 const exprt &expr,
120 const value_set_dereferencet::valuet &shadow_dereference)
121{
122#ifdef DEBUG_SHADOW_MEMORY
124 log.debug(),
125 [ns,
126 shadowed_address,
127 expr,
129 matched_base_address,
130 shadow_dereference](messaget::mstreamt &mstream) {
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,
148 const shadow_memory_statet::shadowed_addresst &shadowed_address)
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,
170 const shadow_memory_statet::shadowed_addresst &shadowed_address,
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,
202 const shadow_memory_statet::shadowed_addresst &shadowed_address)
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{
214 if(can_cast_expr<typecast_exprt>(string_expr))
215 return extract_field_name(to_typecast_expr(string_expr).op());
216 else if(can_cast_expr<address_of_exprt>(string_expr))
217 return extract_field_name(to_address_of_expr(string_expr).object());
218 else if(can_cast_expr<index_exprt>(string_expr))
219 return extract_field_name(to_index_expr(string_expr).array());
220 else if(can_cast_expr<string_constantt>(string_expr))
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();
261 remove_array_type_l2(original_expr.type());
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 &
299get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state)
300{
301 auto field_type_it = state.shadow_memory.fields.local_fields.find(field_name);
302 if(field_type_it != state.shadow_memory.fields.local_fields.end())
303 {
304 return field_type_it->second;
305 }
306 field_type_it = state.shadow_memory.fields.global_fields.find(field_name);
307 CHECK_RETURN(field_type_it != state.shadow_memory.fields.global_fields.end());
308 return field_type_it->second;
309}
310
311const typet &
312get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state)
313{
314 const exprt &field_init_expr = get_field_init_expr(field_name, state);
315 return field_init_expr.type();
316}
317
319 const std::vector<exprt> &value_set,
320 const exprt &address)
321{
322 if(
323 address.id() == ID_constant && address.type().id() == ID_pointer &&
324 to_constant_expr(address).is_zero())
325 {
326 for(const auto &e : value_set)
327 {
328 if(e.id() != ID_object_descriptor)
329 continue;
330
331 const exprt &expr = to_object_descriptor_expr(e).object();
332 if(expr.id() == ID_null_object)
333 return true;
334 }
335 return false;
336 }
337
338 for(const auto &e : value_set)
339 {
340 if(e.id() == ID_unknown || e.id() == ID_object_descriptor)
341 return true;
342 }
343 return false;
344}
345
350{
351 if(value.type().id() != ID_floatbv)
352 {
353 return value;
354 }
355 return make_byte_extract(
356 value,
359}
360
369 const exprt &value,
370 const typet &type,
371 const typet &field_type,
372 exprt::operandst &values)
373{
374 INVARIANT(
376 "Cannot combine with *or* elements of a non-bitvector type.");
377 const size_t size =
379 values.push_back(typecast_exprt::conditional_cast(value, field_type));
380 for(size_t i = 1; i < size; ++i)
381 {
382 values.push_back(typecast_exprt::conditional_cast(
383 lshr_exprt(value, from_integer(8 * i, size_type())), field_type));
384 }
385}
386
398 exprt element,
399 const typet &field_type,
400 const namespacet &ns,
401 const messaget &log,
402 const bool is_union,
403 exprt::operandst &values)
404{
406 if(element.type().id() == ID_unsignedbv || element.type().id() == ID_signedbv)
407 {
408 exprt value = element;
409 if(is_union)
410 {
411 extract_bytes_of_bv(value, element.type(), field_type, values);
412 }
413 else
414 {
415 values.push_back(typecast_exprt::conditional_cast(value, field_type));
416 }
417 }
418 else
419 {
420 exprt value = compute_or_over_bytes(element, field_type, ns, log, is_union);
421 values.push_back(typecast_exprt::conditional_cast(value, field_type));
422 }
423}
424
432static exprt or_values(const exprt::operandst &values, const typet &field_type)
433{
434 if(values.size() == 1)
435 {
436 return values[0];
437 }
438 return multi_ary_exprt(ID_bitor, values, field_type);
439}
440
442 const exprt &expr,
443 const typet &field_type,
444 const namespacet &ns,
445 const messaget &log,
446 const bool is_union)
447{
448 INVARIANT(
449 can_cast_type<c_bool_typet>(field_type) ||
450 can_cast_type<bool_typet>(field_type),
451 "Can aggregate bytes with *or* only if the shadow memory type is _Bool.");
452
453 if(
454 expr.type().id() == ID_struct || expr.type().id() == ID_union ||
455 expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag)
456 {
457 const auto &components =
458 (expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag)
461 exprt::operandst values;
462 for(const auto &component : components)
463 {
464 if(component.get_is_padding())
465 {
466 continue;
467 }
469 member_exprt(expr, component), field_type, ns, log, is_union, values);
470 }
471 return or_values(values, field_type);
472 }
473 else if(expr.type().id() == ID_array)
474 {
475 const array_typet &array_type = to_array_type(expr.type());
476 if(array_type.size().is_constant())
477 {
478 exprt::operandst values;
479 const mp_integer size =
481 for(mp_integer index = 0; index < size; ++index)
482 {
484 index_exprt(expr, from_integer(index, array_type.index_type())),
485 field_type,
486 ns,
487 log,
488 is_union,
489 values);
490 }
491 return or_values(values, field_type);
492 }
493 else
494 {
495 log.warning()
496 << "Shadow memory: cannot compute or over variable-size array "
497 << format(expr) << messaget::eom;
498 }
499 }
500 exprt::operandst values;
501 if(is_union)
502 {
505 expr.type(),
506 field_type,
507 values);
508 }
509 else
510 {
511 values.push_back(typecast_exprt::conditional_cast(
512 conditional_cast_floatbv_to_unsignedbv(expr), field_type));
513 }
514 return or_values(values, field_type);
515}
516
525std::pair<exprt, exprt> compare_to_collection(
526 const std::vector<exprt>::const_iterator &expr_iterator,
527 const std::vector<exprt>::const_iterator &end)
528{
529 // We need at least an element in the collection
530 INVARIANT(expr_iterator != end, "Cannot compute max of an empty collection");
531 const exprt &current_expr = *expr_iterator;
532
533 // Iterator for the other elements in the collection in the interval denoted
534 // by `expr_iterator` and `end`.
535 std::vector<exprt>::const_iterator expr_to_compare_to =
536 std::next(expr_iterator);
537 if(expr_to_compare_to == end)
538 {
539 return {nil_exprt{}, current_expr};
540 }
541
542 std::vector<exprt> comparisons;
543 for(; expr_to_compare_to != end; ++expr_to_compare_to)
544 {
545 // Compare the current element with the n-th following it
546 comparisons.emplace_back(
547 binary_predicate_exprt(current_expr, ID_gt, *expr_to_compare_to));
548 }
549
550 return {and_exprt(comparisons), current_expr};
551}
552
559 const std::vector<std::pair<exprt, exprt>> &conditions_and_values)
560{
561 // We need at least one element
562 INVARIANT(
563 conditions_and_values.size() > 0,
564 "Cannot compute max of an empty collection");
565
566 // We use reverse-iterator, so the last element is the one in the last else
567 // case.
568 auto reverse_ite = conditions_and_values.rbegin();
569
570 // The last element must have `nil_exprt` as condition
571 INVARIANT(
572 reverse_ite->first == nil_exprt{},
573 "Last element of condition-value list must have nil_exprt condition.");
574
575 exprt res = std::move(reverse_ite->second);
576
577 for(++reverse_ite; reverse_ite != conditions_and_values.rend(); ++reverse_ite)
578 {
579 res = if_exprt(reverse_ite->first, reverse_ite->second, res);
580 }
581
582 return res;
583}
584
588static exprt create_max_expr(const std::vector<exprt> &values)
589{
590 std::vector<std::pair<exprt, exprt>> rows;
591 rows.reserve(values.size());
592 for(auto byte_it = values.begin(); byte_it != values.end(); ++byte_it)
593 {
594 // Create a pair condition-element where the condition is the comparison of
595 // the element with all the ones contained in the rest of the collection.
596 rows.emplace_back(compare_to_collection(byte_it, values.end()));
597 }
598
600}
601
603 const exprt &expr,
604 const typet &field_type,
605 const namespacet &ns)
606{
607 // Compute the bit-width of the type of `expr`.
608 std::size_t size = boolbv_widtht{ns}(expr.type());
609
610 // Compute how many bytes are in `expr`
611 std::size_t byte_count = size / config.ansi_c.char_width;
612
613 // Extract each byte of `expr` by using byte_extract.
614 std::vector<exprt> extracted_bytes;
615 extracted_bytes.reserve(byte_count);
616 for(std::size_t i = 0; i < byte_count; ++i)
617 {
618 extracted_bytes.emplace_back(make_byte_extract(
619 expr, from_integer(i, unsigned_long_int_type()), field_type));
620 }
621
622 // Compute the max of the bytes extracted from `expr`.
623 exprt max_expr = create_max_expr(extracted_bytes);
624
625 INVARIANT(
626 max_expr.type() == field_type,
627 "Aggregated max value type must be the same as shadow memory field's "
628 "type.");
629
630 return max_expr;
631}
632
634 const std::vector<std::pair<exprt, exprt>> &conds_values)
635{
637 !conds_values.empty(), "build_if_else_expr requires non-empty argument");
638 exprt result = nil_exprt();
639 for(const auto &cond_value : conds_values)
640 {
641 if(result.is_nil())
642 {
643 result = cond_value.second;
644 }
645 else
646 {
647 result = if_exprt(cond_value.first, cond_value.second, result);
648 }
649 }
650 return result;
651}
652
659static bool
660are_types_compatible(const typet &expr_type, const typet &shadow_type)
661{
662 if(expr_type.id() != ID_pointer || shadow_type.id() != ID_pointer)
663 return true;
664
665 // We filter out the particularly annoying case of char ** being definitely
666 // incompatible with char[].
667 const typet &expr_subtype = to_pointer_type(expr_type).base_type();
668 const typet &shadow_subtype = to_pointer_type(shadow_type).base_type();
669
670 if(
671 expr_subtype.id() == ID_pointer &&
672 to_pointer_type(expr_subtype).base_type().id() != ID_pointer &&
673 shadow_subtype.id() == ID_array &&
674 to_array_type(shadow_subtype).element_type().id() != ID_pointer)
675 {
676 return false;
677 }
678 if(
679 shadow_subtype.id() == ID_pointer &&
680 to_pointer_type(shadow_subtype).base_type().id() != ID_pointer &&
681 expr_subtype.id() != ID_pointer)
682 {
683 return false;
684 }
685 return true;
686}
687
691static void clean_string_constant(exprt &expr)
692{
693 const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr);
694 if(
695 index_expr && index_expr->index().is_zero() &&
696 can_cast_expr<string_constantt>(index_expr->array()))
697 {
698 expr = index_expr->array();
699 }
700}
701
706static void adjust_array_types(typet &type)
707{
709 if(!pointer_type)
710 {
711 return;
712 }
713 if(
714 const auto *array_type =
716 {
717 pointer_type->base_type() = array_type->element_type();
718 }
719 if(pointer_type->base_type().id() == ID_string_constant)
720 {
722 }
723}
724
732 const exprt &shadowed_address,
733 const exprt &matched_base_address,
734 const namespacet &ns,
735 const messaget &log)
736{
737 typet shadowed_address_type = shadowed_address.type();
738 adjust_array_types(shadowed_address_type);
739 exprt lhs =
740 typecast_exprt::conditional_cast(shadowed_address, shadowed_address_type);
742 matched_base_address, shadowed_address_type);
743 exprt base_cond = simplify_expr(equal_exprt(lhs, rhs), ns);
744 if(
745 base_cond.id() == ID_equal &&
746 to_equal_expr(base_cond).lhs() == to_equal_expr(base_cond).rhs())
747 {
748 return true_exprt();
749 }
750 if(base_cond.id() == ID_equal)
751 {
752 const equal_exprt &equal_expr = to_equal_expr(base_cond);
753 const bool equality_types_match =
754 equal_expr.lhs().type() == equal_expr.rhs().type();
756 equality_types_match,
757 "types of expressions on each side of equality should match",
758 irep_pretty_diagnosticst{equal_expr.lhs()},
759 irep_pretty_diagnosticst{equal_expr.rhs()});
760 }
761
762 return base_cond;
763}
764
771 const exprt &dereference_pointer,
772 const exprt &expr,
773 const namespacet &ns,
774 const messaget &log)
775{
776 typet expr_type = expr.type();
777 adjust_array_types(expr_type);
778 exprt expr_cond = simplify_expr(
780 typecast_exprt::conditional_cast(expr, expr_type),
781 typecast_exprt::conditional_cast(dereference_pointer, expr_type)),
782 ns);
783 if(
784 expr_cond.id() == ID_equal &&
785 to_equal_expr(expr_cond).lhs() == to_equal_expr(expr_cond).rhs())
786 {
787 return true_exprt();
788 }
789 if(expr_cond.id() == ID_equal)
790 {
791 const equal_exprt &equal_expr = to_equal_expr(expr_cond);
792 const bool equality_types_match =
793 equal_expr.lhs().type() == equal_expr.rhs().type();
795 equality_types_match,
796 "types of expressions on each side of equality should match",
797 irep_pretty_diagnosticst{equal_expr.lhs()},
798 irep_pretty_diagnosticst{equal_expr.rhs()});
799 }
800 return expr_cond;
801}
802
814 const exprt &shadow,
815 const object_descriptor_exprt &matched_base_descriptor,
816 const exprt &expr,
817 const namespacet &ns,
818 const messaget &log)
819{
820 object_descriptor_exprt shadowed_object = matched_base_descriptor;
821 shadowed_object.object() = shadow;
822 value_set_dereferencet::valuet shadow_dereference =
823 value_set_dereferencet::build_reference_to(shadowed_object, expr, ns);
824#ifdef DEBUG_SHADOW_MEMORY
825 log.debug() << "Shadow memory: shadow-deref: "
826 << format(shadow_dereference.value) << messaget::eom;
827#endif
828 return shadow_dereference;
829}
830
831/* foreach shadowed_address in SM:
832 * if(incompatible(shadow.object, object)) continue; // Type incompatibility
833 * base_match = object == shadow_object; // Do the base obj match the SM obj
834 * if(!base_match) continue;
835 * if(object is null) continue; // Done in the caller
836 * if(type_of(dereference object is void)
837 * // we terminate as we don't know how big is the memory at that location
838 * shadowed_dereference.pointer = deref(shadow.shadowed_object, expr);
839 * aggregate the object depending on the type
840 * expr_match = shadowed_dereference == expr
841 * if(!expr_match)
842 * continue;
843 * shadow_dereference = deref(shadow.object, expr);
844 * if(expr_match)
845 * result = shadow_dereference.value [exact match]
846 * break;
847 * if(base_match) [shadow memory matches]
848 * result += (expr_match, shadow_dereference.value)
849 * break;
850 * result += (base_match & expr_match, shadow_dereference.value)
851*/
852std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
853 const namespacet &ns,
854 const messaget &log,
855 const exprt &matched_object,
856 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
857 const typet &field_type,
858 const exprt &expr,
859 const typet &lhs_type,
860 bool &exact_match)
861{
862 std::vector<std::pair<exprt, exprt>> result;
863
864 for(const auto &shadowed_address : addresses)
865 {
866 log_try_shadow_address(ns, log, shadowed_address);
867 if(!are_types_compatible(expr.type(), shadowed_address.address.type()))
868 {
869 log_are_types_incompatible(ns, expr, shadowed_address, log);
870 continue;
871 }
872 const object_descriptor_exprt &matched_base_descriptor =
873 to_object_descriptor_expr(matched_object);
874 exprt matched_base_address =
875 address_of_exprt(matched_base_descriptor.object());
876 clean_string_constant(to_address_of_expr(matched_base_address).op());
877
878 // NULL has already been handled in the caller; skip.
879 if(matched_base_descriptor.object().id() == ID_null_object)
880 {
881 continue;
882 }
883
884 // Used only to check if the pointer is `void`
886 value_set_dereferencet::build_reference_to(matched_object, expr, ns);
887
888 if(is_void_pointer(dereference.pointer.type()))
889 {
890 std::stringstream s;
891 s << "Shadow memory: cannot get shadow memory via type void* for "
892 << format(expr)
893 << ". Insert a cast to the type that you want to access.";
894 throw invalid_input_exceptiont(s.str());
895 }
896
897 // Replace original memory with the shadow object (symbolic dereferencing is
898 // performed during symex later on).
899 const value_set_dereferencet::valuet shadow_dereference =
901 shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
903 ns,
904 log,
905 shadowed_address,
906 matched_base_address,
908 expr,
909 shadow_dereference);
910
911 const bool is_union = matched_base_descriptor.type().id() == ID_union ||
912 matched_base_descriptor.type().id() == ID_union_tag;
913
914 exprt value;
915 // Aggregate the value depending on the type
916 if(field_type.id() == ID_c_bool || field_type.id() == ID_bool)
917 {
918 // Value is of bool type, so aggregate with or.
921 shadow_dereference.value, field_type, ns, log, is_union),
922 lhs_type);
923 }
924 else
925 {
926 // Value is of other (bitvector) type, so aggregate with max
927 value = compute_max_over_bytes(shadow_dereference.value, field_type, ns);
928 }
929
930 const exprt base_cond = get_matched_base_cond(
931 shadowed_address.address, matched_base_address, ns, log);
932 shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
933 if(base_cond.is_false())
934 {
935 continue;
936 }
937
938 const exprt expr_cond =
939 get_matched_expr_cond(dereference.pointer, expr, ns, log);
940 if(expr_cond.is_false())
941 {
942 continue;
943 }
944
945 if(base_cond.is_true() && expr_cond.is_true())
946 {
947#ifdef DEBUG_SHADOW_MEMORY
948 log.debug() << "exact match" << messaget::eom;
949#endif
950 exact_match = true;
951 result.clear();
952 result.emplace_back(base_cond, value);
953 break;
954 }
955
956 if(base_cond.is_true())
957 {
958 // No point looking at further shadow addresses
959 // as only one of them can match.
960#ifdef DEBUG_SHADOW_MEMORY
961 log.debug() << "base match" << messaget::eom;
962#endif
963 result.clear();
964 result.emplace_back(expr_cond, value);
965 break;
966 }
967 else
968 {
969#ifdef DEBUG_SHADOW_MEMORY
970 log.debug() << "conditional match" << messaget::eom;
971#endif
972 result.emplace_back(and_exprt(base_cond, expr_cond), value);
973 }
974 }
975 return result;
976}
977
978// Unfortunately.
981{
982 if(expr.object().id() == ID_symbol)
983 {
984 return expr;
985 }
986 if(expr.offset().id() == ID_unknown)
987 {
988 return expr;
989 }
990
991 object_descriptor_exprt result = expr;
992 mp_integer offset =
994 exprt object = expr.object();
995
996 while(true)
997 {
998 if(object.id() == ID_index)
999 {
1000 const index_exprt &index_expr = to_index_expr(object);
1001 mp_integer index =
1003
1004 offset += *pointer_offset_size(index_expr.type(), ns) * index;
1005 object = index_expr.array();
1006 }
1007 else if(object.id() == ID_member)
1008 {
1009 const member_exprt &member_expr = to_member_expr(object);
1010 const auto &struct_op = member_expr.struct_op();
1011 const struct_typet &struct_type =
1012 struct_op.type().id() == ID_struct_tag
1013 ? ns.follow_tag(to_struct_tag_type(struct_op.type()))
1014 : to_struct_type(struct_op.type());
1015 offset +=
1016 *member_offset(struct_type, member_expr.get_component_name(), ns);
1017 object = struct_op;
1018 }
1019 else
1020 {
1021 break;
1022 }
1023 }
1024 result.object() = object;
1025 result.offset() = from_integer(offset, expr.offset().type());
1026 return result;
1027}
1028
1030 const namespacet &ns,
1031 const messaget &log,
1032 const std::vector<exprt> &value_set,
1033 const exprt &expr)
1034{
1035 INVARIANT(
1037 "Cannot check if value_set contains only NULL as `expr` type is not a "
1038 "pointer.");
1039 const null_pointer_exprt null_pointer(to_pointer_type(expr.type()));
1040 if(value_set.size() == 1 && contains_null_or_invalid(value_set, null_pointer))
1041 {
1042 log_value_set_contains_only_null(log, ns, expr, null_pointer);
1043 return true;
1044 }
1045 return false;
1046}
1047
1049static std::vector<std::pair<exprt, exprt>>
1051 const exprt &expr,
1052 const exprt &matched_object,
1053 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1054 const namespacet &ns,
1055 const messaget &log,
1056 bool &exact_match)
1057{
1058 std::vector<std::pair<exprt, exprt>> result;
1059 for(const auto &shadowed_address : addresses)
1060 {
1061 log_try_shadow_address(ns, log, shadowed_address);
1062
1063 if(!are_types_compatible(expr.type(), shadowed_address.address.type()))
1064 {
1065 log_shadow_memory_incompatible_types(log, ns, expr, shadowed_address);
1066 continue;
1067 }
1068
1069 object_descriptor_exprt matched_base_descriptor =
1070 normalize(to_object_descriptor_expr(matched_object), ns);
1071
1074 matched_base_descriptor, expr, ns);
1075
1076 exprt matched_base_address =
1077 address_of_exprt(matched_base_descriptor.object());
1078 clean_string_constant(to_address_of_expr(matched_base_address).op());
1079
1080 // NULL has already been handled in the caller; skip.
1081 if(matched_base_descriptor.object().id() == ID_null_object)
1082 {
1083 continue;
1084 }
1085 const value_set_dereferencet::valuet shadow_dereference =
1087 shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
1089 ns,
1090 log,
1091 shadowed_address,
1092 matched_base_address,
1094 expr,
1095 shadow_dereference);
1096
1097 const exprt base_cond = get_matched_base_cond(
1098 shadowed_address.address, matched_base_address, ns, log);
1099 shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
1100 if(base_cond.is_false())
1101 {
1102 continue;
1103 }
1104
1105 const exprt expr_cond =
1106 get_matched_expr_cond(dereference.pointer, expr, ns, log);
1107 if(expr_cond.is_false())
1108 {
1109 continue;
1110 }
1111
1112 if(base_cond.is_true() && expr_cond.is_true())
1113 {
1114 log_shadow_memory_message(log, "exact match");
1115
1116 exact_match = true;
1117 result.clear();
1118 result.push_back({base_cond, shadow_dereference.pointer});
1119 break;
1120 }
1121
1122 if(base_cond.is_true())
1123 {
1124 // No point looking at further shadow addresses
1125 // as only one of them can match.
1126 log_shadow_memory_message(log, "base match");
1127
1128 result.clear();
1129 result.emplace_back(expr_cond, shadow_dereference.pointer);
1130 break;
1131 }
1132 else
1133 {
1134 log_shadow_memory_message(log, "conditional match");
1135 result.emplace_back(
1136 and_exprt(base_cond, expr_cond), shadow_dereference.pointer);
1137 }
1138 }
1139 return result;
1140}
1141
1142std::optional<exprt> get_shadow_memory(
1143 const exprt &expr,
1144 const std::vector<exprt> &value_set,
1145 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1146 const namespacet &ns,
1147 const messaget &log,
1148 size_t &mux_size)
1149{
1150 std::vector<std::pair<exprt, exprt>> conds_values;
1151 for(const auto &matched_object : value_set)
1152 {
1153 if(matched_object.id() != ID_object_descriptor)
1154 {
1155 log.warning() << "Shadow memory: value set contains unknown for "
1156 << format(expr) << messaget::eom;
1157 continue;
1158 }
1159 if(
1160 to_object_descriptor_expr(matched_object).root_object().id() ==
1161 ID_integer_address)
1162 {
1163 log.warning() << "Shadow memory: value set contains integer_address for "
1164 << format(expr) << messaget::eom;
1165 continue;
1166 }
1167 if(matched_object.type().get_bool(ID_C_is_failed_symbol))
1168 {
1169 log.warning() << "Shadow memory: value set contains failed symbol for "
1170 << format(expr) << messaget::eom;
1171 continue;
1172 }
1173
1174 bool exact_match = false;
1175 auto per_value_set_conds_values = get_shadow_memory_for_matched_object(
1176 expr, matched_object, addresses, ns, log, exact_match);
1177
1178 if(!per_value_set_conds_values.empty())
1179 {
1180 if(exact_match)
1181 {
1182 conds_values.clear();
1183 }
1184 conds_values.insert(
1185 conds_values.begin(),
1186 per_value_set_conds_values.begin(),
1187 per_value_set_conds_values.end());
1188 mux_size += conds_values.size() - 1;
1189 if(exact_match)
1190 {
1191 break;
1192 }
1193 }
1194 }
1195 if(!conds_values.empty())
1196 {
1197 return build_if_else_expr(conds_values);
1198 }
1199 return {};
1200}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
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
unsignedbv_typet size_type()
Definition c_types.cpp:50
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
bitvector_typet char_type()
Definition c_types.cpp:106
bool can_cast_type< c_bool_typet >(const typet &type)
Check whether a reference to a typet is a c_bool_typet.
Definition c_types.h:115
Operator to return the address of an object.
Boolean AND.
Definition std_expr.h:2120
Arrays with given size.
Definition std_types.h:807
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:33
const exprt & size() const
Definition std_types.h:840
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
std::size_t get_width() const
Definition std_types.h:920
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:1361
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
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:2370
Array index operator.
Definition std_expr.h:1465
exprt & index()
Definition std_expr.h:1505
exprt & array()
Definition std_expr.h:1495
Thrown when user-provided input cannot be processed.
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
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:2841
const exprt & struct_op() const
Definition std_expr.h:2879
irep_idt get_component_name() const
Definition std_expr.h:2863
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & debug() const
Definition message.h:421
mstreamt & warning() const
Definition message.h:396
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: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:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
The NIL expression.
Definition std_expr.h:3073
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
void set_expression(exprt expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
Definition ssa_expr.cpp:138
const exprt & get_original_expr() const
Definition ssa_expr.h:33
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
The Boolean constant true.
Definition std_expr.h:3055
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
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
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
static format_containert< T > format(const T &o)
Definition format.h:37
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)
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
bool can_cast_expr< dereference_exprt >(const exprt &base)
bool can_cast_expr< address_of_exprt >(const exprt &base)
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:80
API to expression classes.
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition std_expr.h:2086
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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2933
bool can_cast_expr< index_exprt >(const exprt &base)
Definition std_expr.h:1517
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:256
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 equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1402
bool can_cast_type< bool_typet >(const typet &base)
Definition std_types.h:44
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition std_types.h:875
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
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition std_types.h:943
bool can_cast_expr< string_constantt >(const exprt &base)
std::size_t char_width
Definition config.h:140
Pointer Dereferencing.