This class applies the loop contract transformation to a loop in a goto function. More...

#include <dfcc_instrument_loop.h>

Collaboration diagram for dfcc_instrument_loopt:

Public Member Functions
	dfcc_instrument_loopt (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
	Constructor for the loop contract instrumentation class. More...

void	operator() (const std::size_t loop_id, const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)
	Replaces a loop by a base + step abstraction generated from its contract. More...

std::size_t	get_max_assigns_clause_size () const
	Maximum number of assigns clause targets. More...

Protected Member Functions
std::unordered_map< exprt, symbol_exprt, irep_hash >	add_prehead_instructions (const std::size_t loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &assigns_instrs, exprt &invariant, const exprt::operandst &assigns, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const irep_idt &symbol_mode)
	Adds instructions of prehead block, and return history variables. More...

goto_programt::instructiont::targett	add_step_instructions (const std::size_t loop_id, const std::size_t cbmc_loop_id, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &havoc_instrs, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &loop_write_set, const exprt &outer_write_set, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars)
	Adds instructions of the step block, and returns the STEP jump target so that it can be used to jump back from the loop body block. More...

void	add_body_instructions (const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &entered_loop, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars, const goto_programt::instructiont::targett &step_case_target, const irep_idt &symbol_mode)
	Adds instructions of the body block. More...

void	add_exit_instructions (const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, goto_programt::targett loop_head, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const std::unordered_map< exprt, symbol_exprt, irep_hash > &history_var_map, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars)
	Adds instructions of the exit block. More...

Protected Attributes
std::size_t	max_assigns_clause_size = 0

goto_modelt &	goto_model

messaget	log

dfcc_libraryt &	library

dfcc_spec_functionst &	spec_functions

dfcc_contract_clauses_codegent &	contract_clauses_codegen

namespacet	ns

Detailed Description

This class applies the loop contract transformation to a loop in a goto function.

Definition at line 35 of file dfcc_instrument_loop.h.

Constructor & Destructor Documentation

◆ dfcc_instrument_loopt()

dfcc_instrument_loopt::dfcc_instrument_loopt	(	goto_modelt &	goto_model,
		message_handlert &	message_handler,
		dfcc_libraryt &	library,
		dfcc_spec_functionst &	spec_functions,
		dfcc_contract_clauses_codegent &	contract_clauses_codegen
	)

Constructor for the loop contract instrumentation class.

Parameters

[in,out]	goto_model	GOTO model being instrumented
[in,out]	message_handler	For status/debug output
[in,out]	library	DFCC instrumentation library functions
[in,out]	spec_functions	Class used to translate assigns clauses to GOTO instructions.
[in,out]	contract_clauses_codegen	Class used to generate GOTO instructions from contract clauses.

Definition at line 27 of file dfcc_instrument_loop.cpp.

Member Function Documentation

◆ add_body_instructions()

void dfcc_instrument_loopt::add_body_instructions	(	const std::size_t	loop_id,
		const std::size_t	cbmc_loop_id,
		goto_functionst::goto_functiont &	goto_function,
		symbol_table_baset &	symbol_table,
		goto_programt::targett	loop_head,
		goto_programt::targett	loop_latch,
		exprt &	invariant,
		const exprt::operandst &	decreases_clauses,
		const symbol_exprt &	entered_loop,
		const symbol_exprt &	in_base_case,
		const std::vector< symbol_exprt > &	old_decreases_vars,
		const std::vector< symbol_exprt > &	new_decreases_vars,
		const goto_programt::instructiont::targett &	step_case_target,
		const irep_idt &	symbol_mode
	)

protected

Adds instructions of the body block.

HEAD: // Loop body block
  ... eval guard ...
  IF (!guard) GOTO EXIT;
  ... loop body ...
  // instrumentation
  entered_loop = true
  // Jump back to the step case if the loop can run at least once
  IF (in_base_case) GOTO STEP;
  ASSERT(loop_invariant);
   new_variant = loop_decreases;
  ASSERT(new_variant < old_variant);
  ASSUME(false);

Parameters

[in]	loop_id	Id assigned to the loop by the `cfg_info` numbering.
[in]	cbmc_loop_id	Id assigned to the loop by CBMC's numbering.
[in,out]	goto_function	The function containing the loop.
[in,out]	symbol_table	Symbol table of the model.
[in]	loop_head	Head node of the loop.
[in]	loop_latch	Latch node of the loop.
[in]	invariant	Loop invariant.
[in]	decreases_clauses	Decreases clause.
[in]	entered_loop	temporary variable `entered_loop`.
[in]	in_base_case	temporary variable `in_base_case`.
[in]	old_decreases_vars	temporary vars of old decreases clauses.
[in]	new_decreases_vars	temporary vars of new decreases clauses.
[in]	step_case_target	Target of the head of the step case block.
[in]	symbol_mode	Language mode of the function.

Definition at line 465 of file dfcc_instrument_loop.cpp.

◆ add_exit_instructions()

void dfcc_instrument_loopt::add_exit_instructions	(	const std::size_t	loop_id,
		const std::size_t	cbmc_loop_id,
		goto_functionst::goto_functiont &	goto_function,
		goto_programt::targett	loop_head,
		const symbol_exprt &	loop_write_set,
		const symbol_exprt &	addr_of_loop_write_set,
		const std::unordered_map< exprt, symbol_exprt, irep_hash > &	history_var_map,
		const symbol_exprt &	entered_loop,
		const symbol_exprt &	initial_invariant,
		const symbol_exprt &	in_base_case,
		const std::vector< symbol_exprt > &	old_decreases_vars,
		const std::vector< symbol_exprt > &	new_decreases_vars
	)

protected

Adds instructions of the exit block.

EXIT:
  // check that step case was checked if loop can run once
  ASSUME (entered_loop ==> !in_base_case);
  DEAD loop_entry history vars, in_base_case;
  DEAD initial_invariant, entered_loop;
  DEAD old_variant, in_loop_havoc_block;
  __write_set_release(w_loop);
  DEAD __ws_loop, ws_loop;
 
  ... postamble ...

An EXIT block is inserted at the target instruction of each exiting instruction.

Parameters

[in]	loop_id	Id assigned to the loop by the `cfg_info` numbering.
[in]	cbmc_loop_id	Id assigned to the loop by CBMC's loop numbering.
[in,out]	goto_function	The function containing the loop.
[in]	loop_head	Head node of the loop.
[in]	loop_write_set	Stack allocated loop write set variable.
[in]	addr_of_loop_write_set	Loop write set pointer variable.
[in]	history_var_map	Map storing history variables of the loop.
[in]	entered_loop	temporary variable `entered_loop`.
[in]	initial_invariant	temporary variable `initial_invariant`.
[in]	in_base_case	temporary variable `in_base_case`.
[in]	old_decreases_vars	temporary vars of old decreases clauses.
[in]	new_decreases_vars	temporary vars of new decreases clauses.

Definition at line 590 of file dfcc_instrument_loop.cpp.

◆ add_prehead_instructions()

std::unordered_map< exprt, symbol_exprt, irep_hash > dfcc_instrument_loopt::add_prehead_instructions	(	const std::size_t	loop_id,
		goto_functionst::goto_functiont &	goto_function,
		symbol_table_baset &	symbol_table,
		goto_programt::targett	loop_head,
		goto_programt::targett	loop_latch,
		goto_programt &	assigns_instrs,
		exprt &	invariant,
		const exprt::operandst &	assigns,
		const symbol_exprt &	loop_write_set,
		const symbol_exprt &	addr_of_loop_write_set,
		const symbol_exprt &	entered_loop,
		const symbol_exprt &	initial_invariant,
		const symbol_exprt &	in_base_case,
		const irep_idt &	symbol_mode
	)

protected

Adds instructions of prehead block, and return history variables.

Occurrences of history expressions in invariant expressions are replaced by fresh variables and instructions to snapshot their value before entering the loop are added to the pre-head instructions. The mapping of history variables to fresh variables is returned by the function.

... preamble ...
 
// Prehead block: Declare & initialize instrumentation variables
snapshot loop_entry history vars;
entered_loop = false
initial_invariant = loop_invariant;
in_base_case = true;
__ws_loop;
ws_loop := address_of(__ws_loop);
ws_loop := __write_set_create();
__write_set_add(ws_loop, loop_assigns);
__write_set_add(ws_loop, local_statics);
GOTO HEAD;

Parameters

[in]	loop_id	Id of the loop to transform.
[in,out]	goto_function	The function containing the loop.
[in,out]	symbol_table	Symbol table of the model.
[in,out]	loop_head	Head node of the loop.
[in,out]	loop_latch	Latch node of the loop.
[out]	assigns_instrs	`goto_programt` that contains instructions of populating assigns into the loop write set.
[in]	invariant	Loop invariants.
[in]	assigns	Assigns targets of the loop.
[in]	loop_write_set	Stack allocated loop write set variable.
[in]	addr_of_loop_write_set	Loop write set pointer variable.
[in]	entered_loop	temporary variable `entered_loop`.
[in]	initial_invariant	temporary variable `initial_invariant`.
[in]	in_base_case	temporary variable `in_base_case`.
[in]	symbol_mode	Language mode of the function.

Returns: history_var_map that maps variables to loop_entry variables.

Definition at line 203 of file dfcc_instrument_loop.cpp.

◆ add_step_instructions()

goto_programt::instructiont::targett dfcc_instrument_loopt::add_step_instructions	(	const std::size_t	loop_id,
		const std::size_t	cbmc_loop_id,
		const irep_idt &	function_id,
		goto_functionst::goto_functiont &	goto_function,
		symbol_table_baset &	symbol_table,
		goto_programt::targett	loop_head,
		goto_programt::targett	loop_latch,
		goto_programt &	havoc_instrs,
		exprt &	invariant,
		const exprt::operandst &	decreases_clauses,
		const symbol_exprt &	loop_write_set,
		const exprt &	outer_write_set,
		const symbol_exprt &	initial_invariant,
		const symbol_exprt &	in_base_case,
		const std::vector< symbol_exprt > &	old_decreases_vars
	)

protected

Adds instructions of the step block, and returns the STEP jump target so that it can be used to jump back from the loop body block.

STEP: // Loop step block: havoc the loop state
  ASSERT(initial_invariant);
  __write_set_check_inclusion(ws_loop, ws_parent);
  in_base_case = false;
  in_loop_havoc_block = true;
  havoc(assigns_clause_targets);
  in_loop_havoc_block = false;
  ASSUME(loop_invariant);
  old_variant = loop_decreases;

Parameters

[in]	loop_id	Id of the loop to transform.
[in]	cbmc_loop_id	Id assigned to the loop by CBMC's loop numbering.
[in]	function_id	Id of the function.
[in,out]	goto_function	The function containing the loop.
[in,out]	symbol_table	Symbol table of the model.
[in]	loop_head	Head node of the loop.
[in]	loop_latch	Latch node of the loop.
[in,out]	havoc_instrs	`goto_programt` that contains instructions of havocing assigns targets in the write set.
[in]	invariant	Loop invariant.
[in]	decreases_clauses	Decreases clause.
[in]	loop_write_set	Stack allocated loop write set variable.
[in]	outer_write_set	The write set of the outer loop.
[in]	initial_invariant	temporary variable `initial_invariant`.
[in]	in_base_case	temporary variable `in_base_case`.
[in]	old_decreases_vars	temporary vars of decreases clauses.

Returns: The STEP jump target.

Definition at line 317 of file dfcc_instrument_loop.cpp.

◆ get_max_assigns_clause_size()

std::size_t dfcc_instrument_loopt::get_max_assigns_clause_size ( ) const

inline

Maximum number of assigns clause targets.

Definition at line 141 of file dfcc_instrument_loop.h.

◆ operator()()

void dfcc_instrument_loopt::operator()	(	const std::size_t	loop_id,
		const irep_idt &	function_id,
		goto_functiont &	goto_function,
		dfcc_cfg_infot &	cfg_info,
		const std::set< symbol_exprt > &	local_statics,
		std::set< irep_idt > &	function_pointer_contracts
	)

Replaces a loop by a base + step abstraction generated from its contract.

Parameters

[in]	loop_id	Id of the loop to transform in `cfg_info`.
[in]	function_id	Id of the function in which that loop is.
[in,out]	goto_function	GOTO function to transform.
[in,out]	cfg_info	Control flow graph information for `goto_function`.
[in]	local_statics	Set of local statics declared in `goto_function`.
[out]	function_pointer_contracts	Destination set for function pointer contracts discovered during the loop contract transformation.

The loop:

``` ... preamble ... HEAD: ... eval guard ... if (!guard) goto EXIT; ... loop body ... goto HEAD; EXIT: ... postamble ... ```

Gets rewritten into:

``` ... preamble ...

// Prehead block: Declare & initialize instrumentation variables snapshot loop_entry history vars; entered_loop = false initial_invariant = loop_invariant; in_base_case = true; __ws_loop; ws_loop := address_of(__ws_loop); __write_set_create(ws_loop); __write_set_add(ws_loop, loop_assigns); __write_set_add(ws_loop, local_statics); GOTO HEAD;

STEP: // Loop step block: havoc the loop state ASSERT(initial_invariant); __write_set_check_inclusion(ws_loop, ws_parent); in_base_case = false; in_loop_havoc_block = true; havoc(assigns_clause_targets); in_loop_havoc_block = false; ASSUME(loop_invariant); old_variant = loop_decreases;

HEAD: // Loop body block ... eval guard ... IF (!guard) GOTO EXIT; ... loop body ... // instrumentation entered_loop = true // Jump back to the step case if the loop can run at least once IF (in_base_case) GOTO STEP; ASSERT(loop_invariant); */ // new_variant = loop_decreases; /** ASSERT(new_variant < old_variant); ASSUME(false);

EXIT: // check that step case was checked if loop can run once ASSUME (entered_loop ==> !in_base_case); DEAD loop_entry history vars, in_base_case; DEAD initial_invariant, entered_loop; DEAD old_variant, in_loop_havoc_block; __write_set_release(w_loop); DEAD __ws_loop, ws_loop;

... postamble ... ```

Where the EXIT block is inserted at the target instruction of each exiting instruction.

Definition at line 42 of file dfcc_instrument_loop.cpp.

Member Data Documentation

◆ contract_clauses_codegen

dfcc_contract_clauses_codegent& dfcc_instrument_loopt::contract_clauses_codegen

protected

Definition at line 153 of file dfcc_instrument_loop.h.

◆ goto_model

goto_modelt& dfcc_instrument_loopt::goto_model

protected

Definition at line 149 of file dfcc_instrument_loop.h.

◆ library

dfcc_libraryt& dfcc_instrument_loopt::library

protected

Definition at line 151 of file dfcc_instrument_loop.h.

◆ log

messaget dfcc_instrument_loopt::log

protected

Definition at line 150 of file dfcc_instrument_loop.h.

◆ max_assigns_clause_size

std::size_t dfcc_instrument_loopt::max_assigns_clause_size = 0

protected

Definition at line 148 of file dfcc_instrument_loop.h.

◆ ns

namespacet dfcc_instrument_loopt::ns

protected

Definition at line 154 of file dfcc_instrument_loop.h.

◆ spec_functions

dfcc_spec_functionst& dfcc_instrument_loopt::spec_functions

protected

Definition at line 152 of file dfcc_instrument_loop.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ dfcc_instrument_loopt()

Member Function Documentation

◆ add_body_instructions()

◆ add_exit_instructions()

◆ add_prehead_instructions()

◆ add_step_instructions()

◆ get_max_assigns_clause_size()

◆ operator()()

Member Data Documentation

◆ contract_clauses_codegen

◆ goto_model

◆ library

◆ log

◆ max_assigns_clause_size

◆ ns

◆ spec_functions