Control granularity of object accesses. More...

#include <field_sensitivity.h>

Public Member Functions
	field_sensitivityt (std::size_t max_array_size, bool should_simplify)

void	field_assignments (const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, const exprt &rhs, symex_targett &target, bool allow_pointer_unsoundness) const
	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	apply (const namespacet &ns, goto_symex_statet &state, ssa_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, bool disjoined_fields_only) 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, bool disjoined_fields_only) 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 &ssa_rhs, symex_targett &target, bool allow_pointer_unsoundness) const
	Assign to the individual fields `lhs_fs` of a non-expanded symbol `lhs`. More...

exprt	simplify_opt (exprt e, const namespacet &ns) const

Private Attributes
const std::size_t	max_field_sensitivity_array_size

const bool	should_simplify

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 116 of file field_sensitivity.h.

Constructor & Destructor Documentation

◆ field_sensitivityt()

field_sensitivityt::field_sensitivityt	(	std::size_t	max_array_size,
		bool	should_simplify
	)

inline

Parameters

max_array_size	maximum size for which field sensitivity will be applied to array cells
should_simplify	simplify expressions

Definition at line 122 of file field_sensitivity.h.

Member Function Documentation

◆ apply() [1/2]

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 34 of file field_sensitivity.cpp.

◆ apply() [2/2]

exprt field_sensitivityt::apply	(	const namespacet &	ns,
		goto_symex_statet &	state,
		ssa_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 22 of file field_sensitivity.cpp.

◆ field_assignments()

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

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
rhs	right-hand-side value that was used in the preceding update of the full object
target	symbolic execution equation store
allow_pointer_unsoundness	allow pointer unsoundness

Definition at line 302 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 &	ssa_rhs,
		symex_targett &	target,
		bool	allow_pointer_unsoundness
	)		const

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
ssa_rhs	right-hand-side value to assign
target	symbolic execution equation store
allow_pointer_unsoundness	allow pointer unsoundness

Definition at line 337 of file field_sensitivity.cpp.

◆ get_fields()

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

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

When disjoined_fields_only is false, the resulting expression must be handled with care as it will have multiple operands but empty id().

Parameters

	ns	a namespace to resolve type symbols/tag types
[in,out]	state	symbolic execution state
	ssa_expr	the expression to evaluate
	disjoined_fields_only	whether to expand unions (`false`) or not (`true`)

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 212 of file field_sensitivity.cpp.

◆ is_divisible()

bool field_sensitivityt::is_divisible	(	const ssa_exprt &	expr,
		bool	disjoined_fields_only
	)		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
disjoined_fields_only	whether to expand unions (`false`) or not (`true`)

Returns: False, if and only if, expr would be a single field-sensitive SSA expression.

Definition at line 521 of file field_sensitivity.cpp.

◆ simplify_opt()

exprt field_sensitivityt::simplify_opt	(	exprt	e,
		const namespacet &	ns
	)		const

private

Definition at line 549 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 201 of file field_sensitivity.h.

◆ should_simplify

const bool field_sensitivityt::should_simplify

private

Definition at line 203 of file field_sensitivity.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/field_sensitivity.h
/home/runner/work/cbmc/cbmc/src/goto-symex/field_sensitivity.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member access

Symbols representing structs

Assignment to a struct

Array access

Symbols representing arrays

Assignment to an array

Constructor & Destructor Documentation

◆ field_sensitivityt()

Member Function Documentation

◆ apply() [1/2]

◆ apply() [2/2]

◆ field_assignments()

◆ field_assignments_rec()

◆ get_fields()

◆ is_divisible()

◆ simplify_opt()

Member Data Documentation

◆ max_field_sensitivity_array_size

◆ should_simplify