Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
127 const statet &saved_state,
178 const irep_idt &function_identifier,
266 const std::string &msg,
327 const irep_idt &function_identifier,
333 const irep_idt &function_identifier,
353 const exprt &full_lhs,
360 const exprt &full_lhs,
367 const exprt &full_lhs,
374 const exprt &full_lhs,
381 const exprt &full_lhs,
388 const exprt &full_lhs,
395 const exprt &full_lhs,
456 _total_vccs != std::numeric_limits<unsigned>::max(),
457 "symex_threaded_step should have been executed at least once before "
458 "attempting to read total_vccs");
466 "symex_threaded_step should have been executed at least once before "
467 "attempting to read remaining_vccs");
482 bool is_backwards_goto);
484 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
Class that provides messages with a built-in verbosity 'level'.
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Functor generating fresh nondet symbols.
bool self_loops_to_assumptions
goto_symext::statet & state
void initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, const irep_idt &function_identifier, goto_programt::const_targett pc, goto_programt::const_targett limit)
Initialise the symbolic execution and the given state with pc as entry point.
virtual void symex_function_call_code(const get_goto_functiont &, statet &, const code_function_callt &)
do function call by inlining
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
void symex_assign_typecast(statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_dead(statet &)
void symex_assign(statet &, const code_assignt &)
virtual void symex_atomic_begin(statet &)
Expression to hold a nondeterministic choice.
void merge_gotos(statet &)
Configuration of the symbolic execution.
static unsigned dynamic_counter
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
unsigned get_total_vccs()
The type of an expression, extends irept.
symex_target_equationt & target
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation, symbol_tablet &new_symbol_table)
Performs symbolic execution using a state and equation that have already been used to symex part of t...
Storage for symbolic execution paths to be resumed later.
path_storaget & path_storage
The trinary if-then-else operator.
const irep_idt guard_identifier
void clean_expr(exprt &, statet &, bool write)
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
Store the what expression by recursively descending into the operands of lhs until the first operand ...
virtual void symex_decl(statet &)
virtual void symex_macro(statet &, const code_function_callt &)
Base class for all expressions.
virtual void do_simplify(exprt &)
virtual void no_body(const irep_idt &)
virtual void symex_printf(statet &, const exprt &rhs)
void symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
void trigger_auto_object(const exprt &, statet &)
virtual void symex_start_thread(statet &)
Expression to hold a symbol (variable)
Storage of symbolic execution paths to resume.
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
virtual void symex_trace(statet &, const code_function_callt &)
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
symex_nondet_generatort build_symex_nondet
void dereference_rec_address_of(exprt &, statet &, guardt &)
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...
codet representation of a function call statement.
virtual void symex_output(statet &, const codet &)
void symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_cpp_delete(statet &, const codet &)
nondet_symbol_exprt operator()(typet &type)
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we're executing.
virtual void dereference(exprt &, statet &, bool write)
void initialize_auto_object(const exprt &, statet &)
bool doing_path_exploration
bool unwinding_assertions
virtual void symex_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
symex entire program starting from entry point
The main class for the forward symbolic simulator.
void return_assignment(statet &)
bool allow_pointer_unsoundness
virtual void symex_end_of_function(statet &)
do function call by inlining
static bool is_index_member_symbol_if(const exprt &expr)
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
exprt make_auto_object(const typet &, statet &)
virtual void symex_other(statet &)
exprt address_arithmetic(const exprt &, statet &, guardt &, bool keep_array)
Evaluate an ID_address_of expression.
void symex_threaded_step(statet &, const get_goto_functiont &)
Invokes symex_step and verifies whether additional threads can be executed.
virtual void symex_goto(statet &)
std::vector< exprt > operandst
void pop_frame(statet &)
pop one call frame
std::vector< framet > call_stackt
unsigned get_remaining_vccs()
void symex_transition(goto_symext::statet &state)
goto_symext(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
void symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void loop_bound_exceeded(statet &, const exprt &guard)
void locality(const irep_idt &function_identifier, statet &, const goto_functionst::goto_functiont &)
preserves locality of local variables of a given function by applying L1 renaming to the local identi...
::goto_functiont goto_functiont
virtual void symex_assume(statet &, const exprt &cond)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Extract member of struct or union.
A collection of goto functions.
virtual ~goto_symext()=default
void symex_throw(statet &)
void validate(const namespacet &ns, const validation_modet vm) const
void symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
unsigned atomic_section_counter
void symex_catch(statet &)
void phi_function(const statet::goto_statet &goto_state, statet &)
void symex_assign_if(statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
bool constant_propagation
virtual void symex_atomic_end(statet &)
symex_targett::assignment_typet assignment_typet
virtual void vcc(const exprt &, const std::string &msg, statet &)
void validate(const namespacet &ns, const validation_modet vm) const
virtual void symex_cpp_new(statet &, const exprt &lhs, const side_effect_exprt &)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
const symex_configt symex_config
virtual void symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
virtual void symex_fkt(statet &, const code_function_callt &)
instructionst::const_iterator const_targett
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Identifies source in the context of symbolic execution.
bool run_validation_checks
Should the additional validation checks be run?
void dereference_rec(exprt &, statet &, guardt &, bool write)
Semantic type conversion.
A codet representing an assignment in the program.
symex_configt(const optionst &options)
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
virtual void symex_input(statet &, const codet &)
void rewrite_quantifiers(exprt &, statet &)
An expression containing a side effect.
void symex_assign_struct_member(statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
void havoc_rec(statet &, const guardt &, const exprt &)
bool should_pause_symex
Have states been pushed onto the workqueue?
Data structure for representing an arbitrary statement in a program.