CBMC
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 
13 
14 template <bool track_forward_jumps, bool track_backward_jumps>
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<
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  {
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.
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  }
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>
158 operator<(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  }
204  UNREACHABLE;
205 }
206 
207 template <bool track_forward_jumps, bool track_backward_jumps>
209 operator==(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  }
245  UNREACHABLE;
246 }
247 
248 template <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  }
328  UNREACHABLE;
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
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