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.

## ◆ field_sensitivityt()

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

Definition at line 85 of file field_sensitivity.h.

## ◆ 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
 ns a namespace to resolve type symbols/tag types [in,out] state symbolic execution state expr an expression to be (recursively) transformed. write set 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
 ns a namespace to resolve type symbols/tag types state symbolic execution state lhs non-expanded symbol target symbolic execution equation store allow_pointer_unsoundness allow 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
 ns a namespace to resolve type symbols/tag types state symbolic execution state lhs_fs expanded symbol lhs non-expanded symbol target symbolic execution equation store allow_pointer_unsoundness allow 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
 ns a namespace to resolve type symbols/tag types [in,out] state symbolic execution state ssa_expr the 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
 expr the 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.

## ◆ 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: