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>
20 
21 #include <util/invariant.h>
22 #include <util/guard.h>
23 #include <util/std_expr.h>
24 #include <util/ssa_expr.h>
25 #include <util/make_unique.h>
26 
29 
30 #include "renaming_level.h"
31 #include "symex_target_equation.h"
32 
33 // central data structure: state
34 class goto_symex_statet final
35 {
36 public:
39 
42  const goto_symex_statet &other,
43  symex_target_equationt *const target)
44  : goto_symex_statet(other) // NOLINT
45  {
46  symex_target = target;
47  }
48 
53 
55  unsigned depth;
56 
60 
61  // we remember all L1 renamings
62  std::set<irep_idt> l1_history;
63 
67 
68  // Map L1 names to (L2) constants
69  std::map<irep_idt, exprt> propagation;
70  void output_propagation_map(std::ostream &);
71 
72  enum levelt { L0=0, L1=1, L2=2 };
73 
74  // performs renaming _up to_ the given level
75  void rename(exprt &expr, const namespacet &ns, levelt level=L2);
76  void rename(
77  typet &type,
78  const irep_idt &l1_identifier,
79  const namespacet &ns,
80  levelt level=L2);
81 
82  void assignment(
83  ssa_exprt &lhs, // L0/L1
84  const exprt &rhs, // L2
85  const namespacet &ns,
86  bool rhs_is_simplified,
87  bool record_value,
88  bool allow_pointer_unsoundness=false);
89 
90  // undoes all levels of renaming
91  void get_original_name(exprt &expr) const;
92  void get_original_name(typet &type) const;
93 protected:
94  void rename_address(exprt &expr, const namespacet &ns, levelt level);
95 
96  void set_l0_indices(ssa_exprt &expr, const namespacet &ns);
97  void set_l1_indices(ssa_exprt &expr, const namespacet &ns);
98  void set_l2_indices(ssa_exprt &expr, const namespacet &ns);
99 
100  // this maps L1 names to (L2) types
101  typedef std::unordered_map<irep_idt, typet> l1_typest;
103 
104 public:
105  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
106 
107  // uses level 1 names, and is used to
108  // do dereferencing
110 
112  {
113  public:
114  unsigned depth;
119  std::map<irep_idt, exprt> propagation;
121  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
123 
124  explicit goto_statet(const goto_symex_statet &s)
125  : depth(s.depth),
126  level2_current_names(s.level2.current_names),
127  value_set(s.value_set),
128  guard(s.guard),
129  source(s.source),
135  {
136  }
137 
138  // the below replicate levelt2 member functions
140  std::unordered_set<ssa_exprt, irep_hash> &vars) const
141  {
142  for(const auto &pair : level2_current_names)
143  vars.insert(pair.second.first);
144  }
145 
146  unsigned level2_current_count(const irep_idt &identifier) const
147  {
148  const auto it = level2_current_names.find(identifier);
149  return it==level2_current_names.end()?0:it->second.second;
150  }
151  };
152 
153  explicit goto_symex_statet(const goto_statet &s)
154  : depth(s.depth),
155  guard(s.guard),
156  source(s.source),
159  value_set(s.value_set),
163  {
165  }
166 
167  // gotos
168  typedef std::list<goto_statet> goto_state_listt;
169  typedef std::map<goto_programt::const_targett, goto_state_listt>
171 
172  // stack frames -- these are used for function calls and
173  // for exceptions
174  struct framet
175  {
176  // function calls
180 
183  bool hidden_function = false;
184 
186 
187  std::set<irep_idt> local_objects;
188 
189  // exceptions
190  std::map<irep_idt, goto_programt::targett> catch_map;
191 
192  // loop and recursion unwinding
193  struct loop_infot
194  {
195  unsigned count = 0;
196  bool is_recursion = false;
197  };
198  std::unordered_map<irep_idt, loop_infot> loop_iterations;
199  };
200 
201  typedef std::vector<framet> call_stackt;
202 
204  {
206  return threads[source.thread_nr].call_stack;
207  }
208 
209  const call_stackt &call_stack() const
210  {
212  return threads[source.thread_nr].call_stack;
213  }
214 
216  {
217  PRECONDITION(!call_stack().empty());
218  return call_stack().back();
219  }
220 
221  const framet &top() const
222  {
223  PRECONDITION(!call_stack().empty());
224  return call_stack().back();
225  }
226 
227  framet &new_frame() { call_stack().push_back(framet()); return top(); }
228  void pop_frame() { call_stack().pop_back(); }
229  const framet &previous_frame() { return *(--(--call_stack().end())); }
230 
231  void print_backtrace(std::ostream &) const;
232 
233  // threads
235  typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;
236  typedef std::list<guardt> a_s_w_entryt;
237  std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> read_in_atomic_section;
238  std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
240 
242 
243  struct threadt
244  {
248  std::map<irep_idt, unsigned> function_frame;
249  unsigned atomic_section_id = 0;
250  };
251 
252  std::vector<threadt> threads;
253 
254  bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
255  bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
256 
259 
261 
264 
268 
271 
272 private:
283  goto_symex_statet(const goto_symex_statet &other) = default;
284 };
285 
286 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
The type of an expression, extends irept.
Definition: type.h:27
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)
std::map< irep_idt, unsigned > function_frame
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
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
Variables whose address is taken.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
bool run_validation_checks
Should the additional validation checks be run?
std::map< irep_idt, exprt > propagation
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
symex_target_equationt * symex_target
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Value Set.
goto_state_mapt goto_state_map
Definition: guard.h:19
void set_l1_indices(ssa_exprt &expr, const namespacet &ns)
goto_programt::const_targett end_of_function
std::map< irep_idt, exprt > propagation
void get_original_name(exprt &expr) const
unsigned level2_current_count(const irep_idt &identifier) const
unsigned depth
distance from entry
goto_programt::const_targett pc
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:115
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
std::set< irep_idt > l1_history
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
void set_l0_indices(ssa_exprt &expr, const namespacet &ns)
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
The NIL expression.
Definition: std_expr.h:4461
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
symex_targett::sourcet calling_location
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:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
std::vector< threadt > threads
Guard Data Structure.
Functor to set the level 2 renaming of SSA expressions.
incremental_dirtyt dirty
current_namest current_names
std::unordered_map< irep_idt, loop_infot > loop_iterations
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:41
std::set< irep_idt > local_objects
symex_level1t level1
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
void set_l2_indices(ssa_exprt &expr, const namespacet &ns)
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
const framet & previous_frame()
symex_level0t level0
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
symex_level2t level2
std::unordered_map< irep_idt, typet > l1_typest
std::vector< framet > call_stackt
std::map< irep_idt, goto_programt::targett > catch_map
symex_level2t::current_namest level2_current_names
Goto Function.
goto_programt::const_targett saved_target
Base class for all expressions.
Definition: expr.h:54
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
Map identifier to ssa_exprt and counter.
call_stackt & call_stack()
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
void output_propagation_map(std::ostream &)
Print the constant propagation map in a human-friendly format.
Local safe pointer analysis.
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.
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
const call_stackt & call_stack() const
symex_renaming_levelt::current_namest old_level1
Functor to set the level 0 renaming of SSA expressions.
std::list< goto_statet > goto_state_listt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
symex_targett::sourcet source
Functor to set the level 1 renaming of SSA expressions.
void rename_address(exprt &expr, const namespacet &ns, levelt level)
symex_targett::sourcet source
Renaming levels.