cprover
Loading...
Searching...
No Matches
shadow_memory_util.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symex Shadow Memory Instrumentation
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H
13#define CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H
14
15#include <util/irep.h>
16#include <util/message.h> // IWYU pragma: keep
17
18#include "goto_symex_state.h" // IWYU pragma: keep
19
20// To enable logging of Shadow Memory functions define DEBUG_SHADOW_MEMORY
21
22class exprt;
23class typet;
24
28 const namespacet &ns,
29 const messaget &log,
30 const irep_idt &field_name,
31 const exprt &expr,
32 const exprt &value);
33
38 const namespacet &ns,
39 const messaget &log,
40 const std::vector<exprt> &value_set);
41
45 const namespacet &ns,
46 const messaget &log,
47 const irep_idt &field_name,
48 const exprt &expr);
49
52 const namespacet &ns,
53 const messaget &log,
54 const exprt &address,
55 const exprt &expr);
56
61 const namespacet &ns,
62 const messaget &log,
63 const char *text,
64 const exprt &expr);
65
71
79void clean_pointer_expr(exprt &expr, const typet &type);
80
83exprt deref_expr(const exprt &expr);
84
89
97const exprt &
99
105std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
106 const namespacet &ns,
107 const messaget &log,
108 const exprt &matched_object,
109 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
110 const typet &field_type,
111 const exprt &expr,
112 const typet &lhs_type,
113 bool &exact_match);
114
123const typet &
125
133 const std::vector<exprt> &value_set,
134 const exprt &address);
135
146 const exprt &expr,
147 const typet &field_type,
148 const namespacet &ns,
149 const messaget &log,
150 const bool is_union);
151
161 const exprt &expr,
162 const typet &field_type,
163 const namespacet &ns);
164
173 const std::vector<std::pair<exprt, exprt>> &conds_values);
174
185 const namespacet &ns,
186 const messaget &log,
187 const std::vector<exprt> &value_set,
188 const exprt &expr);
189
197 const exprt &expr,
198 const std::vector<exprt> &value_set,
199 const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
200 const namespacet &ns,
201 const messaget &log,
202 size_t &mux_size);
203
204#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
Central data structure: state.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The type of an expression, extends irept.
Definition type.h:29
Symbolic Execution.
void replace_invalid_object_by_null(exprt &expr)
Replace an invalid object by a null pointer.
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.
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.
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...
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.
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.
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,...
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 ...
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.
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.
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 clean_pointer_expr(exprt &expr, const typet &type)
Clean the given pointer expression so that it has the right shape for being used for identifying shad...
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.
optionalt< 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.