goto_sideeffects.cpp File Reference

#include <algorithm>
#include <goto-programs/destructor.h>
#include <goto-programs/goto_convert_class.h>
#include <irep2/irep2_utils.h>
#include <util/arith/arith_tools.h>
#include <util/config/config.h>
#include <util/lang/c_types.h>
#include <util/symtab/cprover_prefix.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/message/message.h>
#include <util/message/format.h>
#include <util/irep/migrate.h>
#include <util/symtab/rename.h>
#include <util/irep/std_expr.h>

Include dependency graph for goto_sideeffects.cpp:

Functions
static void	collect_and_conjuncts (const exprt &expr, exprt::operandst &out)
	Recursively flatten a (possibly nested) binary && expression into a flat list of conjuncts.
static exprt	rebuild_and_chain (const exprt::operandst &conjuncts, std::size_t i)
	Rebuild a right-associative nested binary && from a flat list of conjuncts starting at index i.
static void	collect_or_disjuncts (const exprt &expr, exprt::operandst &out)
	Recursively flatten a (possibly nested) binary || expression into a flat list of disjuncts.
static exprt	rebuild_or_chain (const exprt::operandst &disjuncts, std::size_t i)
	Rebuild a right-to-left nested binary || from a flat list of disjuncts starting at index i.
static const exprt *	quantifier_bound_var (const exprt &arg)
	Extract the symbol bound by a quantifier from its first argument, which has the shape (possibly typecast) address_of(symbol).
static irep_idt	quantifier_bound_var_id (const exprt &arg)
static bool	mentions_symbol (const exprt &e, const std::set< irep_idt > &ids)
static exprt *	old_raw_call_under (exprt &deref)
	__ESBMC_old(base[j]) with j bound by the enclosing quantifier takes the address of one element, which has no value outside the quantifier and so cannot be hoisted.
static const exprt *	bound_array_index (const exprt &target, const std::set< irep_idt > &bound_vars)
	&(base[j]) is address_of(index_exprt(base, j)) when base has real array type – the target's own type is already the element type.
static const exprt *	bound_ptr_param_offset (const exprt &target, const std::set< irep_idt > &bound_vars)
	A decayed pointer's p[j] desugars at the frontend to (p + j), so &(p[j]) is address_of(dereference(+(p, j))), not address_of(index_exprt(...)).
static const exprt *	bound_array_element (const exprt &addr, const std::set< irep_idt > &bound_vars)
	The array element addr addresses, when its index reaches bound_vars and its base is an array or a pointer parameter.
static void	lift_old_over_bound_index (exprt &expr, const std::set< irep_idt > &bound_vars, const namespacet &ns)
static bool	is_braced_list (const exprt &e)
static bool	is_assigned_whole (const exprt &assign)
	x=f(...), and a mem-initializer from a braced list, which initialises the member in place: convert_assign lowers both without removing the rhs first.
static bool	is_braced_temporary (const exprt &e)
	A class temporary initialised from a braced list, whose class elements remove_temporary_object constructs in place.
static bool	has_non_call_sideeffect (const exprt &e)
	A side effect other than a nested function call (e.g.
static std::size_t	count_symbol_occurrences (const exprt &e, const irep_idt &id)
static bool	symbol_before_sideeffects (const exprt &e, const irep_idt &id, bool &seen_id)
	Post-order (evaluation-order) walk: true when the occurrence of id precedes every other side effect in e.
static bool	substitutes_in_eval_order (const exprt &e, const irep_idt &id)
static bool	param_under_address_of (const exprt &e, const std::set< irep_idt > &ids)
	Substituting an argument under address_of would take the address of an rvalue or conflate distinct parameter objects (e.g.
static void	replace_symbols_in_expr (exprt &e, const std::map< irep_idt, exprt > &map)
static const symbolt *	quantifier_intrinsic_call (const exprt &e, const namespacet &ns)
	Returns the __ESBMC_forall/__ESBMC_exists symbol when e is a call to a quantifier intrinsic, nullptr otherwise.
static bool	flatten_body_statements (const codet &code, std::vector< const codet * > &out)
static bool	summary_eval (const exprt &e, const summary_statet &st, exprt &out)
	Substitute tracked locals in e with their env values.
static bool	summary_apply_effect (const exprt &e, summary_statet &st)
	Apply a discarded expression statement (or a for-loop iterator) to st.
static bool	summarize_code (const codet &code, summary_statet &st, const namespacet &ns)
	Symbolically execute one structured statement of the callee, updating st.
static irep_idt	compound_assign_operator (const irep_idt &statement, bool is_float)
static bool	is_promoted_to_int (const typet &type)

Variables
static constexpr unsigned	max_quantifier_inline_depth = 16

Function Documentation

bound_array_element()

const exprt * bound_array_element ( const exprt & addr, const std::set< irep_idt > & bound_vars )

static

The array element addr addresses, when its index reaches bound_vars and its base is an array or a pointer parameter.

A pointer with a symbolic extent has no whole object to snapshot; bound_ptr_param_offset defers that to contracts.cpp once the extent is known.

bound_array_index()

const exprt * bound_array_index ( const exprt & target, const std::set< irep_idt > & bound_vars )

static

&(base[j]) is address_of(index_exprt(base, j)) when base has real array type – the target's own type is already the element type.

bound_ptr_param_offset()

const exprt * bound_ptr_param_offset ( const exprt & target, const std::set< irep_idt > & bound_vars )

static

A decayed pointer's p[j] desugars at the frontend to (p + j), so &(p[j]) is address_of(dereference(+(p, j))), not address_of(index_exprt(...)).

No named object to snapshot here, only N bytes reachable through p, with N known only once the contracts pass resolves __ESBMC_is_fresh (#7057). Restrict to a bare symbol base so contracts.cpp can look it up in param_extents by identifier; an lvalue reached through a pointer (e.g. a struct field) is deferred (documented follow-up). Return the "+" node itself: like bound_array_index's index_exprt, it already has op0()=base, op1()=index – but unlike the array case, its own type is the *pointer type, not the element type (the caller must go through ->type().subtype() instead).

collect_and_conjuncts()

void collect_and_conjuncts ( const exprt & expr, exprt::operandst & out )

static

Recursively flatten a (possibly nested) binary && expression into a flat list of conjuncts.

Clang represents A && B && C as and(and(A,B),C).

collect_or_disjuncts()

void collect_or_disjuncts ( const exprt & expr, exprt::operandst & out )

static

Recursively flatten a (possibly nested) binary || expression into a flat list of disjuncts.

Clang represents A || B || C as or(or(A,B),C).

compound_assign_operator()

irep_idt compound_assign_operator ( const irep_idt & statement, bool is_float )

static

count_symbol_occurrences()

std::size_t count_symbol_occurrences ( const exprt & e, const irep_idt & id )

static

flatten_body_statements()

bool flatten_body_statements ( const codet & code, std::vector< const codet * > & out )

static

has_non_call_sideeffect()

bool has_non_call_sideeffect ( const exprt & e )

static

A side effect other than a nested function call (e.g.

++ on a parameter) cannot be replicated by argument substitution.

is_assigned_whole()

bool is_assigned_whole ( const exprt & assign )

static

x=f(...), and a mem-initializer from a braced list, which initialises the member in place: convert_assign lowers both without removing the rhs first.

is_braced_list()

bool is_braced_list ( const exprt & e )

static

is_braced_temporary()

bool is_braced_temporary ( const exprt & e )

static

A class temporary initialised from a braced list, whose class elements remove_temporary_object constructs in place.

is_promoted_to_int()

bool is_promoted_to_int ( const typet & type )

static

lift_old_over_bound_index()

void lift_old_over_bound_index ( exprt & expr, const std::set< irep_idt > & bound_vars, const namespacet & ns )

static

mentions_symbol()

bool mentions_symbol ( const exprt & e, const std::set< irep_idt > & ids )

static

old_raw_call_under()

exprt * old_raw_call_under ( exprt & deref )

static

__ESBMC_old(base[j]) with j bound by the enclosing quantifier takes the address of one element, which has no value outside the quantifier and so cannot be hoisted.

Snapshot the array instead — __ESBMC_old(base)[j] — leaving an operand the bound variable does not reach, so the ordinary hoisting applies and the contract layer materialises one array snapshot in place of one per index (#4219). A pointer parameter base is also rewritten, snapshotting the pointer's value and deferring the actual region copy to the contracts pass, which is the only place the pointer's __ESBMC_is_fresh extent is known (#7057). The __ESBMC_old_raw call under deref, which the __ESBMC_old macro wraps as *(T*)__ESBMC_old_raw(&x), or nullptr if this is not one.

param_under_address_of()

bool param_under_address_of ( const exprt & e, const std::set< irep_idt > & ids )

static

Substituting an argument under address_of would take the address of an rvalue or conflate distinct parameter objects (e.g.

&a != &b).

quantifier_bound_var()

const exprt * quantifier_bound_var ( const exprt & arg )

static

Extract the symbol bound by a quantifier from its first argument, which has the shape (possibly typecast) address_of(symbol).

quantifier_bound_var_id()

irep_idt quantifier_bound_var_id ( const exprt & arg )

static

quantifier_intrinsic_call()

const symbolt * quantifier_intrinsic_call ( const exprt & e, const namespacet & ns )

static

Returns the __ESBMC_forall/__ESBMC_exists symbol when e is a call to a quantifier intrinsic, nullptr otherwise.

rebuild_and_chain()

exprt rebuild_and_chain ( const exprt::operandst & conjuncts, std::size_t i )

static

Rebuild a right-associative nested binary && from a flat list of conjuncts starting at index i.

rebuild_or_chain()

exprt rebuild_or_chain ( const exprt::operandst & disjuncts, std::size_t i )

static

Rebuild a right-to-left nested binary || from a flat list of disjuncts starting at index i.

replace_symbols_in_expr()

void replace_symbols_in_expr ( exprt & e, const std::map< irep_idt, exprt > & map )

static

substitutes_in_eval_order()

bool substitutes_in_eval_order ( const exprt & e, const irep_idt & id )

static

summarize_code()

bool summarize_code ( const codet & code, summary_statet & st, const namespacet & ns )

static

Symbolically execute one structured statement of the callee, updating st.

Returns false for any construct the summarizer cannot soundly turn into a pure expression.

summary_apply_effect()

bool summary_apply_effect ( const exprt & e, summary_statet & st )

static

Apply a discarded expression statement (or a for-loop iterator) to st.

A plain =' assignment or a bare ++/–' on a tracked local scalar updates its value; a side-effect-free expression has no effect; anything else fails. The clang frontend lowers an assignment used as a statement (including an if'/for' controlled statement) to a side_effect_exprt("assign") rather than a code_assignt, which is why this is the only assignment form handled.

summary_eval()

bool summary_eval ( const exprt & e, const summary_statet & st, exprt & out )

static

Substitute tracked locals in e with their env values.

Fails when e has a side effect, takes the address of a tracked local, or — after substitution — still mentions a callee-local (a read before assignment the summarizer cannot model).

symbol_before_sideeffects()

bool symbol_before_sideeffects ( const exprt & e, const irep_idt & id, bool & seen_id )

static

Post-order (evaluation-order) walk: true when the occurrence of id precedes every other side effect in e.

Substituting a side-effecting value at a later position would reorder calls across a sequence point.

Variable Documentation

max_quantifier_inline_depth

unsigned max_quantifier_inline_depth = 16

staticconstexpr