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