#include <cstdlib>
#include <algorithm>
#include <map>
#include <goto-programs/contracts/contracts.h>
#include <util/expr/type_byte_size.h>
#include <goto-programs/remove_no_op.h>
#include <util/expr/base_type.h>
#include <util/lang/c_types.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/irep/std_expr.h>
#include <util/symtab/symbol.h>
#include <util/symtab/pretty.h>
#include <irep2/irep2_expr.h>
#include <irep2/irep2_utils.h>
#include <util/message/message.h>
#include <util/config/options.h>

Include dependency graph for contracts.cpp:

Classes
struct	var_assignment_info

Functions
static bool	should_add_clause_instruction (const expr2tc &clause, goto_program_instruction_typet inst_type)
	Determine whether a contract clause instruction (ASSERT or ASSUME) should be emitted for the given clause expression.
static expr2tc	transform_operands_if_changed (const expr2tc &expr, const std::function< expr2tc(const expr2tc &)> &transform)
	Apply a recursive transformation to all operands of an expression, returning a (possibly modified) clone only when a change actually occurred.
static bool	is_fresh_function (const std::string &funcname)
	Check if function name is __ESBMC_is_fresh (handles Clang USR format).
static bool	asserted_unconditionally (const expr2tc &e, const irep_idt &name)
	Whether `e` asserts the symbol `name` unconditionally: reachable from the root through conjunctions, never under a disjunction, negation or conditional.
static bool	is_fresh_in_ensures (goto_programt::const_targett it, const goto_programt &body)
	Check if is_fresh call is in ensures clause by examining next instruction.
static bool	states_separation (const code_function_call2t &call, const expr2tc &requires_clause)
	Whether an __ESBMC_is_fresh call states separation, i.e.
static expr2tc	inline_temporary_variables (const expr2tc &expr, const goto_programt &function_body, const goto_programt::const_targett &assume_location)
static bool	is_contract_intrinsic (const std::string &funcname)
	Contract intrinsics keep their own materialisation in the wrapper, which knows how to turn them into allocations, snapshots or quantifiers rather than a plain re-issued call.
static void	collect_symbol_names (const expr2tc &e, std::set< irep_idt > &out)
static std::set< goto_programt::const_targett >	select_clause_calls (std::set< irep_idt > &referenced, const std::set< irep_idt > &body_decls, const goto_programt &body)
	Calls in `body` whose results `referenced` depends on, transitively.
static std::set< irep_idt >	declared_in (const goto_programt &body)
	Symbols declared in `body`.
static std::vector< var_assignment_info >	find_all_assignments (const irep_idt &var_name, const goto_programt &function_body, const goto_programt::const_targett &target_location)
static expr2tc	reconstruct_conditional_value (const irep_idt &var_name, const goto_programt &body, const goto_programt::const_targett &use)
	Reconstruct the value a temporary holds at `use`, by walking forward over the region between its declaration and `use` and tracking the path condition under which each assignment reaches that point.
static bool	has_empty_assigns_marker (const goto_programt &function_body)
static bool	declares_frame_condition (const std::vector< expr2tc > &assigns_targets, const goto_programt &function_body)
static bool	reaches_through_pointer (const expr2tc &e)
static expr2tc	unwrap_array_decay (const expr2tc &expr)
static expr2tc	havoc_place (const expr2tc &target)
static bool	skip_pointee_havoc (const type2tc &pointee)
static expr2tc	havoc_through_pointer (const expr2tc &place, const namespacet &ns)
static bool	is_python_module_global (const symbolt &s)
static bool	is_esbmc_internal_symbol (const symbolt &s)
static expr2tc	find_stack_used_symbol (const expr2tc &e)
static BigInt	callee_frame_bits (const goto_programt &body, const namespacet &ns)
static expr2tc	substitute_frame_size (const expr2tc &e, const BigInt &bits)
template<typename Value>
static void	assign_stack_used (goto_programt &dest, const expr2tc &first, const expr2tc &second, Value value, const locationt &location, const char *comment)
static bool	is_clause_assume (const goto_programt::instructiont &i)
static bool	is_clause_check (const goto_programt::instructiont &i, const goto_programt::instructiont &clause)
	The GOTO pointer/arithmetic-safety pass emits auto-generated ASSERTs (e.g.
static void	erase_instructions (goto_programt &body, const std::set< goto_programt::targett > &doomed)
	Erase `doomed` from `body`, retargeting jumps to the next survivor.
static void	remove_clause_assumes (goto_programt &body)
	Remove the requires/ensures ASSUMEs goto_convert emitted into `body`, with the safety assertions generated from each.
static expr2tc	byte_malloc (const expr2tc &size_bytes)
	Build malloc(size_bytes) typed as u8*, so the allocation is exactly size_bytes regardless of the pointee width.
static bool	is_old_temp_symbol (const expr2tc &expr)
	The Clang temporaries that carry an __ESBMC_old() value all have "___ESBMC_old" in their name; that name is the only handle on them, which is why replace_old_in_expr matches on it too.
static bool	reads_old (const expr2tc &expr)
static expr2tc	named_base_object (const expr2tc &ptr)
static bool	find_ptr_region_use (const expr2tc &expr, const irep_idt &old_temp_thename, type2tc &out_elem_type, bool inside_quantifier=false)
	After the goto_sideeffects.cpp pointer-parameter lift, __ESBMC_old(ptr[j]) reaches this pass as dereference2t(add2t(typecast2t(old-temp-symbol), j)) – the pointer-region counterpart of the array case's already-working index2t(dereference2t(typecast2t(old-temp-symbol)), j).
static expr2tc	assigns_target_base (const expr2tc &target, const irep_idt &field)
	The base pointer of an assigns target that covers `field`, or nil if the target has some other shape.
static bool	get_comparison_sides (expr2tc &expr, expr2tc &side1, expr2tc &side2)
	Helper: extract mutable pointers to side_1 and side_2 of any comparison expression.
static bool	matches_replace_pattern (const std::string &func_name, const std::set< std::string > &to_replace)
	Helper: check if a function name matches any pattern in to_replace.
static const code_function_call2t *	as_is_fresh_call (goto_programt::const_targett it)
	The __ESBMC_is_fresh call at `it`, or nullptr if it is not one.
static size_t	fresh_param_index (const expr2tc &ptr, const code_typet::argumentst &params)
	The position of the parameter `ptr` names, or params.size() if it names none.
static void	collect_clause_globals (const expr2tc &e, const namespacet &ns, std::vector< expr2tc > &out)
	The separations a caller must discharge for the fresh parameters.
static std::vector< expr2tc >	is_fresh_separations (const code_typet::argumentst &params, const std::vector< expr2tc > &actual_args, const std::set< size_t > &fresh_params, const std::vector< expr2tc > &fresh_others, const std::vector< expr2tc > &clause_globals)
static bool	havoc_pointed_to_array (const expr2tc &target, const locationt &call_location, goto_programt &replacement)
static void	write_back_call_result (const expr2tc &ret_val, const expr2tc &call_result, const locationt &call_location, goto_programt &replacement)
static bool	contains_symbol (const expr2tc &e, const irep_idt &name)
static bool	dereferences_symbol (const expr2tc &e, const irep_idt &name)
	Whether `e` reads or writes through `name` rather than merely naming it.
static void	warn_unstated_extents (const symbolt &func, const locationt &location, const std::vector< std::string > &params)
	Tell the user why a dereference may fail: the contract states no extent for these parameters, so the harness leaves their extent unconstrained.

Function Documentation

◆ as_is_fresh_call()

const code_function_call2t * as_is_fresh_call ( goto_programt::const_targett it )

static

The __ESBMC_is_fresh call at it, or nullptr if it is not one.

◆ asserted_unconditionally()

bool asserted_unconditionally	(	const expr2tc &	e,
		const irep_idt &	name )

static

Whether e asserts the symbol name unconditionally: reachable from the root through conjunctions, never under a disjunction, negation or conditional.

A conditional __ESBMC_requires(n <= 0 || __ESBMC_is_fresh(p, n)) claims nothing about p on the other branch, so an obligation derived from it must not be imposed on every caller.

◆ assign_stack_used()

template<typename Value>

void assign_stack_used	(	goto_programt &	dest,
		const expr2tc &	first,
		const expr2tc &	second,
		Value	value,
		const locationt &	location,
		const char *	comment )

static

◆ assigns_target_base()

expr2tc assigns_target_base	(	const expr2tc &	target,
		const irep_idt &	field )

static

The base pointer of an assigns target that covers field, or nil if the target has some other shape.

Used to decide whether a snapshotted parameter could be another name for memory the clause permits writing.

Two shapes qualify. __ESBMC_assigns(*p) covers the whole pointee and so every field. p->field, optionally indexed, covers just that field, which is what keeps the exemption from reaching a sibling. A bare p names the pointer rather than the pointee, so it grants nothing here.

Note that array decay already lowers p->arr to index(member(...), 0) upstream, so stripping indices here does not lose a distinction that existed: assigns(p->arr) and assigns(p->arr[0]) reach this identically. Should per-index checking of the declared base ever be tightened, this stripping has to be revisited with it.

◆ byte_malloc()

expr2tc byte_malloc ( const expr2tc & size_bytes )

static

Build malloc(size_bytes) typed as u8*, so the allocation is exactly size_bytes regardless of the pointee width.

The result is assigned to a T * lvalue without a cast. That is deliberate and load-bearing: symex_assign dispatches on is_sideeffect2t(rhs) at the top level, so wrapping the malloc in a typecast hides it and the assignment is never routed to symex_mem. symex_mem inserts the cast itself (memory_alloc.cpp: if (rhs->type != lhs->type) rhs = typecast2tc(...)).

◆ callee_frame_bits()

BigInt callee_frame_bits	(	const goto_programt &	body,
		const namespacet &	ns )

static

◆ collect_clause_globals()

void collect_clause_globals	(	const expr2tc &	e,
		const namespacet &	ns,
		std::vector< expr2tc > &	out )

static

The separations a caller must discharge for the fresh parameters.

__ESBMC_is_fresh(p, n) says p addresses a fresh object, so it is separate from everything else the caller can reach, not merely from the other is_fresh parameters. The enforce harness grants exactly that, by backing p on its own and excluding it from the aliasing introduced for #6551, so every one of those separations has to be discharged at the call. Otherwise a caller passes one object twice, the assumed ensures becomes self-contradictory, and everything after the call is discharged vacuously (the first case in #6542). Static-lifetime objects the contract's clauses name, as addresses. A fresh pointer is separate from everything the caller can reach, so it is separate from these too, and only the ones the contract mentions are worth asserting.

◆ collect_symbol_names()

void collect_symbol_names	(	const expr2tc &	e,
		std::set< irep_idt > &	out )

static

◆ contains_symbol()

bool contains_symbol	(	const expr2tc &	e,
		const irep_idt &	name )

static

◆ declared_in()

std::set< irep_idt > declared_in ( const goto_programt & body )

static

Symbols declared in body.

A call can bind a global directly (g = compute();); re-declaring that in the wrapper would shadow the very object the clause is about, so only body-local temporaries are lifted.

◆ declares_frame_condition()

bool declares_frame_condition	(	const std::vector< expr2tc > &	assigns_targets,
		const goto_programt &	function_body )

static

◆ dereferences_symbol()

bool dereferences_symbol	(	const expr2tc &	e,
		const irep_idt &	name )

static

Whether e reads or writes through name rather than merely naming it.

◆ erase_instructions()

void erase_instructions	(	goto_programt &	body,
		const std::set< goto_programt::targett > &	doomed )

static

Erase doomed from body, retargeting jumps to the next survivor.

◆ find_all_assignments()

std::vector< var_assignment_info > find_all_assignments	(	const irep_idt &	var_name,
		const goto_programt &	function_body,
		const goto_programt::const_targett &	target_location )

static

◆ find_ptr_region_use()

bool find_ptr_region_use	(	const expr2tc &	expr,
		const irep_idt &	old_temp_thename,
		type2tc &	out_elem_type,
		bool	inside_quantifier = false )

static

After the goto_sideeffects.cpp pointer-parameter lift, __ESBMC_old(ptr[j]) reaches this pass as dereference2t(add2t(typecast2t(old-temp-symbol), j)) – the pointer-region counterpart of the array case's already-working index2t(dereference2t(typecast2t(old-temp-symbol)), j).

Find such a use of old_temp_thename anywhere under expr, recording its index expression and element type. #7057. A user can hand-write (__ESBMC_old(p) + i) outside any quantifier and get the identical dereference(add(dereference(typecast(old-temp)), i)) shape the pointer-region lift produces for __ESBMC_old(p[j]) – the __ESBMC_old(x) macro's own *(T)old_raw(&x) already contributes the inner dereference, so the two are structurally indistinguishable. The lift can only ever fire inside a quantifier's body (it is only invoked from convert_quantifier_calls), so inside_quantifier restricts matches to there, excluding a hand-written use outside one. #7057.

◆ find_stack_used_symbol()

expr2tc find_stack_used_symbol ( const expr2tc & e )

static

◆ fresh_param_index()

size_t fresh_param_index	(	const expr2tc &	ptr,
		const code_typet::argumentst &	params )

static

The position of the parameter ptr names, or params.size() if it names none.

Recorded before rebinding to actual arguments, which makes two formals bound to one actual indistinguishable from one formal named twice.

◆ get_comparison_sides()

bool get_comparison_sides	(	expr2tc &	expr,
		expr2tc *&	side1,
		expr2tc *&	side2 )

static

Helper: extract mutable pointers to side_1 and side_2 of any comparison expression.

Returns false if the expression is not a comparison.

◆ has_empty_assigns_marker()

bool has_empty_assigns_marker ( const goto_programt & function_body )

static

◆ havoc_place()

expr2tc havoc_place ( const expr2tc & target )

static

◆ havoc_pointed_to_array()

bool havoc_pointed_to_array	(	const expr2tc &	target,
		const locationt &	call_location,
		goto_programt &	replacement )

static

◆ havoc_through_pointer()

expr2tc havoc_through_pointer	(	const expr2tc &	place,
		const namespacet &	ns )

static

◆ inline_temporary_variables()

expr2tc inline_temporary_variables	(	const expr2tc &	expr,
		const goto_programt &	function_body,
		const goto_programt::const_targett &	assume_location )

static

◆ is_clause_assume()

bool is_clause_assume ( const goto_programt::instructiont & i )

static

◆ is_clause_check()

bool is_clause_check	(	const goto_programt::instructiont &	i,
		const goto_programt::instructiont &	clause )

static

The GOTO pointer/arithmetic-safety pass emits auto-generated ASSERTs (e.g.

SAME-OBJECT for a pointer comparison) from a clause expression, immediately preceding its ASSUME; for an ensures clause they reference __ESBMC_return_value, which is unbound in the original body, yielding a spurious violation (#5043). goto_check gives each of them the clause's own location. A user assertion can share it when it comes from the same macro expansion, so it is told apart by its property.

◆ is_contract_intrinsic()

bool is_contract_intrinsic ( const std::string & funcname )

static

Contract intrinsics keep their own materialisation in the wrapper, which knows how to turn them into allocations, snapshots or quantifiers rather than a plain re-issued call.

◆ is_esbmc_internal_symbol()

bool is_esbmc_internal_symbol ( const symbolt & s )

static

◆ is_fresh_function()

bool is_fresh_function ( const std::string & funcname )

static

Check if function name is __ESBMC_is_fresh (handles Clang USR format).

◆ is_fresh_in_ensures()

bool is_fresh_in_ensures	(	goto_programt::const_targett	it,
		const goto_programt &	body )

static

Check if is_fresh call is in ensures clause by examining next instruction.

◆ is_fresh_separations()

std::vector< expr2tc > is_fresh_separations	(	const code_typet::argumentst &	params,
		const std::vector< expr2tc > &	actual_args,
		const std::set< size_t > &	fresh_params,
		const std::vector< expr2tc > &	fresh_others,
		const std::vector< expr2tc > &	clause_globals )

static

◆ is_old_temp_symbol()

bool is_old_temp_symbol ( const expr2tc & expr )

static

The Clang temporaries that carry an __ESBMC_old() value all have "___ESBMC_old" in their name; that name is the only handle on them, which is why replace_old_in_expr matches on it too.

◆ is_python_module_global()

bool is_python_module_global ( const symbolt & s )

static

◆ matches_replace_pattern()

bool matches_replace_pattern	(	const std::string &	func_name,
		const std::set< std::string > &	to_replace )

static

Helper: check if a function name matches any pattern in to_replace.

Matching rules:

"*" matches everything
Otherwise, exact match against func_name or its unqualified tail (the part after the last "@"), e.g. pattern "foo" matches "c:@F@foo"

◆ named_base_object()

expr2tc named_base_object ( const expr2tc & ptr )

static

◆ reaches_through_pointer()

bool reaches_through_pointer ( const expr2tc & e )

static

◆ reads_old()

bool reads_old ( const expr2tc & expr )

static

◆ reconstruct_conditional_value()

expr2tc reconstruct_conditional_value	(	const irep_idt &	var_name,
		const goto_programt &	body,
		const goto_programt::const_targett &	use )

static

Reconstruct the value a temporary holds at use, by walking forward over the region between its declaration and use and tracking the path condition under which each assignment reaches that point.

Clang lowers a conditional whose arms contain calls – in an ensures clause that means __ESBMC_old – into a temporary written on both arms:

ASSIGN v = NONDET
IF !G THEN GOTO L
ASSIGN v = <then>
GOTO M

L: ASSIGN v = <else> M: <use of v>

Picking one assignment loses the guard and the other arm, which yields an ensures that is neither what was written nor a safe approximation of it: it can be stronger (a false failure) or weaker (a false VERIFICATION SUCCESSFUL). See #6499. Folding the reaching assignments back into an if-then-else recovers the clause exactly.

Returns: The reconstructed value, or nil when the region is not a forward-only DAG. Nil means "cannot reconstruct", never "no value": callers must diagnose rather than fall back to a guess.

◆ remove_clause_assumes()

void remove_clause_assumes ( goto_programt & body )

static

Remove the requires/ensures ASSUMEs goto_convert emitted into body, with the safety assertions generated from each.

◆ select_clause_calls()

std::set< goto_programt::const_targett > select_clause_calls	(	std::set< irep_idt > &	referenced,
		const std::set< irep_idt > &	body_decls,
		const goto_programt &	body )

static

Calls in body whose results referenced depends on, transitively.

A clause call may take another call's result (outer(inner(x))), so the operands of everything selected are themselves candidates; iterate until the referenced set stops growing. referenced is grown in place.

◆ should_add_clause_instruction()

bool should_add_clause_instruction	(	const expr2tc &	clause,
		goto_program_instruction_typet	inst_type )

static

Determine whether a contract clause instruction (ASSERT or ASSUME) should be emitted for the given clause expression.

Returns false for trivially-redundant constant-bool clauses:

ASSERT false_constant → always failing; keep it (returns true)
ASSERT true_constant → no-op assertion; skip it (returns false)
ASSUME true_constant → trivially satisfied; skip it (returns false)
ASSUME false_constant → unsatisfiable; still meaningful; keep it (returns true)
Non-constant → always emit (returns true)

◆ skip_pointee_havoc()

bool skip_pointee_havoc ( const type2tc & pointee )

static

◆ states_separation()

bool states_separation	(	const code_function_call2t &	call,
		const expr2tc &	requires_clause )

static

Whether an __ESBMC_is_fresh call states separation, i.e.

the requires clause asserts it unconditionally. Under a guard the contract claims nothing on the other branch, so the harness must not grant it there either.

◆ substitute_frame_size()

expr2tc substitute_frame_size	(	const expr2tc &	e,
		const BigInt &	bits )

static

◆ transform_operands_if_changed()

expr2tc transform_operands_if_changed	(	const expr2tc &	expr,
		const std::function< expr2tc(const expr2tc &)> &	transform )

static

Apply a recursive transformation to all operands of an expression, returning a (possibly modified) clone only when a change actually occurred.

This avoids an unnecessary clone when the transformation is a no-op.

Parameters

expr	Source expression (not modified)
transform	Function applied to each direct sub-expression; if it returns the same pointer, no change is recorded

Returns: Either expr unchanged or a clone with updated operands

◆ unwrap_array_decay()

expr2tc unwrap_array_decay ( const expr2tc & expr )

static

◆ warn_unstated_extents()

void warn_unstated_extents	(	const symbolt &	func,
		const locationt &	location,
		const std::vector< std::string > &	params )

static

Tell the user why a dereference may fail: the contract states no extent for these parameters, so the harness leaves their extent unconstrained.

◆ write_back_call_result()

void write_back_call_result	(	const expr2tc &	ret_val,
		const expr2tc &	call_result,
		const locationt &	call_location,
		goto_programt &	replacement )

static

Classes

Functions

Function Documentation

◆ as_is_fresh_call()

◆ asserted_unconditionally()

◆ assign_stack_used()

◆ assigns_target_base()

◆ byte_malloc()

◆ callee_frame_bits()

◆ collect_clause_globals()

◆ collect_symbol_names()

◆ contains_symbol()

◆ declared_in()

◆ declares_frame_condition()

◆ dereferences_symbol()

◆ erase_instructions()

◆ find_all_assignments()

◆ find_ptr_region_use()

◆ find_stack_used_symbol()

◆ fresh_param_index()

◆ get_comparison_sides()

◆ has_empty_assigns_marker()

◆ havoc_place()

◆ havoc_pointed_to_array()

◆ havoc_through_pointer()

◆ inline_temporary_variables()

◆ is_clause_assume()

◆ is_clause_check()

◆ is_contract_intrinsic()

◆ is_esbmc_internal_symbol()

◆ is_fresh_function()

◆ is_fresh_in_ensures()

◆ is_fresh_separations()

◆ is_old_temp_symbol()

◆ is_python_module_global()

◆ matches_replace_pattern()

◆ named_base_object()

◆ reaches_through_pointer()

◆ reads_old()

◆ reconstruct_conditional_value()

◆ remove_clause_assumes()

◆ select_clause_calls()

◆ should_add_clause_instruction()

◆ skip_pointee_havoc()

◆ states_separation()

◆ substitute_frame_size()

◆ transform_operands_if_changed()

◆ unwrap_array_decay()

◆ warn_unstated_extents()

◆ write_back_call_result()