cprover
goto_symext Class Reference

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

#include <goto_symex.h>

Inheritance diagram for goto_symext:
[legend]
Collaboration diagram for goto_symext:
[legend]

Public Types

typedef goto_symex_statet statet
 

Public Member Functions

 goto_symext (const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)
 
virtual ~goto_symext ()
 
virtual void operator() (const goto_functionst &goto_functions)
 symex all at once, starting from entry point More...
 
virtual void operator() (const goto_functionst &goto_functions, const goto_programt &goto_program)
 symex starting from given goto program More...
 
virtual void operator() (statet &state, const goto_functionst &goto_functions, const goto_programt &goto_program)
 start symex in a given state More...
 
virtual void symex_step (const goto_functionst &goto_functions, statet &state)
 execute just one step More...
 
virtual void symex_step_goto (statet &state, bool taken)
 

Public Attributes

unsigned total_vccs
 
unsigned remaining_vccs
 
bool constant_propagation
 
optionst options
 
symbol_tabletnew_symbol_table
 
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...
 

Protected Types

typedef symex_targett::assignment_typet assignment_typet
 

Protected Member Functions

void new_name (symbolt &symbol)
 
void clean_expr (exprt &expr, statet &state, bool write)
 
void replace_array_equal (exprt &expr)
 
void trigger_auto_object (const exprt &expr, statet &state)
 
void initialize_auto_object (const exprt &expr, statet &state)
 
void process_array_expr (exprt &expr)
 
void process_array_expr_rec (exprt &expr, const typet &type) const
 
exprt make_auto_object (const typet &type)
 
virtual void dereference (exprt &expr, statet &state, const bool write)
 
void dereference_rec (exprt &expr, statet &state, guardt &guard, const bool write)
 
void dereference_rec_address_of (exprt &expr, statet &state, guardt &guard)
 
exprt address_arithmetic (const exprt &expr, statet &state, guardt &guard, bool keep_array)
 Evaluate an ID_address_of expression. More...
 
virtual void symex_transition (statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)
 
virtual void symex_transition (statet &state)
 
virtual void symex_goto (statet &state)
 
virtual void symex_start_thread (statet &state)
 
virtual void symex_atomic_begin (statet &state)
 
virtual void symex_atomic_end (statet &state)
 
virtual void symex_decl (statet &state)
 
virtual void symex_decl (statet &state, const symbol_exprt &expr)
 
virtual void symex_dead (statet &state)
 
virtual void symex_other (const goto_functionst &goto_functions, statet &state)
 
virtual void vcc (const exprt &expr, const std::string &msg, statet &state)
 
virtual void symex_assume (statet &state, const exprt &cond)
 
void merge_gotos (statet &state)
 
virtual void merge_goto (const statet::goto_statet &goto_state, statet &state)
 
void merge_value_sets (const statet::goto_statet &goto_state, statet &dest)
 
void phi_function (const statet::goto_statet &goto_state, statet &state)
 
virtual bool get_unwind (const symex_targett::sourcet &source, unsigned unwind)
 
virtual void loop_bound_exceeded (statet &state, const exprt &guard)
 
void pop_frame (statet &state)
 pop one call frame More...
 
void return_assignment (statet &state)
 
virtual void no_body (const irep_idt &identifier)
 
virtual void symex_function_call (const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
 
virtual void symex_end_of_function (statet &state)
 do function call by inlining More...
 
virtual void symex_function_call_symbol (const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
 
virtual void symex_function_call_code (const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
 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 &goto_function, statet &state, const exprt::operandst &arguments)
 
void locality (const irep_idt function_identifier, statet &state, const goto_functionst::goto_functiont &goto_function)
 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)
 
void symex_throw (statet &state)
 
void symex_catch (statet &state)
 
virtual void do_simplify (exprt &expr)
 
void symex_assign_rec (statet &state, const code_assignt &code)
 
virtual void symex_assign (statet &state, const code_assignt &code)
 
void symex_assign_rec (statet &state, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
 
void symex_assign_symbol (statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
 
void symex_assign_typecast (statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
 
void symex_assign_array (statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
 
void symex_assign_struct_member (statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
 
void symex_assign_if (statet &state, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
 
void symex_assign_byte_extract (statet &state, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
 
virtual void symex_gcc_builtin_va_arg_next (statet &state, const exprt &lhs, const side_effect_exprt &code)
 
virtual void symex_malloc (statet &state, const exprt &lhs, const side_effect_exprt &code)
 
virtual void symex_cpp_delete (statet &state, const codet &code)
 
virtual void symex_cpp_new (statet &state, const exprt &lhs, const side_effect_exprt &code)
 
virtual void symex_fkt (statet &state, const code_function_callt &code)
 
virtual void symex_macro (statet &state, const code_function_callt &code)
 
virtual void symex_trace (statet &state, const code_function_callt &code)
 
virtual void symex_printf (statet &state, const exprt &lhs, const exprt &rhs)
 
virtual void symex_input (statet &state, const codet &code)
 
virtual void symex_output (statet &state, const codet &code)
 
void read (exprt &expr)
 
void replace_nondet (exprt &expr)
 
void rewrite_quantifiers (exprt &expr, statet &state)
 

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 namespacetns
 
symex_targetttarget
 
unsigned atomic_section_counter
 
irep_idt guard_identifier
 

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.

Definition at line 41 of file goto_symex.h.

Member Typedef Documentation

§ assignment_typet

Definition at line 265 of file goto_symex.h.

§ statet

Definition at line 66 of file goto_symex.h.

Constructor & Destructor Documentation

§ goto_symext()

goto_symext::goto_symext ( const namespacet _ns,
symbol_tablet _new_symbol_table,
symex_targett _target 
)
inline

Definition at line 44 of file goto_symex.h.

References options, and optionst::set_option().

§ ~goto_symext()

virtual goto_symext::~goto_symext ( )
inlinevirtual

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

Referenced by no_body().

§ add_to_lhs()

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

§ address_arithmetic()

§ clean_expr()

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

§ dereference()

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

§ dereference_rec()

§ dereference_rec_address_of()

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

§ do_simplify()

§ get_unwind()

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

Reimplemented in symex_bmct.

Definition at line 412 of file symex_goto.cpp.

Referenced by symex_goto(), and symex_transition().

§ 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 29 of file symex_function_call.cpp.

Referenced by no_body(), and symex_function_call_code().

§ initialize_auto_object()

§ is_index_member_symbol_if()

bool goto_symext::is_index_member_symbol_if ( const exprt expr)
staticprotected

Definition at line 67 of file symex_dereference.cpp.

References irept::id(), to_if_expr(), to_index_expr(), and to_member_expr().

§ locality()

§ loop_bound_exceeded()

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

§ make_auto_object()

exprt goto_symext::make_auto_object ( const typet type)
protected

§ merge_goto()

§ merge_gotos()

void goto_symext::merge_gotos ( statet state)
protected

§ merge_value_sets()

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

§ new_name()

void goto_symext::new_name ( symbolt symbol)
protected

Definition at line 47 of file symex_main.cpp.

References symbol_tablet::add(), get_new_name(), new_symbol_table, and ns.

§ no_body()

§ operator()() [1/3]

void goto_symext::operator() ( const goto_functionst goto_functions)
virtual

symex all at once, starting from entry point

symex from entry point

Definition at line 174 of file symex_main.cpp.

References goto_functions_templatet< goto_programt >::entry_point(), and goto_functions_templatet< bodyT >::function_map.

Referenced by operator()().

§ operator()() [2/3]

void goto_symext::operator() ( const goto_functionst goto_functions,
const goto_programt goto_program 
)
virtual

symex starting from given goto program

symex starting from given program

Definition at line 165 of file symex_main.cpp.

References operator()().

§ operator()() [3/3]

§ parameter_assignments()

§ phi_function()

§ pop_frame()

§ process_array_expr()

§ process_array_expr_rec()

§ read()

void goto_symext::read ( exprt expr)
protected

§ replace_array_equal()

void goto_symext::replace_array_equal ( exprt expr)
protected

§ replace_nondet()

void goto_symext::replace_nondet ( exprt expr)
protected

§ return_assignment()

§ rewrite_quantifiers()

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

§ symex_assign()

§ 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

§ 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

§ 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

§ symex_assign_rec() [1/2]

§ symex_assign_rec() [2/2]

§ 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

§ symex_assign_symbol()

§ 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

§ symex_assume()

§ symex_atomic_begin()

§ symex_atomic_end()

§ symex_catch()

void goto_symext::symex_catch ( statet state)
protected

§ symex_cpp_delete()

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

Definition at line 424 of file symex_builtin_functions.cpp.

Referenced by symex_other().

§ symex_cpp_new()

§ symex_dead()

§ symex_decl() [1/2]

void goto_symext::symex_decl ( statet state)
protectedvirtual

§ symex_decl() [2/2]

§ symex_end_of_function()

void goto_symext::symex_end_of_function ( statet state)
protectedvirtual

§ symex_fkt()

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

Definition at line 470 of file symex_builtin_functions.cpp.

References Forall_operands, and exprt::reserve_operands().

Referenced by symex_function_call_symbol().

§ symex_function_call()

void goto_symext::symex_function_call ( const goto_functionst goto_functions,
statet state,
const code_function_callt call 
)
protectedvirtual

Definition at line 172 of file symex_function_call.cpp.

References code_function_callt::function(), and symex_function_call_symbol().

Referenced by no_body(), and symex_step().

§ symex_function_call_code()

§ symex_function_call_symbol()

§ symex_gcc_builtin_va_arg_next()

§ symex_goto()

§ symex_input()

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

§ symex_macro()

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

§ symex_malloc()

§ symex_other()

§ symex_output()

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

§ symex_printf()

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

§ symex_start_thread()

§ symex_step()

§ symex_step_goto()

§ symex_throw()

void goto_symext::symex_throw ( statet state)
protected

§ symex_trace()

§ symex_transition() [1/2]

§ symex_transition() [2/2]

§ trigger_auto_object()

§ vcc()

Friends And Related Function Documentation

§ symex_dereference_statet

friend class symex_dereference_statet
friend

Definition at line 108 of file goto_symex.h.

Member Data Documentation

§ atomic_section_counter

unsigned goto_symext::atomic_section_counter
protected

Definition at line 106 of file goto_symex.h.

Referenced by symex_atomic_begin().

§ constant_propagation

bool goto_symext::constant_propagation

Definition at line 94 of file goto_symex.h.

Referenced by bmct::bmct(), scratch_programt::check_sat(), and symex_assign_symbol().

§ dynamic_counter

unsigned goto_symext::dynamic_counter =0
staticprotected

Definition at line 334 of file goto_symex.h.

Referenced by make_auto_object(), symex_cpp_new(), and symex_malloc().

§ guard_identifier

irep_idt goto_symext::guard_identifier
protected

Definition at line 152 of file goto_symex.h.

Referenced by phi_function(), and symex_goto().

§ 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 101 of file goto_symex.h.

Referenced by dereference_rec(), and bmct::run().

§ new_symbol_table

§ nondet_count

unsigned goto_symext::nondet_count =0
staticprotected

Definition at line 333 of file goto_symex.h.

Referenced by replace_nondet().

§ ns

§ options

§ remaining_vccs

unsigned goto_symext::remaining_vccs

Definition at line 92 of file goto_symex.h.

Referenced by bmct::run(), and vcc().

§ target

§ total_vccs

unsigned goto_symext::total_vccs

Definition at line 92 of file goto_symex.h.

Referenced by bmct::run(), and vcc().


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