#include <dependence_graph.h>

Inheritance diagram for dependence_grapht:

Collaboration diagram for dependence_grapht:

Public Types
typedef std::map< irep_idt, cfg_post_dominatorst >	post_dominators_mapt

Public Types inherited from ait< dep_graph_domaint >
typedef goto_programt::const_targett	locationt

Public Types inherited from ai_baset
typedef ai_domain_baset	statet

typedef goto_programt::const_targett	locationt

Public Types inherited from grapht< dep_nodet >
typedef dep_nodet	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
	dependence_grapht (const namespacet &_ns)

void	initialize (const goto_functionst &goto_functions)
	Initialize all the abstract states for a whole program. More...

void	initialize (const goto_programt &goto_program)
	Initialize all the abstract states for a single function. More...

void	finalize ()
	Override this to add a cleanup or post-processing step after fixedpoint has run. More...

void	add_dep (dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)

const post_dominators_mapt &	cfg_post_dominators () const

const reaching_definitions_analysist &	reaching_definitions () const

virtual statet &	get_state (goto_programt::const_targett l)
	Get the state for the given location, creating it in a default way if it doesn't exist. More...

Public Member Functions inherited from ait< dep_graph_domaint >
	ait ()

dep_graph_domaint &	operator[] (locationt l)

const dep_graph_domaint &	operator[] (locationt l) const

std::unique_ptr< statet >	abstract_state_before (locationt t) const override
	Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More...

void	clear () override
	Reset the abstract state. More...

Public Member Functions inherited from ai_baset
	ai_baset ()

virtual	~ai_baset ()

void	operator() (const irep_idt &function_identifier, const goto_programt &goto_program, const namespacet &ns)
	Run abstract interpretation on a single function. More...

void	operator() (const goto_functionst &goto_functions, const namespacet &ns)
	Run abstract interpretation on a whole program. More...

void	operator() (const goto_modelt &goto_model)
	Run abstract interpretation on a whole program. More...

void	operator() (const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
	Run abstract interpretation on a single function. More...

virtual std::unique_ptr< statet >	abstract_state_after (locationt l) const
	Get a copy of the abstract state after the given instruction, without needing to know what kind of domain or history is used. More...

virtual void	output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
	Output the abstract states for a whole program. More...

void	output (const goto_modelt &goto_model, std::ostream &out) const
	Output the abstract states for a whole program. More...

void	output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
	Output the abstract states for a function. More...

void	output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
	Output the abstract states for a function. More...

virtual jsont	output_json (const namespacet &ns, const goto_functionst &goto_functions) const
	Output the abstract states for the whole program as JSON. More...

jsont	output_json (const goto_modelt &goto_model) const
	Output the abstract states for a whole program as JSON. More...

jsont	output_json (const namespacet &ns, const goto_programt &goto_program) const
	Output the abstract states for a single function as JSON. More...

jsont	output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
	Output the abstract states for a single function as JSON. More...

virtual xmlt	output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
	Output the abstract states for the whole program as XML. More...

xmlt	output_xml (const goto_modelt &goto_model) const
	Output the abstract states for the whole program as XML. More...

xmlt	output_xml (const namespacet &ns, const goto_programt &goto_program) const
	Output the abstract states for a single function as XML. More...

xmlt	output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
	Output the abstract states for a single function as XML. More...

Public Member Functions inherited from grapht< dep_nodet >
node_indext	add_node ()

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 dep_nodet ::node_indext >	depth_limited_search (typename dep_nodet ::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 dep_nodet ::node_indext >	depth_limited_search (std::vector< typename dep_nodet ::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_successors (const node_indext &n) const

void	output_dot (std::ostream &out) const

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

Protected Attributes
const namespacet &	ns

post_dominators_mapt	post_dominators

reaching_definitions_analysist	rd

Protected Attributes inherited from ait< dep_graph_domaint >
state_mapt	state_map

Protected Attributes inherited from grapht< dep_nodet >
nodest	nodes

Additional Inherited Members
Protected Types inherited from ait< dep_graph_domaint >
typedef std::unordered_map< locationt, dep_graph_domaint, const_target_hash, pointee_address_equalt >	state_mapt

Protected Types inherited from ai_baset
typedef std::map< unsigned, locationt >	working_sett
	The work queue, sorted by location number. More...

Protected Member Functions inherited from ait< dep_graph_domaint >
const statet &	find_state (locationt l) const override
	Get the state for the given location if it already exists; throw an exception if it doesn't. More...

bool	merge (const statet &src, locationt from, locationt to) override

std::unique_ptr< statet >	make_temporary_state (const statet &s) override
	Make a copy of a state. More...

void	fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override

Protected Member Functions inherited from ai_baset
virtual void	initialize (const goto_functionst::goto_functiont &goto_function)
	Initialize all the abstract states for a single function. More...

void	entry_state (const goto_programt &goto_program)
	Set the abstract state of the entry location of a single function to the entry state required by the analysis. More...

void	entry_state (const goto_functionst &goto_functions)
	Set the abstract state of the entry location of a whole program to the entry state required by the analysis. More...

virtual void	output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const
	Output the abstract states for a single function. More...

virtual jsont	output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
	Output the abstract states for a single function as JSON. More...

virtual xmlt	output_xml (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
	Output the abstract states for a single function as XML. More...

locationt	get_next (working_sett &working_set)
	Get the next location from the work queue. More...

void	put_in_working_set (working_sett &working_set, locationt l)

bool	fixedpoint (const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
	Run the fixedpoint algorithm until it reaches a fixed point. More...

void	sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)

void	concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)

bool	visit (const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
	Perform one step of abstract interpretation from location l Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More...

bool	do_function_call_rec (const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)

bool	do_function_call (const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns)

Protected Member Functions inherited from grapht< dep_nodet >
void	shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const

std::vector< typename dep_nodet ::node_indext >	depth_limited_search (std::vector< typename dep_nodet ::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const
	Run recursive depth-limited search on the graph, starting. More...

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

Detailed Description

Definition at line 217 of file dependence_graph.h.

Member Typedef Documentation

◆ post_dominators_mapt

typedef std::map<irep_idt, cfg_post_dominatorst> dependence_grapht::post_dominators_mapt

Definition at line 225 of file dependence_graph.h.

Constructor & Destructor Documentation

◆ dependence_grapht()

dependence_grapht::dependence_grapht ( const namespacet & _ns )

inlineexplicit

Definition at line 227 of file dependence_graph.h.

Member Function Documentation

◆ add_dep()

void dependence_grapht::add_dep	(	dep_edget::kindt	kind,
		goto_programt::const_targett	from,
		goto_programt::const_targett	to
	)

Definition at line 307 of file dependence_graph.cpp.

◆ cfg_post_dominators()

const post_dominators_mapt& dependence_grapht::cfg_post_dominators ( ) const

inline

Definition at line 264 of file dependence_graph.h.

◆ finalize()

void dependence_grapht::finalize ( )

inlinevirtual

Override this to add a cleanup or post-processing step after fixedpoint has run.

Reimplemented from ai_baset.

Definition at line 251 of file dependence_graph.h.

◆ get_state()

virtual statet& dependence_grapht::get_state ( goto_programt::const_targett l )

inlinevirtual

Get the state for the given location, creating it in a default way if it doesn't exist.

Reimplemented from ait< dep_graph_domaint >.

Definition at line 274 of file dependence_graph.h.

◆ initialize() [1/2]

void dependence_grapht::initialize ( const goto_functionst & goto_functions )

inlinevirtual

Initialize all the abstract states for a whole program.

Override this to do custom per-analysis initialization.

Reimplemented from ai_baset.

Definition at line 233 of file dependence_graph.h.

◆ initialize() [2/2]

void dependence_grapht::initialize ( const goto_programt & goto_program )

inlinevirtual

Initialize all the abstract states for a single function.

Override this to do custom per-domain initialization.

Reimplemented from ai_baset.

Definition at line 239 of file dependence_graph.h.

◆ reaching_definitions()

const reaching_definitions_analysist& dependence_grapht::reaching_definitions ( ) const

inline

Definition at line 269 of file dependence_graph.h.

Member Data Documentation

◆ ns

const namespacet& dependence_grapht::ns

protected

Definition at line 290 of file dependence_graph.h.

◆ post_dominators

post_dominators_mapt dependence_grapht::post_dominators

protected

Definition at line 292 of file dependence_graph.h.

◆ rd

reaching_definitions_analysist dependence_grapht::rd

protected

Definition at line 293 of file dependence_graph.h.

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

analyses/dependence_graph.h
analyses/dependence_graph.cpp

Public Types

Public Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ post_dominators_mapt

Constructor & Destructor Documentation

◆ dependence_grapht()

Member Function Documentation

◆ add_dep()

◆ cfg_post_dominators()

◆ finalize()

◆ get_state()

◆ initialize() [1/2]

◆ initialize() [2/2]

◆ reaching_definitions()

Member Data Documentation

◆ ns

◆ post_dominators

◆ rd