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