39#ifdef DEBUG_SHADOW_MEMORY
42 mstream <<
"Shadow memory: set_field: " << id2string(field_name)
43 <<
" for " << format(expr) <<
" to " << format(value)
55#ifdef DEBUG_SHADOW_MEMORY
58 mstream <<
"Shadow memory: get_field: " << id2string(field_name)
59 <<
" for " << format(expr) << messaget::eom;
67 const std::vector<exprt> &value_set)
69#ifdef DEBUG_SHADOW_MEMORY
72 for(const auto &e : value_set)
74 mstream <<
"Shadow memory: value_set: " << format(e) << messaget::eom;
87#ifdef DEBUG_SHADOW_MEMORY
90 mstream <<
"Shadow memory: value_set_match: " << format(address)
91 <<
" <-- " << format(expr) << messaget::eom;
102#ifdef DEBUG_SHADOW_MEMORY
105 mstream <<
"Shadow memory: " << text <<
": " << format(expr)
118 const exprt &matched_base_address,
123#ifdef DEBUG_SHADOW_MEMORY
130 matched_base_address,
132 mstream <<
"Shadow memory: value_set_match: " << messaget::eom;
133 mstream <<
"Shadow memory: base: " << format(shadowed_address.address)
134 <<
" <-- " << format(matched_base_address) << messaget::eom;
135 mstream <<
"Shadow memory: cell: " << format(dereference.pointer)
136 <<
" <-- " << format(expr) << messaget::eom;
137 mstream <<
"Shadow memory: shadow_ptr: "
138 << format(shadow_dereference.pointer) << messaget::eom;
139 mstream <<
"Shadow memory: shadow_val: "
140 << format(shadow_dereference.value) << messaget::eom;
151#ifdef DEBUG_SHADOW_MEMORY
154 mstream <<
"Shadow memory: trying shadowed address: "
155 << format(shadowed_address.address) << messaget::eom;
163#ifdef DEBUG_SHADOW_MEMORY
174#ifdef DEBUG_SHADOW_MEMORY
175 log.
debug() <<
"Shadow memory: incompatible types "
186 const exprt &null_pointer)
188#ifdef DEBUG_SHADOW_MEMORY
191 mstream <<
"Shadow memory: value set match: " << format(null_pointer)
192 <<
" <-- " << format(expr) << messaget::eom;
193 mstream <<
"Shadow memory: ignoring set field on NULL object"
205#ifdef DEBUG_SHADOW_MEMORY
206 log.
debug() <<
"Shadow memory: incompatible types "
223 return string_expr.
get(ID_value);
265 if(expr.
id() == ID_string_constant)
284 expr.
id() == ID_symbol && expr.
type().
id() == ID_pointer &&
305 return field_type_it->second;
309 return field_type_it->second;
316 return field_init_expr.
type();
320 const std::vector<exprt> &value_set,
321 const exprt &address)
325 for(
const auto &e : value_set)
327 if(e.id() != ID_object_descriptor)
331 if(expr.
id() == ID_null_object)
337 for(
const auto &e : value_set)
339 if(e.id() == ID_unknown || e.id() == ID_object_descriptor)
350 if(value.
type().
id() != ID_floatbv)
370 const typet &field_type,
375 "Cannot combine with *or* elements of a non-bitvector type.");
379 for(
size_t i = 1; i < size; ++i)
398 const typet &field_type,
405 if(element.
type().
id() == ID_unsignedbv || element.
type().
id() == ID_signedbv)
407 exprt value = element;
433 if(values.size() == 1)
442 const typet &field_type,
450 "Can aggregate bytes with *or* only if the shadow memory type is _Bool.");
453 expr.
type().
id() == ID_struct || expr.
type().
id() == ID_union ||
454 expr.
type().
id() == ID_struct_tag || expr.
type().
id() == ID_union_tag)
456 const auto &components =
457 (expr.
type().
id() == ID_struct_tag || expr.
type().
id() == ID_union_tag)
472 else if(expr.
type().
id() == ID_array)
480 for(
mp_integer index = 0; index < size; ++index)
495 <<
"Shadow memory: cannot compute or over variable-size array "
525 const std::vector<exprt>::const_iterator &expr_iterator,
526 const std::vector<exprt>::const_iterator &end)
529 INVARIANT(expr_iterator != end,
"Cannot compute max of an empty collection");
530 const exprt ¤t_expr = *expr_iterator;
534 std::vector<exprt>::const_iterator expr_to_compare_to =
535 std::next(expr_iterator);
536 if(expr_to_compare_to == end)
541 std::vector<exprt> comparisons;
542 for(; expr_to_compare_to != end; ++expr_to_compare_to)
545 comparisons.emplace_back(
549 return {
and_exprt(comparisons), current_expr};
558 const std::vector<std::pair<exprt, exprt>> &conditions_and_values)
562 conditions_and_values.size() > 0,
563 "Cannot compute max of an empty collection");
567 auto reverse_ite = conditions_and_values.rbegin();
572 "Last element of condition-value list must have nil_exprt condition.");
574 exprt res = std::move(reverse_ite->second);
576 for(++reverse_ite; reverse_ite != conditions_and_values.rend(); ++reverse_ite)
578 res =
if_exprt(reverse_ite->first, reverse_ite->second, res);
589 std::vector<std::pair<exprt, exprt>> rows;
590 rows.reserve(values.size());
591 for(
auto byte_it = values.begin(); byte_it != values.end(); ++byte_it)
603 const typet &field_type,
610 std::size_t byte_count = size /
config.ansi_c.char_width;
613 std::vector<exprt> extracted_bytes;
614 extracted_bytes.reserve(byte_count);
615 for(std::size_t i = 0; i < byte_count; ++i)
625 max_expr.
type() == field_type,
626 "Aggregated max value type must be the same as shadow memory field's "
633 const std::vector<std::pair<exprt, exprt>> &conds_values)
636 !conds_values.empty(),
"build_if_else_expr requires non-empty argument");
638 for(
const auto &cond_value : conds_values)
642 result = cond_value.second;
646 result =
if_exprt(cond_value.first, cond_value.second, result);
661 if(expr_type.
id() != ID_pointer || shadow_type.
id() != ID_pointer)
670 expr_subtype.
id() == ID_pointer &&
672 shadow_subtype.
id() == ID_array &&
673 to_array_type(shadow_subtype).element_type().
id() != ID_pointer)
678 shadow_subtype.
id() == ID_pointer &&
680 expr_subtype.
id() != ID_pointer)
694 index_expr && index_expr->index().is_zero() &&
697 expr = index_expr->array();
713 const auto *array_type =
718 if(
pointer_type->base_type().id() == ID_string_constant)
731 const exprt &shadowed_address,
732 const exprt &matched_base_address,
736 typet shadowed_address_type = shadowed_address.
type();
741 matched_base_address, shadowed_address_type);
744 base_cond.
id() == ID_equal &&
749 if(base_cond.
id() == ID_equal)
752 const bool equality_types_match =
755 equality_types_match,
756 "types of expressions on each side of equality should match",
770 const exprt &dereference_pointer,
783 expr_cond.
id() == ID_equal &&
788 if(expr_cond.
id() == ID_equal)
791 const bool equality_types_match =
794 equality_types_match,
795 "types of expressions on each side of equality should match",
820 shadowed_object.
object() = shadow;
823#ifdef DEBUG_SHADOW_MEMORY
824 log.
debug() <<
"Shadow memory: shadow-deref: "
827 return shadow_dereference;
854 const exprt &matched_object,
855 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
856 const typet &field_type,
858 const typet &lhs_type,
861 std::vector<std::pair<exprt, exprt>> result;
863 for(
const auto &shadowed_address : addresses)
873 exprt matched_base_address =
878 if(matched_base_descriptor.
object().
id() == ID_null_object)
890 s <<
"Shadow memory: cannot get shadow memory via type void* for "
892 <<
". Insert a cast to the type that you want to access.";
900 shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
905 matched_base_address,
910 const bool is_union = matched_base_descriptor.
type().
id() == ID_union ||
911 matched_base_descriptor.
type().
id() == ID_union_tag;
915 if(field_type.
id() == ID_c_bool || field_type.
id() == ID_bool)
920 shadow_dereference.
value, field_type, ns, log, is_union),
930 shadowed_address.address, matched_base_address, ns, log);
937 const exprt expr_cond =
946#ifdef DEBUG_SHADOW_MEMORY
951 result.emplace_back(base_cond, value);
959#ifdef DEBUG_SHADOW_MEMORY
963 result.emplace_back(expr_cond, value);
968#ifdef DEBUG_SHADOW_MEMORY
971 result.emplace_back(
and_exprt(base_cond, expr_cond), value);
997 if(
object.
id() == ID_index)
1004 object = index_expr.
array();
1006 else if(
object.
id() == ID_member)
1009 const auto &struct_op = member_expr.
struct_op();
1011 struct_op.type().
id() == ID_struct_tag
1023 result.
object() = object;
1031 const std::vector<exprt> &value_set,
1036 "Cannot check if value_set contains only NULL as `expr` type is not a "
1048static std::vector<std::pair<exprt, exprt>>
1051 const exprt &matched_object,
1052 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1057 std::vector<std::pair<exprt, exprt>> result;
1058 for(
const auto &shadowed_address : addresses)
1073 matched_base_descriptor, expr, ns);
1075 exprt matched_base_address =
1080 if(matched_base_descriptor.
object().
id() == ID_null_object)
1086 shadowed_address.shadow, matched_base_descriptor, expr, ns, log);
1091 matched_base_address,
1094 shadow_dereference);
1097 shadowed_address.address, matched_base_address, ns, log);
1104 const exprt expr_cond =
1117 result.push_back({base_cond, shadow_dereference.
pointer});
1128 result.emplace_back(expr_cond, shadow_dereference.
pointer);
1134 result.emplace_back(
1143 const std::vector<exprt> &value_set,
1144 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
1149 std::vector<std::pair<exprt, exprt>> conds_values;
1150 for(
const auto &matched_object : value_set)
1152 if(matched_object.id() != ID_object_descriptor)
1154 log.
warning() <<
"Shadow memory: value set contains unknown for "
1162 log.
warning() <<
"Shadow memory: value set contains integer_address for "
1166 if(matched_object.type().get_bool(ID_C_is_failed_symbol))
1168 log.
warning() <<
"Shadow memory: value set contains failed symbol for "
1173 bool exact_match =
false;
1175 expr, matched_object, addresses, ns, log, exact_match);
1177 if(!per_value_set_conds_values.empty())
1181 conds_values.clear();
1183 conds_values.insert(
1184 conds_values.begin(),
1185 per_value_set_conds_values.begin(),
1186 per_value_set_conds_values.end());
1187 mux_size += conds_values.size() - 1;
1194 if(!conds_values.empty())
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()
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
Operator to return the address of an object.
typet index_type() const
The type of the index expressions into any instance of this type.
const exprt & size() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
std::size_t get_width() const
Operator to dereference a pointer.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
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 & get(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
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...
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.
void set_expression(exprt expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
const exprt & get_original_expr() const
Structure type, corresponds to C style structs.
const componentst & components() const
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 can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
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.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
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.
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.