12 #ifndef CPROVER_ANALYSES_CFG_DOMINATORS_H
13 #define CPROVER_ANALYSES_CFG_DOMINATORS_H
35 template <
class P,
class T,
bool post_dom>
39 typedef std::set<T, typename P::target_less_than>
target_sett;
120 template <
class P,
class T,
bool post_dom>
125 cfg_dominators.
output(out);
130 template <
class P,
class T,
bool post_dom>
138 template <
class P,
class T,
bool post_dom>
145 template <
class P,
class T,
bool post_dom>
148 std::list<T> worklist;
150 if(cfgt::nodes_empty(program))
154 entry_node = cfgt::get_last_node(program);
156 entry_node = cfgt::get_first_node(program);
157 typename cfgt::nodet &n = cfg.get_node(entry_node);
158 n.dominators.insert(entry_node);
160 for(
typename cfgt::edgest::const_iterator
161 s_it=(post_dom?n.
in:n.
out).begin();
162 s_it!=(post_dom?n.
in:n.
out).end();
164 worklist.push_back(cfg[s_it->first].PC);
170 for(
auto &cfg_entry : cfg.entry_map)
172 if(cfg[cfg_entry.second].PC == entry_node)
175 typename cfgt::nodet &n_it = cfg[cfg_entry.second];
178 (n_it.
out.size() == 1 && n_it.
out.begin()->first == cfg_entry.second))
180 n_it.dominators.insert(cfg[cfg_entry.second].PC);
181 for(
const auto &predecessor : n_it.
in)
182 worklist.push_back(cfg[predecessor.first].PC);
187 while(!worklist.empty())
190 T current=worklist.front();
191 worklist.pop_front();
194 typename cfgt::nodet &node = cfg.get_node(current);
195 if(node.dominators.empty())
197 for(
const auto &edge : (post_dom ? node.
out : node.
in))
198 if(!cfg[edge.first].dominators.empty())
200 node.dominators=cfg[edge.first].dominators;
201 node.dominators.insert(current);
207 for(
const auto &edge : (post_dom ? node.
out : node.
in))
209 const target_sett &other=cfg[edge.first].dominators;
213 typename target_sett::const_iterator n_it=node.dominators.begin();
214 typename target_sett::const_iterator o_it=other.begin();
217 while(n_it!=node.dominators.end() && o_it!=other.end())
221 else if(
typename P::target_less_than()(*n_it, *o_it))
224 node.dominators.erase(n_it++);
226 else if(
typename P::target_less_than()(*o_it, *n_it))
235 while(n_it!=node.dominators.end())
242 node.dominators.erase(n_it++);
249 for(
const auto &edge : (post_dom ? node.
in : node.
out))
251 worklist.push_back(cfg[edge.first].PC);
271 out << target->code().pretty();
275 template <
class P,
class T,
bool post_dom>
278 for(
const auto &node : cfg.entries())
284 out <<
" post-dominated by ";
286 out <<
" dominated by ";
288 for(
const auto &d : cfg[node.second].dominators)
312 out << node->location_number;
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false > cfg_dominatorst
void dominators_pretty_print_node(const T &node, std::ostream &out)
Pretty-print a single node in the dominator tree.
std::ostream & operator<<(std::ostream &out, const cfg_dominators_templatet< P, T, post_dom > &cfg_dominators)
Print the result of the dominator computation.
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, true > cfg_post_dominatorst
base_grapht::node_indext entryt
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
bool dominates(T lhs, T rhs) const
Returns true if program point lhs dominates rhs.
procedure_local_cfg_baset< nodet, P, T > cfgt
cfgt::nodet & get_node(const T &program_point)
Get the graph node (which gives dominators, predecessors and successors) for program_point.
void output(std::ostream &) const
Print the result of the dominator computation.
void operator()(P &program)
Compute dominators.
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.
void fixedpoint(P &program)
Computes the MOP for the dominator analysis.
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.
std::set< T, typename P::target_less_than > target_sett
bool program_point_reachable(T program_point) const
Returns true if the program point for program_point_node is reachable from the entry point.
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
void initialise(P &program)
Initialises the elements of the fixed point analysis.
cfgt::entryt get_node_index(const T &program_point) const
Get the graph node index for program_point.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
Goto Programs with Functions.