-
Notifications
You must be signed in to change notification settings - Fork 273
/
Copy pathloop_analysis.h
214 lines (173 loc) · 5.63 KB
/
loop_analysis.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
/*******************************************************************\
Module: Loop analysis
Author: Diffblue Ltd
\*******************************************************************/
/// \file
/// Data structure representing a loop in a GOTO program and an interface shared
/// by all analyses that find program loops.
#ifndef CPROVER_ANALYSES_LOOP_ANALYSIS_H
#define CPROVER_ANALYSES_LOOP_ANALYSIS_H
#include <goto-programs/goto_model.h>
template <class T, typename C>
class loop_analysist;
/// A loop, specified as a set of instructions
template <class T, typename C>
class loop_templatet
{
typedef std::set<T, C> loop_instructionst;
loop_instructionst loop_instructions;
friend loop_analysist<T, C>;
public:
loop_templatet() = default;
template <typename InstructionSet>
explicit loop_templatet(InstructionSet &&instructions)
: loop_instructions(std::forward<InstructionSet>(instructions))
{
}
/// Returns true if \p instruction is in this loop
bool virtual contains(const T instruction) const
{
return !loop_instructions.empty() && loop_instructions.count(instruction);
}
// NOLINTNEXTLINE(readability/identifiers)
typedef typename loop_instructionst::const_iterator const_iterator;
/// Iterator over this loop's instructions
const_iterator begin() const
{
return loop_instructions.begin();
}
/// Iterator over this loop's instructions
const_iterator end() const
{
return loop_instructions.end();
}
/// Number of instructions in this loop
std::size_t size() const
{
return loop_instructions.size();
}
/// Returns true if this loop contains no instructions
bool empty() const
{
return loop_instructions.empty();
}
/// Adds \p instruction to this loop.
/// \return true if the instruction is new
bool insert_instruction(const T instruction)
{
return loop_instructions.insert(instruction).second;
}
};
template <class T, typename C>
class loop_analysist
{
public:
typedef loop_templatet<T, C> loopt;
// map loop headers to loops
typedef std::map<T, loopt, C> loop_mapt;
loop_mapt loop_map;
virtual void output(std::ostream &) const;
/// Returns true if \p instruction is the header of any loop
bool is_loop_header(const T instruction) const
{
return loop_map.count(instruction);
}
loop_analysist() = default;
};
template <typename T, typename C>
class loop_with_parent_analysis_templatet : loop_templatet<T, C>
{
typedef loop_analysist<T, C> parent_analysist;
public:
explicit loop_with_parent_analysis_templatet(parent_analysist &loop_analysis)
: loop_analysis(loop_analysis)
{
}
template <typename InstructionSet>
explicit loop_with_parent_analysis_templatet(
parent_analysist &loop_analysis,
InstructionSet &&instructions)
: loop_templatet<T, C>(std::forward<InstructionSet>(instructions)),
loop_analysis(loop_analysis)
{
}
/// Returns true if \p instruction is in \p loop
bool loop_contains(
const typename loop_analysist<T, C>::loopt &loop,
const T instruction) const
{
return loop.loop_instructions.count(instruction);
}
/// Get the \ref parent_analysist analysis this loop relates to
const parent_analysist &get_loop_analysis() const
{
return loop_analysis;
}
/// Get the \ref parent_analysist analysis this loop relates to
parent_analysist &get_loop_analysis()
{
return loop_analysis;
}
private:
parent_analysist &loop_analysis;
};
template <class T, typename C>
class linked_loop_analysist : loop_analysist<T, C>
{
public:
linked_loop_analysist() = default;
/// Returns true if \p instruction is in \p loop
bool loop_contains(
const typename loop_analysist<T, C>::loopt &loop,
const T instruction) const
{
return loop.loop_instructions.count(instruction);
}
// The loop structures stored in `loop_map` contain back-pointers to this
// class, so we forbid copying or moving the analysis struct. If this becomes
// necessary then either add a layer of indirection or update the loop_map
// back-pointers on copy/move.
linked_loop_analysist(const linked_loop_analysist &) = delete;
linked_loop_analysist(linked_loop_analysist &&) = delete;
linked_loop_analysist &operator=(const linked_loop_analysist &) = delete;
linked_loop_analysist &operator=(linked_loop_analysist &&) = delete;
};
/// Print all natural loops that were found
template <class T, typename C>
void loop_analysist<T, C>::output(std::ostream &out) const
{
for(const auto &loop : loop_map)
{
unsigned n = loop.first->location_number;
std::unordered_set<std::size_t> backedge_location_numbers;
for(const auto &backedge : loop.first->incoming_edges)
backedge_location_numbers.insert(backedge->location_number);
out << n << " is head of { ";
std::vector<std::size_t> loop_location_numbers;
for(const auto &loop_instruction_it : loop.second)
loop_location_numbers.push_back(loop_instruction_it->location_number);
std::sort(loop_location_numbers.begin(), loop_location_numbers.end());
for(const auto location_number : loop_location_numbers)
{
if(location_number != loop_location_numbers.at(0))
out << ", ";
out << location_number;
if(backedge_location_numbers.count(location_number))
out << " (backedge)";
}
out << " }\n";
}
}
template <class LoopAnalysis>
void show_loops(const goto_modelt &goto_model, std::ostream &out)
{
for(const auto &gf_entry : goto_model.goto_functions.function_map)
{
out << "*** " << gf_entry.first << '\n';
LoopAnalysis loop_analysis;
loop_analysis(gf_entry.second.body);
loop_analysis.output(out);
out << '\n';
}
}
#endif // CPROVER_ANALYSES_LOOP_ANALYSIS_H