CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Attributes | List of all members
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_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 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< 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, message_handlert &)
 
void  initialize (const goto_functionst &goto_functions)
  Initialize all the abstract states for a whole program.
 
void  initialize (const irep_idt &function, const goto_programt &goto_program)
  Initialize all the abstract states for a single function.
 
void  finalize ()
  Override this to add a cleanup or post-processing step after fixedpoint has run.
 
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
 
- Public Member Functions inherited from ait< dep_graph_domaint >
  ait ()
 
  ait (std::unique_ptr< ai_domain_factory_baset > &&df)
 
const dep_graph_domaint &  operator[] (locationt l) const
  Find the analysis result for a given location.
 
- 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.
 
void  operator() (const goto_functionst &goto_functions, const namespacet &ns)
  Run abstract interpretation on a whole program.
 
void  operator() (const abstract_goto_modelt &goto_model)
  Run abstract interpretation on a whole program.
 
void  operator() (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
  Run abstract interpretation on a single function.
 
virtual ctrace_set_ptrt  abstract_traces_before (locationt l) const
  Returns all of the histories that have reached the start of the instruction.
 
virtual ctrace_set_ptrt  abstract_traces_after (locationt l) const
  Returns all of the histories that have reached the end of the instruction.
 
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.
 
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.
 
virtual cstate_ptrt  abstract_state_before (const trace_ptrt &p) const
  The same interfaces but with histories.
 
virtual cstate_ptrt  abstract_state_after (const trace_ptrt &p) const
 
virtual void  clear ()
  Reset the abstract state.
 
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.
 
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.
 
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.
 
virtual void  output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
  Output the abstract states for a whole program.
 
void  output (const goto_modelt &goto_model, std::ostream &out) const
  Output the abstract states for a whole program.
 
void  output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
  Output the abstract states for a function.
 
virtual jsont  output_json (const namespacet &ns, const goto_functionst &goto_functions) const
  Output the abstract states for the whole program as JSON.
 
jsont  output_json (const goto_modelt &goto_model) const
  Output the abstract states for a whole program as JSON.
 
jsont  output_json (const namespacet &ns, const goto_programt &goto_program) const
  Output the abstract states for a single function as JSON.
 
jsont  output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
  Output the abstract states for a single function as JSON.
 
virtual xmlt  output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
  Output the abstract states for the whole program as XML.
 
xmlt  output_xml (const goto_modelt &goto_model) const
  Output the abstract states for the whole program as XML.
 
xmlt  output_xml (const namespacet &ns, const goto_programt &goto_program) const
  Output the abstract states for a single function as XML.
 
xmlt  output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
  Output the abstract states for a single function as XML.
 
- Public Member Functions inherited from grapht< 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.
 
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.
 
void  disconnect_unreachable (node_indext src)
  Removes any edges between nodes in a graph that are unreachable from a given start node.
 
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.
 
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.
 
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.
 
void  make_chordal ()
  Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges.
 
std::size_t  connected_subgraphs (std::vector< node_indext > &subgraph_nr)
  Find connected subgraphs in an undirected graph.
 
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.
 
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.
 
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 Attributes

friend  dep_graph_domain_factoryt
 
friend  dep_graph_domaint
 
const namespacet &  ns
 
post_dominators_mapt  post_dominators
 
reaching_definitions_analysist  rd
 
std::map< irep_idt, goto_programt::const_targett >  end_function_map
 
- Protected Attributes inherited from ai_baset
std::unique_ptr< ai_history_factory_baset >  history_factory
  For creating history objects.
 
std::unique_ptr< ai_domain_factory_baset >  domain_factory
  For creating domain objects.
 
std::unique_ptr< ai_storage_baset >  storage
 
message_handlert &  message_handler
 
- Protected Attributes inherited from grapht< dep_nodet >
nodest  nodes
 

Additional Inherited Members

- Protected Types inherited from ai_baset
typedef trace_sett  working_sett
  The work queue, sorted using the history's ordering operator.
 
- Protected Member Functions inherited from ait< dep_graph_domaint >
virtual statet &  get_state (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.
 
- Protected Member Functions inherited from ai_recursive_interproceduralt
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.
 
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.
 
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.
 
trace_ptrt  get_next (working_sett &working_set)
  Get the next location from the work queue.
 
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.
 
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.
 
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.
 
virtual std::unique_ptr< statet >  make_temporary_state (const statet &s)
  Make a copy of a state.
 
- 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 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.
 
void  tarjan (class tarjant &t, node_indext v) const
 

Detailed Description

Definition at line 218 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 226 of file dependence_graph.h.

Constructor & Destructor Documentation

◆  dependence_grapht()

dependence_grapht::dependence_grapht ( const namespacet &  _ns,
message_handlert &  message_handler 
)

Definition at line 366 of file dependence_graph.cpp.

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 376 of file dependence_graph.cpp.

◆  cfg_post_dominators()

const post_dominators_mapt & dependence_grapht::cfg_post_dominators ( ) const
inline

Definition at line 279 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 264 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 230 of file dependence_graph.h.

◆  initialize() [2/2]

void 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 246 of file dependence_graph.h.

◆  reaching_definitions()

const reaching_definitions_analysist & dependence_grapht::reaching_definitions ( ) const
inline

Definition at line 284 of file dependence_graph.h.

Member Data Documentation

◆  dep_graph_domain_factoryt

friend dependence_grapht::dep_graph_domain_factoryt
protected

Definition at line 290 of file dependence_graph.h.

◆  dep_graph_domaint

friend dependence_grapht::dep_graph_domaint
protected

Definition at line 291 of file dependence_graph.h.

◆  end_function_map

std::map<irep_idt, goto_programt::const_targett> dependence_grapht::end_function_map
protected

Definition at line 296 of file dependence_graph.h.

◆  ns

const namespacet& dependence_grapht::ns
protected

Definition at line 292 of file dependence_graph.h.

◆  post_dominators

post_dominators_mapt dependence_grapht::post_dominators
protected

Definition at line 294 of file dependence_graph.h.

◆  rd

reaching_definitions_analysist dependence_grapht::rd
protected

Definition at line 295 of file dependence_graph.h.

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

AltStyle によって変換されたページ (->オリジナル) /