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
 
typedef std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
 

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)
 
virtual ~goto_symext ()
 
virtual void symex_from_entry_point_of (const goto_functionst &goto_functions, symbol_tablet &new_symbol_table)
 symex entire program starting from entry point More...
 
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 More...
 
virtual void resume_symex_from_saved_state (const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *const saved_equation, symbol_tablet &new_symbol_table)
 Performs symbolic execution using a state and equation that have already been used to symex part of the program. More...
 
virtual void symex_with_state (statet &, const goto_functionst &, symbol_tablet &)
 symex entire program starting from entry point More...
 
virtual void symex_with_state (statet &, const get_goto_functiont &, symbol_tablet &)
 symex entire program starting from entry point More...
 
virtual void symex_instruction_range (statet &, const goto_functionst &, const irep_idt &function_identifier, goto_programt::const_targett first, goto_programt::const_targett limit)
 Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached. More...
 
virtual void symex_instruction_range (statet &state, const get_goto_functiont &get_goto_function, const irep_idt &function_identifier, goto_programt::const_targett first, goto_programt::const_targett limit)
 Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached. More...
 
virtual void symex_step_goto (statet &, bool taken)
 
unsigned get_total_vccs ()
 
unsigned get_remaining_vccs ()
 

Public Attributes

bool should_pause_symex
 Have states been pushed onto the workqueue? 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

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. More...
 
void symex_threaded_step (statet &, const get_goto_functiont &)
 Invokes symex_step and verifies whether additional threads can be executed. More...
 
virtual void symex_step (const get_goto_functiont &, statet &)
 do just one step More...
 
void clean_expr (exprt &, statet &, bool write)
 
void trigger_auto_object (const exprt &, statet &)
 
void initialize_auto_object (const exprt &, statet &)
 
void process_array_expr (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 &, const bool write)
 
void dereference_rec (exprt &, statet &, guardt &, const bool write)
 
void dereference_rec_address_of (exprt &, statet &, guardt &)
 
exprt address_arithmetic (const exprt &, statet &, guardt &, bool keep_array)
 Evaluate an ID_address_of expression. More...
 
virtual void symex_transition (statet &, goto_programt::const_targett to, bool is_backwards_goto=false)
 
virtual void symex_transition (statet &state)
 
virtual void symex_goto (statet &)
 
virtual void symex_start_thread (statet &)
 
virtual void symex_atomic_begin (statet &)
 
virtual void symex_atomic_end (statet &)
 
virtual void symex_decl (statet &)
 
virtual void symex_decl (statet &, const symbol_exprt &expr)
 
virtual void symex_dead (statet &)
 
virtual void symex_other (statet &)
 
virtual void vcc (const exprt &, const std::string &msg, statet &)
 
virtual void symex_assume (statet &, const exprt &cond)
 
void merge_gotos (statet &)
 
virtual void merge_goto (const statet::goto_statet &goto_state, statet &)
 
void merge_value_sets (const statet::goto_statet &goto_state, statet &dest)
 
void phi_function (const statet::goto_statet &goto_state, statet &)
 
virtual bool get_unwind (const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
 
virtual void loop_bound_exceeded (statet &, const exprt &guard)
 
void pop_frame (statet &)
 pop one call frame More...
 
void return_assignment (statet &)
 
virtual void no_body (const irep_idt &)
 
virtual void symex_function_call (const get_goto_functiont &, statet &, const code_function_callt &)
 
virtual void symex_end_of_function (statet &)
 do function call by inlining More...
 
virtual void symex_function_call_symbol (const get_goto_functiont &, statet &, const code_function_callt &)
 
virtual void symex_function_call_code (const get_goto_functiont &, statet &, const code_function_callt &)
 do function call by inlining More...
 
virtual bool get_unwind_recursion (const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
 
void parameter_assignments (const irep_idt function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
 
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 identifiers More...
 
void add_end_of_function (exprt &code, const irep_idt &identifier)
 
nondet_symbol_exprt build_symex_nondet (typet &type)
 
void symex_throw (statet &)
 
void symex_catch (statet &)
 
virtual void do_simplify (exprt &)
 
void symex_assign (statet &, const code_assignt &)
 
void havoc_rec (statet &, const guardt &, const exprt &)
 
void symex_assign_rec (statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
 
void symex_assign_symbol (statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
 
void symex_assign_typecast (statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
 
void symex_assign_array (statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
 
void symex_assign_struct_member (statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
 
void symex_assign_if (statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
 
void symex_assign_byte_extract (statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
 
virtual void symex_gcc_builtin_va_arg_next (statet &, const exprt &lhs, const side_effect_exprt &)
 
virtual void symex_allocate (statet &, const exprt &lhs, const side_effect_exprt &)
 
virtual void symex_cpp_delete (statet &, const codet &)
 
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. More...
 
virtual void symex_fkt (statet &, const code_function_callt &)
 
virtual void symex_macro (statet &, const code_function_callt &)
 
virtual void symex_trace (statet &, const code_function_callt &)
 
virtual void symex_printf (statet &, const exprt &rhs)
 
virtual void symex_input (statet &, const codet &)
 
virtual void symex_output (statet &, const codet &)
 
void read (exprt &)
 
void replace_nondet (exprt &)
 
void rewrite_quantifiers (exprt &, statet &)
 

Static Protected Member Functions

static bool is_index_member_symbol_if (const exprt &expr)
 
static exprt add_to_lhs (const exprt &lhs, const exprt &what)
 

Protected Attributes

const unsigned max_depth
 
const bool doing_path_exploration
 
const bool allow_pointer_unsoundness
 
const bool constant_propagation
 
const bool self_loops_to_assumptions
 
const bool simplify_opt
 
const bool unwinding_assertions
 
const bool partial_loops
 
const std::string debug_level
 
const symbol_tabletouter_symbol_table
 The symbol table associated with the goto-program that we're executing. 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...
 
symex_target_equationttarget
 
unsigned atomic_section_counter
 
messaget log
 
const irep_idt guard_identifier
 
path_storagetpath_storage
 
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 symex has ended, so that bmct can read those values even after the state has been deallocated.

unsigned _total_vccs
 
unsigned _remaining_vccs
 

Static Protected Attributes

static unsigned nondet_count =0
 
static unsigned dynamic_counter =0
 

Friends

class symex_dereference_statet
 

Detailed Description

The main class for the forward symbolic simulator.

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

Definition at line 46 of file goto_symex.h.

Member Typedef Documentation

◆ assignment_typet

Definition at line 403 of file goto_symex.h.

◆ get_goto_functiont

Definition at line 89 of file goto_symex.h.

◆ statet

Definition at line 49 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 
)
inline

Definition at line 51 of file goto_symex.h.

◆ ~goto_symext()

virtual goto_symext::~goto_symext ( )
inlinevirtual

Definition at line 83 of file goto_symex.h.

Member Function Documentation

◆ add_end_of_function()

void goto_symext::add_end_of_function ( exprt code,
const irep_idt identifier 
)
protected

◆ add_to_lhs()

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

Definition at line 94 of file symex_assign.cpp.

◆ address_arithmetic()

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

Evaluate an ID_address_of expression.

Definition at line 92 of file symex_dereference.cpp.

◆ build_symex_nondet()

nondet_symbol_exprt goto_symext::build_symex_nondet ( typet type)
protected

Definition at line 25 of file goto_symex.cpp.

◆ clean_expr()

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

Definition at line 138 of file symex_clean_expr.cpp.

◆ dereference()

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

Definition at line 378 of file symex_dereference.cpp.

◆ dereference_rec()

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

Definition at line 248 of file symex_dereference.cpp.

◆ dereference_rec_address_of()

void goto_symext::dereference_rec_address_of ( exprt expr,
statet state,
guardt guard 
)
protected

Definition at line 26 of file symex_dereference.cpp.

◆ do_simplify()

void goto_symext::do_simplify ( exprt expr)
protectedvirtual

Definition at line 19 of file goto_symex.cpp.

◆ get_remaining_vccs()

unsigned goto_symext::get_remaining_vccs ( )
inline

Definition at line 513 of file goto_symex.h.

◆ get_total_vccs()

unsigned goto_symext::get_total_vccs ( )
inline

Definition at line 504 of file goto_symex.h.

◆ get_unwind()

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

Reimplemented in symex_bmct.

Definition at line 540 of file symex_goto.cpp.

◆ get_unwind_recursion()

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

Reimplemented in symex_bmct.

Definition at line 21 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 20 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()

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

Initialise the symbolic execution and the given state with pc as entry point.

Parameters
stateSymex state to initialise.
get_goto_functionproducer for GOTO functions
function_identifierThe function in which the instructions are
pcfirst instruction to symex
limitfinal instruction, which itself will not be symexed.

Definition at line 121 of file symex_main.cpp.

◆ is_index_member_symbol_if()

bool goto_symext::is_index_member_symbol_if ( const exprt expr)
staticprotected

Definition at line 66 of file symex_dereference.cpp.

◆ locality()

void goto_symext::locality ( const irep_idt  function_identifier,
statet state,
const goto_functionst::goto_functiont goto_function 
)
protected

preserves locality of local variables of a given function by applying L1 renaming to the local identifiers

Definition at line 370 of file symex_function_call.cpp.

◆ loop_bound_exceeded()

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

Definition at line 507 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 statet::goto_statet goto_state,
statet state 
)
protectedvirtual

Reimplemented in symex_bmct.

Definition at line 346 of file symex_goto.cpp.

◆ merge_gotos()

void goto_symext::merge_gotos ( statet state)
protected

Definition at line 322 of file symex_goto.cpp.

◆ merge_value_sets()

void goto_symext::merge_value_sets ( const statet::goto_statet goto_state,
statet dest 
)
protected

Definition at line 368 of file symex_goto.cpp.

◆ no_body()

virtual void goto_symext::no_body ( const irep_idt )
inlineprotectedvirtual

Reimplemented in symex_bmct.

Definition at line 349 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

Definition at line 29 of file symex_function_call.cpp.

◆ phi_function()

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

Definition at line 381 of file symex_goto.cpp.

◆ pop_frame()

void goto_symext::pop_frame ( statet state)
protected

pop one call frame

Definition at line 318 of file symex_function_call.cpp.

◆ process_array_expr()

void goto_symext::process_array_expr ( 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 24 of file symex_clean_expr.cpp.

◆ read()

void goto_symext::read ( exprt )
protected

◆ replace_nondet()

void goto_symext::replace_nondet ( exprt expr)
protected

Definition at line 32 of file goto_symex.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 *const  saved_equation,
symbol_tablet new_symbol_table 
)
virtual

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

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

Definition at line 229 of file symex_main.cpp.

◆ return_assignment()

void goto_symext::return_assignment ( statet state)
protected

Definition at line 427 of file symex_function_call.cpp.

◆ rewrite_quantifiers()

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

Definition at line 106 of file symex_main.cpp.

◆ symex_allocate()

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

Definition at line 44 of file symex_builtin_functions.cpp.

◆ symex_assign()

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

Definition at line 24 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,
guardt guard,
assignment_typet  assignment_type 
)
protected

Definition at line 308 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,
guardt guard,
assignment_typet  assignment_type 
)
protected

Definition at line 459 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,
guardt guard,
assignment_typet  assignment_type 
)
protected

Definition at line 426 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,
guardt guard,
assignment_typet  assignment_type 
)
protected

Definition at line 128 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,
guardt guard,
assignment_typet  assignment_type 
)
protected

Definition at line 355 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,
guardt guard,
assignment_typet  assignment_type 
)
protected

Definition at line 210 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,
guardt guard,
assignment_typet  assignment_type 
)
protected

Definition at line 290 of file symex_assign.cpp.

◆ symex_assume()

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

Definition at line 77 of file symex_main.cpp.

◆ symex_atomic_begin()

void goto_symext::symex_atomic_begin ( statet state)
protectedvirtual

Definition at line 16 of file symex_atomic_section.cpp.

◆ symex_atomic_end()

void goto_symext::symex_atomic_end ( statet state)
protectedvirtual

Definition at line 36 of file symex_atomic_section.cpp.

◆ symex_catch()

void goto_symext::symex_catch ( statet )
protected

Definition at line 14 of file symex_catch.cpp.

◆ symex_cpp_delete()

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

Definition at line 445 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

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

Parameters
stateSymex state
lhsleft-hand side of assignment
coderight-hand side containing side effect

Definition at line 383 of file symex_builtin_functions.cpp.

◆ symex_dead()

void goto_symext::symex_dead ( statet state)
protectedvirtual

Definition at line 20 of file symex_dead.cpp.

◆ symex_decl() [1/2]

void goto_symext::symex_decl ( statet state)
protectedvirtual

Definition at line 22 of file symex_decl.cpp.

◆ symex_decl() [2/2]

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

Definition at line 35 of file symex_decl.cpp.

◆ symex_end_of_function()

void goto_symext::symex_end_of_function ( statet state)
protectedvirtual

do function call by inlining

Definition at line 359 of file symex_function_call.cpp.

◆ symex_fkt()

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

Definition at line 493 of file symex_builtin_functions.cpp.

◆ symex_from_entry_point_of() [1/2]

void goto_symext::symex_from_entry_point_of ( const goto_functionst goto_functions,
symbol_tablet new_symbol_table 
)
virtual

symex entire program starting from entry point

The state that goto_symext maintains has a large memory footprint. This method deallocates the state as soon as symbolic execution has completed, so use it if you don't care about having the state around afterwards.

Definition at line 280 of file symex_main.cpp.

◆ symex_from_entry_point_of() [2/2]

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

symex entire program starting from entry point

The state that goto_symext maintains has a large memory footprint. This method deallocates the state as soon as symbolic execution has completed, so use it if you don't care about having the state around afterwards.

Definition at line 288 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

Definition at line 170 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

do function call by inlining

Definition at line 213 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

Definition at line 184 of file symex_function_call.cpp.

◆ symex_gcc_builtin_va_arg_next()

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

Definition at line 224 of file symex_builtin_functions.cpp.

◆ symex_goto()

void goto_symext::symex_goto ( statet state)
protectedvirtual

Definition at line 23 of file symex_goto.cpp.

◆ symex_input()

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

Definition at line 330 of file symex_builtin_functions.cpp.

◆ symex_instruction_range() [1/2]

void goto_symext::symex_instruction_range ( statet state,
const goto_functionst goto_functions,
const irep_idt function_identifier,
goto_programt::const_targett  first,
goto_programt::const_targett  limit 
)
virtual

Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached.

This is useful to explicitly symex certain ranges of a program, e.g. in an incremental decision procedure.

Parameters
stateSymex state to start with.
goto_functionsGOTO model to symex.
function_identifierThe function with the instruction range
firstEntry point in form of a first instruction.
limitFinal instruction, which itself will not be symexed.

Definition at line 251 of file symex_main.cpp.

◆ symex_instruction_range() [2/2]

void goto_symext::symex_instruction_range ( statet state,
const get_goto_functiont get_goto_function,
const irep_idt function_identifier,
goto_programt::const_targett  first,
goto_programt::const_targett  limit 
)
virtual

Symexes from the first instruction and the given state, terminating as soon as the last instruction is reached.

This is useful to explicitly symex certain ranges of a program, e.g. in an incremental decision procedure.

Parameters
stateSymex state to start with.
get_goto_functionretrieves a function body
function_identifierThe function with the instruction range
firstEntry point in form of a first instruction.
limitFinal instruction, which itself will not be symexed.

Definition at line 266 of file symex_main.cpp.

◆ symex_macro()

void goto_symext::symex_macro ( statet ,
const code_function_callt code 
)
protectedvirtual

Definition at line 518 of file symex_builtin_functions.cpp.

◆ symex_other()

void goto_symext::symex_other ( statet state)
protectedvirtual

Definition at line 77 of file symex_other.cpp.

◆ symex_output()

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

Definition at line 354 of file symex_builtin_functions.cpp.

◆ symex_printf()

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

Definition at line 305 of file symex_builtin_functions.cpp.

◆ symex_start_thread()

void goto_symext::symex_start_thread ( statet state)
protectedvirtual

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

do just one step

Reimplemented in symex_bmct.

Definition at line 316 of file symex_main.cpp.

◆ symex_step_goto()

void goto_symext::symex_step_goto ( statet state,
bool  taken 
)
virtual

Definition at line 305 of file symex_goto.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
stateCurrent GOTO symex step.
get_goto_functionfunction that retrieves function bodies

Definition at line 150 of file symex_main.cpp.

◆ symex_throw()

void goto_symext::symex_throw ( statet state)
protected

Definition at line 14 of file symex_throw.cpp.

◆ symex_trace()

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

Definition at line 455 of file symex_builtin_functions.cpp.

◆ symex_transition() [1/2]

void goto_symext::symex_transition ( statet state,
goto_programt::const_targett  to,
bool  is_backwards_goto = false 
)
protectedvirtual

Definition at line 25 of file symex_main.cpp.

◆ symex_transition() [2/2]

virtual void goto_symext::symex_transition ( statet state)
inlineprotectedvirtual

Definition at line 297 of file goto_symex.h.

◆ symex_with_state() [1/2]

void goto_symext::symex_with_state ( statet state,
const goto_functionst goto_functions,
symbol_tablet new_symbol_table 
)
virtual

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

Definition at line 183 of file symex_main.cpp.

◆ symex_with_state() [2/2]

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

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

Definition at line 194 of file symex_main.cpp.

◆ trigger_auto_object()

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

Definition at line 83 of file auto_objects.cpp.

◆ vcc()

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

Definition at line 49 of file symex_main.cpp.

Friends And Related Function Documentation

◆ symex_dereference_statet

friend class symex_dereference_statet
friend

Definition at line 253 of file goto_symex.h.

Member Data Documentation

◆ _remaining_vccs

unsigned goto_symext::_remaining_vccs
protected

Definition at line 500 of file goto_symex.h.

◆ _total_vccs

unsigned goto_symext::_total_vccs
protected

Definition at line 500 of file goto_symex.h.

◆ allow_pointer_unsoundness

const bool goto_symext::allow_pointer_unsoundness
protected

Definition at line 215 of file goto_symex.h.

◆ atomic_section_counter

unsigned goto_symext::atomic_section_counter
protected

Definition at line 249 of file goto_symex.h.

◆ constant_propagation

const bool goto_symext::constant_propagation
protected

Definition at line 226 of file goto_symex.h.

◆ debug_level

const std::string goto_symext::debug_level
protected

Definition at line 231 of file goto_symex.h.

◆ doing_path_exploration

const bool goto_symext::doing_path_exploration
protected

Definition at line 214 of file goto_symex.h.

◆ dynamic_counter

unsigned goto_symext::dynamic_counter =0
staticprotected

Definition at line 472 of file goto_symex.h.

◆ guard_identifier

const irep_idt goto_symext::guard_identifier
protected

Definition at line 289 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 223 of file goto_symex.h.

◆ log

messaget goto_symext::log
mutableprotected

Definition at line 251 of file goto_symex.h.

◆ max_depth

const unsigned goto_symext::max_depth
protected

Definition at line 213 of file goto_symex.h.

◆ nondet_count

unsigned goto_symext::nondet_count =0
staticprotected

Definition at line 471 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 247 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 that we're executing.

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

Definition at line 238 of file goto_symex.h.

◆ partial_loops

const bool goto_symext::partial_loops
protected

Definition at line 230 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 490 of file goto_symex.h.

◆ path_storage

path_storaget& goto_symext::path_storage
protected

Definition at line 478 of file goto_symex.h.

◆ self_loops_to_assumptions

const bool goto_symext::self_loops_to_assumptions
protected

Definition at line 227 of file goto_symex.h.

◆ should_pause_symex

bool goto_symext::should_pause_symex

Have states been pushed onto the workqueue?

If this flag is set at the end of a symbolic execution run, it means that symex 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 symex from that state.

Definition at line 184 of file goto_symex.h.

◆ simplify_opt

const bool goto_symext::simplify_opt
protected

Definition at line 228 of file goto_symex.h.

◆ target

symex_target_equationt& goto_symext::target
protected

Definition at line 248 of file goto_symex.h.

◆ unwinding_assertions

const bool goto_symext::unwinding_assertions
protected

Definition at line 229 of file goto_symex.h.


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