cprover
|
State type in value_set_domaint, used in value-set analysis and goto-symex. More...
#include <value_set.h>
Classes | |
struct | entryt |
Represents a row of a value_sett . More... | |
class | object_map_dt |
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances). More... | |
Public Types | |
typedef irep_idt | idt |
typedef optionalt< mp_integer > | offsett |
Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset . More... | |
typedef reference_counting< object_map_dt > | object_mapt |
Reference-counts instances of object_map_dt , such that multiple instructions' value_sett instances can share them. More... | |
typedef std::set< exprt > | expr_sett |
Set of expressions; only used for the get API, not for internal data representation. More... | |
typedef std::set< unsigned int > | dynamic_object_id_sett |
Set of dynamic object numbers, equivalent to a set of dynamic_object_exprt s with corresponding IDs. More... | |
typedef std::unordered_map< idt, entryt, string_hash > | valuest |
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets. More... | |
Public Member Functions | |
value_sett () | |
virtual | ~value_sett ()=default |
bool | offset_is_zero (const offsett &offset) const |
exprt | to_expr (const object_map_dt::value_type &it) const |
Converts an object_map_dt entry object_number -> offset into an object_descriptor_exprt with .object() == object_numbering.at(object_number) and .offset() == offset . More... | |
void | set (object_mapt &dest, const object_map_dt::value_type &it) const |
Sets an entry in object map dest to match an existing entry it from a different map. More... | |
bool | insert (object_mapt &dest, const object_map_dt::value_type &it) const |
Merges an existing entry into an object map. More... | |
bool | insert (object_mapt &dest, const exprt &src) const |
Adds an expression to an object map, with unknown offset. More... | |
bool | insert (object_mapt &dest, const exprt &src, const mp_integer &offset_value) const |
Adds an expression to an object map, with known offset. More... | |
bool | insert (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const |
Adds a numbered expression and offset to an object map. More... | |
bool | insert (object_mapt &dest, const exprt &expr, const offsett &offset) const |
Adds an expression and offset to an object map. More... | |
void | get_value_set (const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const |
Gets values pointed to by expr , including following dereference operators (i.e. More... | |
expr_sett & | get (const idt &identifier, const std::string &suffix) |
Appears to be unimplemented. More... | |
void | clear () |
const entryt * | find_entry (const idt &id) const |
Finds an entry in this value-set. More... | |
entryt & | get_entry (const entryt &e, const typet &type, const namespacet &ns) |
Gets or inserts an entry in this value-set. More... | |
void | output (const namespacet &ns, std::ostream &out) const |
Pretty-print this value-set. More... | |
bool | make_union (object_mapt &dest, const object_mapt &src) const |
Merges two RHS expression sets. More... | |
bool | make_union (const valuest &new_values) |
Merges an entire existing value_sett's data into this one. More... | |
bool | make_union (const value_sett &new_values) |
Merges an entire existing value_sett's data into this one. More... | |
void | guard (const exprt &expr, const namespacet &ns) |
Transforms this value-set by assuming an expression holds. More... | |
void | apply_code (const codet &code, const namespacet &ns) |
Transforms this value-set by executing a given statement against it. More... | |
void | assign (const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets) |
Transforms this value-set by executing executing the assignment lhs := rhs against it. More... | |
void | do_function_call (const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns) |
Transforms this value-set by executing the actual -> formal parameter assignments for a particular callee. More... | |
void | do_end_function (const exprt &lhs, const namespacet &ns) |
Transforms this value-set by assigning this function's return value to a given LHS expression. More... | |
void | get_reference_set (const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const |
Gets the set of expressions that expr may refer to, according to this value set. More... | |
bool | eval_pointer_offset (exprt &expr, const namespacet &ns) const |
Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-set's information. More... | |
Static Public Member Functions | |
static bool | field_sensitive (const irep_idt &id, const typet &type, const namespacet &) |
Public Attributes | |
unsigned | location_number |
Matches the location_number field of the instruction that corresponds to this value_sett instance in value_set_domaint's state map. More... | |
valuest | values |
Stores the LHS ID -> RHS expression set map. More... | |
Static Public Attributes | |
static object_numberingt | object_numbering |
Global shared object numbering, used to abbreviate expressions stored in value sets. More... | |
Protected Member Functions | |
void | get_value_set (const exprt &expr, object_mapt &dest, const namespacet &ns, bool is_simplified) const |
Reads the set of objects pointed to by expr , including making recursive lookups for dereference operations etc. More... | |
void | get_reference_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const |
See the other overload of get_reference_set . More... | |
void | get_reference_set_rec (const exprt &expr, object_mapt &dest, const namespacet &ns) const |
See get_reference_set. More... | |
void | dereference_rec (const exprt &src, exprt &dest) const |
Sets dest to src with any wrapping typecasts removed. More... | |
exprt | make_member (const exprt &src, const irep_idt &component_name, const namespacet &ns) |
Extracts a member from a struct- or union-typed expression. More... | |
virtual void | get_value_set_rec (const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const |
Subclass customisation point for recursion over RHS expression: More... | |
virtual void | assign_rec (const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets) |
Subclass customisation point for recursion over LHS expression: More... | |
virtual void | apply_code_rec (const codet &code, const namespacet &ns) |
Subclass customisation point for applying code to this domain: More... | |
Private Member Functions | |
virtual void | adjust_assign_rhs_values (const exprt &rhs, const namespacet &, object_mapt &rhs_values) const |
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set before it is passed into assign. More... | |
virtual void | apply_assign_side_effects (const exprt &lhs, const exprt &rhs, const namespacet &) |
Subclass customisation point to apply global side-effects to this domain, after RHS values are read but before they are written. More... | |
State type in value_set_domaint, used in value-set analysis and goto-symex.
Represents a mapping from expressions to the addresses that may be stored there; for example, a global that is either null or points to a heap-allocated object, which itself has two fields, one pointing to another heap object and the other having unknown target, would be represented:
global_x -> { null, <dynamic_object1, 0> } dynamic_object1.field1 -> { <dynamic_object2, 0> } dynamic_object1.field2 -> { * (unknown) }
LHS expressions can be either symbols or fields thereof, and are stored as strings; RHS expressions may be symbols, dynamic objects, integer addresses (as in (int*)0x1234
) or unknown (printed as *
), and are stored as pairs of an exprt
and an optional offset if known (0 for both dynamic objects in the example given above). RHS expressions are represented using numbering to avoid storing redundant duplicate expressions.
Definition at line 41 of file value_set.h.
typedef std::set<unsigned int> value_sett::dynamic_object_id_sett |
Set of dynamic object numbers, equivalent to a set of dynamic_object_exprt
s with corresponding IDs.
Used only in internal implementation details.
Definition at line 273 of file value_set.h.
typedef std::set<exprt> value_sett::expr_sett |
Set of expressions; only used for the get
API, not for internal data representation.
Definition at line 268 of file value_set.h.
typedef irep_idt value_sett::idt |
Definition at line 63 of file value_set.h.
Reference-counts instances of object_map_dt
, such that multiple instructions' value_sett
instances can share them.
For example, if we have a pair of instructions with value-sets:
x = new A; x -> { dynamic_object1 } y = new B; x -> { dynamic_object1 } y -> { dynamic_object2 }
Then the set { dynamic_object1 }, represented by an object_map_dt
, can be shared between the two value_sett
instances.
Definition at line 163 of file value_set.h.
typedef optionalt<mp_integer> value_sett::offsett |
Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset
.
Definition at line 67 of file value_set.h.
typedef std::unordered_map<idt, entryt, string_hash> value_sett::valuest |
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets.
Note this data structure is somewhat denormalized, for example mapping
dynamic_object1.field2 -> entryt { .identifier = dynamic_object1, .suffix = .field2, .object_map = ... }
The components of the ID are thus duplicated in the valuest
key and in entryt
fields.
Definition at line 291 of file value_set.h.
|
inline |
Definition at line 44 of file value_set.h.
|
virtualdefault |
|
inlineprivatevirtual |
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set before it is passed into assign.
For example, this is used in one subclass to tag and thus differentiate values that originated in a particular place, vs. those that have been copied.
Definition at line 530 of file value_set.h.
|
inlineprivatevirtual |
Subclass customisation point to apply global side-effects to this domain, after RHS values are read but before they are written.
For example, this is used in a recency-analysis plugin to demote existing most-recent objects to general case ones.
Definition at line 544 of file value_set.h.
|
inline |
Transforms this value-set by executing a given statement against it.
For example, assignment statements will update valuest
by reading the value-set corresponding to their right-hand side and assigning it to their LHS.
code | instruction to apply |
ns | global namespace |
Definition at line 381 of file value_set.h.
|
protectedvirtual |
Subclass customisation point for applying code to this domain:
Definition at line 1468 of file value_set.cpp.
void value_sett::assign | ( | const exprt & | lhs, |
const exprt & | rhs, | ||
const namespacet & | ns, | ||
bool | is_simplified, | ||
bool | add_to_sets | ||
) |
Transforms this value-set by executing executing the assignment lhs := rhs
against it.
lhs | written expression |
rhs | read expression |
ns | global namespace |
is_simplified | if false, simplify will be used to simplify RHS and LHS before execution. If you know they are already simplified, set this to save a little time. |
add_to_sets | if true, execute a weak assignment (the LHS possible values are added to but not overwritten). Otherwise execute a strong (overwriting) assignment. Note the nature of lhs may internally prevent a strong assignment, as in x == y ? z : w := a , where either y or z MAY, but not MUST, be overwritten. |
Definition at line 1151 of file value_set.cpp.
|
protectedvirtual |
Subclass customisation point for recursion over LHS expression:
Do not take a reference to object_numbering's storage as we may call object_numbering.number(), which may reallocate it.
Definition at line 1273 of file value_set.cpp.
|
inline |
Definition at line 309 of file value_set.h.
Sets dest
to src
with any wrapping typecasts removed.
Definition at line 960 of file value_set.cpp.
void value_sett::do_end_function | ( | const exprt & | lhs, |
const namespacet & | ns | ||
) |
Transforms this value-set by assigning this function's return value to a given LHS expression.
Note this has no effect if remove_returns
has been run, in which case returns are explicitly passed via global variables named function_name#return_value
and are handled via the usual apply_code
path.
lhs | expression that receives the return value |
ns | global namespace |
Definition at line 1456 of file value_set.cpp.
void value_sett::do_function_call | ( | const irep_idt & | function, |
const exprt::operandst & | arguments, | ||
const namespacet & | ns | ||
) |
Transforms this value-set by executing the actual -> formal parameter assignments for a particular callee.
For example, for function f(int* x, void* y)
and call f(&g, &h)
this would execute assignments x := &g
and y := &h
.
function | function being called |
arguments | actual arguments |
ns | global namespace |
Definition at line 1410 of file value_set.cpp.
bool value_sett::eval_pointer_offset | ( | exprt & | expr, |
const namespacet & | ns | ||
) | const |
Tries to resolve any pointer_offset_exprt
expressions in expr
to constant integers using this value-set's information.
For example, if expr
contained POINTER_OFFSET(y)
, and this value set indicates y
points to object z
offset 4
, then the expression will be replaced by constant 4
. If we don't know where y
points, or it may point to multiple distinct offsets, then the expression will be left alone.
expr | expression whose pointer offsets should be replaced |
ns | global namespace |
Definition at line 267 of file value_set.cpp.
|
static |
Definition at line 39 of file value_set.cpp.
const value_sett::entryt * value_sett::find_entry | ( | const idt & | id | ) | const |
Finds an entry in this value-set.
The interface differs from get_entry because get_value_set_rec wants to check for a struct's first component before stripping the suffix as is done in get_entry.
id | identifier to find. |
Definition at line 54 of file value_set.cpp.
Appears to be unimplemented.
value_sett::entryt & value_sett::get_entry | ( | const entryt & | e, |
const typet & | type, | ||
const namespacet & | ns | ||
) |
Gets or inserts an entry in this value-set.
e | entry to find. Its id and suffix fields will be used to find a corresponding entry; if a fresh entry is created its object_map (RHS value set) will be copied; otherwise it will be ignored. Therefore it should probably be left blank and any RHS updates conducted against the returned reference. |
type | type of e.identifier , used to determine whether e 's suffix should be used to find a field-sensitive value-set or whether a single entry should be shared by all of symbol e.identifier . |
ns | global namespace |
Definition at line 61 of file value_set.cpp.
|
inlineprotected |
See the other overload of get_reference_set
.
This one returns object numbers and offsets instead of expressions.
Definition at line 471 of file value_set.h.
void value_sett::get_reference_set | ( | const exprt & | expr, |
value_setst::valuest & | dest, | ||
const namespacet & | ns | ||
) | const |
Gets the set of expressions that expr
may refer to, according to this value set.
Note the contrast with get_value_set
: if x
holds a pointer to y
, then get_value_set(x)
includes y
while get_reference_set(x)
returns { x }
.
expr | query expression | |
[out] | dest | overwritten with result expression set |
ns | global namespace |
Definition at line 978 of file value_set.cpp.
|
protected |
See get_reference_set.
Definition at line 993 of file value_set.cpp.
|
protected |
Reads the set of objects pointed to by expr
, including making recursive lookups for dereference operations etc.
expr | query expression |
dest | [out]: overwritten by the set of object numbers pointed to |
ns; | global namespace |
is_simplified | if false, simplify expr before reading. |
Definition at line 341 of file value_set.cpp.
void value_sett::get_value_set | ( | const exprt & | expr, |
value_setst::valuest & | dest, | ||
const namespacet & | ns | ||
) | const |
Gets values pointed to by expr
, including following dereference operators (i.e.
this is not a simple lookup in valuest
).
expr | query expression | |
[out] | dest | assigned a set of expressions that expr may point to |
ns | global namespace |
Definition at line 320 of file value_set.cpp.
|
protectedvirtual |
Subclass customisation point for recursion over RHS expression:
Do not take a reference to object_numbering's storage as we may call object_numbering.number(), which may reallocate it.
Do not take a reference to object_numbering's storage as we may call object_numbering.number(), which may reallocate it.
Definition at line 378 of file value_set.cpp.
void value_sett::guard | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
Transforms this value-set by assuming an expression holds.
Currently this can only mark dynamic objects valid; all other assumptions are ignored.
expr | condition to assume |
ns | global namespace |
Definition at line 1591 of file value_set.cpp.
|
inline |
Adds an expression and offset to an object map.
If the destination map has an existing entry for the same expression with a differing offset its offset is marked unknown.
dest | object map to update |
expr | expression to add |
offset | offset into expr (may be unknown). |
Definition at line 228 of file value_set.h.
|
inline |
Adds an expression to an object map, with unknown offset.
If the destination map has an existing entry for the same expression its offset is marked unknown.
dest | object map to update |
src | expression to add |
Definition at line 191 of file value_set.h.
|
inline |
Adds an expression to an object map, with known offset.
If the destination map has an existing entry for the same expression with a differing offset its offset is marked unknown.
dest | object map to update |
src | expression to add |
offset_value | offset into src |
Definition at line 202 of file value_set.h.
|
inline |
Merges an existing entry into an object map.
If the destination map has an existing entry for the same expression with a different offset its offset is marked unknown (so e.g. x -> 0
and x -> 1
merge into x -> ?
).
dest | object map to update. |
it | iterator pointing to new entry |
Definition at line 181 of file value_set.h.
bool value_sett::insert | ( | object_mapt & | dest, |
object_numberingt::number_type | n, | ||
const offsett & | offset | ||
) | const |
Adds a numbered expression and offset to an object map.
If the destination map has an existing entry for the same expression with a differing offset its offset is marked unknown.
dest | object map to update |
n | object number to add; must be mapped to the corresponding expression by object_numbering . |
offset | offset into object n (may be unknown). |
Definition at line 79 of file value_set.cpp.
|
protected |
Extracts a member from a struct- or union-typed expression.
Usually that means making a member_exprt
, but this can shortcut extracting members from constants or with-expressions.
src | base struct-or-union-typed expression |
component_name | member to extract |
ns | global namespace |
Definition at line 1625 of file value_set.cpp.
|
inline |
Merges an entire existing value_sett's data into this one.
Definition at line 361 of file value_set.h.
bool value_sett::make_union | ( | const valuest & | new_values | ) |
Merges an entire existing value_sett's data into this one.
new_values | new values to merge in |
Definition at line 213 of file value_set.cpp.
bool value_sett::make_union | ( | object_mapt & | dest, |
const object_mapt & | src | ||
) | const |
Merges two RHS expression sets.
[in,out] | dest | set to merge into |
src | set to merge in |
Definition at line 252 of file value_set.cpp.
|
inline |
Definition at line 68 of file value_set.h.
void value_sett::output | ( | const namespacet & | ns, |
std::ostream & | out | ||
) | const |
Pretty-print this value-set.
ns | global namespace | |
[out] | out | stream to write to |
Definition at line 103 of file value_set.cpp.
|
inline |
Sets an entry in object map dest
to match an existing entry it
from a different map.
Any existing entry for the same exprt
is overwritten.
dest | object map to update. |
it | iterator pointing to new entry |
Definition at line 170 of file value_set.h.
exprt value_sett::to_expr | ( | const object_map_dt::value_type & | it | ) | const |
Converts an object_map_dt
entry object_number -> offset
into an object_descriptor_exprt
with .object() == object_numbering.at(object_number)
and .offset() == offset
.
Definition at line 193 of file value_set.cpp.
unsigned value_sett::location_number |
Matches the location_number field of the instruction that corresponds to this value_sett instance in value_set_domaint's state map.
Definition at line 57 of file value_set.h.
|
static |
Global shared object numbering, used to abbreviate expressions stored in value sets.
Definition at line 61 of file value_set.h.
valuest value_sett::values |
Stores the LHS ID -> RHS expression set map.
See valuest
documentation for more detail.
Definition at line 346 of file value_set.h.