cprover
Loading...
Searching...
No Matches
scratch_program_symext Struct Reference

#include <scratch_program.h>

Inheritance diagram for scratch_program_symext:
Collaboration diagram for scratch_program_symext:

Public Member Functions

 scratch_program_symext (message_handlert &mh, const symbol_table_baset &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
std::unique_ptr< statetinitialize_entry_point_state (const get_goto_functiont &get_goto_function)
Public Member Functions inherited from goto_symext
 goto_symext (message_handlert &mh, const symbol_table_baset &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
 Construct a goto_symext to execute a particular program.
virtual ~goto_symext ()=default
 A virtual destructor allowing derived classes to be cleaned up correctly.
virtual symbol_tablet symex_from_entry_point_of (const get_goto_functiont &get_goto_function, const shadow_memory_field_definitionst &fields)
 Symbolically execute the entire program starting from entry point.
virtual void initialize_path_storage_from_entry_point_of (const get_goto_functiont &get_goto_function, symbol_table_baset &new_symbol_table, const shadow_memory_field_definitionst &fields)
 Puts the initial state of the entry point function into the path storage.
virtual symbol_tablet resume_symex_from_saved_state (const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation)
 Performs symbolic execution using a state and equation that have already been used to symbolically execute part of the program.
virtual symbol_tablet symex_with_state (statet &state, const get_goto_functiont &get_goto_functions)
 Symbolically execute the entire program starting from entry point.
virtual bool check_break (const irep_idt &loop_id, unsigned unwind)
 Defines condition for interrupting symbolic execution for a specific loop.
unsigned get_total_vccs () const
unsigned get_remaining_vccs () const
void validate (const validation_modet vm) const

Additional Inherited Members

Public Types inherited from goto_symext
typedef goto_symex_statet statet
 A type abbreviation for goto_symex_statet.
typedef std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
 The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Static Public Member Functions inherited from goto_symext
static get_goto_functiont get_goto_function (abstract_goto_modelt &goto_model)
 Return a function to get/load a goto function from the given goto model Create a default delegate to retrieve function bodies from a goto_functionst.
Public Attributes inherited from goto_symext
bool should_pause_symex
 Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution run, it means that symbolic execution has been paused because we encountered a GOTO instruction while doing path exploration, and thus pushed the successor states of the GOTO onto path_storage.
bool ignore_assertions = false
 If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
irep_idt language_mode
 language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.
Protected Types inherited from goto_symext
typedef symex_targett::assignment_typet assignment_typet
Protected Member Functions inherited from goto_symext
std::unique_ptr< statetinitialize_entry_point_state (const get_goto_functiont &get_goto_function)
 Initialize the symbolic execution and the given state with the beginning of the entry point function.
void symex_threaded_step (statet &state, const get_goto_functiont &get_goto_function)
 Invokes symex_step and verifies whether additional threads can be executed.
virtual void symex_step (const get_goto_functiont &get_goto_function, statet &state)
 Called for each step in the symbolic execution This calls print_symex_step to print symex's current instruction if required, then execute_next_instruction to execute the actual instruction body.
void execute_next_instruction (const get_goto_functiont &get_goto_function, statet &state)
 Executes the instruction state.source.pc Case-switches over the type of the instruction being executed and calls another function appropriate to the instruction type, for example symex_function_call if the current instruction is a function call, symex_goto if the current instruction is a goto, etc.
void kill_instruction_local_symbols (statet &state)
 Kills any variables in instruction_local_symbols (these are currently always let-bound variables defined in the course of executing the current instruction), then clears instruction_local_symbols.
void print_symex_step (statet &state)
 Prints the route of symex as it walks through the code.
messaget::mstreamtprint_callstack_entry (const symex_targett::sourcet &target)
exprt clean_expr (exprt expr, statet &state, bool write)
 Clean up an expression.
void trigger_auto_object (const exprt &, statet &)
void initialize_auto_object (const exprt &, statet &)
void process_array_expr (statet &, exprt &)
 Given an expression, find the root object and the offset into it.
exprt make_auto_object (const typet &, statet &)
virtual void dereference (exprt &, statet &, bool write)
 Replace all dereference operations within expr with explicit references to the objects they may refer to. For example, the expression *p1 + *p2 might be rewritten to obj1 + (p2 == &obj2 ? obj2 : obj3) in the case where p1 is known to point to obj1 and p2 points to either obj2 or obj3. The expression, and any object references introduced, are renamed to L1 in the process (so in fact we would get obj1!0@3 + (p2!0@1 == .... rather than the exact example given above).
symbol_exprt cache_dereference (exprt &dereference_result, statet &state)
void dereference_rec (exprt &expr, statet &state, bool write, bool is_in_quantifier)
exprt address_arithmetic (const exprt &, statet &, bool keep_array)
virtual void symex_goto (statet &state)
 Symbolically execute a GOTO instruction.
void symex_unreachable_goto (statet &state)
 Symbolically execute a GOTO instruction in the context of unreachable code.
void symex_set_return_value (statet &state, const exprt &return_value)
 Symbolically execute a SET_RETURN_VALUE instruction.
virtual void symex_start_thread (statet &state)
 Symbolically execute a START_THREAD instruction.
virtual void symex_atomic_begin (statet &state)
 Symbolically execute an ATOMIC_BEGIN instruction.
virtual void symex_atomic_end (statet &state)
 Symbolically execute an ATOMIC_END instruction.
virtual void symex_decl (statet &state)
 Symbolically execute a DECL instruction.
virtual void symex_decl (statet &state, const symbol_exprt &expr)
 Symbolically execute a DECL instruction for the given symbol or simulate such an execution for a synthetic symbol.
virtual void symex_dead (statet &state)
 Symbolically execute a DEAD instruction.
void symex_dead (statet &state, const symbol_exprt &symbol_expr)
 Kill a symbol, as if it had been the subject of a DEAD instruction.
virtual void symex_other (statet &state)
 Symbolically execute an OTHER instruction.
void symex_assert (const goto_programt::instructiont &, statet &)
void apply_goto_condition (goto_symex_statet &current_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns)
 Propagate constants and points-to information implied by a GOTO condition.
void try_filter_value_sets (goto_symex_statet &state, exprt condition, const value_sett &original_value_set, value_sett *jump_taken_value_set, value_sett *jump_not_taken_value_set, const namespacet &ns)
 Try to filter value sets based on whether possible values of a pointer-typed symbol make the condition true or false.
virtual void vcc (const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)
 Symbolically execute a verification condition (assertion).
virtual void symex_assume (statet &state, const exprt &cond)
 Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.
void symex_assume_l2 (statet &, const exprt &cond)
void merge_gotos (statet &state)
 Merge all branches joining at the current program point.
virtual void merge_goto (const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state)
 Merge a single branch, the symbolic state of which is held in goto_state, into the current overall symbolic state.
void phi_function (const goto_statet &goto_state, statet &dest_state)
 Merge the SSA assignments from goto_state into dest_state.
virtual bool should_stop_unwind (const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind)
 Determine whether to unwind a loop.
virtual void loop_bound_exceeded (statet &state, const exprt &guard)
virtual void symex_function_call (const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction)
 Symbolically execute a FUNCTION_CALL instruction.
virtual void locality (const irep_idt &function_identifier, goto_symext::statet &state, const goto_functionst::goto_functiont &goto_function)
 Preserves locality of parameters of a given function by applying L1 renaming to them.
virtual void symex_end_of_function (statet &)
 Symbolically execute a END_FUNCTION instruction.
virtual void symex_function_call_symbol (const get_goto_functiont &get_goto_function, statet &state, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
 Symbolic execution of a call to a function call.
virtual void symex_function_call_post_clean (const get_goto_functiont &get_goto_function, statet &state, const exprt &cleaned_lhs, const symbol_exprt &function, const exprt::operandst &cleaned_arguments)
 Symbolic execution of a function call by inlining.
virtual bool get_unwind_recursion (const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
void parameter_assignments (const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
 Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are deduced from the type of goto_function.
void symex_throw (statet &state)
 Symbolically execute a THROW instruction.
void symex_catch (statet &state)
 Symbolically execute a CATCH instruction.
virtual void do_simplify (exprt &expr, const value_sett &value_set)
void symex_assign (statet &state, const exprt &lhs, const exprt &rhs)
 Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
bool constant_propagate_assignment_with_side_effects (statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs)
 Attempt to constant propagate side effects of the assignment (if any)
void constant_propagate_empty_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Create an empty string constant.
bool constant_propagate_string_concat (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate string concatenation.
bool constant_propagate_string_substring (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate getting a substring of a string.
bool constant_propagate_integer_to_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate converting an integer to a string.
bool constant_propagate_delete_char_at (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate deleting a character from a string.
bool constant_propagate_delete (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate deleting a substring from a string.
bool constant_propagate_set_length (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate setting the length of a string.
bool constant_propagate_set_char_at (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate setting the char at the given index.
bool constant_propagate_trim (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant propagate trim operations.
bool constant_propagate_case_change (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper)
 Attempt to constant propagate case changes, both upper and lower.
bool constant_propagate_replace (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
 Attempt to constant proagate character replacement.
void assign_string_constant (statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array)
 Assign constant string length and string data given by a char array to given ssa variables.
const symboltget_new_string_data_symbol (statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array)
 Installs a new symbol in the symbol table to represent the given character array, and assigns the character array to the symbol.
void associate_array_to_pointer (statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data)
 Generate array to pointer association primitive.
std::optional< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string (const statet &state, const exprt &content)
void havoc_rec (statet &state, const guardt &guard, const exprt &dest)
Static Protected Member Functions inherited from goto_symext
static std::optional< std::reference_wrapper< const constant_exprt > > try_evaluate_constant (const statet &state, const exprt &expr)
Protected Attributes inherited from goto_symext
const symex_configt symex_config
 The configuration to use for this symbolic execution.
const symbol_table_basetouter_symbol_table
 The symbol table associated with the goto-program being executed.
namespacet ns
 Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol table owned by the goto_symex_statet object used during symbolic execution.
guard_managertguard_manager
 Used to create guards.
symex_target_equationttarget
 The equation that this execution is building up.
unsigned atomic_section_counter
 A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.
std::vector< symbol_exprtinstruction_local_symbols
 Variables that should be killed at the end of the current symex_step invocation.
messaget log
 The messaget to write log messages to.
std::size_t path_segment_vccs
 Execute any let expressions in expr using symex_assignt::assign_symbol.
complexity_limitert complexity_module
shadow_memoryt shadow_memory
 Shadow memory instrumentation API.
unsigned _total_vccs
unsigned _remaining_vccs

Detailed Description

Definition at line 34 of file scratch_program.h.

Constructor & Destructor Documentation

◆ scratch_program_symext()

scratch_program_symext::scratch_program_symext ( message_handlert & mh,
const symbol_table_baset & outer_symbol_table,
symex_target_equationt & _target,
const optionst & options,
path_storaget & path_storage,
guard_managert & guard_manager )
inline

Definition at line 36 of file scratch_program.h.

Member Function Documentation

◆ initialize_entry_point_state()

std::unique_ptr< statet > scratch_program_symext::initialize_entry_point_state ( const get_goto_functiont & get_goto_function)
inline

Definition at line 54 of file scratch_program.h.


The documentation for this struct was generated from the following file: