Get a list of (condition, value) pairs for a certain pointer from the shadow memory, where each pair denotes the value of the pointer expression if the condition evaluates to true.

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.

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_set.

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 _Bool.

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 signed/unsigned bitvector (where the value is arbitrary up until the max represented by the bitvector size).

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.

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.

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.

Detailed Description

Symex Shadow Memory Instrumentation Utilities.

Definition in file shadow_memory_util.h.

Function Documentation

◆ build_if_else_expr()

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.

Parameters: conds_values Contains pairs <e1, e2>, where e1 is going to be used as an antecedent for an if_expr, and e2 is going to be used as the consequent.

Returns: An if_exprt of the form if e1 then e2 else if e3 then e4 else ...

Note: the expression created will not have the first condition as the first element will serve fallback if all the other conditions are false.

Definition at line 632 of file shadow_memory_util.cpp.

◆ check_value_set_contains_only_null_ptr()

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.

Parameters: ns the namespace within which we're going to perform symbol lookups

log the message log to which we're going to print debugging messages, if debugging is set

value_set the collection to check if it contains only the NULL pointer

expr a pointer-typed expression

Returns: true if value_set contains only a NULL pointer expression

Definition at line 1028 of file shadow_memory_util.cpp.

◆ clean_pointer_expr()

void clean_pointer_expr ( exprt & expr )

Clean the given pointer expression so that it has the right shape for being used for identifying shadow memory.

This handles some quirks regarding array sizes containing L2 symbols and string constants not having char-pointer type.

Parameters: expr The pointer to the original memory, e.g. as passed to __CPROVER_field_get.

Definition at line 253 of file shadow_memory_util.cpp.

◆ compute_max_over_bytes()

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 signed/unsigned bitvector (where the value is arbitrary up until the max represented by the bitvector size).

Parameters: expr the expression to extract the max from

field_type the type of the shadow memory field to return

ns the namespace to perform type-lookups into

Returns: the aggregated max byte-sized value contained in expr Note that the expr type size must be known at compile time.

Definition at line 601 of file shadow_memory_util.cpp.

◆ compute_or_over_bytes()

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 _Bool.

Parameters: expr the type to compute the or over each of its bytes

field_type the type of the shadow memory (must be c_bool or bool)

ns the namespace within which we're going to perform symbol lookups

log the message log to which we're going to print debugging messages, if debugging is set

is_union true if the expression expr is part of a union.

Returns: the aggregated or byte-sized value contained in expr

Definition at line 440 of file shadow_memory_util.cpp.

◆ contains_null_or_invalid()

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_set.

Parameters: address A pointer expressions that we are using as the query.

value_set The search space for the query.

Returns: true if the object can be null or invalid in the value set, false otherwise.

Definition at line 319 of file shadow_memory_util.cpp.

◆ deref_expr()

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 just unboxes it and returns its content.

Definition at line 243 of file shadow_memory_util.cpp.

◆ extract_field_name()

irep_idt extract_field_name ( const exprt & string_expr )

Extracts the field name identifier from a string expression, e.g.

as passed as argument to a __CPROVER_field_decl_local call.

Parameters: string_expr The string argument expression

Returns: The identifier denoted by the string argument expression

Definition at line 213 of file shadow_memory_util.cpp.

◆ get_field_init_expr()

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.

Parameters: field_name The field whose initialisation expression we want to retrieve.

state The goto symex state within which we want to search for the expression.

Returns: The expression the field was initialised with.

Definition at line 300 of file shadow_memory_util.cpp.

◆ get_field_init_type()

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.

Parameters: field_name The name of the field whose value type we want to query.

state The symex_state within which the query is executed (the field's value is looked up).

Returns: The type of the value the field was initialised with (actually, the type of the value the field currently is associated with, but it's invariant since the declaration).

Definition at line 313 of file shadow_memory_util.cpp.

◆ get_shadow_dereference_candidates()

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, where each pair denotes the value of the pointer expression if the condition evaluates to true.

Returns: A vector of pair<expr, expr> corresponding to a condition and value. (See above for explanation).

Definition at line 851 of file shadow_memory_util.cpp.

◆ get_shadow_memory()

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.

Returns: if potential values are present for that object inside the value set, then we get back an if e1 then e2 else (if e3 else e4... expression, where e1, e3, ... are guards (conditions) and e2, e4, etc are the possible values of the object within the value set.

Definition at line 1141 of file shadow_memory_util.cpp.

◆ replace_invalid_object_by_null()

void replace_invalid_object_by_null ( exprt & expr )

Replace an invalid object by a null pointer.

Works recursively on the operands (child nodes) of the expression, as well.

Parameters: expr The (root) expression where substitution will happen.

Definition at line 281 of file shadow_memory_util.cpp.

◆ shadow_memory_log_get_field()

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.

Mainly used for debugging purposes.

Definition at line 49 of file shadow_memory_util.cpp.

◆ shadow_memory_log_set_field()

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.

Mainly for use for debugging purposes.

Definition at line 32 of file shadow_memory_util.cpp.

◆ shadow_memory_log_text_and_expr()

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.

The log will be a specific message given to it, along with an expression passed along to it.

Definition at line 96 of file shadow_memory_util.cpp.

◆ shadow_memory_log_value_set()

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.

Mainly for use for debugging purposes. Dual to shadow_memory_log_get_field.

Definition at line 64 of file shadow_memory_util.cpp.

◆ shadow_memory_log_value_set_match()

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.

Definition at line 80 of file shadow_memory_util.cpp.