cprover
path_symex_history.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: History for path-based symbolic simulator
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H
13 #define CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H
14 
15 #include <cassert>
16 #include <limits>
17 
18 #include <util/base_exceptions.h>
19 #include <util/std_expr.h>
20 
21 #include "loc_ref.h"
22 
23 class path_symex_stept;
24 
25 // This is a reference to a path_symex_stept,
26 // and is really cheap to copy. These references are stable,
27 // even though the underlying vector is not.
29 {
30 public:
32  class path_symex_historyt &_history):
33  index(std::numeric_limits<std::size_t>::max()),
34  history(&_history)
35  {
36  }
37 
39  index(std::numeric_limits<std::size_t>::max()), history(nullptr)
40  {
41  }
42 
43  bool is_nil() const
44  {
45  return index==std::numeric_limits<std::size_t>::max();
46  }
47 
49  {
51  history!=nullptr, nullptr_exceptiont, "history is null");
52  return *history;
53  }
54 
55  // pre-decrement
57 
58  path_symex_stept &operator*() const { return get(); }
59  path_symex_stept *operator->() const { return &get(); }
60 
61  void generate_successor();
62 
63  // build a forward-traversable version of the history
64  void build_history(std::vector<path_symex_step_reft> &dest) const;
65 
66 protected:
67  // we use a vector to store all steps
68  std::size_t index;
70 
71  path_symex_stept &get() const;
72 };
73 
75 
76 // the actual history node
78 {
79 public:
80  enum kindt
81  {
83  } branch;
84 
85  bool is_branch_taken() const
86  {
87  return branch==BRANCH_TAKEN;
88  }
89 
90  bool is_branch_not_taken() const
91  {
92  return branch==BRANCH_NOT_TAKEN;
93  }
94 
95  bool is_branch() const
96  {
98  }
99 
101 
102  // the thread that did the step
103  unsigned thread_nr;
104 
105  // the instruction that was executed
107 
111 
112  bool hidden;
113 
116  guard(nil_exprt()),
117  ssa_rhs(nil_exprt()),
118  full_lhs(nil_exprt()),
119  hidden(false)
120  {
121  }
122 
123  // interface to solvers; this converts a single step
124  void convert(decision_proceduret &dest) const;
125 
126  void output(std::ostream &) const;
127 };
128 
129 // converts the full history
131  decision_proceduret &dest,
133 {
134  while(!src.is_nil())
135  {
136  src->convert(dest);
137  --src;
138  }
139 
140  return dest;
141 }
142 
143 // this stores the forest of histories
145 {
146 public:
147  typedef std::vector<path_symex_stept> step_containert;
149 
150  // TODO: consider typedefing path_symex_historyt
151  void clear()
152  {
153  step_container.clear();
154  }
155 };
156 
158 {
160  history!=nullptr, nullptr_exceptiont, "history is null");
161  path_symex_step_reft old=*this;
162  index=history->step_container.size();
164  history->step_container.back().predecessor=old;
165 }
166 
168 {
169  *this=get().predecessor;
170  return *this;
171 }
172 
174 {
176  history!=nullptr, nullptr_exceptiont, "history is null");
177  assert(!is_nil());
178  return history->step_container[index];
179 }
180 
181 #endif // CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:209
decision_proceduret & operator<<(decision_proceduret &dest, path_symex_step_reft src)
void build_history(std::vector< path_symex_step_reft > &dest) const
path_symex_step_reft & operator--()
path_symex_stept & get() const
void convert(decision_proceduret &dest) const
STL namespace.
path_symex_historyt & get_history() const
enum path_symex_stept::kindt branch
path_symex_step_reft(class path_symex_historyt &_history)
bool is_branch() const
The NIL expression.
Definition: std_expr.h:3764
path_symex_step_reft predecessor
API to expression classes.
std::vector< path_symex_stept > step_containert
step_containert step_container
class path_symex_historyt * history
Base class for all expressions.
Definition: expr.h:46
path_symex_stept & operator*() const
bool is_branch_not_taken() const
path_symex_stept * operator->() const
void output(std::ostream &) const
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool is_branch_taken() const
Generic exception types primarily designed for use with invariants.
Program Locations.