12 #ifndef CPROVER_ANALYSES_CFG_DOMINATORS_H 13 #define CPROVER_ANALYSES_CFG_DOMINATORS_H 25 template <
class P,
class T,
bool post_dom>
43 void output(std::ostream &)
const;
51 template <
class P,
class T,
bool post_dom>
56 cfg_dominators.
output(out);
61 template <
class P,
class T,
bool post_dom>
69 template <
class P,
class T,
bool post_dom>
76 template <
class P,
class T,
bool post_dom>
79 std::list<T> worklist;
81 if(cfg.nodes_empty(program))
85 entry_node=cfg.get_last_node(program);
87 entry_node=cfg.get_first_node(program);
88 typename cfgt::nodet &n=cfg[cfg.entry_map[entry_node]];
89 n.dominators.insert(entry_node);
91 for(
typename cfgt::edgest::const_iterator
92 s_it=(post_dom?n.
in:n.
out).begin();
93 s_it!=(post_dom?n.
in:n.
out).end();
95 worklist.push_back(cfg[s_it->first].PC);
97 while(!worklist.empty())
100 T current=worklist.front();
101 worklist.pop_front();
104 typename cfgt::nodet &node=cfg[cfg.entry_map[current]];
105 if(node.dominators.empty())
107 for(
const auto &edge : (post_dom ? node.
out : node.
in))
108 if(!cfg[edge.first].dominators.empty())
110 node.dominators=cfg[edge.first].dominators;
111 node.dominators.insert(current);
117 for(
const auto &edge : (post_dom ? node.
out : node.
in))
119 const target_sett &other=cfg[edge.first].dominators;
123 typename target_sett::const_iterator n_it=node.dominators.begin();
124 typename target_sett::const_iterator o_it=other.begin();
127 while(n_it!=node.dominators.end() && o_it!=other.end())
134 node.dominators.erase(n_it++);
145 while(n_it!=node.dominators.end())
152 node.dominators.erase(n_it++);
159 for(
const auto &edge : (post_dom ? node.
in : node.
out))
161 worklist.push_back(cfg[edge.first].PC);
180 out << target->code.pretty();
184 template <
class P,
class T,
bool post_dom>
187 for(
const auto &node : cfg.entry_map)
193 out <<
" post-dominated by ";
195 out <<
" dominated by ";
197 for(
const auto &d : cfg[node.second].dominators)
221 out << node->location_number;
224 #endif // CPROVER_ANALYSES_CFG_DOMINATORS_H void initialise(P &program)
Initialises the elements of the fixed point analysis.
std::set< T > target_sett
void fixedpoint(P &program)
Computes the MOP for the dominator analysis.
std::ostream & operator<<(std::ostream &out, const cfg_dominators_templatet< P, T, post_dom > &cfg_dominators)
Print the result of the dominator computation.
Goto Programs with Functions.
void dominators_pretty_print_node(const T &node, std::ostream &out)
Pretty-print a single node in the dominator tree.
instructionst::iterator targett
instructionst::const_iterator const_targett
void output(std::ostream &) const
Print the result of the dominator computation.
A generic container class for the GOTO intermediate representation of one function.
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, true > cfg_post_dominatorst
void operator()(P &program)
Compute dominators.
procedure_local_cfg_baset< nodet, P, T > cfgt
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false > cfg_dominatorst