cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
local_control_flow_history.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Abstract Interpretation
4
5
Author: Martin Brain, martin.brain@cs.ox.ac.uk
6
7
\*******************************************************************/
8
11
12
#include "
local_control_flow_history.h
"
13
14
template
<
bool
track_forward_jumps,
bool
track_backward_jumps>
15
ai_history_baset::step_returnt
16
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>::step
(
17
locationt
to,
18
const
trace_sett
&others,
19
trace_ptrt
caller_hist)
const
20
{
21
// First compute what the new history could be,
22
// then find it in others or possibly merge it if the limit is hit
23
24
std::shared_ptr<
const
local_control_flow_historyt
<
25
track_forward_jumps,
26
track_backward_jumps>>
27
next_step =
nullptr
;
28
29
// Local branching is the key step
30
if
(
31
current_loc
->is_goto() &&
32
(
current_loc
->is_backwards_goto() ? track_backward_jumps
33
: track_forward_jumps))
34
{
35
bool
branch_taken = (
current_loc
->get_target() == to) &&
36
!(
current_loc
->get_target() == std::next(
current_loc
));
37
// Slight oddity -- we regard branches to the next instruction as not taken
38
// regardless of their guard condition. This is slightly more general than
39
// is_skip() but without changing the step() interface to have a "taken"
40
// flag we will have to assume taken or not taken and not taken seems safer.
41
42
auto
decision = std::make_shared<local_control_flow_decisiont>(
43
current_loc
, branch_taken,
control_flow_decision_history
);
44
next_step = std::make_shared<
45
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>
>(
46
to, decision,
max_histories_per_location
);
47
}
48
else
if
(
49
current_loc
->is_function_call() &&
50
std::next(this->current_loc)->location_number != to->location_number)
51
{
52
// Because the history is local (to avoid massive explosion in work)
53
// the history at function start should be a merge of all callers.
54
// As we dont' need to enforce the number of histories we return directly.
55
if
(others.size() == 0)
56
{
57
next_step = std::make_shared<
58
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>
>(
59
to,
nullptr
,
max_histories_per_location
);
60
return
std::make_pair(
ai_history_baset::step_statust::NEW
, next_step);
61
}
62
else
63
{
64
INVARIANT
(
65
others.size() == 1,
66
"Function start should have at most one merged history"
);
67
INVARIANT
(
68
to_local_control_flow_history
(*(others.begin()))
69
->is_path_merge_history(),
70
"The one history must be a merge point"
);
71
72
return
std::make_pair(
73
ai_history_baset::step_statust::MERGED
, *(others.begin()));
74
}
75
}
76
else
if
(
current_loc
->is_end_function())
77
{
78
// This is slightly complicated as we have to drop the current,
79
// callee history and pick up the caller history.
80
PRECONDITION
(caller_hist !=
ai_history_baset::no_caller_history
);
81
82
next_step = std::make_shared<
83
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>
>(
84
to,
85
to_local_control_flow_history
(caller_hist)->control_flow_decision_history,
86
max_histories_per_location
);
87
}
88
else
89
{
90
// No changes to be made to the control_flow_decision_history
91
// Is a local step forward with no branching (or a skipped function call).
92
next_step = std::make_shared<
93
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>
>(
94
to,
control_flow_decision_history
,
max_histories_per_location
);
95
}
96
INVARIANT
(
97
next_step !=
nullptr
,
"All branches should create a candidate history"
);
98
99
// Now check whether this already exists
100
auto
it = others.find(next_step);
101
if
(it == others.end())
102
{
103
if
(
has_histories_per_location_limit
())
104
{
105
auto
number_of_histories = others.size();
106
107
if
(number_of_histories <
max_histories_per_location
- 1)
108
{
109
// Still below limit so we can add one
110
return
std::make_pair(
ai_history_baset::step_statust::NEW
, next_step);
111
}
112
else
if
(number_of_histories ==
max_histories_per_location
- 1)
113
{
114
// Last space --> we must create the merged history
115
next_step = std::make_shared<
local_control_flow_historyt
<
116
track_forward_jumps,
117
track_backward_jumps>>(to,
nullptr
,
max_histories_per_location
);
118
return
std::make_pair(
ai_history_baset::step_statust::NEW
, next_step);
119
}
120
else
if
(others.size() ==
max_histories_per_location
)
121
{
122
// Already at limit, need to return the merged history
123
124
// This relies on operator< sorting null after other pointers
125
auto
last_history_pointer = std::prev(others.end());
126
127
INVARIANT
(
128
to_local_control_flow_history
(*last_history_pointer)
129
->
is_path_merge_history
(),
130
"The last history must be the merged one"
);
131
132
return
std::make_pair(
133
ai_history_baset::step_statust::MERGED
, *last_history_pointer);
134
}
135
else
136
{
137
INVARIANT
(
138
others.size() <=
max_histories_per_location
,
139
"Histories-per-location limit should be enforced"
);
140
}
141
}
142
else
143
{
144
// No limit so ...
145
return
std::make_pair(
ai_history_baset::step_statust::NEW
, next_step);
146
}
147
}
148
else
149
{
150
// An equivalent history is already available so return that
151
return
std::make_pair(
ai_history_baset::step_statust::MERGED
, *it);
152
}
153
UNREACHABLE
;
154
}
155
156
template
<
bool
track_forward_jumps,
bool
track_backward_jumps>
157
bool
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>::
158
operator<
(
const
ai_history_baset
&op)
const
159
{
160
auto
other =
dynamic_cast<
161
const
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>
162
&
>
(op);
163
164
// Primary sort on the current location because it is fast, clusters relevant
165
// things. The side effect is that this can give depth-first search which may
166
// not be that "fair" when limiting the histories per location.
167
if
(this->
current_loc
->location_number < other.current_loc->location_number)
168
{
169
return
true
;
170
}
171
else
if
(
172
this->
current_loc
->location_number > other.current_loc->location_number)
173
{
174
return
false
;
175
}
176
else
177
{
178
if
(
179
this->
control_flow_decision_history
==
180
other.control_flow_decision_history)
181
{
182
// They are equal so...
183
return
false
;
184
}
185
else
if
(other.control_flow_decision_history ==
nullptr
)
186
{
187
// Special case so that the merged control flow history is last step's
188
// others set also means that non-merged histories are strictly preferred
189
// on the work queue
190
return
true
;
191
}
192
else
if
(this->
control_flow_decision_history
==
nullptr
)
193
{
194
// Another one, also guarding what we are about to do...
195
return
false
;
196
}
197
else
198
{
199
return
(
200
*(this->
control_flow_decision_history
) <
201
*(other.control_flow_decision_history));
202
}
203
}
204
UNREACHABLE
;
205
}
206
207
template
<
bool
track_forward_jumps,
bool
track_backward_jumps>
208
bool
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>::
209
operator==
(
const
ai_history_baset
&op)
const
210
{
211
auto
other =
dynamic_cast<
212
const
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>
213
&
>
(op);
214
215
// Make the short-cutting clear
216
if
(this->
current_loc
->location_number == other.current_loc->location_number)
217
{
218
if
(
219
this->
control_flow_decision_history
==
220
other.control_flow_decision_history)
221
{
222
return
true
;
223
}
224
else
if
(
225
this->
control_flow_decision_history
==
nullptr
||
226
other.control_flow_decision_history ==
nullptr
)
227
{
228
// Only one is null so clearly can't be equal
229
return
false
;
230
}
231
else
232
{
233
// Don't have unique construction so in things like step it is possible
234
// to get two distinct local_control_flow_decisiont objects that are equal
235
// in value.
236
return
(
237
*(this->
control_flow_decision_history
) ==
238
*(other.control_flow_decision_history));
239
}
240
}
241
else
242
{
243
return
false
;
244
}
245
UNREACHABLE
;
246
}
247
248
template
<
bool
track_forward_jumps,
bool
track_backward_jumps>
249
void
local_control_flow_historyt<track_forward_jumps, track_backward_jumps>::
250
output
(std::ostream &out)
const
251
{
252
out <<
"local_control_flow_history : location "
253
<<
current_loc
->location_number;
254
lcfd_ptrt
working =
control_flow_decision_history
;
255
while
(working !=
nullptr
)
256
{
257
out <<
" after "
<< working->
branch_location
->location_number;
258
if
(working->
branch_taken
)
259
{
260
out <<
" taken"
;
261
}
262
else
263
{
264
out <<
" not taken"
;
265
}
266
working = working->
previous
;
267
}
268
return
;
269
}
270
271
bool
local_control_flow_decisiont::
272
operator<
(
const
local_control_flow_decisiont
&op)
const
273
{
274
// Lower locations first, generally this means depth first
275
if
(
276
this->
branch_location
->location_number <
277
op.
branch_location
->location_number)
278
{
279
return
true
;
280
}
281
else
if
(
282
this->
branch_location
->location_number >
283
op.
branch_location
->location_number)
284
{
285
return
false
;
286
}
287
else
288
{
289
INVARIANT
(
290
this->
branch_location
->location_number ==
291
op.
branch_location
->location_number,
292
"Implied by if-then-else"
);
293
294
if
(!this->
branch_taken
&& op.
branch_taken
)
295
{
296
return
true
;
// Branch not taken takes priority
297
}
298
else
if
(this->
branch_taken
&& !op.
branch_taken
)
299
{
300
return
false
;
// The reverse case of above
301
}
302
else
303
{
304
INVARIANT
(
305
this->
branch_taken
== op.
branch_taken
,
"Implied by if-then-else"
);
306
307
if
(this->
previous
== op.
previous
)
308
{
309
return
false
;
// They are the same decision chain
310
}
311
else
if
(this->
previous
==
nullptr
)
312
{
313
// This prioritises complete histories over merged ones
314
return
false
;
315
}
316
else
if
(op.
previous
==
nullptr
)
317
{
318
// Again, the reverse
319
return
true
;
320
}
321
else
322
{
323
// Neither is null so sort by recursing along the list
324
return
*(this->
previous
) < *(op.
previous
);
325
}
326
}
327
}
328
UNREACHABLE
;
329
}
330
331
bool
local_control_flow_decisiont::
332
operator==
(
const
local_control_flow_decisiont
&op)
const
333
{
334
// Compare location numbers because we can't be sure that
335
// both location iterators are from the same function
336
// and so the iterators may not be comparable
337
if
(
338
this->
branch_location
->location_number ==
339
op.
branch_location
->location_number)
340
{
341
if
(this->
branch_taken
== op.
branch_taken
)
342
{
343
if
(this->
previous
== op.
previous
)
344
{
345
return
true
;
346
}
347
else
348
{
349
if
((this->
previous
!=
nullptr
) && (op.
previous
!=
nullptr
))
350
{
351
return
*(this->
previous
) == *(op.
previous
);
352
}
353
}
354
}
355
}
356
return
false
;
357
}
358
359
// Instantiate the versions we need
360
template
ai_history_baset::step_returnt
361
local_control_flow_historyt<true, true>::step
(
362
locationt to,
363
const
trace_sett &others,
364
trace_ptrt caller_hist)
const
;
365
366
template
ai_history_baset::step_returnt
367
local_control_flow_historyt<true, false>::step
(
368
locationt to,
369
const
trace_sett &others,
370
trace_ptrt caller_hist)
const
;
371
372
template
ai_history_baset::step_returnt
373
local_control_flow_historyt<false, true>::step
(
374
locationt to,
375
const
trace_sett &others,
376
trace_ptrt caller_hist)
const
;
377
378
template
ai_history_baset::step_returnt
379
local_control_flow_historyt<false, false>::step
(
380
locationt to,
381
const
trace_sett &others,
382
trace_ptrt caller_hist)
const
;
ai_history_baset::trace_ptrt
std::shared_ptr< const ai_history_baset > trace_ptrt
History objects are intended to be immutable so they can be shared to reduce memory overhead.
Definition
ai_history.h:43
ai_history_baset::step_statust::NEW
@ NEW
Definition
ai_history.h:83
ai_history_baset::step_statust::MERGED
@ MERGED
Definition
ai_history.h:84
ai_history_baset::step_returnt
std::pair< step_statust, trace_ptrt > step_returnt
Definition
ai_history.h:88
ai_history_baset::no_caller_history
static const trace_ptrt no_caller_history
Definition
ai_history.h:121
ai_history_baset::ai_history_baset
ai_history_baset(locationt)
Create a new history starting from a given location This is used to start the analysis from scratch P...
Definition
ai_history.h:49
ai_history_baset::locationt
goto_programt::const_targett locationt
Definition
ai_history.h:39
ai_history_baset::trace_sett
std::set< trace_ptrt, compare_historyt > trace_sett
Definition
ai_history.h:79
local_control_flow_decisiont::local_control_flow_decisiont
local_control_flow_decisiont(locationt loc, bool taken, lcfd_ptrt ptr)
Definition
local_control_flow_history.h:32
local_control_flow_decisiont::previous
lcfd_ptrt previous
Definition
local_control_flow_history.h:30
local_control_flow_decisiont::operator<
bool operator<(const local_control_flow_decisiont &op) const
Definition
local_control_flow_history.cpp:272
local_control_flow_decisiont::operator==
bool operator==(const local_control_flow_decisiont &op) const
Definition
local_control_flow_history.cpp:332
local_control_flow_decisiont::branch_location
locationt branch_location
Definition
local_control_flow_history.h:27
local_control_flow_decisiont::branch_taken
bool branch_taken
Definition
local_control_flow_history.h:28
local_control_flow_historyt::operator<
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
Definition
local_control_flow_history.cpp:158
local_control_flow_historyt::local_control_flow_historyt
local_control_flow_historyt(locationt loc)
Definition
local_control_flow_history.h:83
local_control_flow_historyt::output
void output(std::ostream &out) const override
Definition
local_control_flow_history.cpp:250
local_control_flow_historyt::operator==
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.
Definition
local_control_flow_history.cpp:209
local_control_flow_historyt::lcfd_ptrt
local_control_flow_decisiont::lcfd_ptrt lcfd_ptrt
Definition
local_control_flow_history.h:48
local_control_flow_historyt::has_histories_per_location_limit
bool has_histories_per_location_limit(void) const
Definition
local_control_flow_history.h:78
local_control_flow_historyt::to_local_control_flow_history
std::shared_ptr< const local_control_flow_historyt< track_forward_jumps, track_backward_jumps > > to_local_control_flow_history(trace_ptrt in) const
Definition
local_control_flow_history.h:59
local_control_flow_historyt::control_flow_decision_history
lcfd_ptrt control_flow_decision_history
Definition
local_control_flow_history.h:51
local_control_flow_historyt::step
step_returnt step(locationt to, const trace_sett &others, trace_ptrt caller_hist) const override
Step creates a new history by advancing the current one to location "to" It is given the set of all o...
Definition
local_control_flow_history.cpp:16
local_control_flow_historyt::max_histories_per_location
size_t max_histories_per_location
Definition
local_control_flow_history.h:52
local_control_flow_historyt::current_loc
locationt current_loc
Definition
local_control_flow_history.h:50
local_control_flow_historyt::is_path_merge_history
bool is_path_merge_history(void) const
Definition
local_control_flow_history.h:71
local_control_flow_history.h
Track function-local control flow for loop unwinding and path senstivity.
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition
invariant.h:525
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition
invariant.h:423
analyses
local_control_flow_history.cpp
Generated by
1.17.0