20 #ifndef CPROVER_ANALYSES_NATURAL_LOOPS_H 21 #define CPROVER_ANALYSES_NATURAL_LOOPS_H 45 template<
class P,
class T>
61 void output(std::ostream &)
const;
89 goto_programt::const_targett>
105 template<
class P,
class T>
108 cfg_dominators(program);
111 cfg_dominators.output(std::cout);
115 for(T m_it=program.instructions.begin();
116 m_it!=program.instructions.end();
119 if(m_it->is_backwards_goto())
121 const auto &target=m_it->get_target();
123 if(target->location_number<=m_it->location_number)
126 cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
129 std::cout <<
"Computing loop for " 130 << m_it->location_number <<
" -> " 131 << target->location_number <<
"\n";
134 if(node.dominators.find(target)!=node.dominators.end())
135 compute_natural_loop(m_it, target);
142 template<
class P,
class T>
145 assert(n->location_number<=m->location_number);
157 while(!
stack.empty())
163 cfg_dominators.cfg[cfg_dominators.cfg.entry_map[p]];
165 for(
const auto &edge : node.in)
167 T q=cfg_dominators.cfg[edge.first].PC;
168 std::pair<typename natural_loopt::const_iterator, bool> result=
177 template<
class P,
class T>
180 for(
const auto &loop : loop_map)
182 unsigned n=loop.first->location_number;
184 out << n <<
" is head of { ";
185 for(
typename natural_loopt::const_iterator l_it=loop.second.begin();
186 l_it!=loop.second.end(); ++l_it)
188 if(l_it!=loop.second.begin())
190 out << (*l_it)->location_number;
196 #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
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
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
Main driver for working out if a class (normally goto_programt) has any natural loops.
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)