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 goto_symext::statet & state
The type of an expression, extends irept.
bool constant_propagation
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
Semantic type conversion.
void return_assignment(statet &)
Generate Equation using Symbolic Execution.
virtual void no_body(const irep_idt &)
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
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...
virtual void symex_goto(statet &)
virtual void symex_fkt(statet &, const code_function_callt &)
Goto Programs with Functions.
static bool is_index_member_symbol_if(const exprt &expr)
void symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
The trinary if-then-else operator.
virtual void symex_macro(statet &, const code_function_callt &)
virtual void symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
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...
virtual void do_simplify(exprt &)
void validate(const namespacet &ns, const validation_modet vm) const
void validate(const namespacet &ns, const validation_modet vm) const
goto_symext(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
void symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
Extract member of struct or union.
virtual void symex_end_of_function(statet &)
do function call by inlining
void symex_catch(statet &)
virtual void symex_atomic_end(statet &)
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.
symex_targett::assignment_typet assignment_typet
void symex_throw(statet &)
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
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 ...
Configuration of the symbolic execution.
symex_nondet_generatort build_symex_nondet
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
virtual ~goto_symext()=default
virtual void symex_atomic_begin(statet &)
void symex_assign_typecast(statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
virtual void symex_other(statet &)
Identifies source in the context of symbolic execution.
bool doing_path_exploration
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.
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
static unsigned dynamic_counter
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we're executing.
exprt address_arithmetic(const exprt &, statet &, guardt &, bool keep_array)
Evaluate an ID_address_of expression.
virtual void symex_assume(statet &, const exprt &cond)
virtual void symex_decl(statet &)
symex_target_equationt & target
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
void symex_transition(goto_symext::statet &state)
void dereference_rec(exprt &, statet &, guardt &, bool write)
bool run_validation_checks
Should the additional validation checks be run?
codet representation of a function call statement.
A collection of goto functions.
path_storaget & path_storage
exprt make_auto_object(const typet &, statet &)
virtual void dereference(exprt &, statet &, bool write)
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
virtual void symex_trace(statet &, const code_function_callt &)
virtual void loop_bound_exceeded(statet &, const exprt &guard)
void pop_frame(statet &)
pop one call frame
void symex_assign_if(statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Storage for symbolic execution paths to be resumed later.
std::vector< exprt > operandst
unsigned atomic_section_counter
virtual void symex_input(statet &, const codet &)
void phi_function(const statet::goto_statet &goto_state, statet &)
void rewrite_quantifiers(exprt &, statet &)
void symex_assign(statet &, const code_assignt &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
The main class for the forward symbolic simulator.
void symex_threaded_step(statet &, const get_goto_functiont &)
Invokes symex_step and verifies whether additional threads can be executed.
std::vector< framet > call_stackt
bool self_loops_to_assumptions
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
void clean_expr(exprt &, statet &, bool write)
Expression to hold a nondeterministic choice.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
void dereference_rec_address_of(exprt &, statet &, guardt &)
bool should_pause_symex
Have states been pushed onto the workqueue?
const symex_configt symex_config
Base class for all expressions.
symex_configt(const optionst &options)
virtual void symex_function_call_code(const get_goto_functiont &, statet &, const code_function_callt &)
do function call by inlining
void trigger_auto_object(const exprt &, statet &)
virtual void symex_output(statet &, const codet &)
void symex_assign_struct_member(statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
void initialize_auto_object(const exprt &, statet &)
bool allow_pointer_unsoundness
virtual void symex_dead(statet &)
virtual void symex_start_thread(statet &)
const irep_idt guard_identifier
void merge_gotos(statet &)
unsigned get_total_vccs()
virtual void symex_printf(statet &, const exprt &rhs)
Expression to hold a symbol (variable)
void symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
nondet_symbol_exprt operator()(typet &type)
bool unwinding_assertions
Data structure for representing an arbitrary statement in a program.
An expression containing a side effect.
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
virtual void symex_cpp_delete(statet &, const codet &)
Expression providing an SSA-renamed symbol of expressions.
Storage of symbolic execution paths to resume.
Functor generating fresh nondet symbols.
unsigned get_remaining_vccs()
A codet representing an assignment in the program.
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
void havoc_rec(statet &, const guardt &, const exprt &)
void symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)