cprover
goto_symext Class Reference

The main class for the forward symbolic simulator. More...

#include <goto_symex.h>

+ Inheritance diagram for goto_symext:
+ Collaboration diagram for goto_symext:

Public Types

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...
 

Public Member Functions

 goto_symext (message_handlert &mh, const symbol_tablet &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 void symex_from_entry_point_of (const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
 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_tablet &new_symbol_table)
 Puts the initial state of the entry point function into the path storage. More...
 
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 symbolically execute part of the program. More...
 
virtual void symex_with_state (statet &state, const get_goto_functiont &get_goto_functions, symbol_tablet &new_symbol_table)
 Symbolically execute the entire program starting from entry point. More...
 
unsigned get_total_vccs () const
 
unsigned get_remaining_vccs () const
 
void validate (const validation_modet vm) const
 

Static Public Member Functions

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

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...
 
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

typedef symex_targett::assignment_typet assignment_typet
 

Protected Member Functions

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. 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::mstreamtprint_callstack_entry (const symex_targett::sourcet &target)
 
void 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...
 
void dereference_rec (exprt &, statet &, bool write)
 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...
 
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 &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. 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 &, const std::string &msg, statet &)
 
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 code_function_callt &code)
 Symbolically execute a FUNCTION_CALL instruction. 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 code_function_callt &code)
 Symbolic execution of a call to a function call. More...
 
virtual void symex_function_call_code (const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &call)
 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 code_assignt &code)
 Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment. More...
 
void havoc_rec (statet &state, const guardt &guard, const exprt &dest)
 
void lift_lets (statet &, exprt &)
 Execute any let expressions in expr using symex_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...
 
void symex_assign_rec (statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, exprt::operandst &, assignment_typet)
 
void symex_assign_from_struct (statet &, const ssa_exprt &lhs, const exprt &full_lhs, const struct_exprt &rhs, exprt::operandst &, assignment_typet)
 Assign a struct expression to a symbol. More...
 
void symex_assign_symbol (statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, exprt::operandst &, assignment_typet)
 
void symex_assign_typecast (statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, exprt::operandst &, assignment_typet)
 
void symex_assign_array (statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, exprt::operandst &, assignment_typet)
 
void symex_assign_struct_member (statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, exprt::operandst &, assignment_typet)
 
void symex_assign_if (statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, exprt::operandst &, assignment_typet)
 
void symex_assign_byte_extract (statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, exprt::operandst &, assignment_typet)
 
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)
 Symbolically execute an assignment instruction that has a CPP new or new array or a Java new array on the right hand side. More...
 
virtual void symex_fkt (statet &state, const code_function_callt &code)
 Symbolically execute a FUNCTION_CALL instruction for a function whose name starts with CPROVER_FKT_PREFIX. More...
 
virtual void symex_trace (statet &state, const code_function_callt &code)
 Symbolically execute a FUNCTION_CALL instruction for the CBMC_trace function. 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

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 op0 is nil: this nil operand is then replaced with what. More...
 

Protected Attributes

const symex_configt symex_config
 The configuration to use for this symbolic execution. More...
 
const symbol_tabletouter_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_managertguard_manager
 Used to create guards. More...
 
symex_target_equationttarget
 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_exprtinstruction_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_storagetpath_storage
 Symbolic execution paths to be resumed later. More...
 
Statistics

The actual number of total and remaining VCCs should be assigned to the relevant members of goto_symex_statet. The members below are used to cache the values from goto_symex_statet after symbolic execution has ended, so that the user of goto_symext can read those values even after the state has been deallocated.

unsigned _total_vccs
 
unsigned _remaining_vccs
 

Static Protected Attributes

static unsigned dynamic_counter =0
 A monotonically increasing index for each created dynamic object. More...
 

Friends

class symex_dereference_statet
 

Detailed Description

The main class for the forward symbolic simulator.

Remarks
Higher-level architectural information on symbolic execution is documented in the Symbolic execution module page.

Definition at line 81 of file goto_symex.h.

Member Typedef Documentation

◆ assignment_typet

Definition at line 534 of file goto_symex.h.

◆ get_goto_functiont

The type of delegate functions that retrieve a goto_functiont for a particular function identifier.

Remarks
This allows goto_symext to be divorced from the particular type of goto_modelt that provides the function bodies

Definition at line 128 of file goto_symex.h.

◆ statet

A type abbreviation for goto_symex_statet.

Definition at line 85 of file goto_symex.h.

Constructor & Destructor Documentation

◆ goto_symext()

goto_symext::goto_symext ( message_handlert mh,
const symbol_tablet outer_symbol_table,
symex_target_equationt _target,
const optionst options,
path_storaget path_storage,
guard_managert guard_manager 
)
inline

Construct a goto_symext to execute a particular program.

Parameters
mhThe message handler to use for log messages
outer_symbol_tableThe symbol table for the program to be executed, excluding any symbols added during the symbolic execution
_targetWhere to store the equation built up by this execution
optionsThe options to use to configure this execution
path_storagePlace to storage symbolic execution paths that have been halted and can be resumed later
guard_managerManager for creating guards

Definition at line 96 of file goto_symex.h.

◆ ~goto_symext()

virtual goto_symext::~goto_symext ( )
virtualdefault

A virtual destructor allowing derived classes to be cleaned up correctly.

Member Function Documentation

◆ add_to_lhs()

exprt goto_symext::add_to_lhs ( const exprt lhs,
const exprt what 
)
staticprotected

Store the what expression by recursively descending into the operands of lhs until the first operand op0 is nil: this nil operand is then replaced with what.

Parameters
lhsNon-symbol pointed-to expression
whatThe expression to be added to the lhs
Returns
The resulting expression

Definition at line 89 of file symex_assign.cpp.

◆ address_arithmetic()

exprt goto_symext::address_arithmetic ( const exprt expr,
statet state,
bool  keep_array 
)
protected

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).

These are ultimately expressed in the form (target_type*)((char*)(&underlying_symbol) + offset).

Parameters
exprexpression to replace with normalised, dereference-free form
stateworking state. See goto_symext::dereference for possible side-effects of a dereference operation.
keep_arrayif true and an underlying object is an array, return its address (&array); otherwise return the address of its first element (`&array[0]).
Returns
the transformed lvalue expression

Definition at line 39 of file symex_dereference.cpp.

◆ apply_goto_condition()

void goto_symext::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 
)
protected

Propagate constants and points-to information implied by a GOTO condition.

See goto_statet::apply_condition for aspects of this which are common to GOTO and ASSUME instructions.

Parameters
current_statestate prior to the GOTO instruction
jump_taken_statestate following taking the GOTO
jump_not_taken_statefall-through state
original_guardthe original GOTO condition
new_guardGOTO condition, L2 renamed and simplified
nsglobal namespace

Definition at line 26 of file symex_goto.cpp.

◆ clean_expr()

void goto_symext::clean_expr ( exprt expr,
statet state,
bool  write 
)
protected

Clean up an expression.

Remarks
this does the following: a) rename non-det choices b) remove pointer dereferencing c) clean up byte_extract on the lhs of an assignment
Parameters
exprThe expression to clean up
state
write

Definition at line 216 of file symex_clean_expr.cpp.

◆ dereference()

void goto_symext::dereference ( exprt expr,
statet state,
bool  write 
)
protectedvirtual

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).

It may have two kinds of side-effect:

  1. When an expression may (or must) point to something which cannot legally be dereferenced, such as a null pointer or an integer cast to a pointer, a "failed object" is created instead, via one of two routes:

    a. if the add_failed_symbols pass has been run then a pointer-typed symbol x will have a corresponding failed symbol x$object. This is replicated according to L1 renaming on demand, so for example on the first failed dereference of x!5@10 we will create x$object!5@10 and add that to the symbol table. This addition is made by symex_dereference_statet::get_or_create_failed_symbol

    b. if such a failed symbol can't be found then symex will create one of its own, called symex::failed_symbol with some suffix. This is done by value_set_dereferencet::dereference

    In either case any newly-created symbol is added to state's symbol table and expr is altered to refer to it. Typically when expr has some legal targets as well this results in an expression like ptr == &real_obj ? real_obj : ptr$object.

  2. Any object whose base-name ends with auto_object is automatically initialised when dereferenced for the first time, creating a tree of pointers leading to fresh objects each time such a pointer is dereferenced. If new objects are created by this mechanism then state will be altered (by symex_assign) to initialise them. See auto_objects.cpp for details.

Definition at line 355 of file symex_dereference.cpp.

◆ dereference_rec()

void goto_symext::dereference_rec ( exprt expr,
statet state,
bool  write 
)
protected

If expr is a dereference_exprt, replace it with explicit references to the objects it may point to.

Otherwise recursively apply this function to expr's operands, with special cases for address-of (handled by goto_symext::address_arithmetic) and certain common expression patterns such as &struct.flexible_array[0] (see inline comments in code). For full details of this method's pointer replacement and potential side- effects see goto_symext::dereference

Definition at line 201 of file symex_dereference.cpp.

◆ do_simplify()

void goto_symext::do_simplify ( exprt expr)
protectedvirtual

Definition at line 18 of file goto_symex.cpp.

◆ execute_next_instruction()

void goto_symext::execute_next_instruction ( const get_goto_functiont get_goto_function,
statet state 
)
protected

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.

Parameters
get_goto_functionThe delegate to retrieve function bodies (see get_goto_functiont)
stateSymbolic execution state for current instruction

Definition at line 519 of file symex_main.cpp.

◆ get_goto_function()

goto_symext::get_goto_functiont goto_symext::get_goto_function ( abstract_goto_modelt goto_model)
static

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.

Parameters
goto_modelThe goto model holding the function map from which to retrieve function bodies
Returns
A delegate to retrieve function bodies from the given goto_functionst

Definition at line 410 of file symex_main.cpp.

◆ get_remaining_vccs()

unsigned goto_symext::get_remaining_vccs ( ) const
inline

Definition at line 709 of file goto_symex.h.

◆ get_total_vccs()

unsigned goto_symext::get_total_vccs ( ) const
inline

Definition at line 700 of file goto_symex.h.

◆ get_unwind_recursion()

bool goto_symext::get_unwind_recursion ( const irep_idt identifier,
unsigned  thread_nr,
unsigned  unwind 
)
protectedvirtual

Reimplemented in symex_bmct.

Definition at line 30 of file symex_function_call.cpp.

◆ havoc_rec()

void goto_symext::havoc_rec ( statet state,
const guardt guard,
const exprt dest 
)
protected

Definition at line 19 of file symex_other.cpp.

◆ initialize_auto_object()

void goto_symext::initialize_auto_object ( const exprt expr,
statet state 
)
protected

Definition at line 37 of file auto_objects.cpp.

◆ initialize_entry_point_state()

std::unique_ptr< goto_symext::statet > goto_symext::initialize_entry_point_state ( const get_goto_functiont get_goto_function)
protected

Initialize the symbolic execution and the given state with the beginning of the entry point function.

Parameters
get_goto_functionproducer for GOTO functions
Returns
Initialized symex state.

Definition at line 330 of file symex_main.cpp.

◆ initialize_path_storage_from_entry_point_of()

void goto_symext::initialize_path_storage_from_entry_point_of ( const get_goto_functiont get_goto_function,
symbol_tablet new_symbol_table 
)
virtual

Puts the initial state of the entry point function into the path storage.

Definition at line 396 of file symex_main.cpp.

◆ kill_instruction_local_symbols()

void goto_symext::kill_instruction_local_symbols ( statet state)
protected

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.

Definition at line 656 of file symex_main.cpp.

◆ lift_let()

void goto_symext::lift_let ( statet state,
const let_exprt let_expr 
)
protected

Execute a single let expression, which should not have any nested let expressions (use lift_lets instead if there might be).

Records the newly-defined variable in instruction_local_symbols, meaning it will be killed when symex_step concludes.

Definition at line 174 of file symex_clean_expr.cpp.

◆ lift_lets()

void goto_symext::lift_lets ( statet state,
exprt rhs 
)
protected

Execute any let expressions in expr using symex_assign_symbol.

The assignments will be made in bottom-up topological but otherwise arbitrary order (i.e. in (let x = let y = 0 in x + y) + (let z = 0 in z) we will defineybeforex, butzandx` could come in either order)

Definition at line 194 of file symex_clean_expr.cpp.

◆ loop_bound_exceeded()

void goto_symext::loop_bound_exceeded ( statet state,
const exprt guard 
)
protectedvirtual

Definition at line 783 of file symex_goto.cpp.

◆ make_auto_object()

exprt goto_symext::make_auto_object ( const typet type,
statet state 
)
protected

Definition at line 19 of file auto_objects.cpp.

◆ merge_goto()

void goto_symext::merge_goto ( const symex_targett::sourcet source,
goto_statet &&  goto_state,
statet state 
)
protectedvirtual

Merge a single branch, the symbolic state of which is held in goto_state, into the current overall symbolic state.

goto_state is no longer expected to be valid afterwards.

Parameters
sourcesource associated with the incoming goto_state
goto_stateA state to be merged into this location
stateSymbolic execution state to be updated

Reimplemented in symex_bmct.

Definition at line 546 of file symex_goto.cpp.

◆ merge_gotos()

void goto_symext::merge_gotos ( statet state)
protected

Merge all branches joining at the current program point.

Applies merge_goto for each goto state (each of which corresponds to previous branch).

Parameters
stateSymbolic execution state to be updated

Definition at line 523 of file symex_goto.cpp.

◆ no_body()

virtual void goto_symext::no_body ( const irep_idt identifier)
inlineprotectedvirtual

Log a warning that a function has no body.

Parameters
identifierThe name of the function with no body

Reimplemented in symex_bmct.

Definition at line 448 of file goto_symex.h.

◆ parameter_assignments()

void goto_symext::parameter_assignments ( const irep_idt function_identifier,
const goto_functionst::goto_functiont goto_function,
statet state,
const exprt::operandst arguments 
)
protected

Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are deduced from the type of goto_function.

Parameters
function_identifiername of the function
goto_functionfunction whose parameters we want to assign
[out]statestate of the goto program
argumentsarguments that are passed to the function

Definition at line 35 of file symex_function_call.cpp.

◆ phi_function()

void goto_symext::phi_function ( const goto_statet goto_state,
statet dest_state 
)
protected

Merge the SSA assignments from goto_state into dest_state.

Parameters
goto_stateA state to be merged into this location
dest_stateSymbolic execution state to be updated

Definition at line 716 of file symex_goto.cpp.

◆ print_callstack_entry()

messaget::mstreamt & goto_symext::print_callstack_entry ( const symex_targett::sourcet target)
protected

Definition at line 419 of file symex_main.cpp.

◆ print_symex_step()

void goto_symext::print_symex_step ( statet state)
protected

Prints the route of symex as it walks through the code.

Used for debugging.

Definition at line 427 of file symex_main.cpp.

◆ process_array_expr()

void goto_symext::process_array_expr ( statet state,
exprt expr 
)
protected

Given an expression, find the root object and the offset into it.

The extra complication to be considered here is that the expression may have any number of ternary expressions mixed with type casts.

Definition at line 123 of file symex_clean_expr.cpp.

◆ resume_symex_from_saved_state()

void goto_symext::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 
)
virtual

Performs symbolic execution using a state and equation that have already been used to symbolically execute part of the program.

The state is not re-initialized; instead, symbolic execution resumes from the program counter of the saved state.

Parameters
get_goto_functionThe delegate to retrieve function bodies (see get_goto_functiont)
saved_stateThe symbolic execution state to resume from
saved_equationThe equation as previously built up
new_symbol_tableA symbol table to store the symbols added during symbolic execution

Definition at line 308 of file symex_main.cpp.

◆ rewrite_quantifiers()

void goto_symext::rewrite_quantifiers ( exprt expr,
statet state 
)
protected

Definition at line 183 of file symex_main.cpp.

◆ should_stop_unwind()

bool goto_symext::should_stop_unwind ( const symex_targett::sourcet source,
const call_stackt context,
unsigned  unwind 
)
protectedvirtual

Determine whether to unwind a loop.

Parameters
source
context
unwind
Returns
true indicates abort, with false we continue

Reimplemented in symex_bmct.

Definition at line 817 of file symex_goto.cpp.

◆ symex_allocate()

void goto_symext::symex_allocate ( statet state,
const exprt lhs,
const side_effect_exprt code 
)
protectedvirtual

Symbolically execute an assignment instruction that has an allocate on the right hand side.

Parameters
stateSymbolic execution state for current instruction
lhsThe expression to assign to
codeThe allocate expression

Definition at line 49 of file symex_builtin_functions.cpp.

◆ symex_assert()

void goto_symext::symex_assert ( const goto_programt::instructiont instruction,
statet state 
)
protected

Definition at line 86 of file symex_main.cpp.

◆ symex_assign()

void goto_symext::symex_assign ( statet state,
const code_assignt code 
)
protected

Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.

Parameters
stateSymbolic execution state for current instruction
codeThe assignment to execute

Definition at line 28 of file symex_assign.cpp.

◆ symex_assign_array()

void goto_symext::symex_assign_array ( statet state,
const index_exprt lhs,
const exprt full_lhs,
const exprt rhs,
exprt::operandst guard,
assignment_typet  assignment_type 
)
protected

Definition at line 537 of file symex_assign.cpp.

◆ symex_assign_byte_extract()

void goto_symext::symex_assign_byte_extract ( statet state,
const byte_extract_exprt lhs,
const exprt full_lhs,
const exprt rhs,
exprt::operandst guard,
assignment_typet  assignment_type 
)
protected

Definition at line 683 of file symex_assign.cpp.

◆ symex_assign_from_struct()

void goto_symext::symex_assign_from_struct ( statet state,
const ssa_exprt lhs,
const exprt full_lhs,
const struct_exprt rhs,
exprt::operandst guard,
assignment_typet  assignment_type 
)
protected

Assign a struct expression to a symbol.

If symex_assign_symbol was used then we would assign the whole symbol, before extracting its components, with results like x = {1, 2}; x..field1 = x.field1; x..field2 = x.field2; This abbreviates the process, directly producing x..field1 = 1; x..field2 = 2;

Parameters
stategoto-symex state
lhssymbol to assign (already renamed to L1)
full_lhsexpression skeleton corresponding to lhs, to be included in the result trace
rhsstruct expression to assign to lhs
guardguard conjuncts that must hold for this assignment to be made
assignment_typeassignment type (see symex_targett::assignment_typet)

Definition at line 392 of file symex_assign.cpp.

◆ symex_assign_if()

void goto_symext::symex_assign_if ( statet state,
const if_exprt lhs,
const exprt full_lhs,
const exprt rhs,
exprt::operandst guard,
assignment_typet  assignment_type 
)
protected

Definition at line 654 of file symex_assign.cpp.

◆ symex_assign_rec()

void goto_symext::symex_assign_rec ( statet state,
const exprt lhs,
const exprt full_lhs,
const exprt rhs,
exprt::operandst guard,
assignment_typet  assignment_type 
)
protected

Definition at line 123 of file symex_assign.cpp.

◆ symex_assign_struct_member()

void goto_symext::symex_assign_struct_member ( statet state,
const member_exprt lhs,
const exprt full_lhs,
const exprt rhs,
exprt::operandst guard,
assignment_typet  assignment_type 
)
protected

Definition at line 584 of file symex_assign.cpp.

◆ symex_assign_symbol()

void goto_symext::symex_assign_symbol ( statet state,
const ssa_exprt lhs,
const exprt full_lhs,
const exprt rhs,
exprt::operandst guard,
assignment_typet  assignment_type 
)
protected

Definition at line 424 of file symex_assign.cpp.

◆ symex_assign_typecast()

void goto_symext::symex_assign_typecast ( statet state,
const typecast_exprt lhs,
const exprt full_lhs,
const exprt rhs,
exprt::operandst guard,
assignment_typet  assignment_type 
)
protected

Definition at line 520 of file symex_assign.cpp.

◆ symex_assume()

void goto_symext::symex_assume ( statet state,
const exprt cond 
)
protectedvirtual

Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.

Parameters
stateSymbolic execution state for current instruction
condThe guard of the assumption

Definition at line 132 of file symex_main.cpp.

◆ symex_assume_l2()

void goto_symext::symex_assume_l2 ( statet state,
const exprt cond 
)
protected

Definition at line 154 of file symex_main.cpp.

◆ symex_atomic_begin()

void goto_symext::symex_atomic_begin ( statet state)
protectedvirtual

Symbolically execute an ATOMIC_BEGIN instruction.

Parameters
stateSymbolic execution state for current instruction

Definition at line 16 of file symex_atomic_section.cpp.

◆ symex_atomic_end()

void goto_symext::symex_atomic_end ( statet state)
protectedvirtual

Symbolically execute an ATOMIC_END instruction.

Parameters
stateSymbolic execution state for current instruction

Definition at line 36 of file symex_atomic_section.cpp.

◆ symex_catch()

void goto_symext::symex_catch ( statet state)
protected

Symbolically execute a CATCH instruction.

Parameters
stateSymbolic execution state for current instruction

Definition at line 14 of file symex_catch.cpp.

◆ symex_cpp_delete()

void goto_symext::symex_cpp_delete ( statet state,
const codet code 
)
protectedvirtual

Symbolically execute an OTHER instruction that does a CPP delete

Parameters
stateSymbolic execution state for current instruction
codeThe cleaned up CPP delete instruction

Definition at line 475 of file symex_builtin_functions.cpp.

◆ symex_cpp_new()

void goto_symext::symex_cpp_new ( statet state,
const exprt lhs,
const side_effect_exprt code 
)
protectedvirtual

Symbolically execute an assignment instruction that has a CPP new or new array or a Java new array on the right hand side.

Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.

Parameters
stateSymbolic execution state for current instruction
lhsThe expression to assign to
codeThe new expression
stateSymex state
lhsleft-hand side of assignment
coderight-hand side containing side effect

Definition at line 413 of file symex_builtin_functions.cpp.

◆ symex_dead() [1/2]

void goto_symext::symex_dead ( statet state)
protectedvirtual

Symbolically execute a DEAD instruction.

Parameters
stateSymbolic execution state for current instruction

Definition at line 19 of file symex_dead.cpp.

◆ symex_dead() [2/2]

void goto_symext::symex_dead ( statet state,
const symbol_exprt symbol_expr 
)
protected

Kill a symbol, as if it had been the subject of a DEAD instruction.

Parameters
stateSymbolic execution state
symbol_exprSymbol to kill

Definition at line 27 of file symex_dead.cpp.

◆ symex_decl() [1/2]

void goto_symext::symex_decl ( statet state)
protectedvirtual

Symbolically execute a DECL instruction.

Parameters
stateSymbolic execution state for current instruction

Definition at line 20 of file symex_decl.cpp.

◆ symex_decl() [2/2]

void goto_symext::symex_decl ( statet state,
const symbol_exprt expr 
)
protectedvirtual

Symbolically execute a DECL instruction for the given symbol or simulate such an execution for a synthetic symbol.

Parameters
stateSymbolic execution state for current instruction
exprThe symbol being declared

Definition at line 33 of file symex_decl.cpp.

◆ symex_end_of_function()

void goto_symext::symex_end_of_function ( statet state)
protectedvirtual

Symbolically execute a END_FUNCTION instruction.

do function call by inlining

Parameters
stateSymbolic execution state for current instruction

Definition at line 377 of file symex_function_call.cpp.

◆ symex_fkt()

void goto_symext::symex_fkt ( statet state,
const code_function_callt code 
)
protectedvirtual

Symbolically execute a FUNCTION_CALL instruction for a function whose name starts with CPROVER_FKT_PREFIX.

Remarks
While the name seems to imply that this would be called when symbolic execution doesn't know what to do, it may actually be derived from a German abbreviation for function. This should not be called as these functions should already be removed
Parameters
stateSymbolic execution state for current instruction
codeThe function call instruction

Definition at line 517 of file symex_builtin_functions.cpp.

◆ symex_from_entry_point_of()

void goto_symext::symex_from_entry_point_of ( const get_goto_functiont get_goto_function,
symbol_tablet new_symbol_table 
)
virtual

Symbolically execute the entire program starting from entry point.

Remarks
The state that goto_symext maintains uses a lot of memory. This method therefore deallocates the state as soon as symbolic execution has completed. This function is useful to callers that don't care about having the state around afterwards.
Parameters
get_goto_functionThe delegate to retrieve function bodies (see get_goto_functiont)
new_symbol_tableA symbol table to store the symbols added during symbolic execution

Definition at line 387 of file symex_main.cpp.

◆ symex_function_call()

void goto_symext::symex_function_call ( const get_goto_functiont get_goto_function,
statet state,
const code_function_callt code 
)
protectedvirtual

Symbolically execute a FUNCTION_CALL instruction.

Only functions that are symbols are supported, see goto_symext::symex_function_call_symbol.

Parameters
get_goto_functionThe delegate to retrieve function bodies (see get_goto_functiont)
stateSymbolic execution state for current instruction
codeThe function call instruction

Definition at line 174 of file symex_function_call.cpp.

◆ symex_function_call_code()

void goto_symext::symex_function_call_code ( const get_goto_functiont get_goto_function,
statet state,
const code_function_callt call 
)
protectedvirtual

Symbolic execution of a function call by inlining.

Records the call in target by appending a function call step and:

  • if the body is available create a new frame, assigns the parameters, and proceed to executing the code of the function.
  • otherwise assign a nondetministic value to the left-hand-side of the call when there is one
    Parameters
    get_goto_functionThe delegate to retrieve function bodies (see get_goto_functiont)
    stateSymbolic execution state for current instruction
    callThe function call instruction

Definition at line 222 of file symex_function_call.cpp.

◆ symex_function_call_symbol()

void goto_symext::symex_function_call_symbol ( const get_goto_functiont get_goto_function,
statet state,
const code_function_callt code 
)
protectedvirtual

Symbolic execution of a call to a function call.

For functions CBMC_trace and functions starting with __CPROVER_fkt see goto_symext::symex_trace and goto_symext::symex_fkt For non-special functions see goto_symext::symex_function_call_code

Parameters
get_goto_functionThe delegate to retrieve function bodies (see get_goto_functiont)
stateSymbolic execution state for current instruction
codeThe function call instruction

Definition at line 188 of file symex_function_call.cpp.

◆ symex_goto()

void goto_symext::symex_goto ( statet state)
protectedvirtual

Symbolically execute a GOTO instruction.

Parameters
stateSymbolic execution state for current instruction

Definition at line 229 of file symex_goto.cpp.

◆ symex_input()

void goto_symext::symex_input ( statet state,
const codet code 
)
protectedvirtual

Symbolically execute an OTHER instruction that does a CPP input.

Parameters
stateSymbolic execution state for current instruction
codeThe cleaned up input instruction

Definition at line 364 of file symex_builtin_functions.cpp.

◆ symex_other()

void goto_symext::symex_other ( statet state)
protectedvirtual

Symbolically execute an OTHER instruction.

Parameters
stateSymbolic execution state for current instruction

Definition at line 76 of file symex_other.cpp.

◆ symex_output()

void goto_symext::symex_output ( statet state,
const codet code 
)
protectedvirtual

Symbolically execute an OTHER instruction that does a CPP output.

Parameters
stateSymbolic execution state for current instruction
codeThe cleaned up output instruction

Definition at line 386 of file symex_builtin_functions.cpp.

◆ symex_printf()

void goto_symext::symex_printf ( statet state,
const exprt rhs 
)
protectedvirtual

Symbolically execute an OTHER instruction that does a CPP printf

Parameters
stateSymbolic execution state for current instruction
rhsThe cleaned up CPP printf instruction

Definition at line 340 of file symex_builtin_functions.cpp.

◆ symex_start_thread()

void goto_symext::symex_start_thread ( statet state)
protectedvirtual

Symbolically execute a START_THREAD instruction.

Parameters
stateSymbolic execution state for current instruction

Definition at line 17 of file symex_start_thread.cpp.

◆ symex_step()

void goto_symext::symex_step ( const get_goto_functiont get_goto_function,
statet state 
)
protectedvirtual

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.

do just one step

Parameters
get_goto_functionThe delegate to retrieve function bodies (see get_goto_functiont)
stateSymbolic execution state for current instruction

Reimplemented in symex_bmct.

Definition at line 509 of file symex_main.cpp.

◆ symex_threaded_step()

void goto_symext::symex_threaded_step ( statet state,
const get_goto_functiont get_goto_function 
)
protected

Invokes symex_step and verifies whether additional threads can be executed.

Parameters
stateSymbolic execution state for current instruction
get_goto_functionThe delegate to retrieve function bodies (see get_goto_functiont)

Definition at line 227 of file symex_main.cpp.

◆ symex_throw()

void goto_symext::symex_throw ( statet state)
protected

Symbolically execute a THROW instruction.

Parameters
stateSymbolic execution state for current instruction

Definition at line 14 of file symex_throw.cpp.

◆ symex_trace()

void goto_symext::symex_trace ( statet state,
const code_function_callt code 
)
protectedvirtual

Symbolically execute a FUNCTION_CALL instruction for the CBMC_trace function.

Parameters
stateSymbolic execution state for current instruction
codeThe function call instruction

Definition at line 485 of file symex_builtin_functions.cpp.

◆ symex_va_start()

void goto_symext::symex_va_start ( statet state,
const exprt lhs,
const side_effect_exprt code 
)
protectedvirtual

Definition at line 248 of file symex_builtin_functions.cpp.

◆ symex_with_state()

void goto_symext::symex_with_state ( statet state,
const get_goto_functiont get_goto_functions,
symbol_tablet new_symbol_table 
)
virtual

Symbolically execute the entire program starting from entry point.

This method uses the state argument as the symbolic execution state, which is useful for examining the state after this method returns. The state that goto_symext maintains has a large memory footprint, so if keeping the state around is not necessary, clients should instead call goto_symext::symex_from_entry_point_of().

Parameters
stateThe symbolic execution state to use for the execution
get_goto_functionsA functor to retrieve function bodies to execute
new_symbol_tableA symbol table to store the symbols added during symbolic execution

Definition at line 251 of file symex_main.cpp.

◆ trigger_auto_object()

void goto_symext::trigger_auto_object ( const exprt expr,
statet state 
)
protected

Definition at line 78 of file auto_objects.cpp.

◆ try_filter_value_sets()

void goto_symext::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 
)
protected

Try to filter value sets based on whether possible values of a pointer-typed symbol make the condition true or false.

We only do this when there is only one pointer-typed symbol in condition.

Parameters
stateThe current state
conditionThe condition which is being evaluated, which it expects will not have been cleaned or renamed. In practice, it's fine if it has been cleaned and renamed up to level L1.
original_value_setThe value set we will read from
jump_taken_value_setThe value set that will be used when the condition is true, so we remove any elements which we can tell will make the condition false, or nullptr if this shouldn't be done
jump_not_taken_value_setThe value set that will be used when the condition is false, so we remove any elements which we can tell will make the condition true, or nullptr if this shouldn't be done
nsA namespace

Definition at line 692 of file symex_main.cpp.

◆ validate()

void goto_symext::validate ( const validation_modet  vm) const
inline

Definition at line 718 of file goto_symex.h.

◆ vcc()

void goto_symext::vcc ( const exprt condition,
const std::string &  msg,
statet state 
)
protectedvirtual

Definition at line 115 of file symex_main.cpp.

Friends And Related Function Documentation

◆ symex_dereference_statet

friend class symex_dereference_statet
friend

Definition at line 297 of file goto_symex.h.

Member Data Documentation

◆ _remaining_vccs

unsigned goto_symext::_remaining_vccs
protected

Definition at line 696 of file goto_symex.h.

◆ _total_vccs

unsigned goto_symext::_total_vccs
protected

Definition at line 696 of file goto_symex.h.

◆ atomic_section_counter

unsigned goto_symext::atomic_section_counter
protected

A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.

Definition at line 287 of file goto_symex.h.

◆ dynamic_counter

unsigned goto_symext::dynamic_counter =0
staticprotected

A monotonically increasing index for each created dynamic object.

Definition at line 665 of file goto_symex.h.

◆ guard_manager

guard_managert& goto_symext::guard_manager
protected

Used to create guards.

Guards created with different guard managers cannot be combined together, so guards created by goto-symex should not escape the scope of this manager.

Definition at line 280 of file goto_symex.h.

◆ instruction_local_symbols

std::vector<symbol_exprt> goto_symext::instruction_local_symbols
protected

Variables that should be killed at the end of the current symex_step invocation.

Currently this is used for let-bound variables executed during symex, whose lifetime is at most one instruction long.

Definition at line 292 of file goto_symex.h.

◆ language_mode

irep_idt goto_symext::language_mode

language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.

Definition at line 258 of file goto_symex.h.

◆ log

messaget goto_symext::log
mutableprotected

The messaget to write log messages to.

Definition at line 295 of file goto_symex.h.

◆ ns

namespacet goto_symext::ns
protected

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.

That symbol table must be owned by goto_symex_statet rather than passed in, in case the state is saved and resumed. This namespacet is used during symbolic execution to look up names from the original goto-program, and the names of dynamically-created objects.

Definition at line 275 of file goto_symex.h.

◆ outer_symbol_table

const symbol_tablet& goto_symext::outer_symbol_table
protected

The symbol table associated with the goto-program being executed.

This symbol table will not have objects that are dynamically created as part of symbolic execution added to it; those object are stored in the symbol table passed as the new_symbol_table argument to the symex_* methods.

Definition at line 266 of file goto_symex.h.

◆ path_segment_vccs

std::size_t goto_symext::path_segment_vccs

Number of VCCs generated during the run of this goto_symext object.

This member is always initialized to 0 upon construction of this object. It therefore differs from goto_symex_statet::total_vccs, which persists across the creation of several goto_symext objects. When CBMC is run in path-exploration mode, the meaning of this member is "the number of VCCs generated between the last branch point and the current instruction," while goto_symex_statet::total_vccs records the total number of VCCs generated along the entire path from the beginning of the program.

Definition at line 685 of file goto_symex.h.

◆ path_storage

path_storaget& goto_symext::path_storage
protected

Symbolic execution paths to be resumed later.

Remarks
Partially-executed symbolic execution paths whose execution can be resumed later

Definition at line 673 of file goto_symex.h.

◆ should_pause_symex

bool goto_symext::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.

The symbolic execution caller should now choose which successor state to continue executing, and resume symbolic execution from that state.

Definition at line 198 of file goto_symex.h.

◆ symex_config

const symex_configt goto_symext::symex_config
protected

The configuration to use for this symbolic execution.

Definition at line 202 of file goto_symex.h.

◆ target

symex_target_equationt& goto_symext::target
protected

The equation that this execution is building up.

Definition at line 283 of file goto_symex.h.


The documentation for this class was generated from the following files: