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 <memory>
16 #include <unordered_set>
17 
18 #include <analyses/dirty.h>
19 
20 #include <util/invariant.h>
21 #include <util/guard.h>
22 #include <util/std_expr.h>
23 #include <util/ssa_expr.h>
24 #include <util/make_unique.h>
25 
28 
29 #include "symex_target_equation.h"
30 
31 // central data structure: state
32 class goto_symex_statet final
33 {
34 public:
37 
40  const goto_symex_statet &other,
41  symex_target_equationt *const target)
42  : goto_symex_statet(other) // NOLINT
43  {
44  symex_target = target;
45  }
46 
51 
53  unsigned depth;
54 
58 
59  // we have a two-level renaming
60 
61  typedef std::map<irep_idt, irep_idt> original_identifierst;
62 
63  // we remember all L1 renamings
64  typedef std::set<irep_idt> l1_historyt;
66 
68  {
69  virtual ~renaming_levelt() { }
70 
71  typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned> > current_namest;
73 
74  unsigned current_count(const irep_idt &identifier) const
75  {
76  current_namest::const_iterator it=
77  current_names.find(identifier);
78  return it==current_names.end()?0:it->second.second;
79  }
80 
81  void increase_counter(const irep_idt &identifier)
82  {
83  PRECONDITION(current_names.find(identifier) != current_names.end());
84  ++current_names[identifier].second;
85  }
86 
87  void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars) const
88  {
89  for(current_namest::const_iterator it=current_names.begin();
90  it!=current_names.end();
91  it++)
92  vars.insert(it->second.first);
93  }
94  };
95 
96  // level 0 -- threads!
97  // renaming built for one particular interleaving
98  struct level0t:public renaming_levelt
99  {
100  void operator()(
101  ssa_exprt &ssa_expr,
102  const namespacet &ns,
103  unsigned thread_nr);
104 
105  level0t() { }
106  virtual ~level0t() { }
107  } level0;
108 
109  // level 1 -- function frames
110  // this is to preserve locality in case of recursion
111 
112  struct level1t:public renaming_levelt
113  {
114  void operator()(ssa_exprt &ssa_expr);
115 
116  void restore_from(const current_namest &other)
117  {
118  current_namest::iterator it=current_names.begin();
119  for(current_namest::const_iterator
120  ito=other.begin();
121  ito!=other.end();
122  ++ito)
123  {
124  while(it!=current_names.end() && it->first<ito->first)
125  ++it;
126  if(it==current_names.end() || ito->first<it->first)
127  current_names.insert(it, *ito);
128  else if(it!=current_names.end())
129  {
130  PRECONDITION(it->first == ito->first);
131  it->second=ito->second;
132  ++it;
133  }
134  }
135  }
136 
137  level1t() { }
138  virtual ~level1t() { }
139  } level1;
140 
141  // level 2 -- SSA
142 
143  struct level2t:public renaming_levelt
144  {
145  level2t() { }
146  virtual ~level2t() { }
147  } level2;
148 
149  // this maps L1 names to (L2) constants
151  {
152  public:
153  typedef std::map<irep_idt, exprt> valuest;
155  void operator()(exprt &expr);
156 
157  void remove(const irep_idt &identifier)
158  {
159  values.erase(identifier);
160  }
161  } propagation;
162 
163  enum levelt { L0=0, L1=1, L2=2 };
164 
165  // performs renaming _up to_ the given level
166  void rename(exprt &expr, const namespacet &ns, levelt level=L2);
167  void rename(
168  typet &type,
169  const irep_idt &l1_identifier,
170  const namespacet &ns,
171  levelt level=L2);
172 
173  void assignment(
174  ssa_exprt &lhs, // L0/L1
175  const exprt &rhs, // L2
176  const namespacet &ns,
177  bool rhs_is_simplified,
178  bool record_value,
179  bool allow_pointer_unsoundness=false);
180 
181  // what to propagate
182  bool constant_propagation(const exprt &expr) const;
183  bool constant_propagation_reference(const exprt &expr) const;
184 
185  // undoes all levels of renaming
186  void get_original_name(exprt &expr) const;
187  void get_original_name(typet &type) const;
188 protected:
189  void rename_address(exprt &expr, const namespacet &ns, levelt level);
190 
191  void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2);
192  // only required for value_set.assign
193  void get_l1_name(exprt &expr) const;
194 
195  // this maps L1 names to (L2) types
196  typedef std::unordered_map<irep_idt, typet> l1_typest;
198 
199 public:
200  // uses level 1 names, and is used to
201  // do dereferencing
203 
205  {
206  public:
207  unsigned depth;
214 
215  explicit goto_statet(const goto_symex_statet &s):
216  depth(s.depth),
217  level2_current_names(s.level2.current_names),
218  value_set(s.value_set),
219  guard(s.guard),
220  source(s.source),
223  {
224  }
225 
226  // the below replicate levelt2 member functions
228  std::unordered_set<ssa_exprt, irep_hash> &vars) const
229  {
230  for(level2t::current_namest::const_iterator
231  it=level2_current_names.begin();
232  it!=level2_current_names.end();
233  it++)
234  vars.insert(it->second.first);
235  }
236 
237  unsigned level2_current_count(const irep_idt &identifier) const
238  {
239  level2t::current_namest::const_iterator it=
240  level2_current_names.find(identifier);
241  return it==level2_current_names.end()?0:it->second.second;
242  }
243  };
244 
245  explicit goto_symex_statet(const goto_statet &s)
246  : depth(s.depth),
247  guard(s.guard),
248  source(s.source),
250  value_set(s.value_set),
252  {
254  }
255 
256  // gotos
257  typedef std::list<goto_statet> goto_state_listt;
258  typedef std::map<goto_programt::const_targett, goto_state_listt>
260 
261  // stack frames -- these are used for function calls and
262  // for exceptions
263  class framet
264  {
265  public:
266  // function calls
270 
274 
276 
277  typedef std::set<irep_idt> local_objectst;
279 
282  hidden_function(false)
283  {
284  }
285 
286  // exceptions
287  typedef std::map<irep_idt, goto_programt::targett> catch_mapt;
289 
290  // loop and recursion unwinding
291  struct loop_infot
292  {
294  count(0),
295  is_recursion(false)
296  {
297  }
298 
299  unsigned count;
301  };
302  typedef std::unordered_map<irep_idt, loop_infot> loop_iterationst;
304  };
305 
306  typedef std::vector<framet> call_stackt;
307 
309  {
311  return threads[source.thread_nr].call_stack;
312  }
313 
314  const call_stackt &call_stack() const
315  {
317  return threads[source.thread_nr].call_stack;
318  }
319 
321  {
322  PRECONDITION(!call_stack().empty());
323  return call_stack().back();
324  }
325 
326  const framet &top() const
327  {
328  PRECONDITION(!call_stack().empty());
329  return call_stack().back();
330  }
331 
332  framet &new_frame() { call_stack().push_back(framet()); return top(); }
333  void pop_frame() { call_stack().pop_back(); }
334  const framet &previous_frame() { return *(--(--call_stack().end())); }
335 
336  // threads
338  typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;
339  typedef std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash>
341  typedef std::list<guardt> a_s_w_entryt;
342  typedef std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
346 
347  class threadt
348  {
349  public:
353  std::map<irep_idt, unsigned> function_frame;
355 
358  {
359  }
360  };
361 
362  typedef std::vector<threadt> threadst;
364 
365  bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
366  bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
367 
369  const irep_idt &id, const goto_functiont &);
370 
371  void switch_to_thread(unsigned t);
374 
376 
379 
384 
385 private:
396  goto_symex_statet(const goto_symex_statet &other) = default;
397 };
398 
399 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
The type of an expression.
Definition: type.h:22
std::map< irep_idt, irep_idt > original_identifierst
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
goto_statet(const goto_symex_statet &s)
Generate Equation using Symbolic Execution.
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
Variables whose address is taken.
renaming_levelt::current_namest old_level1
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
goto_symex_statet::level0t level0
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
symex_target_equationt * symex_target
void increase_counter(const irep_idt &identifier)
void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2)
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".
unsigned depth
distance from entry
goto_symex_statet::level2t level2
std::map< irep_idt, exprt > valuest
bool constant_propagation_reference(const exprt &expr) const
this function determines which reference-typed expressions are constant
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:115
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_sectiont
void populate_dirty_for_function(const irep_idt &id, const goto_functiont &)
The NIL expression.
Definition: std_expr.h:4510
std::set< irep_idt > local_objectst
const framet & top() const
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::map< irep_idt, goto_programt::targett > catch_mapt
std::map< irep_idt, unsigned > function_frame
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
goto_symex_statet::level1t level1
Guard Data Structure.
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
incremental_dirtyt dirty
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:41
goto_state_mapt goto_state_map
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
const framet & previous_frame()
goto_symex_statet(const goto_symex_statet &other, symex_target_equationt *const target)
Fake "copy constructor" that initializes the symex_target member.
std::list< guardt > a_s_w_entryt
std::unordered_map< irep_idt, loop_infot > loop_iterationst
std::unordered_map< irep_idt, typet > l1_typest
std::vector< framet > call_stackt
void get_l1_name(exprt &expr) const
void operator()(ssa_exprt &ssa_expr)
unsigned current_count(const irep_idt &identifier) const
goto_programt::const_targett saved_target
Base class for all expressions.
Definition: expr.h:42
l1_historyt l1_history
call_stackt & call_stack()
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
std::map< goto_programt::const_targett, goto_state_listt > goto_state_mapt
goto_symex_statet(const goto_statet &s)
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
const call_stackt & call_stack() const
symex_targett::sourcet calling_location
void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
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
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