CBMC
call_stack_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 "call_stack_history.h"
13 
15  locationt to,
16  const trace_sett &others,
17  trace_ptrt caller_hist) const
18 {
19  DATA_INVARIANT(current_stack != nullptr, "current_stack must exist");
20 
21  cse_ptrt next_stack = nullptr;
22 
23  // First construct what the new history would be.
24  // This requires special handling if this edge is a function call or return
25  if(current_stack->current_location->is_function_call())
26  {
27  locationt l_return = std::next(current_stack->current_location);
28 
29  if(l_return->location_number == to->location_number)
30  {
31  // Is skipping the function call, only update the location
32  next_stack = cse_ptrt(
33  std::make_shared<call_stack_entryt>(l_return, current_stack->caller));
34  }
35  else
36  {
37  // An interprocedural (call) edge; add to the current stack
38 
39  // If the recursion limit has been reached
40  // shorten the stack / merge with the most recent invocation
41  // before we extend
42  cse_ptrt shorten = current_stack;
43 
45  {
46  unsigned int number_of_recursive_calls = 0;
47  cse_ptrt first_found = nullptr; // The most recent recursive call
48 
49  // Iterate back through the call stack
50  for(cse_ptrt i = current_stack->caller; i != nullptr; i = i->caller)
51  {
52  if(
53  i->current_location->location_number ==
54  current_stack->current_location->location_number)
55  {
56  // Found a recursive instance
57  if(first_found == nullptr)
58  {
59  first_found = i;
60  }
61  ++number_of_recursive_calls;
62  if(number_of_recursive_calls == recursion_limit)
63  {
64  shorten = first_found;
65  break;
66  }
67  }
68  }
69  }
70 
71  next_stack = cse_ptrt(std::make_shared<call_stack_entryt>(to, shorten));
72  }
73  }
74  else if(current_stack->current_location->is_end_function())
75  {
76  if(current_stack->caller == nullptr)
77  {
78  // Trying to return but there was no caller?
79  // Refuse to do the transition outright
80  return std::make_pair(ai_history_baset::step_statust::BLOCKED, nullptr);
81  }
82  else
83  {
84  INVARIANT(
86  "return from function should have a caller");
87 
88  // The expected call return site...
89  locationt l_caller_return =
90  std::next(current_stack->caller->current_location);
91 
92  if(l_caller_return->location_number == to->location_number)
93  {
94  INVARIANT(
95  std::next(caller_hist->current_location())->location_number ==
96  l_caller_return->location_number,
97  "caller and caller_hist should be consistent");
98  // It is tempting to think that...
99  // INVARIANT(*(current_stack->caller) ==
100  // *(std::dynamic_pointer_cast<const call_stack_historyt>
101  // (caller_hist)->current_stack),
102  // "call stacks should match");
103  // and that we could just use caller_hist->current_stack here.
104  // This fails when you hit the recursion limit so that the
105  // caller_hist has a deep stack but *this has a shallow one.
106 
107  // ... which is where we are going
108  next_stack = cse_ptrt(std::make_shared<call_stack_entryt>(
109  to, current_stack->caller->caller));
110  }
111  else
112  {
113  // Not possible to return to somewhere other than the call site
114  return std::make_pair(ai_history_baset::step_statust::BLOCKED, nullptr);
115  }
116  }
117  }
118  else
119  {
120  // Just update the location
121  next_stack =
122  cse_ptrt(std::make_shared<call_stack_entryt>(to, current_stack->caller));
123  }
124  INVARIANT(next_stack != nullptr, "All branches should initialise next_stack");
125 
126  // Create the potential next history
127  trace_ptrt next(new call_stack_historyt(next_stack, recursion_limit));
128  // It would be nice to use make_shared here but ... that doesn't work with
129  // protected constructors
130 
131  // If there is already an equivalent history, merge with that instead
132  auto it = others.find(next);
133 
134  if(it == others.end())
135  {
136  return std::make_pair(ai_history_baset::step_statust::NEW, next);
137  }
138  else
139  {
140  return std::make_pair(ai_history_baset::step_statust::MERGED, *it);
141  }
142 }
143 
145 {
146  auto other = dynamic_cast<const call_stack_historyt *>(&op);
147  PRECONDITION(other != nullptr);
148 
149  return *(this->current_stack) < *(other->current_stack);
150 }
151 
153 {
154  auto other = dynamic_cast<const call_stack_historyt *>(&op);
155  PRECONDITION(other != nullptr);
156 
157  return *(this->current_stack) == *(other->current_stack);
158 }
159 
160 void call_stack_historyt::output(std::ostream &out) const
161 {
162  out << "call_stack_history : stack "
163  << current_stack->current_location->location_number;
164  cse_ptrt working = current_stack->caller;
165  while(working != nullptr)
166  {
167  out << " from " << working->current_location->location_number;
168  working = working->caller;
169  }
170  return;
171 }
172 
174 operator<(const call_stack_entryt &op) const
175 {
176  if(
177  this->current_location->location_number <
178  op.current_location->location_number)
179  {
180  return true;
181  }
182  else if(
183  this->current_location->location_number >
184  op.current_location->location_number)
185  {
186  return false;
187  }
188  else
189  {
190  INVARIANT(
191  this->current_location->location_number ==
192  op.current_location->location_number,
193  "Implied by if-then-else");
194 
195  if(this->caller == op.caller)
196  {
197  return false; // Because they are equal
198  }
199  else if(this->caller == nullptr)
200  {
201  return true; // Shorter stacks are 'lower'
202  }
203  else if(op.caller == nullptr)
204  {
205  return false;
206  }
207  else
208  {
209  // Sort by the rest of the stack
210  return *(this->caller) < *(op.caller);
211  }
212  }
213  UNREACHABLE;
214 }
215 
217 operator==(const call_stack_entryt &op) const
218 {
219  if(
220  this->current_location->location_number ==
221  op.current_location->location_number)
222  {
223  if(this->caller == op.caller)
224  {
225  return true;
226  }
227  else if(this->caller != nullptr && op.caller != nullptr)
228  {
229  return *(this->caller) == *(op.caller);
230  }
231  }
232  return false;
233 }
History for tracking the call stack and performing interprocedural analysis.
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
bool operator<(const call_stack_entryt &op) const
bool operator==(const call_stack_entryt &op) const
Records the call stack Care must be taken when using this on recursive code; it will need the domain ...
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
std::shared_ptr< const call_stack_entryt > cse_ptrt
call_stack_historyt(cse_ptrt cur_stack, unsigned int rec_lim)
const locationt & current_location(void) const override
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
void output(std::ostream &out) const override
bool has_recursion_limit(void) const
unsigned int recursion_limit
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.
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...
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463