cprover
dependence_grapht Class Reference

#include <dependence_graph.h>

+ Inheritance diagram for dependence_grapht:
+ Collaboration diagram for dependence_grapht:

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)
 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_maptcfg_post_dominators () const
 
const reaching_definitions_analysistreaching_definitions () const
 
virtual statetget_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_domaintoperator[] (locationt l)
 
const dep_graph_domaintoperator[] (locationt l) const
 
std::unique_ptr< statetabstract_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< statetabstract_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 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
 The work queue, sorted by location number. More...
 
- Protected Member Functions inherited from ait< dep_graph_domaint >
const statetfind_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< statetmake_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_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 217 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 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: