cprover
ai_history.h
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 #ifndef CPROVER_ANALYSES_AI_HISTORY_H
13 #define CPROVER_ANALYSES_AI_HISTORY_H
14 
15 #include <memory>
16 
18 
19 #include <util/json.h>
20 #include <util/xml.h>
21 
34 
37 {
38 public:
40 
43  typedef std::shared_ptr<const ai_history_baset> trace_ptrt;
44 
45 protected:
50  {
51  }
52 
54  {
55  }
56 
57 public:
59  {
60  }
61 
73  {
74  bool operator()(const trace_ptrt &l, const trace_ptrt &r) const
75  {
76  return *l < *r;
77  }
78  };
79  typedef std::set<trace_ptrt, compare_historyt> trace_sett; // Order matters!
80 
81  enum class step_statust
82  {
83  NEW,
84  MERGED,
85  BLOCKED
86  };
87 
88  typedef std::pair<step_statust, trace_ptrt> step_returnt;
111  virtual step_returnt step(locationt to, const trace_sett &others) const = 0;
112 
114  virtual bool operator<(const ai_history_baset &op) const = 0;
115 
117  virtual bool operator==(const ai_history_baset &op) const = 0;
118 
121  virtual const locationt &current_location(void) const = 0;
122 
129  virtual bool should_widen(const ai_history_baset &other) const
130  {
131  return false;
132  }
133 
134  virtual void output(std::ostream &out) const
135  {
136  }
137  virtual jsont output_json(void) const;
138  virtual xmlt output_xml(void) const;
139 };
140 
145 {
146 protected:
147  // DATA_INVARIANT(current.is_dereferenceable(), "Must not be _::end()")
149 
150 public:
152  {
153  }
154 
156  : ai_history_baset(old), current(old.current)
157  {
158  }
159 
160  step_returnt step(locationt to, const trace_sett &others) const override
161  {
162  trace_ptrt next(new ahistoricalt(to));
163 
164  if(others.empty())
165  {
166  return std::make_pair(step_statust::NEW, next);
167  }
168  else
169  {
170  // Aggressively merge histories because they are indistinguishable
171  INVARIANT(others.size() == 1, "Only needs one history per location");
172 
173  const auto it = others.begin();
174  INVARIANT(
175  *(*(it)) == *next,
176  "The next location in history map must contain next history");
177 
178  return std::make_pair(step_statust::MERGED, *it);
179  }
180  }
181 
182  bool operator<(const ai_history_baset &op) const override
183  {
184  PRECONDITION(dynamic_cast<const ahistoricalt *>(&op) != nullptr);
185 
186  return this->current_location()->location_number <
187  op.current_location()->location_number;
188  }
189 
190  bool operator==(const ai_history_baset &op) const override
191  {
192  PRECONDITION(dynamic_cast<const ahistoricalt *>(&op) != nullptr);
193 
194  // It would be nice to:
195  // return this->current == op.current
196  // But they may point to different goto_programs,
197  // giving undefined behaviour in C++
198  // So (safe due to data invariant & uniqueness of location numbers) ...
199  return this->current_location()->location_number ==
200  op.current_location()->location_number;
201  }
202 
203  const locationt &current_location(void) const override
204  {
205  return current;
206  }
207 
208  // Use default widening
209  // without history there is no reason to say any location is better than
210  // another to widen.
211  bool should_widen(const ai_history_baset &other) const override
212  {
213  return ai_history_baset::should_widen(other);
214  }
215 
216  void output(std::ostream &out) const override
217  {
218  out << "ahistorical : location " << current_location()->location_number;
219  }
220 };
221 
226 {
227 protected:
228  class call_stack_entryt;
229  typedef std::shared_ptr<const call_stack_entryt> cse_ptrt;
231  {
232  public:
235 
237  {
238  }
239 
240  bool operator<(const call_stack_entryt &op) const;
241  bool operator==(const call_stack_entryt &op) const;
242  };
243 
245  // DATA_INVARIANT(current_stack != nullptr, "current_stack must exist");
246  // DATA_INVARIANT(current_stack->current.is_dereferenceable(),
247  // "Must not be _::end()")
248 
249  // At what point to merge with a previous call stack when handling recursion
250  // Setting to 0 disables completely
251  unsigned int recursion_limit;
252 
253  bool has_recursion_limit(void) const
254  {
255  return recursion_limit != 0;
256  }
257 
258  call_stack_historyt(cse_ptrt cur_stack, unsigned int rec_lim)
259  : ai_history_baset(cur_stack->current_location),
260  current_stack(cur_stack),
261  recursion_limit(rec_lim)
262  {
263  PRECONDITION(
264  cur_stack != nullptr); // A little late by now but worth documenting
265  }
266 
267 public:
269  : ai_history_baset(l),
270  current_stack(std::make_shared<call_stack_entryt>(l, nullptr)),
271  recursion_limit(0)
272  {
273  }
274 
275  call_stack_historyt(locationt l, unsigned int rec_lim)
276  : ai_history_baset(l),
277  current_stack(std::make_shared<call_stack_entryt>(l, nullptr)),
278  recursion_limit(rec_lim)
279  {
280  }
281 
283  : ai_history_baset(old),
286  {
287  }
288 
289  step_returnt step(locationt to, const trace_sett &others) const override;
290 
291  bool operator<(const ai_history_baset &op) const override;
292  bool operator==(const ai_history_baset &op) const override;
293 
294  const locationt &current_location(void) const override
295  {
296  return current_stack->current_location;
297  }
298 
299  // Use default widening
300  // Typically this would be used for loops, which are not tracked
301  // it would be possible to use this to improve the handling of recursion
302  bool should_widen(const ai_history_baset &other) const override
303  {
304  return ai_history_baset::should_widen(other);
305  }
306 
307  void output(std::ostream &out) const override;
308 };
309 
316 {
317 public:
320 
322  {
323  }
324 };
325 
327 template <typename traceT>
329 {
330 public:
332  {
333  ai_history_baset::trace_ptrt p(new traceT(l));
334  return p;
335  }
336 };
337 
338 // Allows passing a recursion limit
340 {
341 protected:
342  unsigned int recursion_limit;
343 
344 public:
345  explicit call_stack_history_factoryt(unsigned int rec_lim)
346  : recursion_limit(rec_lim)
347  {
348  }
349 
351  {
353  std::make_shared<call_stack_historyt>(l, recursion_limit));
354  return p;
355  }
356 
358  {
359  }
360 };
361 
362 #endif // CPROVER_ANALYSES_AI_HISTORY_H
call_stack_historyt::output
void output(std::ostream &out) const override
Definition: ai_history.cpp:158
call_stack_historyt::call_stack_entryt::call_stack_entryt
call_stack_entryt(locationt l, cse_ptrt p)
Definition: ai_history.h:236
ai_history_baset::operator==
virtual bool operator==(const ai_history_baset &op) const =0
History objects should be comparable.
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
ahistoricalt
The common case of history is to only care about where you are now, not how you got there!...
Definition: ai_history.h:145
ai_history_baset::current_location
virtual const locationt & current_location(void) const =0
The current location in the history, used to compute the transformer POSTCONDITION(return value is de...
ai_history_baset::step_statust::BLOCKED
@ BLOCKED
call_stack_history_factoryt::recursion_limit
unsigned int recursion_limit
Definition: ai_history.h:342
call_stack_historyt::call_stack_historyt
call_stack_historyt(locationt l, unsigned int rec_lim)
Definition: ai_history.h:275
ai_history_baset::~ai_history_baset
virtual ~ai_history_baset()
Definition: ai_history.h:58
ai_history_baset::compare_historyt
In a number of places we need to work with sets of histories so that these (a) make use of the immuta...
Definition: ai_history.h:73
goto_model.h
call_stack_historyt::call_stack_entryt::operator<
bool operator<(const call_stack_entryt &op) const
Definition: ai_history.cpp:172
ai_history_baset::step
virtual step_returnt step(locationt to, const trace_sett &others) const =0
Step creates a new history by advancing the current one to location "to" It is given the set of all o...
call_stack_historyt::should_widen
bool should_widen(const ai_history_baset &other) const override
Domains with a substantial height may need to widen when merging this method allows the history to pr...
Definition: ai_history.h:302
ai_history_factory_baset::epoch
virtual ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt)=0
Creates a new history from the given starting point.
ahistoricalt::operator==
bool operator==(const ai_history_baset &op) const override
History objects should be comparable.
Definition: ai_history.h:190
ahistoricalt::operator<
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
Definition: ai_history.h:182
call_stack_historyt::has_recursion_limit
bool has_recursion_limit(void) const
Definition: ai_history.h:253
jsont
Definition: json.h:25
xml.h
ai_history_baset::ai_history_baset
ai_history_baset(const ai_history_baset &)
Definition: ai_history.h:53
ai_history_baset::operator<
virtual bool operator<(const ai_history_baset &op) const =0
The order for history_sett.
ahistoricalt::ahistoricalt
ahistoricalt(locationt l)
Definition: ai_history.h:151
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
ahistoricalt::current
locationt current
Definition: ai_history.h:148
ai_history_baset::step_statust
step_statust
Definition: ai_history.h:82
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
call_stack_history_factoryt
Definition: ai_history.h:340
ai_history_baset::output_xml
virtual xmlt output_xml(void) const
Definition: ai_history.cpp:22
ahistoricalt::ahistoricalt
ahistoricalt(const ahistoricalt &old)
Definition: ai_history.h:155
ai_history_factory_default_constructort
An easy factory implementation for histories that don't need parameters.
Definition: ai_history.h:329
call_stack_historyt::call_stack_historyt
call_stack_historyt(const call_stack_historyt &old)
Definition: ai_history.h:282
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
call_stack_historyt::call_stack_entryt::current_location
locationt current_location
Definition: ai_history.h:233
call_stack_historyt::operator<
bool operator<(const ai_history_baset &op) const override
The order for history_sett.
Definition: ai_history.cpp:142
ahistoricalt::should_widen
bool should_widen(const ai_history_baset &other) const override
Domains with a substantial height may need to widen when merging this method allows the history to pr...
Definition: ai_history.h:211
ai_history_baset::output_json
virtual jsont output_json(void) const
Definition: ai_history.cpp:14
ahistoricalt::output
void output(std::ostream &out) const override
Definition: ai_history.h:216
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
ahistoricalt::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.h:160
ai_history_factory_baset::~ai_history_factory_baset
virtual ~ai_history_factory_baset()
Definition: ai_history.h:321
call_stack_historyt::recursion_limit
unsigned int recursion_limit
Definition: ai_history.h:251
call_stack_history_factoryt::~call_stack_history_factoryt
virtual ~call_stack_history_factoryt()
Definition: ai_history.h:357
call_stack_historyt::call_stack_historyt
call_stack_historyt(locationt l)
Definition: ai_history.h:268
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
ai_history_factory_default_constructort::epoch
ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt l) override
Creates a new history from the given starting point.
Definition: ai_history.h:331
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
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_factory_baset
As more detailed histories can get complex (for example, nested loops or deep, mutually recursive cal...
Definition: ai_history.h:316
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
json.h
ai_history_baset::compare_historyt::operator()
bool operator()(const trace_ptrt &l, const trace_ptrt &r) const
Definition: ai_history.h:74
ai_history_baset::step_returnt
std::pair< step_statust, trace_ptrt > step_returnt
Definition: ai_history.h:88
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
ahistoricalt::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:203
r
static int8_t r
Definition: irep_hash.h:59
ai_history_baset::should_widen
virtual bool should_widen(const ai_history_baset &other) const
Domains with a substantial height may need to widen when merging this method allows the history to pr...
Definition: ai_history.h:129
call_stack_history_factoryt::call_stack_history_factoryt
call_stack_history_factoryt(unsigned int rec_lim)
Definition: ai_history.h:345
call_stack_history_factoryt::epoch
ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt l) override
Creates a new history from the given starting point.
Definition: ai_history.h:350
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