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 #include <unordered_set>
18 
19 #include <analyses/guard.h>
20 
22 #include <util/invariant.h>
23 #include <util/make_unique.h>
24 #include <util/nodiscard.h>
25 #include <util/ssa_expr.h>
26 #include <util/std_expr.h>
27 
28 #include "call_stack.h"
29 #include "field_sensitivity.h"
30 #include "frame.h"
31 #include "goto_state.h"
32 #include "renaming_level.h"
33 #include "symex_target_equation.h"
34 
35 class incremental_dirtyt;
36 
45 class goto_symex_statet final : public goto_statet
46 {
47 public:
49  const symex_targett::sourcet &,
50  std::size_t max_field_sensitive_array_size,
51  guard_managert &manager,
52  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
54 
57  const goto_symex_statet &other,
58  symex_target_equationt *const target)
59  : goto_symex_statet(other) // NOLINT
60  {
61  symex_target = target;
62  }
63 
65 
70 
71  // Manager is required to be able to resize the thread vector
74 
76 
101  template <levelt level = L2>
103 
106  template <levelt level>
108  rename_ssa(ssa_exprt ssa, const namespacet &ns);
109 
110  template <levelt level = L2>
111  void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
112 
113  NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
114 
117  ssa_exprt lhs, // L0/L1
118  const exprt &rhs, // L2
119  const namespacet &ns,
120  bool rhs_is_simplified,
121  bool record_value,
122  bool allow_pointer_unsoundness = false);
123 
125 
126 protected:
127  template <levelt>
128  void rename_address(exprt &expr, const namespacet &ns);
129 
131  template <levelt level>
133  set_indices(ssa_exprt expr, const namespacet &ns);
134 
135  // this maps L1 names to (L2) types
136  typedef std::unordered_map<irep_idt, typet> l1_typest;
138 
139 public:
140  // guards
142  {
143  static irep_idt id = "goto_symex::\\guard";
144  return id;
145  }
146 
148  {
150  return threads[source.thread_nr].call_stack;
151  }
152 
153  const call_stackt &call_stack() const
154  {
156  return threads[source.thread_nr].call_stack;
157  }
158 
166  const symbol_exprt &expr,
167  std::function<std::size_t(const irep_idt &)> index_generator,
168  const namespacet &ns);
169 
174  ssa_exprt declare(ssa_exprt ssa, const namespacet &ns);
175 
176  void print_backtrace(std::ostream &) const;
177 
178  // threads
179  typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;
180  typedef std::list<guardt> a_s_w_entryt;
181  std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> read_in_atomic_section;
182  std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
184 
185  struct threadt
186  {
190  std::map<irep_idt, unsigned> function_frame;
191  unsigned atomic_section_id = 0;
194  {
195  }
196  };
197 
198  std::vector<threadt> threads;
199 
201  {
202  NOT_SHARED,
204  SHARED
205  };
206 
207  bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
208  bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
210  write_is_shared(const ssa_exprt &expr, const namespacet &ns) const;
211 
212  std::stack<bool> record_events;
213 
214  const incremental_dirtyt *dirty = nullptr;
215 
217 
220 
224 
227 
228  unsigned total_vccs = 0;
229  unsigned remaining_vccs = 0;
230 
232  void drop_existing_l1_name(const irep_idt &l1_identifier)
233  {
234  level2.current_names.erase(l1_identifier);
235  }
236 
238  void drop_l1_name(const irep_idt &l1_identifier)
239  {
240  level2.current_names.erase_if_exists(l1_identifier);
241  }
242 
243  std::function<std::size_t(const irep_idt &)> get_l2_name_provider() const
244  {
245  return fresh_l2_name_provider;
246  }
247 
249  static bool is_read_only_object(const exprt &lvalue)
250  {
251  // Note ID_constant can occur due to a partial write to a string constant,
252  // (i.e. something like byte_extract int from "hello" offset 2), which
253  // simplifies to a plain constant.
254  return lvalue.id() == ID_string_constant || lvalue.id() == ID_null_object ||
255  lvalue.id() == "zero_string" || lvalue.id() == "is_zero_string" ||
256  lvalue.id() == "zero_string_length" || lvalue.id() == ID_constant;
257  }
258 
259 private:
260  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
261 
272  goto_symex_statet(const goto_symex_statet &other) = default;
273 };
274 
276  : depth(s.depth),
277  level2(s.level2),
278  value_set(s.value_set),
279  guard(s.guard),
280  reachable(s.reachable),
281  propagation(s.propagation),
282  atomic_section_id(s.atomic_section_id)
283 {
284 }
285 
286 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
guard_exprt
Definition: guard_expr.h:26
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symex_target_equation.h
goto_symex_statet::threadt::atomic_section_id
unsigned atomic_section_id
Definition: goto_symex_state.h:191
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
goto_symex_statet::drop_l1_name
void drop_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
Definition: goto_symex_state.h:238
goto_symex_statet::print_backtrace
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
Definition: goto_symex_state.cpp:763
goto_symex_statet::a_s_r_entryt
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
Definition: goto_symex_state.h:179
goto_symex_statet::remaining_vccs
unsigned remaining_vccs
Definition: goto_symex_state.h:229
goto_symex_statet::threadt::pc
goto_programt::const_targett pc
Definition: goto_symex_state.h:187
NODISCARD
#define NODISCARD
Definition: nodiscard.h:22
goto_symex_statet::level1
symex_level1t level1
Definition: goto_symex_state.h:75
goto_symex_statet::assignment
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)
Definition: goto_symex_state.cpp:76
goto_symex_statet::guard_identifier
static irep_idt guard_identifier()
Definition: goto_symex_state.h:141
typet
The type of an expression, extends irept.
Definition: type.h:28
goto_symex_statet::l2_rename_rvalues
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
Definition: goto_symex_state.cpp:285
goto_symex_statet::dirty
const incremental_dirtyt * dirty
Definition: goto_symex_state.h:214
goto_symex_statet::read_in_atomic_section
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
Definition: goto_symex_state.h:181
goto_symex_statet::has_saved_jump_target
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
Definition: goto_symex_state.h:219
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:45
goto_symex_statet::~goto_symex_statet
~goto_symex_statet()
sharing_mapt::erase_if_exists
void erase_if_exists(const key_type &k)
Erase element if it exists.
Definition: sharing_map.h:264
goto_symex_statet::call_stack
const call_stackt & call_stack() const
Definition: goto_symex_state.h:153
goto_symex_statet::fresh_l2_name_provider
std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider
Definition: goto_symex_state.h:260
goto_symex_statet::guard_manager
guard_managert & guard_manager
Definition: goto_symex_state.h:72
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:39
invariant.h
goto_symex_statet::written_in_atomic_section
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
Definition: goto_symex_state.h:183
nodiscard.h
exprt
Base class for all expressions.
Definition: expr.h:52
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
goto_symex_statet::threadt::threadt
threadt(guard_managert &guard_manager)
Definition: goto_symex_state.h:192
goto_symex_statet::is_read_only_object
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
Definition: goto_symex_state.h:249
field_sensitivityt
Control granularity of object accesses.
Definition: field_sensitivity.h:80
goto_symex_statet::rename_ssa
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
goto_symex_statet::write_is_shared_resultt::SHARED
call_stackt
Definition: call_stack.h:14
goto_symex_statet::goto_symex_statet
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)
Definition: goto_symex_state.cpp:35
goto_state.h
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:16
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
guard.h
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:22
goto_symex_statet::l2_thread_write_encoding
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
Definition: goto_symex_state.cpp:514
goto_symex_statet::threadt::guard
guardt guard
Definition: goto_symex_state.h:188
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:198
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:147
make_unique.h
goto_symex_statet::has_saved_next_instruction
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
Definition: goto_symex_state.h:223
goto_symex_statet::symbol_table
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
Definition: goto_symex_state.h:69
goto_symex_statet::l2_thread_read_encoding
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
Definition: goto_symex_state.cpp:356
goto_symex_statet::total_vccs
unsigned total_vccs
Definition: goto_symex_state.h:228
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
renaming_level.h
goto_statet::level2
symex_level2t level2
Definition: goto_state.h:34
goto_symex_statet::write_is_shared_resultt
write_is_shared_resultt
Definition: goto_symex_state.h:200
goto_symex_statet::symex_target
symex_target_equationt * symex_target
Definition: goto_symex_state.h:73
goto_statet::goto_statet
goto_statet()=delete
Constructors.
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_symex_statet::l1_typest
std::unordered_map< irep_idt, typet > l1_typest
Definition: goto_symex_state.h:136
goto_symex_statet::write_is_shared
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
Definition: goto_symex_state.cpp:486
frame.h
goto_statet
Container for data that varies per program point, e.g.
Definition: goto_state.h:27
goto_symex_statet::field_sensitivity
field_sensitivityt field_sensitivity
Definition: goto_symex_state.h:124
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:40
goto_symex_statet::goto_symex_statet
goto_symex_statet(const goto_symex_statet &other, symex_target_equationt *const target)
Fake "copy constructor" that initializes the symex_target member.
Definition: goto_symex_state.h:56
goto_symex_statet::run_validation_checks
bool run_validation_checks
Should the additional validation checks be run?
Definition: goto_symex_state.h:226
goto_symex_statet::a_s_w_entryt
std::list< guardt > a_s_w_entryt
Definition: goto_symex_state.h:180
ssa_expr.h
symex_level2t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:83
goto_symex_statet::threadt
Definition: goto_symex_state.h:185
goto_symex_statet::declare
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...
Definition: goto_symex_state.cpp:809
goto_symex_statet::threadt::function_frame
std::map< irep_idt, unsigned > function_frame
Definition: goto_symex_state.h:190
goto_symex_statet::set_indices
NODISCARD renamedt< ssa_exprt, level > set_indices(ssa_exprt expr, const namespacet &ns)
Update values up to level.
goto_symex_statet::write_is_shared_resultt::NOT_SHARED
goto_symex_statet::write_is_shared_resultt::IN_ATOMIC_SECTION
goto_symex_statet::record_events
std::stack< bool > record_events
Definition: goto_symex_state.h:212
symex_level1t
Functor to set the level 1 renaming of SSA expressions.
Definition: renaming_level.h:52
call_stack.h
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
goto_symex_statet::rename
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::saved_target
goto_programt::const_targett saved_target
Definition: goto_symex_state.h:216
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
field_sensitivity.h
incremental_dirtyt
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:118
goto_symex_statet::threadt::call_stack
call_stackt call_stack
Definition: goto_symex_state.h:189
goto_symex_statet::get_l2_name_provider
std::function< std::size_t(const irep_idt &)> get_l2_name_provider() const
Definition: goto_symex_state.h:243
true_exprt
The Boolean constant true.
Definition: std_expr.h:3954
sharing_mapt::erase
void erase(const key_type &k)
Erase element, element must exist in map.
Definition: sharing_map.h:1137
std_expr.h
goto_symex_statet::add_object
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.
Definition: goto_symex_state.cpp:784
goto_function.h
goto_symex_statet::rename_address
void rename_address(exprt &expr, const namespacet &ns)
Definition: goto_symex_state.cpp:543
goto_symex_statet::l1_types
l1_typest l1_types
Definition: goto_symex_state.h:137
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:26
goto_symex_statet::drop_existing_l1_name
void drop_existing_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
Definition: goto_symex_state.h:232