cprover
value_sett Class Reference

State type in value_set_domaint, used in value-set analysis and goto-symex. More...

#include <value_set.h>

+ Collaboration diagram for value_sett:

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_integeroffsett
 Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset. More...
 
typedef reference_counting< object_map_dtobject_mapt
 Reference-counts instances of object_map_dt, such that multiple instructions' value_sett instances can share them. More...
 
typedef std::set< exprtexpr_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_exprts with corresponding IDs. More...
 
typedef std::unordered_map< idt, entryt, string_hashvaluest
 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_settget (const idt &identifier, const std::string &suffix)
 Appears to be unimplemented. More...
 
void clear ()
 
const entrytfind_entry (const idt &id) const
 Finds an entry in this value-set. More...
 
entrytget_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...
 

Detailed Description

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.

Member Typedef Documentation

◆ dynamic_object_id_sett

typedef std::set<unsigned int> value_sett::dynamic_object_id_sett

Set of dynamic object numbers, equivalent to a set of dynamic_object_exprts with corresponding IDs.

Used only in internal implementation details.

Definition at line 273 of file value_set.h.

◆ expr_sett

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.

◆ idt

Definition at line 63 of file value_set.h.

◆ object_mapt

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.

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

◆ valuest

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.

Constructor & Destructor Documentation

◆ value_sett()

value_sett::value_sett ( )
inline

Definition at line 44 of file value_set.h.

◆ ~value_sett()

virtual value_sett::~value_sett ( )
virtualdefault

Member Function Documentation

◆ adjust_assign_rhs_values()

virtual void value_sett::adjust_assign_rhs_values ( const exprt rhs,
const namespacet ,
object_mapt rhs_values 
) const
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.

◆ apply_assign_side_effects()

virtual void value_sett::apply_assign_side_effects ( const exprt lhs,
const exprt rhs,
const namespacet  
)
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.

◆ apply_code()

void value_sett::apply_code ( const codet code,
const namespacet ns 
)
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.

Parameters
codeinstruction to apply
nsglobal namespace

Definition at line 381 of file value_set.h.

◆ apply_code_rec()

void value_sett::apply_code_rec ( const codet code,
const namespacet ns 
)
protectedvirtual

Subclass customisation point for applying code to this domain:

Definition at line 1468 of file value_set.cpp.

◆ assign()

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.

Parameters
lhswritten expression
rhsread expression
nsglobal namespace
is_simplifiedif 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_setsif 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.

◆ assign_rec()

void value_sett::assign_rec ( const exprt lhs,
const object_mapt values_rhs,
const std::string &  suffix,
const namespacet ns,
bool  add_to_sets 
)
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.

◆ clear()

void value_sett::clear ( void  )
inline

Definition at line 309 of file value_set.h.

◆ dereference_rec()

void value_sett::dereference_rec ( const exprt src,
exprt dest 
) const
protected

Sets dest to src with any wrapping typecasts removed.

Definition at line 960 of file value_set.cpp.

◆ do_end_function()

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.

Parameters
lhsexpression that receives the return value
nsglobal namespace

Definition at line 1456 of file value_set.cpp.

◆ do_function_call()

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.

Parameters
functionfunction being called
argumentsactual arguments
nsglobal namespace

Definition at line 1410 of file value_set.cpp.

◆ eval_pointer_offset()

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.

Parameters
exprexpression whose pointer offsets should be replaced
nsglobal namespace
Returns
true if any offset expression was successfully replaced.

Definition at line 267 of file value_set.cpp.

◆ field_sensitive()

bool value_sett::field_sensitive ( const irep_idt id,
const typet type,
const namespacet ns 
)
static

Definition at line 39 of file value_set.cpp.

◆ find_entry()

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.

Parameters
ididentifier to find.
Returns
a constant pointer to an entry if found, or null otherwise. Note the pointer may be invalidated by insert operations, including get_entry.

Definition at line 54 of file value_set.cpp.

◆ get()

expr_sett& value_sett::get ( const idt identifier,
const std::string &  suffix 
)

Appears to be unimplemented.

◆ get_entry()

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.

Parameters
eentry 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.
typetype 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.
nsglobal namespace

Definition at line 61 of file value_set.cpp.

◆ get_reference_set() [1/2]

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

Parameters
exprquery expression
[out]destoverwritten with result expression set
nsglobal namespace

Definition at line 978 of file value_set.cpp.

◆ get_reference_set() [2/2]

void value_sett::get_reference_set ( const exprt expr,
object_mapt dest,
const namespacet ns 
) const
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.

◆ get_reference_set_rec()

void value_sett::get_reference_set_rec ( const exprt expr,
object_mapt dest,
const namespacet ns 
) const
protected

See get_reference_set.

Definition at line 993 of file value_set.cpp.

◆ get_value_set() [1/2]

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

Parameters
exprquery expression
[out]destassigned a set of expressions that expr may point to
nsglobal namespace

Definition at line 320 of file value_set.cpp.

◆ get_value_set() [2/2]

void value_sett::get_value_set ( const exprt expr,
object_mapt dest,
const namespacet ns,
bool  is_simplified 
) const
protected

Reads the set of objects pointed to by expr, including making recursive lookups for dereference operations etc.

Parameters
exprquery expression
dest[out]: overwritten by the set of object numbers pointed to
ns;global namespace
is_simplifiedif false, simplify expr before reading.

Definition at line 341 of file value_set.cpp.

◆ get_value_set_rec()

void value_sett::get_value_set_rec ( const exprt expr,
object_mapt dest,
const std::string &  suffix,
const typet original_type,
const namespacet ns 
) const
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.

◆ guard()

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.

Parameters
exprcondition to assume
nsglobal namespace

Definition at line 1591 of file value_set.cpp.

◆ insert() [1/5]

bool value_sett::insert ( object_mapt dest,
const object_map_dt::value_type it 
) const
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 -> ?).

Parameters
destobject map to update.
ititerator pointing to new entry

Definition at line 181 of file value_set.h.

◆ insert() [2/5]

bool value_sett::insert ( object_mapt dest,
const exprt src 
) const
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.

Parameters
destobject map to update
srcexpression to add

Definition at line 191 of file value_set.h.

◆ insert() [3/5]

bool value_sett::insert ( object_mapt dest,
const exprt src,
const mp_integer offset_value 
) const
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.

Parameters
destobject map to update
srcexpression to add
offset_valueoffset into src

Definition at line 202 of file value_set.h.

◆ insert() [4/5]

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.

Parameters
destobject map to update
nobject number to add; must be mapped to the corresponding expression by object_numbering.
offsetoffset into object n (may be unknown).

Definition at line 79 of file value_set.cpp.

◆ insert() [5/5]

bool value_sett::insert ( object_mapt dest,
const exprt expr,
const offsett offset 
) const
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.

Parameters
destobject map to update
exprexpression to add
offsetoffset into expr (may be unknown).

Definition at line 228 of file value_set.h.

◆ make_member()

exprt value_sett::make_member ( const exprt src,
const irep_idt component_name,
const namespacet ns 
)
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.

Parameters
srcbase struct-or-union-typed expression
component_namemember to extract
nsglobal namespace

Definition at line 1625 of file value_set.cpp.

◆ make_union() [1/3]

bool value_sett::make_union ( object_mapt dest,
const object_mapt src 
) const

Merges two RHS expression sets.

Parameters
[in,out]destset to merge into
srcset to merge in
Returns
true if anything changed.

Definition at line 252 of file value_set.cpp.

◆ make_union() [2/3]

bool value_sett::make_union ( const valuest new_values)

Merges an entire existing value_sett's data into this one.

Parameters
new_valuesnew values to merge in
Returns
true if anything changed.

Definition at line 213 of file value_set.cpp.

◆ make_union() [3/3]

bool value_sett::make_union ( const value_sett new_values)
inline

Merges an entire existing value_sett's data into this one.

Returns
true if anything changed.

Definition at line 361 of file value_set.h.

◆ offset_is_zero()

bool value_sett::offset_is_zero ( const offsett offset) const
inline

Definition at line 68 of file value_set.h.

◆ output()

void value_sett::output ( const namespacet ns,
std::ostream &  out 
) const

Pretty-print this value-set.

Parameters
nsglobal namespace
[out]outstream to write to

Definition at line 103 of file value_set.cpp.

◆ set()

void value_sett::set ( object_mapt dest,
const object_map_dt::value_type it 
) const
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.

Parameters
destobject map to update.
ititerator pointing to new entry

Definition at line 170 of file value_set.h.

◆ to_expr()

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.

Member Data Documentation

◆ location_number

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.

◆ object_numbering

object_numberingt value_sett::object_numbering
static

Global shared object numbering, used to abbreviate expressions stored in value sets.

Definition at line 61 of file value_set.h.

◆ values

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.


The documentation for this class was generated from the following files: