cprover
natural_loops.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Compute natural loops in a goto_function
4 
5 Author: Georg Weissenbacher, georg@weissenbacher.name
6 
7 \*******************************************************************/
8 
19 
20 #ifndef CPROVER_ANALYSES_NATURAL_LOOPS_H
21 #define CPROVER_ANALYSES_NATURAL_LOOPS_H
22 
23 #include <stack>
24 #include <iosfwd>
25 #include <set>
26 
28 
29 #include "cfg_dominators.h"
30 
45 template<class P, class T>
47 {
48 public:
49  typedef std::set<T> natural_loopt;
50 
51  // map loop headers to loops
52  typedef std::map<T, natural_loopt> loop_mapt;
53 
55 
56  void operator()(P &program)
57  {
58  compute(program);
59  }
60 
61  void output(std::ostream &) const;
62 
64  {
65  return cfg_dominators;
66  }
67 
69  {
70  }
71 
72  explicit natural_loops_templatet(P &program)
73  {
74  compute(program);
75  }
76 
77 protected:
80 
81  void compute(P &program);
82  void compute_natural_loop(T, T);
83 };
84 
88  public natural_loops_templatet<const goto_programt,
89  goto_programt::const_targett>
90 {
91 };
92 
95 
97  const goto_modelt &,
98  std::ostream &out);
99 
100 #ifdef DEBUG
101 #include <iostream>
102 #endif
103 
105 template<class P, class T>
107 {
108  cfg_dominators(program);
109 
110 #ifdef DEBUG
111  cfg_dominators.output(std::cout);
112 #endif
113 
114  // find back-edges m->n
115  for(T m_it=program.instructions.begin();
116  m_it!=program.instructions.end();
117  ++m_it)
118  {
119  if(m_it->is_backwards_goto())
120  {
121  const auto &target=m_it->get_target();
122 
123  if(target->location_number<=m_it->location_number)
124  {
125  const nodet &node=
126  cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
127 
128  #ifdef DEBUG
129  std::cout << "Computing loop for "
130  << m_it->location_number << " -> "
131  << target->location_number << "\n";
132  #endif
133 
134  if(node.dominators.find(target)!=node.dominators.end())
135  compute_natural_loop(m_it, target);
136  }
137  }
138  }
139 }
140 
142 template<class P, class T>
144 {
145  assert(n->location_number<=m->location_number);
146 
147  std::stack<T> stack;
148 
149  natural_loopt &loop=loop_map[n];
150 
151  loop.insert(n);
152  loop.insert(m);
153 
154  if(n!=m)
155  stack.push(m);
156 
157  while(!stack.empty())
158  {
159  T p=stack.top();
160  stack.pop();
161 
162  const nodet &node=
163  cfg_dominators.cfg[cfg_dominators.cfg.entry_map[p]];
164 
165  for(const auto &edge : node.in)
166  {
167  T q=cfg_dominators.cfg[edge.first].PC;
168  std::pair<typename natural_loopt::const_iterator, bool> result=
169  loop.insert(q);
170  if(result.second)
171  stack.push(q);
172  }
173  }
174 }
175 
177 template<class P, class T>
178 void natural_loops_templatet<P, T>::output(std::ostream &out) const
179 {
180  for(const auto &loop : loop_map)
181  {
182  unsigned n=loop.first->location_number;
183 
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)
187  {
188  if(l_it!=loop.second.begin())
189  out << ", ";
190  out << (*l_it)->location_number;
191  }
192  out << " }\n";
193  }
194 }
195 
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
Definition: natural_loops.h:63
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
Definition: natural_loops.h:87
cfg_dominators_templatet< P, T, false >::cfgt::nodet nodet
Definition: natural_loops.h:79
std::set< T > natural_loopt
Definition: natural_loops.h:49
natural_loops_templatet< goto_programt, goto_programt::targett > natural_loops_mutablet
Definition: natural_loops.h:94
std::map< T, natural_loopt > loop_mapt
Definition: natural_loops.h:52
Main driver for working out if a class (normally goto_programt) has any natural loops.
Definition: natural_loops.h:46
Symbol Table + CFG.
cfg_dominators_templatet< P, T, false > cfg_dominators
Definition: natural_loops.h:78
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)
Definition: natural_loops.h:72
void show_natural_loops(const goto_modelt &, std::ostream &out)
Compute dominators for CFG of goto_function.
#define stack(x)
Definition: parser.h:144
void compute(P &program)
Finds all back-edges and computes the natural loops.
void operator()(P &program)
Definition: natural_loops.h:56