#include <goto_loop_invariant.h>

Inheritance diagram for goto_loop_invariantt:

Public Member Functions
	goto_loop_invariantt (const irep_idt &_function_name, goto_functionst &_goto_functions, goto_functiont &_goto_function, contextt &_context, bool _use_frame_rule)
Public Member Functions inherited from goto_loopst
	goto_loopst (const irep_idt &_function_name, goto_functionst &_goto_functions, goto_functiont &_goto_function)
void	find_function_loops ()
void	dump () const
const function_loopst &	get_loops () const
function_loopst &	get_loops ()

Static Public Attributes
static constexpr size_t	kMaxInvariantSearchBack = 10
	Maximum number of instructions to search backwards from the loop head when locating the LOOP_INVARIANT instruction.

Protected Member Functions
void	goto_loop_invariant ()
void	convert_loop_with_invariant (loopst &loop)
std::vector< expr2tc >	extract_loop_invariants (const loopst &loop)
std::vector< expr2tc >	extract_loop_assigns (const loopst &loop)
void	extract_and_remove_side_effects (goto_programt::targett loop_head, const loopst &loop, const std::vector< expr2tc > &invariants, goto_programt &side_effects_out)
	Collect DECL/FUNCTION_CALL instructions immediately before LOOP_INVARIANT that define temporaries used in the invariant.
void	insert_assert_before_loop (goto_programt::targett &loop_head, const std::vector< expr2tc > &invariants, const goto_programt &side_effects)
bool	pointees_havocable (const loopst &loop) const
	False when a pointee the loop writes is out of the havoc's reach, which leaves the loop to the unwinder.
void	havoc_pointees (const loopst &loop, const locationt &loc, goto_programt &dest) const
	Havoc the objects the loop writes through a pointer.
void	insert_havoc_and_assume_before_condition (goto_programt::targett loop_head, const loopst &loop, const std::vector< expr2tc > &invariants, const std::vector< expr2tc > &loop_assigns, goto_programt &side_effects)
void	insert_inductive_step_and_termination (const loopst &loop, const std::vector< expr2tc > &invariants, const goto_programt &side_effects)
Protected Member Functions inherited from goto_loopst
void	create_function_loop (goto_programt::instructionst::iterator loop_head, goto_programt::instructionst::iterator loop_exit)
void	get_modified_variables (goto_programt::instructionst::iterator instruction, function_loopst::iterator loop, std::vector< irep_idt > &function_name)
bool	compute_function_summary (const irep_idt &fname, std::vector< irep_idt > &in_progress, function_summaryt &out)
	Compute (or fetch the cached) summary of fname.
bool	summarise_call (const code_function_call2t &call, std::vector< irep_idt > &in_progress, function_summaryt &local, std::vector< expr2tc > &written_ptrs)
	Fold a call inside a callee into that callee's summary.
void	collect_address_taken (const expr2tc &expr, function_summaryt &out) const
	A variable whose address the callee takes can be reassigned through that address, which collect_lhs_symbols does not see.
void	collect_loop_symbols (const expr2tc &expr, loopst::loop_varst &out) const
	Collect the leaf symbols of expr into out, applying check_var_name.
void	collect_lhs_symbols (const expr2tc &expr, function_summaryt &out) const
	Walk an assignment LHS, classifying each leaf symbol: storage that is actually written goes to modified, sub-expressions used to locate that storage (pointer in *p, index in arr[i]) go to unmodified.
void	add_modified_var (loopst &loop, const expr2tc &expr)
void	add_unmodified_var (loopst &loop, const expr2tc &expr)
void	add_loop_var (loopst &loop, const expr2tc &expr, bool is_modified)

Static Protected Member Functions
static void	collect_symbols (const expr2tc &expr, std::set< irep_idt > &symbols)
	Collect all symbol names reachable from an expression tree.
static type2tc	havoc_pointee_type (const expr2tc &ptr, const namespacet &ns)
	The type of *ptr when the havoc can cover it, nil otherwise: a pointee with no static width (a VLA, an infinite array, an unresolved type) has no nondet value to build, and a large aggregate costs more to encode than the loop it replaces – the 1024-element poly of quantified_array_invariant goes from under a second to minutes (issue #7502).
Static Protected Member Functions inherited from goto_loopst
static void	merge_summary (const function_summaryt &from, function_summaryt &out)
static void	note_pointer_write (const expr2tc &target, function_summaryt &local, std::vector< expr2tc > &written_ptrs)
static void	apply_callee_summary (loopst &loop, const function_summaryt &summary, const code_function_call2t &call)

Protected Attributes
contextt &	context
bool	use_frame_rule
frame_enforcert *	active_frame_enforcer = nullptr
	Frame enforcer shared between the havoc step (ASSUME) and the inductive step (ASSERT compliance check) for the currently-processed loop.
std::vector< expr2tc >	active_loop_assigns
	Assigns targets for the current loop (mirrors loop_assigns passed to insert_havoc_and_assume_before_condition, kept for use in the ASSERT step).
Protected Attributes inherited from goto_loopst
irep_idt	function_name
goto_functionst &	goto_functions
goto_functiont &	goto_function
function_loopst	function_loops
std::unordered_map< irep_idt, function_summaryt, irep_id_hash >	function_summary_cache

Static Protected Attributes
static constexpr unsigned	kMaxHavocPointeeBits = 1024
	Largest pointee, in bits, the havoc will cover.

Additional Inherited Members
Protected Types inherited from goto_loopst
typedef std::list< loopst >	function_loopst

Constructor & Destructor Documentation

◆ goto_loop_invariantt()

goto_loop_invariantt::goto_loop_invariantt	(	const irep_idt &	_function_name,
		goto_functionst &	_goto_functions,
		goto_functiont &	_goto_function,
		contextt &	_context,
		bool	_use_frame_rule )

inline

Member Function Documentation

◆ collect_symbols()

void goto_loop_invariantt::collect_symbols	(	const expr2tc &	expr,
		std::set< irep_idt > &	symbols )

staticprotected

Collect all symbol names reachable from an expression tree.

◆ convert_loop_with_invariant()

void goto_loop_invariantt::convert_loop_with_invariant ( loopst & loop )

protected

◆ extract_and_remove_side_effects()

void goto_loop_invariantt::extract_and_remove_side_effects	(	goto_programt::targett	loop_head,
		const loopst &	loop,
		const std::vector< expr2tc > &	invariants,
		goto_programt &	side_effects_out )

protected

Collect DECL/FUNCTION_CALL instructions immediately before LOOP_INVARIANT that define temporaries used in the invariant.

Remove them from the GOTO program and place them in side_effects_out for re-insertion before each ASSERT/ASSUME so they are re-evaluated with the havoc'd variables.

◆ extract_loop_assigns()

std::vector< expr2tc > goto_loop_invariantt::extract_loop_assigns ( const loopst & loop )

protected

◆ extract_loop_invariants()

std::vector< expr2tc > goto_loop_invariantt::extract_loop_invariants ( const loopst & loop )

protected

◆ goto_loop_invariant()

void goto_loop_invariantt::goto_loop_invariant ( )

protected

◆ havoc_pointee_type()

type2tc goto_loop_invariantt::havoc_pointee_type	(	const expr2tc &	ptr,
		const namespacet &	ns )

staticprotected

The type of *ptr when the havoc can cover it, nil otherwise: a pointee with no static width (a VLA, an infinite array, an unresolved type) has no nondet value to build, and a large aggregate costs more to encode than the loop it replaces – the 1024-element poly of quantified_array_invariant goes from under a second to minutes (issue #7502).

◆ havoc_pointees()

void goto_loop_invariantt::havoc_pointees	(	const loopst &	loop,
		const locationt &	loc,
		goto_programt &	dest ) const

protected

Havoc the objects the loop writes through a pointer.

Storage a loop writes through a pointer has no named symbol, so havoc the pointed-to object through the pointer itself and let symex resolve it against its own value set.

Without this the pointee keeps its pre-loop value across the abstract iteration and a claim about it after the loop is decided on state the loop overwrote (issue #7478).

◆ insert_assert_before_loop()

void goto_loop_invariantt::insert_assert_before_loop	(	goto_programt::targett &	loop_head,
		const std::vector< expr2tc > &	invariants,
		const goto_programt &	side_effects )

protected

◆ insert_havoc_and_assume_before_condition()

void goto_loop_invariantt::insert_havoc_and_assume_before_condition	(	goto_programt::targett	loop_head,
		const loopst &	loop,
		const std::vector< expr2tc > &	invariants,
		const std::vector< expr2tc > &	loop_assigns,
		goto_programt &	side_effects )

protected

◆ insert_inductive_step_and_termination()

void goto_loop_invariantt::insert_inductive_step_and_termination	(	const loopst &	loop,
		const std::vector< expr2tc > &	invariants,
		const goto_programt &	side_effects )

protected

◆ pointees_havocable()

bool goto_loop_invariantt::pointees_havocable ( const loopst & loop ) const

protected

False when a pointee the loop writes is out of the havoc's reach, which leaves the loop to the unwinder.

Member Data Documentation

◆ active_frame_enforcer

frame_enforcert* goto_loop_invariantt::active_frame_enforcer = nullptr

protected

Frame enforcer shared between the havoc step (ASSUME) and the inductive step (ASSERT compliance check) for the currently-processed loop.

Allocated in insert_havoc_and_assume_before_condition, freed in convert_loop_with_invariant after insert_inductive_step_and_termination.

◆ active_loop_assigns

std::vector<expr2tc> goto_loop_invariantt::active_loop_assigns

protected

Assigns targets for the current loop (mirrors loop_assigns passed to insert_havoc_and_assume_before_condition, kept for use in the ASSERT step).

◆ context

contextt& goto_loop_invariantt::context

protected

◆ kMaxHavocPointeeBits

unsigned goto_loop_invariantt::kMaxHavocPointeeBits = 1024

staticconstexprprotected

Largest pointee, in bits, the havoc will cover.

Measured on quantified_array_invariant: 128 bits is free, 4096 costs eight seconds and 16384 nine minutes.

◆ kMaxInvariantSearchBack

size_t goto_loop_invariantt::kMaxInvariantSearchBack = 10

staticconstexpr

Maximum number of instructions to search backwards from the loop head when locating the LOOP_INVARIANT instruction.

A typical for-loop init (DECL + ASSIGN for the counter) contributes 2 steps, leaving ample room for up to ~4 extra declarations before the invariant. This is the only definition: goto_loop_invariant.cpp's free functions name it qualified, so extract_invariants_near, extract_loop_assigns and extract_and_remove_side_effects search the same window, and so does goto_synthesise_loop_invariants when deciding whether a loop already carries a user-written invariant.

◆ use_frame_rule

bool goto_loop_invariantt::use_frame_rule

protected

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

src/goto-programs/goto_loop_invariant.h
src/goto-programs/goto_loop_invariant.cpp

Public Member Functions

Static Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Static Protected Attributes

Additional Inherited Members

Constructor & Destructor Documentation

◆ goto_loop_invariantt()

Member Function Documentation

◆ collect_symbols()

◆ convert_loop_with_invariant()

◆ extract_and_remove_side_effects()

◆ extract_loop_assigns()

◆ extract_loop_invariants()

◆ goto_loop_invariant()

◆ havoc_pointee_type()

◆ havoc_pointees()

◆ insert_assert_before_loop()

◆ insert_havoc_and_assume_before_condition()

◆ insert_inductive_step_and_termination()

◆ pointees_havocable()

Member Data Documentation

◆ active_frame_enforcer

◆ active_loop_assigns

◆ context

◆ kMaxHavocPointeeBits

◆ kMaxInvariantSearchBack

◆ use_frame_rule