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< statet > | initialize_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. More... | |
| virtual | ~goto_symext ()=default |
| A virtual destructor allowing derived classes to be cleaned up correctly. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| virtual symbol_tablet | symex_with_state (statet &state, const get_goto_functiont &get_goto_functions) |
| Symbolically execute the entire program starting from entry point. More... | |
| virtual bool | check_break (const irep_idt &loop_id, unsigned unwind) |
| Defines condition for interrupting symbolic execution for a specific loop. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| bool | ignore_assertions = false |
| If this flag is set to true then assertions will be temporarily ignored by the symbolic executions. More... | |
| 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. More... | |
| std::size_t | path_segment_vccs |
| Number of VCCs generated during the run of this goto_symext object. More... | |
| Protected Types inherited from goto_symext | |
| typedef symex_targett::assignment_typet | assignment_typet |
| Protected Member Functions inherited from goto_symext | |
| std::unique_ptr< statet > | initialize_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. More... | |
| void | symex_threaded_step (statet &state, const get_goto_functiont &get_goto_function) |
| Invokes symex_step and verifies whether additional threads can be executed. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| void | print_symex_step (statet &state) |
| Prints the route of symex as it walks through the code. More... | |
| messaget::mstreamt & | print_callstack_entry (const symex_targett::sourcet &target) |
| exprt | clean_expr (exprt expr, statet &state, bool write) |
| Clean up an expression. More... | |
| 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. More... | |
| 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. More... | |
| symbol_exprt | cache_dereference (exprt &dereference_result, statet &state) |
| void | dereference_rec (exprt &expr, statet &state, bool write, bool is_in_quantifier) |
If expr is a dereference_exprt, replace it with explicit references to the objects it may point to. More... | |
| exprt | address_arithmetic (const exprt &, statet &, bool keep_array) |
Transforms an lvalue expression by replacing any dereference operations it contains with explicit references to the objects they may point to (using goto_symext::dereference_rec), and translates byte_extract, member and index operations into integer offsets from a root symbol (if any). More... | |
| virtual void | symex_goto (statet &state) |
| Symbolically execute a GOTO instruction. More... | |
| void | symex_unreachable_goto (statet &state) |
| Symbolically execute a GOTO instruction in the context of unreachable code. More... | |
| void | symex_set_return_value (statet &state, const exprt &return_value) |
| Symbolically execute a SET_RETURN_VALUE instruction. More... | |
| virtual void | symex_start_thread (statet &state) |
| Symbolically execute a START_THREAD instruction. More... | |
| virtual void | symex_atomic_begin (statet &state) |
| Symbolically execute an ATOMIC_BEGIN instruction. More... | |
| virtual void | symex_atomic_end (statet &state) |
| Symbolically execute an ATOMIC_END instruction. More... | |
| virtual void | symex_decl (statet &state) |
| Symbolically execute a DECL instruction. More... | |
| 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. More... | |
| virtual void | symex_dead (statet &state) |
| Symbolically execute a DEAD instruction. More... | |
| void | symex_dead (statet &state, const symbol_exprt &symbol_expr) |
| Kill a symbol, as if it had been the subject of a DEAD instruction. More... | |
| virtual void | symex_other (statet &state) |
| Symbolically execute an OTHER instruction. More... | |
| void | symex_assert (const goto_programt::instructiont &, statet &) |
| void | apply_goto_condition (goto_symex_statet ¤t_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. More... | |
| 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. More... | |
| virtual void | vcc (const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state) |
| Symbolically execute a verification condition (assertion). More... | |
| virtual void | symex_assume (statet &state, const exprt &cond) |
| Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption. More... | |
| void | symex_assume_l2 (statet &, const exprt &cond) |
| void | merge_gotos (statet &state) |
| Merge all branches joining at the current program point. More... | |
| 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. More... | |
| void | phi_function (const goto_statet &goto_state, statet &dest_state) |
| Merge the SSA assignments from goto_state into dest_state. More... | |
| virtual bool | should_stop_unwind (const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) |
| Determine whether to unwind a loop. More... | |
| virtual void | loop_bound_exceeded (statet &state, const exprt &guard) |
| virtual void | no_body (const irep_idt &identifier) |
| Log a warning that a function has no body. More... | |
| 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. More... | |
| 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. More... | |
| virtual void | symex_end_of_function (statet &) |
| Symbolically execute a END_FUNCTION instruction. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| void | symex_throw (statet &state) |
| Symbolically execute a THROW instruction. More... | |
| void | symex_catch (statet &state) |
| Symbolically execute a CATCH instruction. More... | |
| virtual void | do_simplify (exprt &expr) |
| 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. More... | |
| 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) More... | |
| void | constant_propagate_empty_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Create an empty string constant. More... | |
| bool | constant_propagate_string_concat (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate string concatenation. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| 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. More... | |
| bool | constant_propagate_trim (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate trim operations. More... | |
| 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. More... | |
| bool | constant_propagate_replace (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant proagate character replacement. More... | |
| 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. More... | |
| const symbolt & | get_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. More... | |
| 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. More... | |
| 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) |
| void | lift_lets (statet &, exprt &) |
Execute any let expressions in expr using symex_assignt::assign_symbol. More... | |
| void | lift_let (statet &state, const let_exprt &let_expr) |
| Execute a single let expression, which should not have any nested let expressions (use lift_lets instead if there might be). More... | |
| virtual void | symex_va_start (statet &, const exprt &lhs, const side_effect_exprt &) |
| virtual void | symex_allocate (statet &state, const exprt &lhs, const side_effect_exprt &code) |
Symbolically execute an assignment instruction that has an allocate on the right hand side. More... | |
| virtual void | symex_cpp_delete (statet &state, const codet &code) |
Symbolically execute an OTHER instruction that does a CPP delete More... | |
| virtual void | symex_cpp_new (statet &state, const exprt &lhs, const side_effect_exprt &code) |
| Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes. More... | |
| virtual void | symex_printf (statet &state, const exprt &rhs) |
Symbolically execute an OTHER instruction that does a CPP printf More... | |
| virtual void | symex_input (statet &state, const codet &code) |
| Symbolically execute an OTHER instruction that does a CPP input. More... | |
| virtual void | symex_output (statet &state, const codet &code) |
| Symbolically execute an OTHER instruction that does a CPP output. More... | |
| void | rewrite_quantifiers (exprt &, statet &) |
| 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. More... | |
| const symbol_table_baset & | outer_symbol_table |
| The symbol table associated with the goto-program being executed. More... | |
| 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. More... | |
| guard_managert & | guard_manager |
| Used to create guards. More... | |
| symex_target_equationt & | target |
| The equation that this execution is building up. More... | |
| unsigned | atomic_section_counter |
| A monotonically increasing index for each encountered ATOMIC_BEGIN instruction. More... | |
| std::vector< symbol_exprt > | instruction_local_symbols |
| Variables that should be killed at the end of the current symex_step invocation. More... | |
| messaget | log |
| The messaget to write log messages to. More... | |
| path_storaget & | path_storage |
| Symbolic execution paths to be resumed later. More... | |
| complexity_limitert | complexity_module |
| shadow_memoryt | shadow_memory |
| Shadow memory instrumentation API. More... | |
| unsigned | _total_vccs |
| unsigned | _remaining_vccs |
Detailed Description
Definition at line 34 of file scratch_program.h.
Constructor & Destructor Documentation
◆ scratch_program_symext()
|
inline |
Definition at line 36 of file scratch_program.h.
Member Function Documentation
◆ initialize_entry_point_state()
|
inline |
Definition at line 54 of file scratch_program.h.
The documentation for this struct was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-instrument/accelerate/scratch_program.h
