cprover
|
#include <interpreter_class.h>
Classes | |
class | memory_cellt |
class | stack_framet |
Public Member Functions | |
interpretert (const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions) | |
void | operator() () |
Protected Types | |
typedef std::unordered_map< irep_idt, unsigned, irep_id_hash > | memory_mapt |
typedef std::vector< memory_cellt > | memoryt |
typedef std::stack< stack_framet > | call_stackt |
Protected Member Functions | |
void | build_memory_map () |
void | build_memory_map (const symbolt &symbol) |
unsigned | get_size (const typet &type) const |
void | step () |
void | execute_assert () |
void | execute_assume () |
void | execute_assign () |
void | execute_goto () |
void | execute_function_call () |
void | execute_other () |
void | execute_decl () |
void | assign (mp_integer address, const std::vector< mp_integer > &rhs) |
void | read (mp_integer address, std::vector< mp_integer > &dest) const |
void | command () |
bool | evaluate_boolean (const exprt &expr) const |
void | evaluate (const exprt &expr, std::vector< mp_integer > &dest) const |
mp_integer | evaluate_address (const exprt &expr) const |
void | show_state () |
Protected Attributes | |
const symbol_tablet & | symbol_table |
const namespacet | ns |
const goto_functionst & | goto_functions |
memory_mapt | memory_map |
memoryt | memory |
std::size_t | stack_pointer |
call_stackt | call_stack |
goto_functionst::function_mapt::const_iterator | function |
goto_programt::const_targett | PC |
goto_programt::const_targett | next_PC |
bool | done |
Definition at line 21 of file interpreter_class.h.
|
protected |
Definition at line 89 of file interpreter_class.h.
|
protected |
Definition at line 40 of file interpreter_class.h.
|
protected |
Definition at line 51 of file interpreter_class.h.
|
inline |
Definition at line 24 of file interpreter_class.h.
|
protected |
Definition at line 233 of file interpreter.cpp.
References interpretert::memory_cellt::identifier, integer2unsigned(), memory, interpretert::memory_cellt::offset, and interpretert::memory_cellt::value.
Referenced by execute_assign(), execute_function_call(), and step().
|
protected |
Definition at line 363 of file interpreter.cpp.
References memory, stack_pointer, symbol_table, and symbol_tablet::symbols.
Referenced by operator()().
|
protected |
Definition at line 378 of file interpreter.cpp.
References get_size(), irept::id(), interpretert::memory_cellt::identifier, symbolt::is_static_lifetime, memory, memory_map, symbolt::name, interpretert::memory_cellt::offset, symbolt::type, and interpretert::memory_cellt::value.
|
protected |
Definition at line 69 of file interpreter.cpp.
Referenced by operator()().
|
protected |
Definition at line 41 of file interpreter_evaluate.cpp.
References binary2integer(), evaluate_address(), forall_operands, from_expr(), fixedbvt::from_expr(), ieee_floatt::from_expr(), fixedbvt::from_integer(), ieee_floatt::from_integer(), function, get_size(), fixedbvt::get_value(), irept::id(), id2string(), integer2binary(), exprt::is_true(), ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), ieee_floatt::pack(), power(), read(), fixedbvt::set_value(), fixedbvt::spec, to_constant_expr(), to_fixedbv_type(), to_floatbv_type(), to_integer(), to_signedbv_type(), to_unsignedbv_type(), exprt::type(), and ieee_floatt::unpack().
Referenced by evaluate_address(), evaluate_boolean(), execute_assign(), execute_function_call(), execute_other(), and step().
|
protected |
Definition at line 408 of file interpreter_evaluate.cpp.
References call_stack, struct_union_typet::components(), evaluate(), namespace_baset::follow(), from_expr(), function, irept::get(), member_exprt::get_component_name(), get_size(), irept::id(), memory_map, ns, exprt::op0(), exprt::op1(), exprt::operands(), to_member_expr(), to_struct_type(), and exprt::type().
Referenced by evaluate(), execute_assign(), and execute_function_call().
|
inlineprotected |
Definition at line 96 of file interpreter_class.h.
References evaluate().
Referenced by execute_assert(), execute_assume(), and execute_goto().
|
protected |
Definition at line 255 of file interpreter.cpp.
References evaluate_boolean(), and PC.
Referenced by step().
|
protected |
Definition at line 211 of file interpreter.cpp.
References assign(), evaluate(), evaluate_address(), get_size(), code_assignt::lhs(), PC, code_assignt::rhs(), to_code_assign(), and exprt::type().
Referenced by step().
|
protected |
Definition at line 249 of file interpreter.cpp.
References evaluate_boolean(), and PC.
Referenced by step().
|
protected |
|
protected |
Definition at line 261 of file interpreter.cpp.
References code_function_callt::arguments(), assign(), call_stack, evaluate(), evaluate_address(), code_function_callt::function(), goto_functions_templatet< bodyT >::function_map, code_typet::parametert::get_identifier(), get_local_identifiers(), get_size(), goto_functions, id2string(), interpretert::memory_cellt::identifier, integer2size_t(), irept::is_not_nil(), code_function_callt::lhs(), interpretert::stack_framet::local_map, namespacet::lookup(), memory, next_PC, ns, interpretert::stack_framet::old_stack_pointer, code_typet::parameters(), PC, interpretert::stack_framet::return_function, interpretert::stack_framet::return_PC, interpretert::stack_framet::return_value_address, irept::set(), stack_pointer, to_code_function_call(), to_code_type(), symbolt::type, and exprt::type().
Referenced by step().
|
protected |
Definition at line 178 of file interpreter.cpp.
References evaluate_boolean(), next_PC, and PC.
Referenced by step().
|
protected |
Definition at line 192 of file interpreter.cpp.
References evaluate(), id2string(), and PC.
Referenced by step().
|
protected |
Definition at line 407 of file interpreter.cpp.
References struct_union_typet::components(), irept::find(), namespace_baset::follow(), irept::id(), integer2unsigned(), ns, typet::subtype(), to_integer(), to_struct_type(), and to_union_type().
Referenced by build_memory_map(), evaluate(), evaluate_address(), execute_assign(), and execute_function_call().
void interpretert::operator() | ( | void | ) |
Definition at line 24 of file interpreter.cpp.
References goto_function_templatet< bodyT >::body, goto_function_templatet< bodyT >::body_available(), build_memory_map(), command(), done, goto_functions_templatet< goto_programt >::entry_point(), goto_functions_templatet< bodyT >::function_map, goto_functions, PC, show_state(), and step().
|
protected |
Definition at line 21 of file interpreter_evaluate.cpp.
References integer2size_t(), and memory.
Referenced by evaluate().
|
protected |
Definition at line 53 of file interpreter.cpp.
References function, ns, and PC.
Referenced by operator()().
|
protected |
Definition at line 85 of file interpreter.cpp.
References ASSERT, ASSIGN, assign(), ASSUME, ATOMIC_BEGIN, ATOMIC_END, call_stack, DEAD, DECL, done, END_FUNCTION, END_THREAD, evaluate(), execute_assert(), execute_assign(), execute_assume(), execute_decl(), execute_function_call(), execute_goto(), execute_other(), function, FUNCTION_CALL, GOTO, LOCATION, next_PC, OTHER, PC, RETURN, SKIP, stack_pointer, and START_THREAD.
Referenced by operator()().
|
protected |
Definition at line 90 of file interpreter_class.h.
Referenced by evaluate_address(), execute_function_call(), and step().
|
protected |
Definition at line 94 of file interpreter_class.h.
Referenced by command(), operator()(), and step().
|
protected |
Definition at line 92 of file interpreter_class.h.
Referenced by evaluate(), evaluate_address(), show_state(), and step().
|
protected |
Definition at line 38 of file interpreter_class.h.
Referenced by execute_function_call(), and operator()().
|
protected |
Definition at line 52 of file interpreter_class.h.
Referenced by assign(), build_memory_map(), execute_function_call(), and read().
|
protected |
Definition at line 41 of file interpreter_class.h.
Referenced by build_memory_map(), and evaluate_address().
|
protected |
Definition at line 93 of file interpreter_class.h.
Referenced by execute_function_call(), execute_goto(), and step().
|
protected |
Definition at line 37 of file interpreter_class.h.
Referenced by evaluate(), evaluate_address(), execute_function_call(), get_size(), and show_state().
|
protected |
Definition at line 93 of file interpreter_class.h.
Referenced by execute_assert(), execute_assign(), execute_assume(), execute_decl(), execute_function_call(), execute_goto(), execute_other(), operator()(), show_state(), and step().
|
protected |
Definition at line 54 of file interpreter_class.h.
Referenced by build_memory_map(), execute_function_call(), and step().
|
protected |
Definition at line 36 of file interpreter_class.h.
Referenced by build_memory_map().