CBMC
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
64template <class P, class T, typename C>
66{
68
69public:
70 typedef typename parentt::loopt lexical_loopt;
71
72 void operator()(P &program)
73 {
74 compute(program);
75 }
76
78
79 explicit lexical_loops_templatet(P &program)
80 {
81 compute(program);
82 }
83
88
89 void output(std::ostream &out) const
90 {
91 parentt::output(out);
93 out << "Note not all loops were in lexical loop form\n";
94 }
95
96 virtual ~lexical_loops_templatet() = default;
97
98protected:
99 void compute(P &program);
100 bool compute_lexical_loop(T, T);
101
103};
104
106 const goto_programt,
110
111#ifdef DEBUG
112# include <iostream>
113#endif
114
116template <class P, class T, typename C>
118{
119 all_in_lexical_loop_form = true;
120
121 // find back-edges m->n
122 for(auto it = program.instructions.begin(); it != program.instructions.end();
123 ++it)
124 {
125 if(it->is_backwards_goto())
126 {
127 const auto &target = it->get_target();
128
129 if(target->location_number <= it->location_number)
130 {
131#ifdef DEBUG
132 std::cout << "Computing loop for " << it->location_number << " -> "
133 << target->location_number << "\n";
134#endif
135
136 if(!compute_lexical_loop(it, target))
137 all_in_lexical_loop_form = false;
138 }
139 }
140 }
141}
142
147template <class P, class T, typename C>
149 T loop_tail,
150 T loop_head)
151{
152 INVARIANT(
153 loop_head->location_number <= loop_tail->location_number,
154 "loop header should come lexically before the tail");
155
156 std::stack<T> stack;
157 std::set<T, C> loop_instructions;
158
159 loop_instructions.insert(loop_head);
160 loop_instructions.insert(loop_tail);
161
162 if(loop_head != loop_tail)
163 stack.push(loop_tail);
164
165 while(!stack.empty())
166 {
167 T loop_instruction = stack.top();
168 stack.pop();
169
170 for(auto predecessor : loop_instruction->incoming_edges)
171 {
172 if(
173 predecessor->location_number > loop_tail->location_number ||
174 predecessor->location_number < loop_head->location_number)
175 {
176 // Not a lexical loop: has an incoming edge from outside.
177 return false;
178 }
179 if(loop_instructions.insert(predecessor).second)
180 stack.push(predecessor);
181 }
182 }
183
184 auto insert_result = parentt::loop_map.emplace(
185 loop_head, lexical_loopt{std::move(loop_instructions)});
186
187 // If this isn't a new loop head (i.e. return_result.second is false) then we
188 // have multiple backedges targeting one loop header: this is not in simple
189 // lexical loop form.
190 return insert_result.second;
191}
192
193inline void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
194{
195 show_loops<lexical_loopst>(goto_model, out);
196}
197
198#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:562
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.
lexical_loops_templatet(P &program)
loop_analysist< T, C > parentt
lexical_loops_templatet()=default
bool all_cycles_in_lexical_loop_form() const
bool compute_lexical_loop(T, T)
Computes the lexical loop for a given back-edge by walking backwards from the tail,...
virtual ~lexical_loops_templatet()=default
void compute(P &program)
Finds all back-edges and computes the lexical loops.
void operator()(P &program)
parentt::loopt lexical_loopt
void output(std::ostream &out) const
Print all natural loops that were found.
virtual void output(std::ostream &) const
Print all natural loops that were found.
Symbol Table + CFG.
lexical_loops_templatet< const goto_programt, goto_programt::const_targett, goto_programt::target_less_than > lexical_loopst
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
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
A total order over targett and const_targett.