CBMC
|
Symex Shadow Memory Instrumentation Utilities. More...
#include "shadow_memory_util.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/format_expr.h>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/pointer_offset_size.h>
#include <util/ssa_expr.h>
#include <util/std_expr.h>
#include <util/string_constant.h>
#include <langapi/language_util.h>
#include <pointer-analysis/value_set_dereference.h>
#include <solvers/flattening/boolbv_width.h>
Go to the source code of this file.
Functions | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
static void | log_are_types_incompatible (const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address, const messaget &log) |
static void | log_value_set_contains_only_null (const messaget &log, const namespacet &ns, const exprt &expr, const exprt &null_pointer) |
static void | log_shadow_memory_incompatible_types (const messaget &log, const namespacet &ns, const exprt &expr, const shadow_memory_statet::shadowed_addresst &shadowed_address) |
irep_idt | extract_field_name (const exprt &string_expr) |
Extracts the field name identifier from a string expression, e.g. More... | |
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. More... | |
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. More... | |
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. More... | |
void | replace_invalid_object_by_null (exprt &expr) |
Replace an invalid object by a null pointer. More... | |
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. More... | |
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. More... | |
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. More... | |
static exprt | conditional_cast_floatbv_to_unsignedbv (const exprt &value) |
Casts a given (float) bitvector expression to an unsigned bitvector. More... | |
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 array values. More... | |
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. More... | |
static exprt | or_values (const exprt::operandst &values, const typet &field_type) |
Translate a list of values into an or expression. More... | |
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. More... | |
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 collection (or nil_exprt if none) and return a pair (condition, element) such that if the condition is true , then the element is the max of the collection in the interval denoted by expr_iterator and end . More... | |
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 as (cond_1 ? val_1 : (cond_2 ? val_2 : ... More... | |
static exprt | create_max_expr (const std::vector< exprt > &values) |
Create an expression encoding the max operation over the collection values More... | |
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). More... | |
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. More... | |
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. More... | |
static void | clean_string_constant (exprt &expr) |
Simplify &string_constant[0] to &string_constant to facilitate expression equality for exact matching. More... | |
static void | adjust_array_types (typet &type) |
Flattens type of the form pointer_type(array_type(element_type)) to pointer_type(element_type) and pointer_type(string_constant_type) to pointer_type(char) . More... | |
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, simplifies the comparison expression and if the lhs and rhs are structurally identical returns true, otherwise returns the comparison. More... | |
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 expression and if the lhs and rhs are structurally identical returns true, otherwise returns the comparison. More... | |
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. More... | |
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 . More... | |
static object_descriptor_exprt | normalize (const object_descriptor_exprt &expr, const namespacet &ns) |
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. More... | |
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. More... | |
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. More... | |
Symex Shadow Memory Instrumentation Utilities.
Definition in file shadow_memory_util.cpp.
|
static |
Flattens type of the form pointer_type(array_type(element_type))
to pointer_type(element_type)
and pointer_type(string_constant_type)
to pointer_type(char)
.
type
will be changed. Definition at line 704 of file shadow_memory_util.cpp.
Checks given types (object type and shadow memory field type) for equality.
We're inspecting only pointer types here - if the two types given are not pointer types, then we assume it to be vacuously true.
expr_type | The type of the real object. |
shadow_type | The type of the shadow memory field's value. |
Definition at line 658 of file shadow_memory_util.cpp.
Build an if-then-else chain from a vector containing pairs of expressions.
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. |
if e1 then e2 else if e3 then e4 else ...
false
. Definition at line 631 of file shadow_memory_util.cpp.
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.
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 |
true
if value_set contains only a NULL
pointer expression Definition at line 1027 of file shadow_memory_util.cpp.
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.
expr | The pointer to the original memory, e.g. as passed to __CPROVER_field_get. |
Definition at line 252 of file shadow_memory_util.cpp.
|
static |
Simplify &string_constant[0] to &string_constant to facilitate expression equality for exact matching.
Definition at line 689 of file shadow_memory_util.cpp.
|
static |
Combine each (condition, value) element in the input collection into a if-then-else expression such as (cond_1 ? val_1 : (cond_2 ? val_2 : ...
: val_n))
conditions_and_values | collection containing codnition-value pairs |
Definition at line 556 of file shadow_memory_util.cpp.
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 collection (or nil_exprt
if none) and return a pair (condition, element)
such that if the condition is true
, then the element is the max of the collection in the interval denoted by expr_iterator
and end
.
expr_iterator | the iterator pointing at the element to compare to. |
end | the end of collection iterator. |
Definition at line 523 of file shadow_memory_util.cpp.
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).
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 |
Definition at line 600 of file shadow_memory_util.cpp.
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.
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. |
or
byte-sized value contained in expr Definition at line 439 of file shadow_memory_util.cpp.
Casts a given (float) bitvector expression to an unsigned bitvector.
value | The expression that we are to conditionally cast. |
id
otherwise. Definition at line 347 of file shadow_memory_util.cpp.
Given a pointer expression check to see if it can be a null pointer or an invalid object within value_set.
address | A pointer expressions that we are using as the query. |
value_set | The search space for the query. |
Definition at line 318 of file shadow_memory_util.cpp.
Create an expression encoding the max operation over the collection values
values | an exprt that encodes the max of values |
exprt
encoding the max operation over the collection values
Definition at line 586 of file shadow_memory_util.cpp.
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 242 of file shadow_memory_util.cpp.
|
static |
Extract byte-sized elements from the input bitvector-typed expression value and places them into the array values.
value | the bitvector typed expression to extract the bytes from |
type | the type of the expression expr (it must be bitvector) |
field_type | the type of the shadow memory |
values | the vector where all the extracted bytes of value will be placed. |
Definition at line 366 of file shadow_memory_util.cpp.
|
static |
Extract the components from the input expression value and places them into the array values.
element | the expression to extract the bytes from |
field_type | the type of the shadow memory |
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 element is part of a union |
values | the vector where all the extracted components of element will be placed. |
Definition at line 395 of file shadow_memory_util.cpp.
Extracts the field name identifier from a string expression, e.g.
as passed as argument to a __CPROVER_field_decl_local call.
string_expr | The string argument expression |
Definition at line 212 of file shadow_memory_util.cpp.
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.
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. |
Definition at line 299 of file shadow_memory_util.cpp.
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.
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). |
Definition at line 312 of file shadow_memory_util.cpp.
|
static |
Function that compares the two arguments shadowed_address and matched_base_address, simplifies the comparison expression and if the lhs and rhs are structurally identical returns true, otherwise returns the comparison.
Definition at line 729 of file shadow_memory_util.cpp.
|
static |
Function that compares the two arguments dereference_pointer and expr, simplifies the comparison expression and if the lhs and rhs are structurally identical returns true, otherwise returns the comparison.
Definition at line 768 of file shadow_memory_util.cpp.
|
static |
Retrieve the shadow value a pointer expression may point to.
shadow | The shadow expression. |
matched_base_descriptor | The base descriptor for the shadow object. |
expr | The pointer expression. |
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. |
valuet
object denoting the dereferenced object within shadow memory, guarded by a appropriate condition (of the form pointer == &shadow_object). Definition at line 811 of file shadow_memory_util.cpp.
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
.
Definition at line 850 of file shadow_memory_util.cpp.
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.
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 1140 of file shadow_memory_util.cpp.
|
static |
Used for set_field and shadow memory copy.
Definition at line 1048 of file shadow_memory_util.cpp.
|
static |
Definition at line 167 of file shadow_memory_util.cpp.
|
static |
Definition at line 198 of file shadow_memory_util.cpp.
|
static |
Generic logging function to log a text if DEBUG_SHADOW_MEMORY is defined.
Definition at line 160 of file shadow_memory_util.cpp.
|
static |
Log trying out a match between an object and a (target) shadow address.
Definition at line 145 of file shadow_memory_util.cpp.
|
static |
Definition at line 181 of file shadow_memory_util.cpp.
|
static |
Log a match between an address and the value set.
This version of the function reports more details, including the base address, the pointer and the shadow value.
Definition at line 113 of file shadow_memory_util.cpp.
|
static |
Definition at line 978 of file shadow_memory_util.cpp.
|
static |
Translate a list of values into an or expression.
Used here in the implementation of aggregation of boolean-typed fields.
field_type | The type of the values of the or expression (expected to be the same). |
values | A list (std::vector) of values collected previously, passed through immediately to the constructed expression as operands. |
Definition at line 430 of file shadow_memory_util.cpp.
|
static |
If the given type is an array type, then remove the L2 level renaming from its size.
type | Type to be modified |
Definition at line 233 of file shadow_memory_util.cpp.
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.
expr | The (root) expression where substitution will happen. |
Definition at line 280 of file shadow_memory_util.cpp.
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 48 of file shadow_memory_util.cpp.
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 31 of file shadow_memory_util.cpp.
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 95 of file shadow_memory_util.cpp.
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 63 of file shadow_memory_util.cpp.
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 79 of file shadow_memory_util.cpp.