cprover
Loading...
Searching...
No Matches
natural_loops.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Compute natural loops in a goto_function
4
5Author: 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
46template <class P, class T>
48{
50
51public:
52 typedef typename parentt::loopt natural_loopt;
53
54 void operator()(P &program)
55 {
56 compute(program);
57 }
58
60 {
61 return cfg_dominators;
62 }
63
65 {
66 }
67
68 explicit natural_loops_templatet(P &program)
69 {
70 compute(program);
71 }
72
73protected:
76
77 void compute(P &program);
79};
80
84 public natural_loops_templatet<const goto_programt,
85 goto_programt::const_targett>
86{
87};
88
91
92inline void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
93{
94 show_loops<natural_loopst>(goto_model, out);
95}
96
97#ifdef DEBUG
98#include <iostream>
99#endif
100
102template<class P, class T>
104{
105 cfg_dominators(program);
106
107#ifdef DEBUG
108 cfg_dominators.output(std::cout);
109#endif
110
111 // find back-edges m->n
112 for(T m_it=program.instructions.begin();
113 m_it!=program.instructions.end();
114 ++m_it)
115 {
116 if(m_it->is_backwards_goto())
117 {
118 const auto &target=m_it->get_target();
119
120 if(target->location_number<=m_it->location_number)
121 {
122 #ifdef DEBUG
123 std::cout << "Computing loop for "
124 << m_it->location_number << " -> "
125 << target->location_number << "\n";
126 #endif
127
128 if(cfg_dominators.dominates(target, m_it))
129 compute_natural_loop(m_it, target);
130 }
131 }
132 }
133}
134
136template<class P, class T>
138{
139 assert(n->location_number<=m->location_number);
140
141 std::stack<T> stack;
142
143 auto insert_result = parentt::loop_map.emplace(n, natural_loopt{});
144 // Note the emplace *may* access a loop that already exists: this happens when
145 // a given header has more than one incoming edge, such as
146 // head: if(x) goto head; else goto head;
147 // In this case this compute routine is run twice, one for each backedge, with
148 // each adding whatever instructions can reach this 'm' (the program point
149 // that branches to the loop header, 'n').
150 natural_loopt &loop = insert_result.first->second;
151
152 loop.insert_instruction(n);
153 loop.insert_instruction(m);
154
155 if(n!=m)
156 stack.push(m);
157
158 while(!stack.empty())
159 {
160 T p=stack.top();
161 stack.pop();
162
163 const nodet &node = cfg_dominators.get_node(p);
164
165 for(const auto &edge : node.in)
166 {
167 T q=cfg_dominators.cfg[edge.first].PC;
168 if(loop.insert_instruction(q))
169 stack.push(q);
170 }
171 }
172}
173
174#endif // CPROVER_ANALYSES_NATURAL_LOOPS_H
Compute dominators for CFG of goto_function.
A loop, specified as a set of instructions.
bool insert_instruction(const T instruction)
Adds instruction to this loop.
Main driver for working out if a class (normally goto_programt) has any natural loops.
natural_loops_templatet(P &program)
void operator()(P &program)
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
cfg_dominators_templatet< P, T, false > cfg_dominators
void compute(P &program)
Finds all back-edges and computes the natural loops.
parentt::loopt natural_loopt
cfg_dominators_templatet< P, T, false >::cfgt::nodet nodet
loop_analysist< T > parentt
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
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 > natural_loops_mutablet
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)