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 
11 
12 #ifndef CPROVER_ANALYSES_NATURAL_LOOPS_H
13 #define CPROVER_ANALYSES_NATURAL_LOOPS_H
14 
15 #include <stack>
16 #include <iosfwd>
17 #include <set>
18 
20 
21 #include "cfg_dominators.h"
22 
23 template<class P, class T>
25 {
26 public:
27  typedef std::set<T> natural_loopt;
28 
29  // map loop headers to loops
30  typedef std::map<T, natural_loopt> loop_mapt;
31 
33 
34  void operator()(P &program)
35  {
36  compute(program);
37  }
38 
39  void output(std::ostream &) const;
40 
42  {
43  return cfg_dominators;
44  }
45 
47  {
48  }
49 
50  explicit natural_loops_templatet(P &program)
51  {
52  compute(program);
53  }
54 
55 protected:
58 
59  void compute(P &program);
60  void compute_natural_loop(T, T);
61 };
62 
64  public natural_loops_templatet<const goto_programt,
65  goto_programt::const_targett>
66 {
67 };
68 
71 
73  const goto_modelt &,
74  std::ostream &out);
75 
77 #ifdef DEBUG
78 #include <iostream>
79 #endif
80 
81 template<class P, class T>
83 {
84  cfg_dominators(program);
85 
86 #ifdef DEBUG
87  cfg_dominators.output(std::cout);
88 #endif
89 
90  // find back-edges m->n
91  for(T m_it=program.instructions.begin();
92  m_it!=program.instructions.end();
93  ++m_it)
94  {
95  if(m_it->is_backwards_goto())
96  {
97  const auto &target=m_it->get_target();
98 
99  if(target->location_number<=m_it->location_number)
100  {
101  const nodet &node=
102  cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
103 
104  #ifdef DEBUG
105  std::cout << "Computing loop for "
106  << m_it->location_number << " -> "
107  << target->location_number << "\n";
108  #endif
109 
110  if(node.dominators.find(target)!=node.dominators.end())
111  compute_natural_loop(m_it, target);
112  }
113  }
114  }
115 }
116 
118 template<class P, class T>
120 {
121  assert(n->location_number<=m->location_number);
122 
123  std::stack<T> stack;
124 
125  natural_loopt &loop=loop_map[n];
126 
127  loop.insert(n);
128  loop.insert(m);
129 
130  if(n!=m)
131  stack.push(m);
132 
133  while(!stack.empty())
134  {
135  T p=stack.top();
136  stack.pop();
137 
138  const nodet &node=
139  cfg_dominators.cfg[cfg_dominators.cfg.entry_map[p]];
140 
141  for(const auto &edge : node.in)
142  {
143  T q=cfg_dominators.cfg[edge.first].PC;
144  std::pair<typename natural_loopt::const_iterator, bool> result=
145  loop.insert(q);
146  if(result.second)
147  stack.push(q);
148  }
149  }
150 }
151 
153 template<class P, class T>
154 void natural_loops_templatet<P, T>::output(std::ostream &out) const
155 {
156  for(const auto &loop : loop_map)
157  {
158  unsigned n=loop.first->location_number;
159 
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)
163  {
164  if(l_it!=loop.second.begin())
165  out << ", ";
166  out << (*l_it)->location_number;
167  }
168  out << " }\n";
169  }
170 }
171 
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
Definition: natural_loops.h:41
cfg_dominators_templatet< P, T, false >::cfgt::nodet nodet
Definition: natural_loops.h:57
std::set< T > natural_loopt
Definition: natural_loops.h:27
natural_loops_templatet< goto_programt, goto_programt::targett > natural_loops_mutablet
Definition: natural_loops.h:70
std::map< T, natural_loopt > loop_mapt
Definition: natural_loops.h:30
Symbol Table + CFG.
cfg_dominators_templatet< P, T, false > cfg_dominators
Definition: natural_loops.h:56
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:50
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.
Definition: natural_loops.h:82
void operator()(P &program)
Definition: natural_loops.h:34