cprover
Loading...
Searching...
No Matches
goto_symex_state.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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 <util/invariant.h>
16#include <util/ssa_expr.h>
17#include <util/std_expr.h>
18#include <util/symbol_table.h>
19
20#include <analyses/guard.h>
21
22#include "call_stack.h"
23#include "field_sensitivity.h"
24#include "goto_state.h"
25#include "renaming_level.h"
26#include "shadow_memory_state.h"
27
28#include <functional>
29
32
41class goto_symex_statet final : public goto_statet
42{
43public:
46 std::size_t max_field_sensitive_array_size,
47 bool should_simplify,
49 guard_managert &manager,
50 std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
52
55 const goto_symex_statet &other,
56 symex_target_equationt *const target)
57 : goto_symex_statet(other) // NOLINT
58 {
59 symex_target = target;
60 }
61
63
68
69 // Manager is required to be able to resize the thread vector
72
74
99 template <levelt level = L2>
100 [[nodiscard]] renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
101
104 template <levelt level>
105 [[nodiscard]] renamedt<ssa_exprt, level>
106 rename_ssa(ssa_exprt ssa, const namespacet &ns);
107
108 template <levelt level = L2>
109 void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
110
111 [[nodiscard]] exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
112
115 ssa_exprt lhs, // L0/L1
116 const exprt &rhs, // L2
117 const namespacet &ns,
118 bool rhs_is_simplified,
119 bool record_value,
120 bool allow_pointer_unsoundness = false);
121
123
125
126protected:
127 template <levelt>
128 void rename_address(exprt &expr, const namespacet &ns);
129
131 template <levelt level>
132 [[nodiscard]] renamedt<ssa_exprt, level>
134
135 // this maps L1 names to (L2) types
136 typedef std::unordered_map<irep_idt, typet> l1_typest;
138
139public:
140 // guards
142 {
143 static irep_idt id = "goto_symex::\\guard";
144 return id;
145 }
146
148 {
149 PRECONDITION(source.thread_nr < threads.size());
150 return threads[source.thread_nr].call_stack;
151 }
152
153 const call_stackt &call_stack() const
154 {
155 PRECONDITION(source.thread_nr < threads.size());
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
198
199 std::vector<threadt> threads;
200
207
208 bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
209 bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
211 write_is_shared(const ssa_exprt &expr, const namespacet &ns) const;
212
213 std::stack<bool> record_events;
214
215 const incremental_dirtyt *dirty = nullptr;
216
218
221
225
228
229 unsigned total_vccs = 0;
230 unsigned remaining_vccs = 0;
231
233 void drop_existing_l1_name(const irep_idt &l1_identifier)
234 {
235 level2.current_names.erase(l1_identifier);
236 }
237
239 void drop_l1_name(const irep_idt &l1_identifier)
240 {
241 level2.current_names.erase_if_exists(l1_identifier);
242 }
243
244 std::function<std::size_t(const irep_idt &)> get_l2_name_provider() const
245 {
247 }
248
250 static bool is_read_only_object(const exprt &lvalue)
251 {
252 // Note ID_constant can occur due to a partial write to a string constant,
253 // (i.e. something like byte_extract int from "hello" offset 2), which
254 // simplifies to a plain constant.
255 return lvalue.id() == ID_string_constant || lvalue.id() == ID_null_object ||
256 lvalue.id() == "zero_string" || lvalue.id() == "is_zero_string" ||
257 lvalue.id() == "zero_string_length" || lvalue.is_constant() ||
258 lvalue.id() == ID_array;
259 }
260
261private:
263 std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
264
275 goto_symex_statet(const goto_symex_statet &other) = default;
276};
277
278#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
Base class for all expressions.
Definition expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
Control granularity of object accesses.
instructionst::const_iterator const_targett
symex_level2t level2
Definition goto_state.h:38
goto_statet()=delete
Constructors.
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...
const call_stackt & call_stack() const
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.
call_stackt & call_stack()
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
goto_symex_statet(const goto_symex_statet &other, symex_target_equationt *const target)
Fake "copy constructor" that initializes the symex_target member.
std::function< std::size_t(const irep_idt &)> get_l2_name_provider() const
exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
shadow_memory_statet shadow_memory
static irep_idt guard_identifier()
const incremental_dirtyt * dirty
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
const irep_idt & language_mode
void rename_address(exprt &expr, const namespacet &ns)
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
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
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...
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.
goto_symex_statet(const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, bool should_simplify, const irep_idt &language_mode, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
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
symex_targett::sourcet source
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
renamedt< ssa_exprt, level > set_indices(ssa_exprt expr, const namespacet &ns)
Update values up to level.
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:118
const irep_idt & id() const
Definition irep.h:388
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
The state maintained by the shadow memory instrumentation during symbolic execution.
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table.
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:3195
The type of an expression, extends irept.
Definition type.h:29
goto_statet class definition
Guard Data Structure.
guard_expr_managert guard_managert
Definition guard.h:28
guard_exprt guardt
Definition guard.h:29
Renaming levels.
Symex Shadow Memory Instrumentation State.
#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
Functor to set the level 1 renaming of SSA expressions.
Identifies source in the context of symbolic execution.
Author: Diffblue Ltd.
dstringt irep_idt