Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
17 #include <unordered_set>
50 std::size_t max_field_sensitive_array_size,
101 template <levelt level = L2>
106 template <levelt level>
110 template <levelt level = L2>
120 bool rhs_is_simplified,
122 bool allow_pointer_unsoundness =
false);
131 template <levelt level>
143 static irep_idt id =
"goto_symex::\\guard";
167 std::function<std::size_t(
const irep_idt &)> index_generator,
182 std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
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;
278 value_set(s.value_set),
280 reachable(s.reachable),
281 propagation(s.propagation),
282 atomic_section_id(s.atomic_section_id)
286 #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.
Generate Equation using Symbolic Execution.
unsigned atomic_section_id
void drop_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
goto_programt::const_targett pc
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)
static irep_idt guard_identifier()
The type of an expression, extends irept.
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
const incremental_dirtyt * dirty
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
Central data structure: state.
void erase_if_exists(const key_type &k)
Erase element if it exists.
const call_stackt & call_stack() const
std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider
guard_managert & guard_manager
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
Base class for all expressions.
symex_targett::sourcet source
threadt(guard_managert &guard_manager)
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
Control granularity of object accesses.
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
goto_symex_statet(const goto_symex_statet &other)=default
Dangerous, do not use.
Expression to hold a symbol (variable)
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)
goto_statet class definition
Expression providing an SSA-renamed symbol of expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
This is unused by this implementation of guards, but can be used by other implementations of the same...
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
std::vector< threadt > threads
call_stackt & call_stack()
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
#define PRECONDITION(CONDITION)
symex_target_equationt * symex_target
goto_statet()=delete
Constructors.
const irep_idt & id() const
std::unordered_map< irep_idt, typet > l1_typest
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
Container for data that varies per program point, e.g.
field_sensitivityt field_sensitivity
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
goto_symex_statet(const goto_symex_statet &other, symex_target_equationt *const target)
Fake "copy constructor" that initializes the symex_target member.
bool run_validation_checks
Should the additional validation checks be run?
std::list< guardt > a_s_w_entryt
symex_renaming_levelt current_names
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...
std::map< irep_idt, unsigned > function_frame
NODISCARD renamedt< ssa_exprt, level > set_indices(ssa_exprt expr, const namespacet &ns)
Update values up to level.
std::stack< bool > record_events
Functor to set the level 1 renaming of SSA expressions.
instructionst::const_iterator const_targett
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_programt::const_targett saved_target
Identifies source in the context of symbolic execution.
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
std::function< std::size_t(const irep_idt &)> get_l2_name_provider() const
The Boolean constant true.
void erase(const key_type &k)
Erase element, element must exist in map.
API to expression classes.
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.
void rename_address(exprt &expr, const namespacet &ns)
Wrapper for expressions or types which have been renamed up to a given level.
void drop_existing_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.