#include <reachability_slicer_class.h>

Collaboration diagram for reachability_slicert:

Classes
struct	search_stack_entryt
	A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in `fixedpoint_to_assertions` and `fixedpoint_from_assertions`. More...

struct	slicer_entryt

Public Member Functions
void	operator() (goto_functionst &goto_functions, const slicing_criteriont &criterion, bool include_forward_reachability, message_handlert &)

Protected Types
typedef cfg_baset< slicer_entryt >	cfgt

typedef std::stack< cfgt::entryt >	queuet

Protected Member Functions
bool	is_same_target (goto_programt::const_targett it1, goto_programt::const_targett it2) const

void	fixedpoint_to_assertions (const is_threadedt &is_threaded, const slicing_criteriont &criterion)
	Perform backward depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently. More...

void	fixedpoint_from_assertions (const is_threadedt &is_threaded, const slicing_criteriont &criterion)
	Perform forwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently. More...

void	slice (goto_functionst &goto_functions)
	This function removes all instructions that have the flag reaches_assertion or reachable_from_assertion set to true;. More...

Protected Attributes
cfgt	cfg

Private Member Functions
std::vector< cfgt::node_indext >	backward_outwards_walk_from (std::vector< cfgt::node_indext >)
	Perform backward depth-first search of the control-flow graph of the goto program, starting from a given set of nodes. More...

void	backward_inwards_walk_from (std::vector< cfgt::node_indext >)
	Perform backward depth-first search of the control-flow graph of the goto program, starting from a given set of nodes. More...

std::vector< cfgt::node_indext >	forward_outwards_walk_from (std::vector< cfgt::node_indext >)
	Perform forwards depth-first search of the control-flow graph of the goto program, starting from a given set of nodes. More...

void	forward_inwards_walk_from (std::vector< cfgt::node_indext >)
	Perform forwards depth-first search of the control-flow graph of the goto program, starting from a given set of nodes. More...

void	forward_walk_call_instruction (const cfgt::nodet &call_node, std::vector< cfgt::node_indext > &callsite_successor_stack, std::vector< cfgt::node_indext > &callee_head_stack)
	Process a call instruction during a forwards reachability walk. More...

std::vector< cfgt::node_indext >	get_sources (const is_threadedt &is_threaded, const slicing_criteriont &criterion)
	Get the set of nodes that correspond to the given criterion, or that can appear in concurrent execution. More...

Detailed Description

Definition at line 21 of file reachability_slicer_class.h.

Member Typedef Documentation

◆ cfgt

typedef cfg_baset<slicer_entryt> reachability_slicert::cfgt

protected

Definition at line 46 of file reachability_slicer_class.h.

◆ queuet

typedef std::stack<cfgt::entryt> reachability_slicert::queuet

protected

Definition at line 49 of file reachability_slicer_class.h.

Member Function Documentation

◆ backward_inwards_walk_from()

void reachability_slicert::backward_inwards_walk_from ( std::vector< cfgt::node_indext > stack )

private

Perform backward depth-first search of the control-flow graph of the goto program, starting from a given set of nodes.

This walks into return sites but not out of call sites; this is the opposite of backward_outwards_walk_from above. Note since the two functions use the same reaches_assertion flag to track where they have been, it is important the outwards walk is performed before the inwards walk, as encountering a function while walking outwards visits strictly more code than when walking inwards.

Parameters

stack nodes to start from

Definition at line 155 of file reachability_slicer.cpp.

◆ backward_outwards_walk_from()

std::vector< reachability_slicert::cfgt::node_indext > reachability_slicert::backward_outwards_walk_from ( std::vector< cfgt::node_indext > stack )

private

Perform backward depth-first search of the control-flow graph of the goto program, starting from a given set of nodes.

At call sites this walks to all possible callers, and at return sites it remembers the site but doesn't walk in (this will be done in backward_inwards_walk_from below).

Parameters

stack nodes to start from

Returns: vector of return-site nodes encountered during the walk

Definition at line 105 of file reachability_slicer.cpp.

◆ fixedpoint_from_assertions()

void reachability_slicert::fixedpoint_from_assertions	(	const is_threadedt &	is_threaded,
		const slicing_criteriont &	criterion
	)

protected

Perform forwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.

Set reaches_assertion to true for every instruction visited.

Parameters

is_threaded	Instructions that might be executed concurrently
criterion	the criterion we are trying to hit

Definition at line 343 of file reachability_slicer.cpp.

◆ fixedpoint_to_assertions()

void reachability_slicert::fixedpoint_to_assertions	(	const is_threadedt &	is_threaded,
		const slicing_criteriont &	criterion
	)

protected

Perform backward depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.

Set reaches_assertion to true for every instruction visited.

Parameters

is_threaded	Instructions that might be executed concurrently
criterion	the criterion we are trying to hit

Definition at line 204 of file reachability_slicer.cpp.

◆ forward_inwards_walk_from()

void reachability_slicert::forward_inwards_walk_from ( std::vector< cfgt::node_indext > stack )

private

Perform forwards depth-first search of the control-flow graph of the goto program, starting from a given set of nodes.

Steps into callsites; ignores return sites, which have been taken care of by forward_outwards_walk_from. Note it is important this is done after the outwards walk, because the outwards walk visits strictly more functions as it visits all possible callers.

Parameters

stack nodes to start from

Definition at line 305 of file reachability_slicer.cpp.

◆ forward_outwards_walk_from()

std::vector< reachability_slicert::cfgt::node_indext > reachability_slicert::forward_outwards_walk_from ( std::vector< cfgt::node_indext > stack )

private

Perform forwards depth-first search of the control-flow graph of the goto program, starting from a given set of nodes.

Steps over and records callsites for a later inwards walk; explores all possible callers at return sites, eventually walking out into __CPROVER__start.

Parameters

stack nodes to start from

Returns: vector of encounted callee head nodes

Definition at line 267 of file reachability_slicer.cpp.

◆ forward_walk_call_instruction()

void reachability_slicert::forward_walk_call_instruction	(	const cfgt::nodet &	call_node,
		std::vector< cfgt::node_indext > &	callsite_successor_stack,
		std::vector< cfgt::node_indext > &	callee_head_stack
	)

private

Process a call instruction during a forwards reachability walk.

Parameters

call_node	function-call graph node. Its single successor will be the head of the callee if the callee body exists, or the call instruction's immediate successor otherwise.
callsite_successor_stack	The index of the callsite's local successor node will be added to this vector if it is reachable.
callee_head_stack	The index of the callee body head node will be added to this vector if the callee has a body.

Definition at line 227 of file reachability_slicer.cpp.

◆ get_sources()

std::vector< reachability_slicert::cfgt::node_indext > reachability_slicert::get_sources	(	const is_threadedt &	is_threaded,
		const slicing_criteriont &	criterion
	)

private

Get the set of nodes that correspond to the given criterion, or that can appear in concurrent execution.

None of these should be sliced away so they are used as a basis for the search.

Parameters

is_threaded	Instructions that might be executed concurrently
criterion	The criterion we care about

Definition at line 63 of file reachability_slicer.cpp.

◆ is_same_target()

bool reachability_slicert::is_same_target	(	goto_programt::const_targett	it1,
		goto_programt::const_targett	it2
	)		const

protected

Definition at line 87 of file reachability_slicer.cpp.

◆ operator()()

void reachability_slicert::operator()	(	goto_functionst &	goto_functions,
		const slicing_criteriont &	criterion,
		bool	include_forward_reachability,
		message_handlert &	message_handler
	)

Definition at line 30 of file reachability_slicer.cpp.

◆ slice()

void reachability_slicert::slice ( goto_functionst & goto_functions )

protected

This function removes all instructions that have the flag reaches_assertion or reachable_from_assertion set to true;.

Definition at line 360 of file reachability_slicer.cpp.

Member Data Documentation

◆ cfg

cfgt reachability_slicert::cfg

protected

Definition at line 47 of file reachability_slicer_class.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/reachability_slicer_class.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/reachability_slicer.cpp

Classes

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Private Member Functions

Detailed Description

Member Typedef Documentation

◆ cfgt

◆ queuet

Member Function Documentation

◆ backward_inwards_walk_from()

◆ backward_outwards_walk_from()

◆ fixedpoint_from_assertions()

◆ fixedpoint_to_assertions()

◆ forward_inwards_walk_from()

◆ forward_outwards_walk_from()

◆ forward_walk_call_instruction()

◆ get_sources()

◆ is_same_target()

◆ operator()()

◆ slice()

Member Data Documentation

◆ cfg