A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program. More...

#include <cfg.h>

Inheritance diagram for cfg_baset< T, P, I >:

Collaboration diagram for cfg_baset< T, P, I >:

Classes
class	entry_mapt

Public Types
typedef base_grapht::node_indext	entryt

typedef base_grapht::nodet	nodet

Public Types inherited from grapht< cfg_base_nodet< T, goto_programt::const_targett > >
typedef cfg_base_nodet< T, goto_programt::const_targett >	nodet

typedef nodet::edgest	edgest

typedef std::vector< nodet >	nodest

typedef nodet::edget	edget

typedef nodet::node_indext	node_indext

typedef std::list< node_indext >	patht

Public Member Functions
	cfg_baset ()

virtual	~cfg_baset ()

void	operator() (const goto_functionst &goto_functions)

void	operator() (P &goto_program)

entryt	get_node_index (const goto_programt::const_targett &program_point) const
	Get the graph node index for `program_point`. More...

nodet &	get_node (const goto_programt::const_targett &program_point)
	Get the CFG graph node relating to `program_point`. More...

const nodet &	get_node (const goto_programt::const_targett &program_point) const
	Get the CFG graph node relating to `program_point`. More...

const entry_mapt &	entries () const
	Get a map from program points to their corresponding node indices. More...

Public Member Functions inherited from grapht< cfg_base_nodet< T, goto_programt::const_targett > >
node_indext	add_node (arguments &&... values)

void	swap (grapht &other)

bool	has_edge (node_indext i, node_indext j) const

const nodet &	operator[] (node_indext n) const

nodet &	operator[] (node_indext n)

void	resize (node_indext s)

std::size_t	size () const

bool	empty () const

const edgest &	in (node_indext n) const

const edgest &	out (node_indext n) const

void	add_edge (node_indext a, node_indext b)

void	remove_edge (node_indext a, node_indext b)

edget &	edge (node_indext a, node_indext b)

void	add_undirected_edge (node_indext a, node_indext b)

void	remove_undirected_edge (node_indext a, node_indext b)

void	remove_in_edges (node_indext n)

void	remove_out_edges (node_indext n)

void	remove_edges (node_indext n)

void	clear ()

void	shortest_path (node_indext src, node_indext dest, patht &path) const

void	shortest_loop (node_indext node, patht &path) const

void	visit_reachable (node_indext src)

std::vector< node_indext >	get_reachable (node_indext src, bool forwards) const
	Run depth-first search on the graph, starting from a single source node. More...

std::vector< node_indext >	get_reachable (const std::vector< node_indext > &src, bool forwards) const
	Run depth-first search on the graph, starting from multiple source nodes. More...

void	disconnect_unreachable (node_indext src)
	Removes any edges between nodes in a graph that are unreachable from a given start node. More...

void	disconnect_unreachable (const std::vector< node_indext > &src)
	Removes any edges between nodes in a graph that are unreachable from a vector of start nodes. More...

std::vector< typename N::node_indext >	depth_limited_search (typename N::node_indext src, std::size_t limit) const
	Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More...

std::vector< typename N::node_indext >	depth_limited_search (std::vector< typename N::node_indext > &src, std::size_t limit) const
	Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More...

void	make_chordal ()
	Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges. More...

std::size_t	connected_subgraphs (std::vector< node_indext > &subgraph_nr)
	Find connected subgraphs in an undirected graph. More...

std::size_t	SCCs (std::vector< node_indext > &subgraph_nr) const
	Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes to components indices. More...

bool	is_dag () const

std::list< node_indext >	topsort () const
	Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph. More...

std::vector< node_indext >	get_predecessors (const node_indext &n) const

std::vector< node_indext >	get_successors (const node_indext &n) const

void	output_dot (std::ostream &out) const

void	for_each_predecessor (const node_indext &n, std::function< void(const node_indext &)> f) const

void	for_each_successor (const node_indext &n, std::function< void(const node_indext &)> f) const

Static Public Member Functions
static I	get_first_node (P &program)

static I	get_last_node (P &program)

static bool	nodes_empty (P &program)

Public Attributes
entry_mapt	entry_map

Protected Member Functions
virtual void	compute_edges_goto (const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)

virtual void	compute_edges_catch (const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)

virtual void	compute_edges_throw (const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)

virtual void	compute_edges_start_thread (const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)

virtual void	compute_edges_function_call (const goto_functionst &goto_functions, const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)

void	compute_edges (const goto_functionst &goto_functions, const goto_programt &goto_program, I PC)

void	compute_edges (const goto_functionst &goto_functions, P &goto_program)

void	compute_edges (const goto_functionst &goto_functions)

Protected Member Functions inherited from grapht< cfg_base_nodet< T, goto_programt::const_targett > >
void	shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const

std::vector< typename N::node_indext >	depth_limited_search (std::vector< typename N::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const
	Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More...

void	tarjan (class tarjant &t, node_indext v) const

Private Types
typedef grapht< cfg_base_nodet< T, I > >	base_grapht

Additional Inherited Members
Protected Attributes inherited from grapht< cfg_base_nodet< T, goto_programt::const_targett > >
nodest	nodes

Detailed Description

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
class cfg_baset< T, P, I >

A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program.

An instance of cfg_baset<T> is a directed graph whose nodes inherit from a user-provided type T and store a pointer to an instruction of some goto program in the field PC. The field PC of every node points to the original GOTO instruction that gave rise to the node, and the field cfg_baset::entry_map maps every GOTO instruction to some CFG node.

The CFG is constructed on the operator() from either one goto_programt or multiple goto_programt objects (stored in a goto_functionst). The edges of the CFG are created on the method compute_edges(), and notably include:

Edges from location A to B if both A and B belong to the same goto_programt and A can flow into B.
An edge from each FUNCTION_CALL instruction and the first instruction of the called function, when that function body is available and its body is non-empty.
For each FUNCTION_CALL instruction found, an edge between the exit point of the called function and the instruction immediately after the FUNCTION_CALL, when the function body is available and its body is non-empty.

Note that cfg_baset is the base class of many other subclasses and the specific edges constructed by operator() can be different in those.

Definition at line 86 of file cfg.h.

Member Typedef Documentation

◆ base_grapht

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

typedef grapht<cfg_base_nodet<T, I> > cfg_baset< T, P, I >::base_grapht

private

Definition at line 88 of file cfg.h.

◆ entryt

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

typedef base_grapht::node_indext cfg_baset< T, P, I >::entryt

Definition at line 91 of file cfg.h.

◆ nodet

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

typedef base_grapht::nodet cfg_baset< T, P, I >::nodet

Definition at line 92 of file cfg.h.

Constructor & Destructor Documentation

◆ cfg_baset()

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

cfg_baset< T, P, I >::cfg_baset ( )

inline

Definition at line 199 of file cfg.h.

◆ ~cfg_baset()

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

virtual cfg_baset< T, P, I >::~cfg_baset ( )

inlinevirtual

Definition at line 203 of file cfg.h.

Member Function Documentation

◆ compute_edges() [1/3]

template<class T , typename P , typename I >

void cfg_baset< T, P, I >::compute_edges ( const goto_functionst & goto_functions )

protected

Definition at line 540 of file cfg.h.

◆ compute_edges() [2/3]

template<class T , typename P , typename I >

void cfg_baset< T, P, I >::compute_edges	(	const goto_functionst &	goto_functions,
		const goto_programt &	goto_program,
		I	PC
	)

protected

Definition at line 454 of file cfg.h.

◆ compute_edges() [3/3]

template<class T , typename P , typename I >

void cfg_baset< T, P, I >::compute_edges	(	const goto_functionst &	goto_functions,
		P &	goto_program
	)

protected

Definition at line 529 of file cfg.h.

◆ compute_edges_catch()

template<class T , typename P , typename I >

void cfg_baset< T, P, I >::compute_edges_catch	(	const goto_programt &	goto_program,
		const goto_programt::instructiont &	instruction,
		goto_programt::const_targett	next_PC,
		entryt &	entry
	)

protectedvirtual

Definition at line 332 of file cfg.h.

◆ compute_edges_function_call()

template<class T , typename P , typename I >

void cfg_baset< T, P, I >::compute_edges_function_call	(	const goto_functionst &	goto_functions,
		const goto_programt &	goto_program,
		const goto_programt::instructiont &	instruction,
		goto_programt::const_targett	next_PC,
		entryt &	entry
	)

protectedvirtual

Definition at line 387 of file cfg.h.

◆ compute_edges_goto()

template<class T , typename P , typename I >

void cfg_baset< T, P, I >::compute_edges_goto	(	const goto_programt &	goto_program,
		const goto_programt::instructiont &	instruction,
		goto_programt::const_targett	next_PC,
		entryt &	entry
	)

protectedvirtual

Definition at line 315 of file cfg.h.

◆ compute_edges_start_thread()

template<class T , typename P , typename I >

void cfg_baset< T, P, I >::compute_edges_start_thread	(	const goto_programt &	goto_program,
		const goto_programt::instructiont &	instruction,
		goto_programt::const_targett	next_PC,
		entryt &	entry
	)

protectedvirtual

Definition at line 360 of file cfg.h.

◆ compute_edges_throw()

template<class T , typename P , typename I >

void cfg_baset< T, P, I >::compute_edges_throw	(	const goto_programt &	goto_program,
		const goto_programt::instructiont &	instruction,
		goto_programt::const_targett	next_PC,
		entryt &	entry
	)

protectedvirtual

Definition at line 350 of file cfg.h.

◆ entries()

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

const entry_mapt& cfg_baset< T, P, I >::entries ( ) const

inline

Get a map from program points to their corresponding node indices.

Use the indices with operator[] similar to those returned by get_node_index.

Definition at line 259 of file cfg.h.

◆ get_first_node()

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

static I cfg_baset< T, P, I >::get_first_node ( P & program )

inlinestatic

Definition at line 264 of file cfg.h.

◆ get_last_node()

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

static I cfg_baset< T, P, I >::get_last_node ( P & program )

inlinestatic

Definition at line 268 of file cfg.h.

◆ get_node() [1/2]

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

nodet& cfg_baset< T, P, I >::get_node ( const goto_programt::const_targett & program_point )

inline

Get the CFG graph node relating to program_point.

Definition at line 245 of file cfg.h.

◆ get_node() [2/2]

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

const nodet& cfg_baset< T, P, I >::get_node ( const goto_programt::const_targett & program_point ) const

inline

Get the CFG graph node relating to program_point.

Definition at line 251 of file cfg.h.

◆ get_node_index()

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

entryt cfg_baset< T, P, I >::get_node_index ( const goto_programt::const_targett & program_point ) const

inline

Get the graph node index for program_point.

Use this with operator[] to get the related graph node (e.g. cfg[cfg.get_node_index(i)], though in that particular case you should just use cfg.get_node(i)). Storing node indices saves a map lookup, so it can be worthwhile when you expect to repeatedly look up the same program point.

Definition at line 239 of file cfg.h.

◆ nodes_empty()

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

static bool cfg_baset< T, P, I >::nodes_empty ( P & program )

inlinestatic

Definition at line 272 of file cfg.h.

◆ operator()() [1/2]

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

void cfg_baset< T, P, I >::operator() ( const goto_functionst & goto_functions )

inline

Definition at line 207 of file cfg.h.

◆ operator()() [2/2]

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

void cfg_baset< T, P, I >::operator() ( P & goto_program )

inline

Definition at line 222 of file cfg.h.

Member Data Documentation

◆ entry_map

template<class T , typename P = const goto_programt, typename I = goto_programt::const_targett>

entry_mapt cfg_baset< T, P, I >::entry_map

Definition at line 152 of file cfg.h.

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

/home/runner/work/cbmc/cbmc/src/goto-programs/cfg.h

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Private Types

Additional Inherited Members

Detailed Description

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett> class cfg_baset< T, P, I >

Member Typedef Documentation

◆ base_grapht

◆ entryt

◆ nodet

Constructor & Destructor Documentation

◆ cfg_baset()

◆ ~cfg_baset()

Member Function Documentation

◆ compute_edges() [1/3]

◆ compute_edges() [2/3]

◆ compute_edges() [3/3]

◆ compute_edges_catch()

◆ compute_edges_function_call()

◆ compute_edges_goto()

◆ compute_edges_start_thread()

◆ compute_edges_throw()

◆ entries()

◆ get_first_node()

◆ get_last_node()

◆ get_node() [1/2]

◆ get_node() [2/2]

◆ get_node_index()

◆ nodes_empty()

◆ operator()() [1/2]

◆ operator()() [2/2]

Member Data Documentation

◆ entry_map

template<class T, typename P = const goto_programt, typename I = goto_programt::const_targett>
class cfg_baset< T, P, I >