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::nodet & | get_node (const T &program_point) const |
Get the graph node (which gives dominators, predecessors and successors) for program_point. More... | |
| cfgt::nodet & | get_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 |
| T | 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
| 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
| 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]
|
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]
|
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()
|
protected |
Computes the MOP for the dominator analysis.
Definition at line 146 of file cfg_dominators.h.
◆ get_node() [1/2]
|
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]
|
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()
|
inline |
Get the graph node index for program_point.
Definition at line 66 of file cfg_dominators.h.
◆ initialise()
|
protected |
Initialises the elements of the fixed point analysis.
Definition at line 139 of file cfg_dominators.h.
◆ operator()()
| void cfg_dominators_templatet< P, T, post_dom >::operator() | ( | P & | program | ) |
Compute dominators.
Definition at line 131 of file cfg_dominators.h.
◆ output()
| 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]
|
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]
|
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
| cfgt cfg_dominators_templatet< P, T, post_dom >::cfg |
Definition at line 47 of file cfg_dominators.h.
◆ entry_node
| 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:
- /home/runner/work/cbmc/cbmc/src/analyses/cfg_dominators.h
