CBMC
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 #include "loop_analysis.h"
31 
47 template <class P, class T, typename C>
49 {
51 
52 public:
53  typedef typename parentt::loopt natural_loopt;
54 
55  void operator()(P &program)
56  {
57  compute(program);
58  }
59 
61  {
62  return cfg_dominators;
63  }
64 
66  {
67  }
68 
69  explicit natural_loops_templatet(P &program)
70  {
71  compute(program);
72  }
73 
74 protected:
77 
78  void compute(P &program);
80 };
81 
85  const goto_programt,
86  goto_programt::const_targett,
87  goto_programt::target_less_than>
88 {
89 };
90 
96 
97 inline void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
98 {
99  show_loops<natural_loopst>(goto_model, out);
100 }
101 
102 #ifdef DEBUG
103 #include <iostream>
104 #endif
105 
107 template <class P, class T, typename C>
109 {
110  cfg_dominators(program);
111 
112 #ifdef DEBUG
113  cfg_dominators.output(std::cout);
114 #endif
115 
116  // find back-edges m->n
117  for(T m_it=program.instructions.begin();
118  m_it!=program.instructions.end();
119  ++m_it)
120  {
121  if(m_it->is_backwards_goto())
122  {
123  const auto &target=m_it->get_target();
124 
125  if(target->location_number<=m_it->location_number)
126  {
127  #ifdef DEBUG
128  std::cout << "Computing loop for "
129  << m_it->location_number << " -> "
130  << target->location_number << "\n";
131  #endif
132 
133  if(cfg_dominators.dominates(target, m_it))
134  compute_natural_loop(m_it, target);
135  }
136  }
137  }
138 }
139 
141 template <class P, class T, typename C>
143 {
144  PRECONDITION(n->location_number <= m->location_number);
145 
146  std::stack<T> stack;
147 
148  auto insert_result = parentt::loop_map.emplace(n, natural_loopt{});
149  // Note the emplace *may* access a loop that already exists: this happens when
150  // a given header has more than one incoming edge, such as
151  // head: if(x) goto head; else goto head;
152  // In this case this compute routine is run twice, one for each backedge, with
153  // each adding whatever instructions can reach this 'm' (the program point
154  // that branches to the loop header, 'n').
155  natural_loopt &loop = insert_result.first->second;
156 
157  loop.insert_instruction(n);
158  loop.insert_instruction(m);
159 
160  if(n!=m)
161  stack.push(m);
162 
163  while(!stack.empty())
164  {
165  T p=stack.top();
166  stack.pop();
167 
168  const nodet &node = cfg_dominators.get_node(p);
169 
170  for(const auto &edge : node.in)
171  {
172  T q=cfg_dominators.cfg[edge.first].PC;
173  if(loop.insert_instruction(q))
174  stack.push(q);
175  }
176  }
177 }
178 
179 #endif // CPROVER_ANALYSES_NATURAL_LOOPS_H
Compute dominators for CFG of goto_function.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
bool insert_instruction(const T instruction)
Adds instruction to this loop.
Definition: loop_analysis.h:74
Main driver for working out if a class (normally goto_programt) has any natural loops.
Definition: natural_loops.h:49
cfg_dominators_templatet< P, T, false > cfg_dominators
Definition: natural_loops.h:75
void operator()(P &program)
Definition: natural_loops.h:55
cfg_dominators_templatet< P, T, false >::cfgt::nodet nodet
Definition: natural_loops.h:76
parentt::loopt natural_loopt
Definition: natural_loops.h:53
void compute_natural_loop(T, T)
Computes the natural loop for a given back-edge (see Muchnick section 7.4)
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
Definition: natural_loops.h:60
loop_analysist< T, C > parentt
Definition: natural_loops.h:50
void compute(P &program)
Finds all back-edges and computes the natural loops.
natural_loops_templatet(P &program)
Definition: natural_loops.h:69
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
Definition: natural_loops.h:88
Symbol Table + CFG.
Data structure representing a loop in a GOTO program and an interface shared by all analyses that fin...
natural_loops_templatet< goto_programt, goto_programt::targett, goto_programt::target_less_than > natural_loops_mutablet
Definition: natural_loops.h:95
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
Definition: natural_loops.h:97
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
A total order over targett and const_targett.
Definition: goto_program.h:392