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 <functional>
16 #include <memory>
17 
18 #include <analyses/guard.h>
19 
20 #include <util/invariant.h>
21 #include <util/nodiscard.h>
22 #include <util/ssa_expr.h>
23 #include <util/std_expr.h>
24 
25 #include "call_stack.h"
26 #include "field_sensitivity.h"
27 #include "goto_state.h"
28 #include "renaming_level.h"
29 #include "symex_target_equation.h"
30 
31 class incremental_dirtyt;
32 
41 class goto_symex_statet final : public goto_statet
42 {
43 public:
45  const symex_targett::sourcet &,
46  std::size_t max_field_sensitive_array_size,
47  guard_managert &manager,
48  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
50 
53  const goto_symex_statet &other,
54  symex_target_equationt *const target)
55  : goto_symex_statet(other) // NOLINT
56  {
57  symex_target = target;
58  }
59 
61 
66 
67  // Manager is required to be able to resize the thread vector
70 
72 
97  template <levelt level = L2>
99 
102  template <levelt level>
104  rename_ssa(ssa_exprt ssa, const namespacet &ns);
105 
106  template <levelt level = L2>
107  void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
108 
109  NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
110 
113  ssa_exprt lhs, // L0/L1
114  const exprt &rhs, // L2
115  const namespacet &ns,
116  bool rhs_is_simplified,
117  bool record_value,
118  bool allow_pointer_unsoundness = false);
119 
121 
122 protected:
123  template <levelt>
124  void rename_address(exprt &expr, const namespacet &ns);
125 
127  template <levelt level>
129  set_indices(ssa_exprt expr, const namespacet &ns);
130 
131  // this maps L1 names to (L2) types
132  typedef std::unordered_map<irep_idt, typet> l1_typest;
134 
135 public:
136  // guards
138  {
139  static irep_idt id = "goto_symex::\\guard";
140  return id;
141  }
142 
144  {
146  return threads[source.thread_nr].call_stack;
147  }
148 
149  const call_stackt &call_stack() const
150  {
152  return threads[source.thread_nr].call_stack;
153  }
154 
162  const symbol_exprt &expr,
163  std::function<std::size_t(const irep_idt &)> index_generator,
164  const namespacet &ns);
165 
170  ssa_exprt declare(ssa_exprt ssa, const namespacet &ns);
171 
172  void print_backtrace(std::ostream &) const;
173 
174  // threads
175  typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;
176  typedef std::list<guardt> a_s_w_entryt;
177  std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> read_in_atomic_section;
178  std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
180 
181  struct threadt
182  {
186  std::map<irep_idt, unsigned> function_frame;
187  unsigned atomic_section_id = 0;
190  {
191  }
192  };
193 
194  std::vector<threadt> threads;
195 
197  {
198  NOT_SHARED,
200  SHARED
201  };
202 
203  bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
204  bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
206  write_is_shared(const ssa_exprt &expr, const namespacet &ns) const;
207 
208  std::stack<bool> record_events;
209 
210  const incremental_dirtyt *dirty = nullptr;
211 
213 
216 
220 
223 
224  unsigned total_vccs = 0;
225  unsigned remaining_vccs = 0;
226 
228  void drop_existing_l1_name(const irep_idt &l1_identifier)
229  {
230  level2.current_names.erase(l1_identifier);
231  }
232 
234  void drop_l1_name(const irep_idt &l1_identifier)
235  {
236  level2.current_names.erase_if_exists(l1_identifier);
237  }
238 
239  std::function<std::size_t(const irep_idt &)> get_l2_name_provider() const
240  {
241  return fresh_l2_name_provider;
242  }
243 
245  static bool is_read_only_object(const exprt &lvalue)
246  {
247  // Note ID_constant can occur due to a partial write to a string constant,
248  // (i.e. something like byte_extract int from "hello" offset 2), which
249  // simplifies to a plain constant.
250  return lvalue.id() == ID_string_constant || lvalue.id() == ID_null_object ||
251  lvalue.id() == "zero_string" || lvalue.id() == "is_zero_string" ||
252  lvalue.id() == "zero_string_length" || lvalue.id() == ID_constant;
253  }
254 
255 private:
256  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
257 
268  goto_symex_statet(const goto_symex_statet &other) = default;
269 };
270 
271 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
Control granularity of object accesses.
instructionst::const_iterator const_targett
Definition: goto_program.h:593
Container for data that varies per program point, e.g.
Definition: goto_state.h:32
symex_level2t level2
Definition: goto_state.h:38
Central data structure: state.
ssa_exprt declare(ssa_exprt ssa, const namespacet &ns)
Add invalid (or a failed symbol) to the value_set if ssa is a pointer, ensure that level2 index of sy...
goto_programt::const_targett saved_target
ssa_exprt add_object(const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)
Instantiate the object expr.
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
std::stack< bool > record_events
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
goto_symex_statet(const goto_symex_statet &other, symex_target_equationt *const target)
Fake "copy constructor" that initializes the symex_target member.
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
static irep_idt guard_identifier()
call_stackt & call_stack()
const incremental_dirtyt * dirty
goto_symex_statet(const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
symex_level1t level1
void rename_address(exprt &expr, const namespacet &ns)
NODISCARD renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
guard_managert & guard_manager
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
const call_stackt & call_stack() const
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
symex_target_equationt * symex_target
std::unordered_map< irep_idt, typet > l1_typest
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
std::list< guardt > a_s_w_entryt
void drop_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
field_sensitivityt field_sensitivity
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
NODISCARD renamedt< ssa_exprt, level > set_indices(ssa_exprt expr, const namespacet &ns)
Update values up to level.
symex_targett::sourcet source
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
std::function< std::size_t(const irep_idt &)> get_l2_name_provider() const
goto_symex_statet(const goto_symex_statet &other)=default
Dangerous, do not use.
bool run_validation_checks
Should the additional validation checks be run?
std::vector< threadt > threads
std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
void drop_existing_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:119
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
void erase_if_exists(const key_type &k)
Erase element if it exists.
Definition: sharing_map.h:274
void erase(const key_type &k)
Erase element, element must exist in map.
Definition: sharing_map.h:1203
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table.
Definition: symbol_table.h:14
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
The Boolean constant true.
Definition: std_expr.h:2856
The type of an expression, extends irept.
Definition: type.h:29
goto_statet class definition
Guard Data Structure.
#define NODISCARD
Definition: nodiscard.h:22
Renaming levels.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
threadt(guard_managert &guard_manager)
std::map< irep_idt, unsigned > function_frame
goto_programt::const_targett pc
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
Functor to set the level 1 renaming of SSA expressions.
symex_renaming_levelt current_names
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
Generate Equation using Symbolic Execution.