38#ifdef DEBUG_SHADOW_MEMORY
39 log.conditional_output(
41 mstream <<
"Shadow memory: set_field: " << id2string(field_name)
42 <<
" for " << format(expr) <<
" to " << format(value)
54#ifdef DEBUG_SHADOW_MEMORY
55 log.conditional_output(
57 mstream <<
"Shadow memory: get_field: " << id2string(field_name)
58 <<
" for " << format(expr) << messaget::eom;
66 const std::vector<exprt> &value_set)
68#ifdef DEBUG_SHADOW_MEMORY
69 log.conditional_output(
71 for(const auto &e : value_set)
73 mstream <<
"Shadow memory: value_set: " << format(e) << messaget::eom;
86#ifdef DEBUG_SHADOW_MEMORY
87 log.conditional_output(
89 mstream <<
"Shadow memory: value_set_match: " << format(address)
90 <<
" <-- " << format(expr) << messaget::eom;
101#ifdef DEBUG_SHADOW_MEMORY
102 log.conditional_output(
104 mstream <<
"Shadow memory: " << text <<
": " << format(expr)
122#ifdef DEBUG_SHADOW_MEMORY
123 log.conditional_output(
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;
150#ifdef DEBUG_SHADOW_MEMORY
151 log.conditional_output(
153 mstream <<
"Shadow memory: trying shadowed address: "
154 << format(shadowed_address.address) << messaget::eom;
162#ifdef DEBUG_SHADOW_MEMORY
173#ifdef DEBUG_SHADOW_MEMORY
174 log.debug() <<
"Shadow memory: incompatible types "
187#ifdef DEBUG_SHADOW_MEMORY
188 log.conditional_output(
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"
204#ifdef DEBUG_SHADOW_MEMORY
205 log.debug() <<
"Shadow memory: incompatible types "
319 const std::vector<exprt> &value_set,
320 const exprt &address)
324 for(
const auto &e : value_set)
336 for(
const auto &e : value_set)
369 const typet &field_type,
374 "Cannot combine with *or* elements of a non-bitvector type.");
378 for(
size_t i = 1; i < size; ++i)
397 const typet &field_type,
406 exprt value = element;
432 if(values.size() == 1)
441 const typet &field_type,
449 "Can aggregate bytes with *or* only if the shadow memory type is _Bool.");
455 const auto &components =
479 for(
mp_integer index = 0; index < size; ++index)
494 <<
"Shadow memory: cannot compute or over variable-size array "
525 const std::vector<exprt>::const_iterator &end)
562 "Cannot compute max of an empty collection");
571 "Last element of condition-value list must have nil_exprt condition.");
588 std::vector<std::pair<exprt, exprt>>
rows;
589 rows.reserve(values.size());
602 const typet &field_type,
625 "Aggregated max value type must be the same as shadow memory field's "
632 const std::vector<std::pair<exprt, exprt>> &
conds_values)
635 !
conds_values.empty(),
"build_if_else_expr requires non-empty argument");
641 result = cond_value.second;
645 result =
if_exprt(cond_value.first, cond_value.second, result);
755 "types of expressions on each side of equality should match",
794 "types of expressions on each side of equality should match",
822#ifdef DEBUG_SHADOW_MEMORY
823 log.debug() <<
"Shadow memory: shadow-deref: "
854 const std::vector<shadow_memory_statet::shadowed_addresst> &
addresses,
855 const typet &field_type,
860 std::vector<std::pair<exprt, exprt>> result;
889 s <<
"Shadow memory: cannot get shadow memory via type void* for "
891 <<
". Insert a cast to the type that you want to access.";
945#ifdef DEBUG_SHADOW_MEMORY
958#ifdef DEBUG_SHADOW_MEMORY
967#ifdef DEBUG_SHADOW_MEMORY
1022 result.
object() = object;
1030 const std::vector<exprt> &value_set,
1035 "Cannot check if value_set contains only NULL as `expr` type is not a "
1047static std::vector<std::pair<exprt, exprt>>
1051 const std::vector<shadow_memory_statet::shadowed_addresst> &
addresses,
1056 std::vector<std::pair<exprt, exprt>> result;
1133 result.emplace_back(
1142 const std::vector<exprt> &value_set,
1143 const std::vector<shadow_memory_statet::shadowed_addresst> &
addresses,
1153 log.warning() <<
"Shadow memory: value set contains unknown for "
1161 log.warning() <<
"Shadow memory: value set contains integer_address for "
1167 log.warning() <<
"Shadow memory: value set contains failed symbol for "
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()
unsignedbv_typet unsigned_long_int_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
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.
Base class for all expressions.
std::vector< exprt > operandst
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
Central data structure: state.
shadow_memory_statet shadow_memory
The trinary if-then-else operator.
const irep_idt & id() const
Extract member of struct or union.
Class that provides messages with a built-in verbosity 'level'.
A base class for multi-ary expressions Associativity is not specified.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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.
Structure type, corresponds to C style structs.
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
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)
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...
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)
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.
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)
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)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
#define POSTCONDITION(CONDITION)
#define UNREACHABLE_BECAUSE(REASON)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
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.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.