cprover
Loading...
Searching...
No Matches
lexical_loops.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Compute lexical loops in a goto_function
4
5Author: Diffblue Ltd
6
7\*******************************************************************/
8
36
37#ifndef CPROVER_ANALYSES_LEXICAL_LOOPS_H
38#define CPROVER_ANALYSES_LEXICAL_LOOPS_H
39
40#include <iosfwd>
41#include <set>
42#include <stack>
43
45
46#include "loop_analysis.h"
47
63template <class P, class T>
65{
67
68public:
69 typedef typename parentt::loopt lexical_loopt;
70
71 void operator()(P &program)
72 {
73 compute(program);
74 }
75
77
78 explicit lexical_loops_templatet(P &program)
79 {
80 compute(program);
81 }
82
87
88 void output(std::ostream &out) const
89 {
90 parentt::output(out);
92 out << "Note not all loops were in lexical loop form\n";
93 }
94
95 virtual ~lexical_loops_templatet() = default;
96
97protected:
98 void compute(P &program);
99 bool compute_lexical_loop(T, T);
100
102};
103
105 const goto_programt,
108
109#ifdef DEBUG
110# include <iostream>
111#endif
112
114template <class P, class T>
116{
117 all_in_lexical_loop_form = true;
118
119 // find back-edges m->n
120 for(auto it = program.instructions.begin(); it != program.instructions.end();
121 ++it)
122 {
123 if(it->is_backwards_goto())
124 {
125 const auto &target = it->get_target();
126
127 if(target->location_number <= it->location_number)
128 {
129#ifdef DEBUG
130 std::cout << "Computing loop for " << it->location_number << " -> "
131 << target->location_number << "\n";
132#endif
133
134 if(!compute_lexical_loop(it, target))
135 all_in_lexical_loop_form = false;
136 }
137 }
138 }
139}
140
145template <class P, class T>
147 T loop_tail,
148 T loop_head)
149{
150 INVARIANT(
151 loop_head->location_number <= loop_tail->location_number,
152 "loop header should come lexically before the tail");
153
154 std::stack<T> stack;
155 std::set<T> loop_instructions;
156
157 loop_instructions.insert(loop_head);
158 loop_instructions.insert(loop_tail);
159
160 if(loop_head != loop_tail)
161 stack.push(loop_tail);
162
163 while(!stack.empty())
164 {
165 T loop_instruction = stack.top();
166 stack.pop();
167
168 for(auto predecessor : loop_instruction->incoming_edges)
169 {
170 if(
171 predecessor->location_number > loop_tail->location_number ||
172 predecessor->location_number < loop_head->location_number)
173 {
174 // Not a lexical loop: has an incoming edge from outside.
175 return false;
176 }
177 if(loop_instructions.insert(predecessor).second)
178 stack.push(predecessor);
179 }
180 }
181
182 auto insert_result = parentt::loop_map.emplace(
183 loop_head, lexical_loopt{std::move(loop_instructions)});
184
185 // If this isn't a new loop head (i.e. return_result.second is false) then we
186 // have multiple backedges targeting one loop header: this is not in simple
187 // lexical loop form.
188 return insert_result.second;
189}
190
191inline void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
192{
193 show_loops<lexical_loopst>(goto_model, out);
194}
195
196#endif // CPROVER_ANALYSES_LEXICAL_LOOPS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
Main driver for working out if a class (normally goto_programt) has any lexical loops.
loop_analysist< T > parentt
lexical_loops_templatet(P &program)
bool all_cycles_in_lexical_loop_form() const
virtual ~lexical_loops_templatet()=default
bool compute_lexical_loop(T, T)
Computes the lexical loop for a given back-edge by walking backwards from the tail,...
void operator()(P &program)
void compute(P &program)
Finds all back-edges and computes the lexical loops.
void output(std::ostream &out) const
Print all natural loops that were found.
parentt::loopt lexical_loopt
lexical_loops_templatet()=default
virtual void output(std::ostream &) const
Print all natural loops that were found.
Symbol Table + CFG.
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
lexical_loops_templatet< const goto_programt, goto_programt::const_targett > lexical_loopst
Data structure representing a loop in a GOTO program and an interface shared by all analyses that fin...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423