cprover
goto_symex_state.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
14 
15 #include <cassert>
16 #include <unordered_set>
17 
18 #include <util/guard.h>
19 #include <util/std_expr.h>
20 #include <util/ssa_expr.h>
21 
24 
25 #include "symex_target.h"
26 
27 class dirtyt;
28 
29 // central data structure: state
31 {
32 public:
34 
35  // distance from entry
36  unsigned depth;
37 
41 
42  void initialize(const goto_functionst &goto_functions);
43 
44  // we have a two-level renaming
45 
46  typedef std::map<irep_idt, irep_idt> original_identifierst;
47 
48  // we remember all L1 renamings
49  typedef std::set<irep_idt> l1_historyt;
50  l1_historyt l1_history;
51 
53  {
54  virtual ~renaming_levelt() { }
55 
56  typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned> > current_namest;
57  current_namest current_names;
58 
59  unsigned current_count(const irep_idt &identifier) const
60  {
61  current_namest::const_iterator it=
62  current_names.find(identifier);
63  return it==current_names.end()?0:it->second.second;
64  }
65 
66  void increase_counter(const irep_idt &identifier)
67  {
68  assert(current_names.find(identifier)!=current_names.end());
69  ++current_names[identifier].second;
70  }
71 
72  void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars) const
73  {
74  for(current_namest::const_iterator it=current_names.begin();
75  it!=current_names.end();
76  it++)
77  vars.insert(it->second.first);
78  }
79  };
80 
81  // level 0 -- threads!
82  // renaming built for one particular interleaving
83  struct level0t:public renaming_levelt
84  {
85  void operator()(
86  ssa_exprt &ssa_expr,
87  const namespacet &ns,
88  unsigned thread_nr);
89 
90  level0t() { }
91  virtual ~level0t() { }
92  } level0;
93 
94  // level 1 -- function frames
95  // this is to preserve locality in case of recursion
96 
97  struct level1t:public renaming_levelt
98  {
99  void operator()(ssa_exprt &ssa_expr);
100 
101  void restore_from(const current_namest &other)
102  {
103  current_namest::iterator it=current_names.begin();
104  for(current_namest::const_iterator
105  ito=other.begin();
106  ito!=other.end();
107  ++ito)
108  {
109  while(it!=current_names.end() && it->first<ito->first)
110  ++it;
111  if(it==current_names.end() || ito->first<it->first)
112  current_names.insert(it, *ito);
113  else if(it!=current_names.end())
114  {
115  assert(it->first==ito->first);
116  it->second=ito->second;
117  ++it;
118  }
119  }
120  }
121 
122  level1t() { }
123  virtual ~level1t() { }
124  } level1;
125 
126  // level 2 -- SSA
127 
128  struct level2t:public renaming_levelt
129  {
130  level2t() { }
131  virtual ~level2t() { }
132  } level2;
133 
134  // this maps L1 names to (L2) constants
136  {
137  public:
138  typedef std::map<irep_idt, exprt> valuest;
139  valuest values;
140  void operator()(exprt &expr);
141 
142  void remove(const irep_idt &identifier)
143  {
144  values.erase(identifier);
145  }
146  } propagation;
147 
148  enum levelt { L0=0, L1=1, L2=2 };
149 
150  // performs renaming _up to_ the given level
151  void rename(exprt &expr, const namespacet &ns, levelt level=L2);
152  void rename(
153  typet &type,
154  const irep_idt &l1_identifier,
155  const namespacet &ns,
156  levelt level=L2);
157 
158  void assignment(
159  ssa_exprt &lhs, // L0/L1
160  const exprt &rhs, // L2
161  const namespacet &ns,
162  bool rhs_is_simplified,
163  bool record_value);
164 
165  // what to propagate
166  bool constant_propagation(const exprt &expr) const;
167  bool constant_propagation_reference(const exprt &expr) const;
168 
169  // undoes all levels of renaming
170  void get_original_name(exprt &expr) const;
171  void get_original_name(typet &type) const;
172 protected:
173  void rename_address(exprt &expr, const namespacet &ns, levelt level);
174 
175  void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2);
176  // only required for value_set.assign
177  void get_l1_name(exprt &expr) const;
178 
179  // this maps L1 names to (L2) types
180  typedef std::unordered_map<irep_idt, typet, irep_id_hash> l1_typest;
181  l1_typest l1_types;
182 
183 public:
184  // uses level 1 names, and is used to
185  // do dereferencing
187 
189  {
190  public:
191  unsigned depth;
198 
199  explicit goto_statet(const goto_symex_statet &s):
200  depth(s.depth),
201  level2_current_names(s.level2.current_names),
202  value_set(s.value_set),
203  guard(s.guard),
204  source(s.source),
205  propagation(s.propagation),
206  atomic_section_id(s.atomic_section_id)
207  {
208  }
209 
210  // the below replicate levelt2 member functions
212  std::unordered_set<ssa_exprt, irep_hash> &vars) const
213  {
214  for(level2t::current_namest::const_iterator
215  it=level2_current_names.begin();
216  it!=level2_current_names.end();
217  it++)
218  vars.insert(it->second.first);
219  }
220 
221  unsigned level2_current_count(const irep_idt &identifier) const
222  {
223  level2t::current_namest::const_iterator it=
224  level2_current_names.find(identifier);
225  return it==level2_current_names.end()?0:it->second.second;
226  }
227  };
228 
229  // gotos
230  typedef std::list<goto_statet> goto_state_listt;
231  typedef std::map<goto_programt::const_targett, goto_state_listt>
233 
234  // stack frames -- these are used for function calls and
235  // for exceptions
236  class framet
237  {
238  public:
239  // function calls
243 
247 
249 
250  typedef std::set<irep_idt> local_objectst;
251  local_objectst local_objects;
252 
254  return_value(nil_exprt()),
255  hidden_function(false)
256  {
257  }
258 
259  // exceptions
260  typedef std::map<irep_idt, goto_programt::targett> catch_mapt;
261  catch_mapt catch_map;
262 
263  // loop and recursion unwinding
264  struct loop_infot
265  {
267  count(0),
268  is_recursion(false)
269  {
270  }
271 
272  unsigned count;
274  };
275  typedef std::unordered_map<irep_idt, loop_infot, irep_id_hash>
278  };
279 
280  typedef std::vector<framet> call_stackt;
281 
282  call_stackt &call_stack()
283  {
284  assert(source.thread_nr<threads.size());
285  return threads[source.thread_nr].call_stack;
286  }
287 
288  const call_stackt &call_stack() const
289  {
290  assert(source.thread_nr<threads.size());
291  return threads[source.thread_nr].call_stack;
292  }
293 
295  {
296  assert(!call_stack().empty());
297  return call_stack().back();
298  }
299 
300  const framet &top() const
301  {
302  assert(!call_stack().empty());
303  return call_stack().back();
304  }
305 
306  framet &new_frame() { call_stack().push_back(framet()); return top(); }
307  void pop_frame() { call_stack().pop_back(); }
308  const framet &previous_frame() { return *(--(--call_stack().end())); }
309 
310  // threads
312  typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;
313  typedef std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash>
315  typedef std::list<guardt> a_s_w_entryt;
316  typedef std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
320 
321  class threadt
322  {
323  public:
326  call_stackt call_stack;
327  std::map<irep_idt, unsigned> function_frame;
329 
331  atomic_section_id(0)
332  {
333  }
334  };
335 
336  typedef std::vector<threadt> threadst;
337  threadst threads;
338 
339  bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
340  bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
341 
342  void switch_to_thread(unsigned t);
344  const dirtyt * dirty;
345 };
346 
347 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
The type of an expression.
Definition: type.h:20
std::map< irep_idt, irep_idt > original_identifierst
goto_statet(const goto_symex_statet &s)
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
void level2_get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
class goto_symex_statet::propagationt propagation
level2t::current_namest level2_current_names
read_in_atomic_sectiont read_in_atomic_section
renaming_levelt::current_namest old_level1
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Goto Programs with Functions.
Generate Equation using Symbolic Execution.
goto_symex_statet::level0t level0
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
void increase_counter(const irep_idt &identifier)
void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2)
symex_targett * symex_target
Value Set.
written_in_atomic_sectiont written_in_atomic_section
Definition: guard.h:19
loop_iterationst loop_iterations
void get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
void switch_to_thread(unsigned t)
void restore_from(const current_namest &other)
void get_original_name(exprt &expr) const
std::set< irep_idt > l1_historyt
unsigned level2_current_count(const irep_idt &identifier) const
bool constant_propagation(const exprt &expr) const
This function determines what expressions are to be propagated as "constants".
goto_symex_statet::level2t level2
void initialize(const goto_functionst &goto_functions)
std::map< irep_idt, exprt > valuest
bool constant_propagation_reference(const exprt &expr) const
this function determines which reference-typed expressions are constant
instructionst::const_iterator const_targett
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_sectiont
The NIL expression.
Definition: std_expr.h:3764
std::set< irep_idt > local_objectst
const framet & top() const
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::map< irep_idt, goto_programt::targett > catch_mapt
std::map< irep_idt, unsigned > function_frame
goto_symex_statet::level1t level1
Guard Data Structure.
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
goto_state_mapt goto_state_map
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
const framet & previous_frame()
std::list< guardt > a_s_w_entryt
const dirtyt * dirty
std::vector< framet > call_stackt
void get_l1_name(exprt &expr) const
unsigned current_count(const irep_idt &identifier) const
Base class for all expressions.
Definition: expr.h:46
l1_historyt l1_history
std::unordered_map< irep_idt, typet, irep_id_hash > l1_typest
call_stackt & call_stack()
Definition: dirty.h:22
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value)
std::map< goto_programt::const_targett, goto_state_listt > goto_state_mapt
const call_stackt & call_stack() const
symex_targett::sourcet calling_location
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_sectiont
goto_programt::const_targett pc
std::list< goto_statet > goto_state_listt
std::unordered_map< irep_idt, loop_infot, irep_id_hash > loop_iterationst
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
symex_targett::sourcet source
std::vector< threadt > threadst
goto_programt::const_targett end_of_function
void rename_address(exprt &expr, const namespacet &ns, levelt level)
symex_targett::sourcet source