66 const goto_functionst::function_mapt::const_iterator
70 throw "main not found";
74 if(!goto_function.body_available())
75 throw "main has no body";
77 pc=goto_function.body.instructions.begin();
108 <<
" ----------------------------------------------------\n";
110 if(
pc==
function->second.body.instructions.end())
112 status() <<
"End of function `" <<
function->first <<
"'\n";
115 function->second.body.output_instruction(
141 <<
"Interpreter help\n" 142 <<
"h: display this menu\n" 143 <<
"j: output json trace\n" 144 <<
"m: output memory dump\n" 145 <<
"o: output goto trace\n" 147 <<
"r: run until completion\n" 148 <<
"s#: step a number of instructions\n" 149 <<
"sa: step across a function\n" 150 <<
"so: step out of a function\n" 156 convert<json_arrayt>(
ns,
steps, json_steps);
197 else if((ch==
's') || (ch==0))
233 if(
pc==
function->second.body.instructions.end())
293 throw "RETURN without call";
295 if(
pc->code.operands().size()==1 &&
303 next_pc=
function->second.body.instructions.end();
318 throw "START_THREAD not yet implemented";
321 throw "END_THREAD not yet implemented";
326 throw "ATOMIC_BEGIN not yet implemented";
330 throw "ATOMIC_END not yet implemented";
339 if(
pc==
function->second.body.instructions.end())
360 throw "encountered instruction with undefined instruction type";
370 if(
pc->targets.empty())
371 throw "taken goto without target";
373 if(
pc->targets.size()>=2)
374 throw "non-deterministic goto encountered";
383 const irep_idt &statement=
pc->code.get_statement();
384 if(statement==ID_expression)
387 pc->code.operands().size()==1,
388 "expression statement expected to have one operand");
392 else if(statement==ID_array_set)
398 while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
400 error() <<
"!! failed to obtain rhs (" << rhs.size() <<
" vs. " 401 << size <<
")\n" <<
eom;
407 else if(statement==ID_output)
412 throw "unexpected OTHER statement: "+
id2string(statement);
428 if(real_type.
id()!=ID_struct)
429 throw "request for member of non-struct";
436 for(
const auto &c : components)
444 throw "access out of struct bounds";
464 if(real_type.
id()==ID_struct)
471 result.reserve_operands(components.size());
475 for(
const auto &c : components)
480 result.copy_to_operands(operand);
485 else if(real_type.
id()==ID_array)
489 const exprt &size_expr=
static_cast<const exprt &
>(type.
find(ID_size));
492 if(size_expr.
id()!=ID_constant)
507 offset+i*subtype_size);
508 result.copy_to_operands(operand);
531 if(real_type.
id()==ID_struct)
538 result.reserve_operands(components.size());
546 result.copy_to_operands(operand);
550 else if(real_type.
id()==ID_array)
553 const exprt &size_expr=
static_cast<const exprt &
>(type.
find(ID_size));
573 offset+i*subtype_size);
574 result.copy_to_operands(operand);
578 else if(real_type.
id()==ID_floatbv)
584 else if(real_type.
id()==ID_fixedbv)
590 else if(real_type.
id()==ID_bool)
597 else if(real_type.
id()==ID_c_bool)
601 else if((real_type.
id()==ID_pointer) || (real_type.
id()==ID_address_of))
607 result.set_value(ID_NULL);
640 throw "interpreter: reading from invalid pointer";
642 else if(real_type.
id()==ID_string)
669 error() <<
"!! failed to obtain rhs (" 670 << rhs.size() <<
" vs. " 689 else if(code_assign.
rhs().
id()==ID_side_effect)
738 throw "assumption failed";
746 throw "program assertion reached";
748 error() <<
"assertion failed at " <<
pc->location_number
762 throw "function call to NULL";
764 throw "out-of-range function call";
775 const goto_functionst::function_mapt::const_iterator f_it=
779 throw "failed to find function "+
id2string(identifier);
785 return_value_address=
788 return_value_address=0;
791 std::vector<mp_vectort> argument_values;
793 argument_values.resize(function_call.
arguments().size());
795 for(std::size_t i=0; i<function_call.
arguments().size(); i++)
800 if(f_it->second.body_available())
811 std::set<irep_idt> locals;
814 for(
const auto &
id : locals)
824 if(argument_values.size()<parameters.size())
825 throw "not enough arguments";
827 for(std::size_t i=0; i<parameters.size(); i++)
836 next_pc=f_it->second.body.instructions.begin();
847 PRECONDITION(!it->second.front().return_assignments.empty());
848 evaluate(it->second.front().return_assignments.back().value, value);
849 if(return_value_address>0)
851 assign(return_value_address, value);
853 it->second.pop_front();
884 if(symbol.
type.
id()==ID_code)
905 if(type.
id()==ID_array)
907 const exprt &size_expr=
static_cast<const exprt &
>(type.
find(ID_size));
910 if(computed_size.size()==1 &&
913 result() <<
"Concretized array with size " << computed_size[0]
922 warning() <<
"Failed to concretize variable array" <<
eom;
943 if(size<=current_size)
957 dynamic_types.insert(std::pair<const irep_idt, typet>(
id, alloc_type));
964 if(type.
id()==ID_array)
967 if(size.
id()==ID_infinity)
971 else if(type.
id()==ID_struct)
974 if(st.components().empty())
990 if(type.
id()==ID_struct)
997 for(
const auto &comp : components)
999 const typet &sub_type=comp.type();
1001 if(sub_type.
id()!=ID_code)
1007 else if(type.
id()==ID_union)
1014 for(
const auto &comp : components)
1016 const typet &sub_type=comp.type();
1018 if(sub_type.
id()!=ID_code)
1019 max_size=std::max(max_size,
get_size(sub_type));
1024 else if(type.
id()==ID_array)
1026 const exprt &size_expr=
static_cast<const exprt &
>(type.
find(ID_size));
1040 return subtype_size*size_mp;
1042 return subtype_size;
1044 else if(type.
id()==ID_symbol)
1073 for(
const auto &cell_address :
memory)
1079 debug() << identifier <<
"[" << offset <<
"]" The type of an expression.
irep_idt name
The unique identifier.
void execute_goto()
executes a goto instruction
typet get_type(const irep_idt &id) const
returns the type object corresponding to id
const std::string & id2string(const irep_idt &d)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
irep_idt address_to_identifier(const mp_integer &address) const
typet concretize_type(const typet &type)
turns a variable length array type into a fixed array type
constant_exprt to_expr() const
string_containert & get_string_container()
Get a reference to the global string container.
mp_integer::ullong_t integer2ulong(const mp_integer &n)
goto_programt::const_targett return_pc
bool evaluate_boolean(const exprt &expr)
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
std::vector< mp_integer > mp_vectort
goto_trace_stept & get_last_step()
std::vector< componentt > componentst
std::vector< parametert > parameterst
const componentst & components() const
function_mapt function_map
Interpreter for GOTO Programs.
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
A constant literal expression.
#define CHECK_RETURN(CONDITION)
static mstreamt & eom(mstreamt &m)
mp_integer old_stack_pointer
goto_programt::const_targett pc
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
void add_step(const goto_trace_stept &step)
mstreamt & warning() const
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
Interpreter for GOTO Programs.
The boolean constant true.
void unpack(const mp_integer &i)
void output(std::ostream &out) const
goto_functionst::function_mapt::const_iterator function
exprt get_value(const typet &type, const mp_integer &offset=0, bool use_non_det=false)
retrives the constant value at memory location offset as an object of type type
const goto_functionst & goto_functions
void from_integer(const mp_integer &i)
API to expression classes.
void show_state()
displays the current position of the pc and corresponding code
mp_integer address_to_offset(const mp_integer &address) const
void initialize(bool init)
Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing...
::goto_functiont goto_functiont
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
#define PRECONDITION(CONDITION)
A side effect that returns a non-deterministically chosen value.
static bool can_build_identifier(const exprt &src)
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
const exprt & size() const
mp_integer base_address_to_actual_size(const mp_integer &address) const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void execute_assign()
executes the assign statement at the current pc value
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Operator to return the address of an object.
constant_exprt to_expr() const
bool unbounded_size(const typet &)
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
The boolean constant false.
void step()
executes a single step and updates the program counter
inverse_memory_mapt inverse_memory_map
void assign(const mp_integer &address, const mp_vectort &rhs)
sets the memory at address with the given rhs value (up to sizeof(rhs))
mp_integer return_value_address
const symbol_tablet & symbol_table
Unbounded, signed integers.
goto_programt::const_targett next_pc
typet type
Type of symbol.
void clear_input_flags()
Clears memoy r/w flag initialization.
goto_functionst::function_mapt::const_iterator return_function
static irep_idt entry_point()
mstreamt & result() const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
mstreamt & status() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const parameterst & parameters() const
struct_typet::componentt get_component(const irep_idt &object, const mp_integer &offset)
retrieves the member at offset
void build_memory_map()
Creates a memory map of all static symbols in the program.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
goto_programt::const_targett pc
void print_memory(bool input_flags)
Prints the current state of the memory map Since messaget mdofifies class members, print functions are nonconst.
goto_programt::const_targett target_assert
virtual void command()
reads a user command and executes it.
dynamic_typest dynamic_types
Expression to hold a symbol (variable)
goto_programt coverage_criteriont message_handlert & message_handler
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
An expression containing a side effect.
struct constructor from list of elements
void execute_other()
executes side effects of 'other' instructions
void resize(uint64_t new_size)
const irep_idt & get_identifier() const
mp_integer base_address_to_alloc_size(const mp_integer &address) const
Expression providing an SSA-renamed symbol of expressions.
const irept & find(const irep_namet &name) const
goto_functionst goto_functions
GOTO functions.
array constructor from list of elements
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
list_input_varst function_input_vars
const irep_idt & get_statement() const
void execute_function_call()
const code_function_callt & to_code_function_call(const codet &code)