CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
local_control_flow_history.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract Interpretation
4
5Author: Martin Brain, martin.brain@cs.ox.ac.uk
6
7\*******************************************************************/
8
11
13
14template <bool track_forward_jumps, bool track_backward_jumps>
18 const trace_sett &others,
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<
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<
59 to, nullptr, max_histories_per_location);
60 return std::make_pair(ai_history_baset::step_statust::NEW, next_step);
61 }
62 else
63 {
65 others.size() == 1,
66 "Function start should have at most one merged history");
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(
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.
81
82 next_step = std::make_shared<
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<
94 to, control_flow_decision_history, max_histories_per_location);
95 }
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(
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 }
154}
155
156template <bool track_forward_jumps, bool track_backward_jumps>
158operator<(const ai_history_baset &op) const
159{
160 auto other = dynamic_cast<
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 }
205}
206
207template <bool track_forward_jumps, bool track_backward_jumps>
209operator==(const ai_history_baset &op) const
210{
211 auto other = dynamic_cast<
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 }
246}
247
248template <bool track_forward_jumps, bool 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
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 }
329}
330
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
362 locationt to,
363 const trace_sett &others,
364 trace_ptrt caller_hist) const;
365
368 locationt to,
369 const trace_sett &others,
370 trace_ptrt caller_hist) const;
371
374 locationt to,
375 const trace_sett &others,
376 trace_ptrt caller_hist) const;
377
380 locationt to,
381 const trace_sett &others,
382 trace_ptrt caller_hist) const;
A history object is an abstraction / representation of the control-flow part of a set of traces.
Definition ai_history.h:37
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
std::pair< step_statust, trace_ptrt > step_returnt
Definition ai_history.h:88
static const trace_ptrt no_caller_history
Definition ai_history.h:121
goto_programt::const_targett locationt
Definition ai_history.h:39
std::set< trace_ptrt, compare_historyt > trace_sett
Definition ai_history.h:79
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ait()
Definition ai.h:565
Records all local control-flow decisions up to a limit of number of histories per location.
bool operator<(const local_control_flow_decisiont &op) const
bool operator==(const local_control_flow_decisiont &op) const
Whether we track forwards and / or backwards jumps is compile-time fixed as it does not need to be va...
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
void output(std::ostream &out) const override
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.
local_control_flow_decisiont::lcfd_ptrt lcfd_ptrt
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...
Track function-local control flow for loop unwinding and path senstivity.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423