cprover
field_sensitivityt Class Reference

Control granularity of object accesses. More...

#include <field_sensitivity.h>

Public Member Functions

 field_sensitivityt (std::size_t max_array_size)
 
void field_assignments (const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, symex_targett &target, bool allow_pointer_unsoundness)
 Assign to the individual fields of a non-expanded symbol lhs. More...
 
exprt apply (const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
 Turn an expression expr into a field-sensitive SSA expression. More...
 
exprt get_fields (const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr) const
 Compute an expression representing the individual components of a field-sensitive SSA representation of ssa_expr. More...
 
bool is_divisible (const ssa_exprt &expr) const
 Determine whether expr would translate to an atomic SSA expression (returns false) or a composite object made of several SSA expressions as components (such as a struct with each member becoming an individual SSA expression, return true in this case). More...
 

Private Member Functions

void field_assignments_rec (const namespacet &ns, goto_symex_statet &state, const exprt &lhs_fs, const exprt &lhs, symex_targett &target, bool allow_pointer_unsoundness)
 Assign to the individual fields lhs_fs of a non-expanded symbol lhs. More...
 

Private Attributes

bool run_apply = true
 whether or not to invoke field_sensitivityt::apply More...
 
const std::size_t max_field_sensitivity_array_size
 

Detailed Description

Control granularity of object accesses.

Field sensitivity is a transformation of the instructions goto-program which mainly replaces some expressions by symbols but can also add assignments to the target equations produced by symbolic execution. The main goal of this transformation is to allow more constants to be propagated during symbolic execution. Note that field sensitivity is not applied as a single pass over the whole goto program but instead applied as the symbolic execution unfolds.

On a high level, field sensitivity replaces member operators, and array accesses with atomic symbols representing a field when possible. In cases where this is not immediately possible, like struct assignments, some things need to be added. The possible cases are described below.

Member access

A member expression struct_expr.field_name is replaced by the symbol struct_expr..field_name; note the use of .. to visually distinguish the symbol from the member expression. This is valid for both lvalues and rvalues. See field_sensitivityt::apply.

Symbols representing structs

In an rvalue, a symbol struct_expr which has a struct type with fields field1, field2, etc, will be replaced by {struct_expr..field_name1; struct_expr..field_name2; …}. See field_sensitivityt::get_fields.

Assignment to a struct

When the symbol is on the left-hand-side, for instance for an assignment struct_expr = other_struct, the assignment is replaced by a sequence of assignments: struct_expr..field_name1 = other_struct..field_name1; struct_expr..field_name2 = other_struct..field_name2; etc. See field_sensitivityt::field_assignments.

Array access

An index expression array[index] when index is constant and array has constant size is replaced by the symbol array[[index]]; note the use of [[ and ]] to visually distinguish the symbol from the index expression. When index is not a constant, array[index] is replaced by {array[[0]]; array[[1]]; …index]. Note that this process does not apply to arrays whose size is not constant, and arrays whose size exceed the bound max_field_sensitivity_array_size. See field_sensitivityt::apply.

Symbols representing arrays

In an rvalue, a symbol array which has array type will be replaced by {array[[0]]; array[[1]]; …}[index]. See field_sensitivityt::get_fields.

Assignment to an array

When the array symbol is on the left-hand-side, for instance for an assignment array = other_array, the assignment is replaced by a sequence of assignments: array[[0]] = other_array[[0]]; array[[1]] = other_array[[1]]; etc. See field_sensitivityt::field_assignments.

Definition at line 80 of file field_sensitivity.h.

Constructor & Destructor Documentation

◆ field_sensitivityt()

field_sensitivityt::field_sensitivityt ( std::size_t  max_array_size)
inlineexplicit
Parameters
max_array_sizemaximum size for which field sensitivity will be applied to array cells

Definition at line 85 of file field_sensitivity.h.

Member Function Documentation

◆ apply()

exprt field_sensitivityt::apply ( const namespacet ns,
goto_symex_statet state,
exprt  expr,
bool  write 
) const

Turn an expression expr into a field-sensitive SSA expression.

Field-sensitive SSA expressions have individual symbols for each component. While the exact granularity is an implementation detail, possible implementations translate a struct-typed symbol into a struct of member expressions, or an array-typed symbol into an array of index expressions. Such expansions are not possible when the symbol is to be written to (i.e., write is true); in such a case only translations from existing member or index expressions into symbols are performed.

Parameters
nsa namespace to resolve type symbols/tag types
[in,out]statesymbolic execution state
expran expression to be (recursively) transformed.
writeset to true if the expression is to be used as an lvalue.
Returns
the transformed expression

Definition at line 21 of file field_sensitivity.cpp.

◆ field_assignments()

void field_sensitivityt::field_assignments ( const namespacet ns,
goto_symex_statet state,
const ssa_exprt lhs,
symex_targett target,
bool  allow_pointer_unsoundness 
)

Assign to the individual fields of a non-expanded symbol lhs.

This is required whenever prior steps have updated the full object rather than individual fields, e.g., in case of assignments to an array at an unknown index.

Parameters
nsa namespace to resolve type symbols/tag types
statesymbolic execution state
lhsnon-expanded symbol
targetsymbolic execution equation store
allow_pointer_unsoundnessallow pointer unsoundness

Definition at line 221 of file field_sensitivity.cpp.

◆ field_assignments_rec()

void field_sensitivityt::field_assignments_rec ( const namespacet ns,
goto_symex_statet state,
const exprt lhs_fs,
const exprt lhs,
symex_targett target,
bool  allow_pointer_unsoundness 
)
private

Assign to the individual fields lhs_fs of a non-expanded symbol lhs.

This is required whenever prior steps have updated the full object rather than individual fields, e.g., in case of assignments to an array at an unknown index.

Parameters
nsa namespace to resolve type symbols/tag types
statesymbolic execution state
lhs_fsexpanded symbol
lhsnon-expanded symbol
targetsymbolic execution equation store
allow_pointer_unsoundnessallow pointer unsoundness

Definition at line 247 of file field_sensitivity.cpp.

◆ get_fields()

exprt field_sensitivityt::get_fields ( const namespacet ns,
goto_symex_statet state,
const ssa_exprt ssa_expr 
) const

Compute an expression representing the individual components of a field-sensitive SSA representation of ssa_expr.

Parameters
nsa namespace to resolve type symbols/tag types
[in,out]statesymbolic execution state
ssa_exprthe expression to evaluate
Returns
Expanded expression; for example, for a ssa_expr of some struct type, a struct_exprt with each component now being an SSA expression is built.

Definition at line 147 of file field_sensitivity.cpp.

◆ is_divisible()

bool field_sensitivityt::is_divisible ( const ssa_exprt expr) const

Determine whether expr would translate to an atomic SSA expression (returns false) or a composite object made of several SSA expressions as components (such as a struct with each member becoming an individual SSA expression, return true in this case).

Parameters
exprthe expression to evaluate
Returns
False, if and only if, expr would be a single field-sensitive SSA expression.

Definition at line 343 of file field_sensitivity.cpp.

Member Data Documentation

◆ max_field_sensitivity_array_size

const std::size_t field_sensitivityt::max_field_sensitivity_array_size
private

Definition at line 149 of file field_sensitivity.h.

◆ run_apply

bool field_sensitivityt::run_apply = true
private

whether or not to invoke field_sensitivityt::apply

Definition at line 147 of file field_sensitivity.h.


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