cprover
dependence_grapht Class Reference

#include <dependence_graph.h>

Inheritance diagram for dependence_grapht:
[legend]
Collaboration diagram for dependence_grapht:
[legend]

Public Types

typedef std::map< irep_idt, cfg_post_dominatorstpost_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< nodetnodest
 
typedef nodet::edget edget
 
typedef nodet::node_indext node_indext
 
typedef std::list< node_indextpatht
 

Public Member Functions

 dependence_grapht (const namespacet &_ns)
 
void initialize (const goto_functionst &goto_functions)
 
void initialize (const goto_programt &goto_program)
 
void finalize ()
 
void add_dep (dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
 
const post_dominators_maptcfg_post_dominators () const
 
const reaching_definitions_analysistreaching_definitions () const
 
virtual statetget_state (goto_programt::const_targett l)
 
- Public Member Functions inherited from ait< dep_graph_domaint >
 ait ()
 
dep_graph_domaintoperator[] (locationt l)
 
const dep_graph_domaintoperator[] (locationt l) const
 
std::unique_ptr< statetabstract_state_before (locationt t) const override
 Accessing individual domains at particular locations (without needing to know what kind of domain or history is used) A pointer to a copy as the method should be const and there are some non-trivial cases including merging domains, etc. More...
 
void clear () override
 Resets the domain. More...
 
- Public Member Functions inherited from ai_baset
 ai_baset ()
 
virtual ~ai_baset ()
 
void operator() (const goto_programt &goto_program, const namespacet &ns)
 Running the interpreter. More...
 
void operator() (const goto_functionst &goto_functions, const namespacet &ns)
 
void operator() (const goto_modelt &goto_model)
 
void operator() (const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
 
virtual std::unique_ptr< statetabstract_state_after (locationt l) const
 Returns the abstract state after the given instruction. More...
 
virtual void output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
 
void output (const goto_modelt &goto_model, std::ostream &out) const
 
void output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
 
void output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
 
virtual jsont output_json (const namespacet &ns, const goto_functionst &goto_functions) const
 Output the domains for the whole program as JSON. More...
 
jsont output_json (const goto_modelt &goto_model) const
 
jsont output_json (const namespacet &ns, const goto_programt &goto_program) const
 
jsont output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
 
virtual xmlt output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
 Output the domains for the whole program as XML. More...
 
xmlt output_xml (const goto_modelt &goto_model) const
 
xmlt output_xml (const namespacet &ns, const goto_programt &goto_program) const
 
xmlt output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
 
- 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 nodetoperator[] (node_indext n) const
 
nodetoperator[] (node_indext n)
 
void resize (node_indext s)
 
std::size_t size () const
 
bool empty () const
 
const edgestin (node_indext n) const
 
const edgestout (node_indext n) const
 
void add_edge (node_indext a, node_indext b)
 
void remove_edge (node_indext a, node_indext b)
 
edgetedge (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_indextget_reachable (node_indext src, bool forwards) const
 Run depth-first search on the graph, starting from a single source node. More...
 
std::vector< node_indextget_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_indextdepth_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_indextdepth_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_indexttopsort () 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_indextget_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 namespacetns
 
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_equaltstate_mapt
 
- Protected Types inherited from ai_baset
typedef std::map< unsigned, locationtworking_sett
 
- Protected Member Functions inherited from ait< dep_graph_domaint >
const statetfind_state (locationt l) const override
 
bool merge (const statet &src, locationt from, locationt to) override
 
std::unique_ptr< statetmake_temporary_state (const statet &s) override
 
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 &)
 
void entry_state (const goto_programt &)
 
void entry_state (const goto_functionst &)
 
virtual void output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const
 
virtual jsont output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
 Output the domains 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 domains for a single function as XML. More...
 
locationt get_next (working_sett &working_set)
 
void put_in_working_set (working_sett &working_set, locationt l)
 
bool fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
void sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)
 
void concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)
 
bool visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
bool do_function_call_rec (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 (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_indextdepth_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 215 of file dependence_graph.h.

Member Typedef Documentation

◆ post_dominators_mapt

Constructor & Destructor Documentation

◆ dependence_grapht()

dependence_grapht::dependence_grapht ( const namespacet _ns)
inlineexplicit

Definition at line 225 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 
)

◆ cfg_post_dominators()

const post_dominators_mapt& dependence_grapht::cfg_post_dominators ( ) const
inline

◆ finalize()

void dependence_grapht::finalize ( )
inlinevirtual

Reimplemented from ai_baset.

Definition at line 249 of file dependence_graph.h.

References ait< dep_graph_domaint >::state_map.

◆ get_state()

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

◆ initialize() [1/2]

void dependence_grapht::initialize ( const goto_functionst goto_functions)
inlinevirtual

Reimplemented from ai_baset.

Definition at line 231 of file dependence_graph.h.

References ai_baset::initialize(), ns, and rd.

◆ initialize() [2/2]

void dependence_grapht::initialize ( const goto_programt goto_program)
inlinevirtual

◆ reaching_definitions()

const reaching_definitions_analysist& dependence_grapht::reaching_definitions ( ) const
inline

Definition at line 267 of file dependence_graph.h.

References rd.

Referenced by dep_graph_domaint::data_dependencies().

Member Data Documentation

◆ ns

const namespacet& dependence_grapht::ns
protected

Definition at line 288 of file dependence_graph.h.

Referenced by initialize().

◆ post_dominators

post_dominators_mapt dependence_grapht::post_dominators
protected

Definition at line 290 of file dependence_graph.h.

Referenced by cfg_post_dominators(), and initialize().

◆ rd

reaching_definitions_analysist dependence_grapht::rd
protected

Definition at line 291 of file dependence_graph.h.

Referenced by initialize(), and reaching_definitions().


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