cprover
path_symex_state.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: State of path-based symbolic simulator
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
13 #define CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
14 
15 #include <util/invariant.h>
16 
17 #include "locs.h"
18 #include "var_map.h"
19 #include "path_symex_history.h"
20 
22 {
23 public:
25  var_mapt &_var_map,
26  const locst &_locs,
27  path_symex_historyt &_path_symex_history):
28  var_map(_var_map),
29  locs(_locs),
30  inside_atomic_section(false),
31  history(_path_symex_history),
32  current_thread(0),
34  no_branches(0),
35  depth(0)
36  {
37  }
38 
40 
41  // These are tied to a particular var_map
42  // and a particular program.
44  const locst &locs;
45 
46  // the value of a variable
47  struct var_statet
48  {
49  // it's a given explicit value or a symbol with given identifier
52 
53  // for uninterpreted functions or arrays we maintain an index set
54  typedef std::set<exprt> index_sett;
56 
58  value(nil_exprt()),
60  {
61  }
62  };
63 
64  // the values of the shared variables
65  typedef std::vector<var_statet> var_valt;
67 
68  // save+restore procedure-local variables
69  typedef std::map<unsigned, var_statet> var_state_mapt;
70 
71  // procedure frame
72  struct framet
73  {
79  };
80 
81  // call stack
82  typedef std::vector<framet> call_stackt;
83 
84  // the state of a thread
85  struct threadt
86  {
87  public:
89  call_stackt call_stack; // the call stack
90  var_valt local_vars; // thread-local variables
91  bool active;
92 
93  threadt():active(true)
94  {
95  }
96  };
97 
98  typedef std::vector<threadt> threadst;
100 
101  // warning: reference is not stable
102  var_statet &get_var_state(const var_mapt::var_infot &var_info);
103 
105 
106  unsigned get_current_thread() const
107  {
108  return current_thread;
109  }
110 
111  void set_current_thread(unsigned _thread)
112  {
113  current_thread=_thread;
114  }
115 
117  {
118  return locs[pc()].target;
119  }
120 
121  bool is_executable() const
122  {
123  return !threads.empty() &&
124  threads[current_thread].active;
125  }
126 
127  // execution history
129 
130  // adds an entry to the history
131  void record_step();
132 
133  // various state transformers
134 
136  {
137  threads.resize(threads.size()+1);
138  return threads.back();
139  }
140 
142  {
143  threads[current_thread].active=false;
144  }
145 
146  loc_reft pc() const
147  {
149  return threads[current_thread].pc;
150  }
151 
152  void next_pc()
153  {
154  threads[current_thread].pc.increase();
155  }
156 
157  void set_pc(loc_reft new_pc)
158  {
159  threads[current_thread].pc=new_pc;
160  }
161 
162  // output
163  void output(std::ostream &out) const;
164  void output(const threadt &thread, std::ostream &out) const;
165 
166  // instantiate expressions with propagation
167  exprt read(const exprt &src)
168  {
169  return read(src, true);
170  }
171 
172  // instantiate without constant propagation
174  {
175  return read(src, false);
176  }
177 
178  exprt dereference_rec(const exprt &src, bool propagate);
179 
180  std::string array_index_as_string(const exprt &) const;
181 
183  {
185  }
186 
187  unsigned get_depth() const
188  {
189  return depth;
190  }
191 
192  unsigned get_no_branches() const
193  {
194  return no_branches;
195  }
196 
197  bool last_was_branch() const
198  {
199  return !history.is_nil() && history->is_branch();
200  }
201 
202  bool is_feasible(class decision_proceduret &) const;
203 
204  bool check_assertion(class decision_proceduret &);
205 
206  // counts how many times we have executed backwards edges
207  typedef std::map<loc_reft, unsigned> unwinding_mapt;
209 
210  // similar for recursive function calls
211  typedef std::map<irep_idt, unsigned> recursion_mapt;
213 
214 protected:
215  unsigned current_thread;
217  unsigned no_branches;
218  unsigned depth;
219 
220  exprt read(
221  const exprt &src,
222  bool propagate);
223 
225  const exprt &src,
226  bool propagate);
227 
229  exprt array_theory(const exprt &src, bool propagate);
230 
232  const exprt &src,
233  bool propagate);
234 
236  const exprt &src,
237  bool propagate);
238 
239  bool is_symbol_member_index(const exprt &src) const;
240 };
241 
243  var_mapt &var_map,
244  const locst &locs,
246 
247 #endif // CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
History for path-based symbolic simulator.
var_state_mapt saved_local_vars
exprt instantiate_rec(const exprt &src, bool propagate)
std::map< loc_reft, unsigned > unwinding_mapt
exprt read_no_propagate(const exprt &src)
exprt instantiate_rec_address(const exprt &src, bool propagate)
unwinding_mapt unwinding_map
path_symex_stept stept
exprt array_theory(const exprt &src, bool propagate)
bool last_was_branch() const
std::string array_index_as_string(const exprt &) const
unsigned no_thread_interleavings
instructionst::const_iterator const_targett
const locst & locs
bool is_branch() const
exprt read(const exprt &src)
The NIL expression.
Definition: std_expr.h:3764
threadt & add_thread()
std::map< unsigned, var_statet > var_state_mapt
std::vector< var_statet > var_valt
path_symex_statet(var_mapt &_var_map, const locst &_locs, path_symex_historyt &_path_symex_history)
#define PRECONDITION(CONDITION)
Definition: invariant.h:225
bool is_feasible(class decision_proceduret &) const
var_statet & get_var_state(const var_mapt::var_infot &var_info)
unsigned get_current_thread() const
unsigned get_no_thread_interleavings() const
exprt dereference_rec(const exprt &src, bool propagate)
Variable Numbering.
exprt read_symbol_member_index(const exprt &src, bool propagate)
exprt expand_structs_and_arrays(const exprt &src)
std::map< irep_idt, unsigned > recursion_mapt
bool check_assertion(class decision_proceduret &)
recursion_mapt recursion_map
goto_programt::const_targett get_instruction() const
std::vector< framet > call_stackt
Definition: locs.h:39
Base class for all expressions.
Definition: expr.h:46
bool is_executable() const
void set_pc(loc_reft new_pc)
unsigned get_no_branches() const
CFG made of Program Locations, built from goto_functionst.
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool is_symbol_member_index(const exprt &src) const
void set_current_thread(unsigned _thread)
loc_reft pc() const
path_symex_step_reft history
std::vector< threadt > threadst
void output(std::ostream &out) const
path_symex_statet initial_state(var_mapt &var_map, const locst &locs, path_symex_historyt &)
unsigned get_depth() const