#include <variable_sensitivity_dependence_graph.h>

Inheritance diagram for variable_sensitivity_dependence_grapht:

Collaboration diagram for variable_sensitivity_dependence_grapht:

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

Public Types inherited from ai_baset
typedef ai_domain_baset	statet

typedef ai_storage_baset::cstate_ptrt	cstate_ptrt

typedef ai_history_baset::trace_ptrt	trace_ptrt

typedef ai_history_baset::trace_sett	trace_sett

typedef ai_storage_baset::ctrace_set_ptrt	ctrace_set_ptrt

typedef goto_programt::const_targett	locationt

Public Types inherited from grapht< vs_dep_nodet >
typedef vs_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
	variable_sensitivity_dependence_grapht (const goto_functionst &goto_functions, const namespacet &_ns, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &_configuration, message_handlert &message_handler)

void	initialize (const irep_idt &function_id, 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 (vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)

post_dominators_mapt &	cfg_post_dominators ()

Public Member Functions inherited from ai_three_way_merget
	ai_three_way_merget (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)

Public Member Functions inherited from ai_recursive_interproceduralt
	ai_recursive_interproceduralt (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)

Public Member Functions inherited from ai_baset
	ai_baset (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh)

virtual	~ai_baset ()

void	operator() (const irep_idt &function_id, 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 abstract_goto_modelt &goto_model)
	Run abstract interpretation on a whole program. More...

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

virtual ctrace_set_ptrt	abstract_traces_before (locationt l) const
	Returns all of the histories that have reached the start of the instruction. More...

virtual ctrace_set_ptrt	abstract_traces_after (locationt l) const
	Returns all of the histories that have reached the end of the instruction. More...

virtual cstate_ptrt	abstract_state_before (locationt l) const
	Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More...

virtual cstate_ptrt	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 cstate_ptrt	abstract_state_before (const trace_ptrt &p) const
	The same interfaces but with histories. More...

virtual cstate_ptrt	abstract_state_after (const trace_ptrt &p) const

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

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

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

virtual xmlt	output_xml (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
	Output the abstract states for a single function as XML. 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_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< vs_dep_nodet >
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

Protected Member Functions
virtual statet &	get_state (locationt l)

variable_sensitivity_dependence_domaint &	operator[] (locationt l)

virtual statet &	get_state (trace_ptrt p)
	Get the state for the given history, creating it with the factory if it doesn't exist. More...

Protected Member Functions inherited from ai_three_way_merget
bool	visit_edge_function_call (const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override

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

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

trace_ptrt	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...

trace_ptrt	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...

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

void	put_in_working_set (working_sett &working_set, trace_ptrt t)

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

virtual void	fixedpoint (trace_ptrt starting_trace, const goto_functionst &goto_functions, const namespacet &ns)

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

virtual bool	visit_function_call (const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

virtual bool	visit_end_function (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)

bool	visit_edge (const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set)

virtual bool	merge (const statet &src, trace_ptrt from, trace_ptrt to)
	Merge the state `src`, flowing from tracet `from` to tracet `to`, into the state currently stored for tracet `to`. More...

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

virtual statet &	get_state (trace_ptrt p)
	Get the state for the given history, creating it with the factory if it doesn't exist. More...

Protected Member Functions inherited from grapht< vs_dep_nodet >
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

Protected Attributes
friend	variable_sensitivity_dependence_domain_factoryt

friend	variable_sensitivity_dependence_domaint

const goto_functionst &	goto_functions

const namespacet &	ns

post_dominators_mapt	post_dominators

Protected Attributes inherited from ai_baset
std::unique_ptr< ai_history_factory_baset >	history_factory
	For creating history objects. More...

std::unique_ptr< ai_domain_factory_baset >	domain_factory
	For creating domain objects. More...

std::unique_ptr< ai_storage_baset >	storage

message_handlert &	message_handler

Protected Attributes inherited from grapht< vs_dep_nodet >
nodest	nodes

Friends
class	variable_sensitivity_dependence_domaint

Additional Inherited Members
Protected Types inherited from ai_baset
typedef trace_sett	working_sett
	The work queue, sorted using the history's ordering operator. More...

Detailed Description

Definition at line 217 of file variable_sensitivity_dependence_graph.h.

Member Typedef Documentation

◆ post_dominators_mapt

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

Definition at line 241 of file variable_sensitivity_dependence_graph.h.

Constructor & Destructor Documentation

◆ variable_sensitivity_dependence_grapht()

variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_grapht	(	const goto_functionst &	goto_functions,
		const namespacet &	_ns,
		variable_sensitivity_object_factory_ptrt	object_factory,
		const vsd_configt &	_configuration,
		message_handlert &	message_handler
	)

explicit

Definition at line 633 of file variable_sensitivity_dependence_graph.cpp.

Member Function Documentation

◆ add_dep()

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

Definition at line 652 of file variable_sensitivity_dependence_graph.cpp.

◆ cfg_post_dominators()

post_dominators_mapt& variable_sensitivity_dependence_grapht::cfg_post_dominators ( )

inline

Definition at line 272 of file variable_sensitivity_dependence_graph.h.

◆ finalize()

void variable_sensitivity_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 256 of file variable_sensitivity_dependence_graph.h.

◆ get_state() [1/2]

virtual statet& variable_sensitivity_dependence_grapht::get_state ( locationt l )

inlineprotectedvirtual

Definition at line 224 of file variable_sensitivity_dependence_graph.h.

◆ get_state() [2/2]

virtual statet& ai_baset::get_state

inlineprotected

Get the state for the given history, creating it with the factory if it doesn't exist.

Definition at line 515 of file ai.h.

◆ initialize()

void variable_sensitivity_dependence_grapht::initialize	(	const irep_idt &	function_id,
		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 251 of file variable_sensitivity_dependence_graph.h.

◆ operator[]()

variable_sensitivity_dependence_domaint& variable_sensitivity_dependence_grapht::operator[] ( locationt l )

inlineprotected

Definition at line 230 of file variable_sensitivity_dependence_graph.h.

Friends And Related Function Documentation

◆ variable_sensitivity_dependence_domaint

friend class variable_sensitivity_dependence_domaint

friend

Definition at line 239 of file variable_sensitivity_dependence_graph.h.

Member Data Documentation

◆ goto_functions

const goto_functionst& variable_sensitivity_dependence_grapht::goto_functions

protected

Definition at line 280 of file variable_sensitivity_dependence_graph.h.

◆ ns

const namespacet& variable_sensitivity_dependence_grapht::ns

protected

Definition at line 281 of file variable_sensitivity_dependence_graph.h.

◆ post_dominators

post_dominators_mapt variable_sensitivity_dependence_grapht::post_dominators

protected

Definition at line 283 of file variable_sensitivity_dependence_graph.h.

◆ variable_sensitivity_dependence_domain_factoryt

friend variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_domain_factoryt

protected

Definition at line 278 of file variable_sensitivity_dependence_graph.h.

◆ variable_sensitivity_dependence_domaint

friend variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_domaint

protected

Definition at line 279 of file variable_sensitivity_dependence_graph.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h
/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Friends

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ post_dominators_mapt

Constructor & Destructor Documentation

◆ variable_sensitivity_dependence_grapht()

Member Function Documentation

◆ add_dep()

◆ cfg_post_dominators()

◆ finalize()

◆ get_state() [1/2]

◆ get_state() [2/2]

◆ initialize()

◆ operator[]()

Friends And Related Function Documentation

◆ variable_sensitivity_dependence_domaint

Member Data Documentation

◆ goto_functions

◆ ns

◆ post_dominators

◆ variable_sensitivity_dependence_domain_factoryt

◆ variable_sensitivity_dependence_domaint