CBMC
cfg_dominators_templatet< P, T, post_dom > Class Template Reference

Dominator graph. More...

#include <cfg_dominators.h>

+ Inheritance diagram for cfg_dominators_templatet< P, T, post_dom >:
+ Collaboration diagram for cfg_dominators_templatet< P, T, post_dom >:

Classes

struct  nodet
 

Public Types

typedef std::set< T, typename P::target_less_than > target_sett
 
typedef procedure_local_cfg_baset< nodet, P, T > cfgt
 

Public Member Functions

void operator() (P &program)
 Compute dominators. More...
 
const cfgt::nodetget_node (const T &program_point) const
 Get the graph node (which gives dominators, predecessors and successors) for program_point. More...
 
cfgt::nodetget_node (const T &program_point)
 Get the graph node (which gives dominators, predecessors and successors) for program_point. More...
 
cfgt::entryt get_node_index (const T &program_point) const
 Get the graph node index for program_point. More...
 
bool dominates (T lhs, const nodet &rhs_node) const
 Returns true if the program point corresponding to rhs_node is dominated by program point lhs. More...
 
bool dominates (T lhs, T rhs) const
 Returns true if program point lhs dominates rhs. More...
 
bool program_point_reachable (const nodet &program_point_node) const
 Returns true if the program point for program_point_node is reachable from the entry point. More...
 
bool program_point_reachable (T program_point) const
 Returns true if the program point for program_point_node is reachable from the entry point. More...
 
void output (std::ostream &) const
 Print the result of the dominator computation. More...
 

Public Attributes

cfgt cfg
 
entry_node
 

Protected Member Functions

void initialise (P &program)
 Initialises the elements of the fixed point analysis. More...
 
void fixedpoint (P &program)
 Computes the MOP for the dominator analysis. More...
 

Detailed Description

template<class P, class T, bool post_dom>
class cfg_dominators_templatet< P, T, post_dom >

Dominator graph.

This computes a control-flow graph (see cfgt) and decorates it with dominator sets per program point, following "A Simple, Fast Dominance Algorithm" by Cooper et al. Templated over the program type (P) and program point type (T), which need to be supported by cfgt. Can compute either dominators or postdominators depending on template parameter post_dom. Use cfg_dominators_templatet::dominates to directly query dominance, or cfg_dominators_templatet::get_node to get the cfgt graph node corresponding to a program point, including the in- and out-edges provided by cfgt as well as the dominator set computed by this class. See also https://en.wikipedia.org/wiki/Dominator_(graph_theory)

Definition at line 36 of file cfg_dominators.h.

Member Typedef Documentation

◆ cfgt

template<class P , class T , bool post_dom>
typedef procedure_local_cfg_baset<nodet, P, T> cfg_dominators_templatet< P, T, post_dom >::cfgt

Definition at line 46 of file cfg_dominators.h.

◆ target_sett

template<class P , class T , bool post_dom>
typedef std::set<T, typename P::target_less_than> cfg_dominators_templatet< P, T, post_dom >::target_sett

Definition at line 39 of file cfg_dominators.h.

Member Function Documentation

◆ dominates() [1/2]

template<class P , class T , bool post_dom>
bool cfg_dominators_templatet< P, T, post_dom >::dominates ( lhs,
const nodet rhs_node 
) const
inline

Returns true if the program point corresponding to rhs_node is dominated by program point lhs.

Saves node lookup compared to the dominates overload that takes two program points, so this version is preferable if you intend to check more than one potential dominator. Note by definition all program points dominate themselves.

Definition at line 76 of file cfg_dominators.h.

◆ dominates() [2/2]

template<class P , class T , bool post_dom>
bool cfg_dominators_templatet< P, T, post_dom >::dominates ( lhs,
rhs 
) const
inline

Returns true if program point lhs dominates rhs.

Note by definition all program points dominate themselves.

Definition at line 83 of file cfg_dominators.h.

◆ fixedpoint()

template<class P , class T , bool post_dom>
void cfg_dominators_templatet< P, T, post_dom >::fixedpoint ( P &  program)
protected

Computes the MOP for the dominator analysis.

Definition at line 146 of file cfg_dominators.h.

◆ get_node() [1/2]

template<class P , class T , bool post_dom>
cfgt::nodet& cfg_dominators_templatet< P, T, post_dom >::get_node ( const T &  program_point)
inline

Get the graph node (which gives dominators, predecessors and successors) for program_point.

Definition at line 60 of file cfg_dominators.h.

◆ get_node() [2/2]

template<class P , class T , bool post_dom>
const cfgt::nodet& cfg_dominators_templatet< P, T, post_dom >::get_node ( const T &  program_point) const
inline

Get the graph node (which gives dominators, predecessors and successors) for program_point.

Definition at line 53 of file cfg_dominators.h.

◆ get_node_index()

template<class P , class T , bool post_dom>
cfgt::entryt cfg_dominators_templatet< P, T, post_dom >::get_node_index ( const T &  program_point) const
inline

Get the graph node index for program_point.

Definition at line 66 of file cfg_dominators.h.

◆ initialise()

template<class P , class T , bool post_dom>
void cfg_dominators_templatet< P, T, post_dom >::initialise ( P &  program)
protected

Initialises the elements of the fixed point analysis.

Definition at line 139 of file cfg_dominators.h.

◆ operator()()

template<class P , class T , bool post_dom>
void cfg_dominators_templatet< P, T, post_dom >::operator() ( P &  program)

Compute dominators.

Definition at line 131 of file cfg_dominators.h.

◆ output()

template<class P , class T , bool post_dom>
void cfg_dominators_templatet< P, T, post_dom >::output ( std::ostream &  out) const

Print the result of the dominator computation.

Definition at line 276 of file cfg_dominators.h.

◆ program_point_reachable() [1/2]

template<class P , class T , bool post_dom>
bool cfg_dominators_templatet< P, T, post_dom >::program_point_reachable ( const nodet program_point_node) const
inline

Returns true if the program point for program_point_node is reachable from the entry point.

Saves a lookup compared to the overload taking a program point, so use this overload if you already have the node.

Definition at line 91 of file cfg_dominators.h.

◆ program_point_reachable() [2/2]

template<class P , class T , bool post_dom>
bool cfg_dominators_templatet< P, T, post_dom >::program_point_reachable ( program_point) const
inline

Returns true if the program point for program_point_node is reachable from the entry point.

Saves a lookup compared to the overload taking a program point, so use this overload if you already have the node.

Definition at line 102 of file cfg_dominators.h.

Member Data Documentation

◆ cfg

template<class P , class T , bool post_dom>
cfgt cfg_dominators_templatet< P, T, post_dom >::cfg

Definition at line 47 of file cfg_dominators.h.

◆ entry_node

template<class P , class T , bool post_dom>
T cfg_dominators_templatet< P, T, post_dom >::entry_node

Definition at line 110 of file cfg_dominators.h.


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