cprover
|
#include <dependence_graph.h>
Public Types | |
typedef std::map< irep_idt, cfg_post_dominatorst > | post_dominators_mapt |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef ai_domain_baset | statet |
typedef goto_programt::const_targett | locationt |
![]() | |
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) |
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_mapt & | cfg_post_dominators () const |
const reaching_definitions_analysist & | reaching_definitions () const |
virtual statet & | get_state (goto_programt::const_targett l) |
![]() | |
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 |
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... | |
![]() | |
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< statet > | abstract_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 |
![]() | |
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 |
![]() | |
state_mapt | state_map |
![]() | |
nodest | nodes |
Additional Inherited Members | |
![]() | |
typedef std::unordered_map< locationt, dep_graph_domaint, const_target_hash, pointee_address_equalt > | state_mapt |
![]() | |
typedef std::map< unsigned, locationt > | working_sett |
![]() | |
const statet & | find_state (locationt l) const override |
bool | merge (const statet &src, locationt from, locationt to) override |
std::unique_ptr< statet > | make_temporary_state (const statet &s) override |
void | fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override |
![]() | |
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) |
![]() | |
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 |
Definition at line 215 of file dependence_graph.h.
typedef std::map<irep_idt, cfg_post_dominatorst> dependence_grapht::post_dominators_mapt |
Definition at line 223 of file dependence_graph.h.
|
inlineexplicit |
Definition at line 225 of file dependence_graph.h.
void dependence_grapht::add_dep | ( | dep_edget::kindt | kind, |
goto_programt::const_targett | from, | ||
goto_programt::const_targett | to | ||
) |
Definition at line 305 of file dependence_graph.cpp.
References grapht< dep_nodet >::nodes, and grapht< dep_nodet >::size().
Referenced by dep_graph_domaint::populate_dep_graph().
|
inline |
Definition at line 262 of file dependence_graph.h.
References post_dominators.
Referenced by dep_graph_domaint::control_dependencies(), and full_slicert::fixedpoint().
|
inlinevirtual |
Reimplemented from ai_baset.
Definition at line 249 of file dependence_graph.h.
References ait< dep_graph_domaint >::state_map.
|
inlinevirtual |
Reimplemented from ait< dep_graph_domaint >.
Definition at line 272 of file dependence_graph.h.
References grapht< dep_nodet >::add_node(), grapht< dep_nodet >::nodes, and ait< dep_graph_domaint >::state_map.
Referenced by dep_graph_domaint::transform().
|
inlinevirtual |
Reimplemented from ai_baset.
Definition at line 231 of file dependence_graph.h.
References ai_baset::initialize(), ns, and rd.
|
inlinevirtual |
Reimplemented from ai_baset.
Definition at line 237 of file dependence_graph.h.
References goto_programt::empty(), goto_programt::get_function_id(), goto_program, ai_baset::initialize(), and post_dominators.
|
inline |
Definition at line 267 of file dependence_graph.h.
References rd.
Referenced by dep_graph_domaint::data_dependencies().
|
protected |
Definition at line 288 of file dependence_graph.h.
Referenced by initialize().
|
protected |
Definition at line 290 of file dependence_graph.h.
Referenced by cfg_post_dominators(), and initialize().
|
protected |
Definition at line 291 of file dependence_graph.h.
Referenced by initialize(), and reaching_definitions().