12 #ifndef CPROVER_ANALYSES_NATURAL_LOOPS_H 13 #define CPROVER_ANALYSES_NATURAL_LOOPS_H 23 template<
class P,
class T>
39 void output(std::ostream &)
const;
65 goto_programt::const_targett>
81 template<
class P,
class T>
84 cfg_dominators(program);
87 cfg_dominators.output(std::cout);
91 for(T m_it=program.instructions.begin();
92 m_it!=program.instructions.end();
95 if(m_it->is_backwards_goto())
97 const auto &target=m_it->get_target();
99 if(target->location_number<=m_it->location_number)
102 cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
105 std::cout <<
"Computing loop for " 106 << m_it->location_number <<
" -> " 107 << target->location_number <<
"\n";
110 if(node.dominators.find(target)!=node.dominators.end())
111 compute_natural_loop(m_it, target);
118 template<
class P,
class T>
121 assert(n->location_number<=m->location_number);
133 while(!
stack.empty())
139 cfg_dominators.cfg[cfg_dominators.cfg.entry_map[p]];
141 for(
const auto &edge : node.in)
143 T q=cfg_dominators.cfg[edge.first].PC;
144 std::pair<typename natural_loopt::const_iterator, bool> result=
153 template<
class P,
class T>
156 for(
const auto &loop : loop_map)
158 unsigned n=loop.first->location_number;
160 out << n <<
" is head of { ";
161 for(
typename natural_loopt::const_iterator l_it=loop.second.begin();
162 l_it!=loop.second.end(); ++l_it)
164 if(l_it!=loop.second.begin())
166 out << (*l_it)->location_number;
172 #endif // CPROVER_ANALYSES_NATURAL_LOOPS_H void output(std::ostream &) const
Print all natural loops that were found.
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
cfg_dominators_templatet< P, T, false >::cfgt::nodet nodet
std::set< T > natural_loopt
natural_loops_templatet< goto_programt, goto_programt::targett > natural_loops_mutablet
std::map< T, natural_loopt > loop_mapt
cfg_dominators_templatet< P, T, false > cfg_dominators
void compute_natural_loop(T, T)
Computes the natural loop for a given back-edge (see Muchnick section 7.4)
natural_loops_templatet(P &program)
void show_natural_loops(const goto_modelt &, std::ostream &out)
natural_loops_templatet()
Compute dominators for CFG of goto_function.
void compute(P &program)
Finds all back-edges and computes the natural loops.
void operator()(P &program)