Go to the documentation of this file.
69 const goto_functionst::function_mapt::const_iterator
73 throw "main not found";
77 if(!goto_function.body_available())
78 throw "main has no body";
80 pc=goto_function.body.instructions.begin();
111 <<
" ----------------------------------------------------\n";
113 if(
pc==
function->second.body.instructions.end())
115 status() <<
"End of function '" <<
function->first <<
"'\n";
118 function->second.body.output_instruction(
144 <<
"Interpreter help\n"
145 <<
"h: display this menu\n"
146 <<
"j: output json trace\n"
147 <<
"m: output memory dump\n"
148 <<
"o: output goto trace\n"
150 <<
"r: run until completion\n"
151 <<
"s#: step a number of instructions\n"
152 <<
"sa: step across a function\n"
153 <<
"so: step out of a function\n"
159 convert<json_arrayt>(
ns,
steps, json_steps);
200 else if((ch==
's') || (ch==0))
236 if(
pc==
function->second.body.instructions.end())
296 throw "RETURN without call";
298 if(
pc->code.operands().size()==1 &&
306 next_pc=
function->second.body.instructions.end();
321 throw "START_THREAD not yet implemented";
324 throw "END_THREAD not yet implemented";
329 throw "ATOMIC_BEGIN not yet implemented";
333 throw "ATOMIC_END not yet implemented";
342 if(
pc==
function->second.body.instructions.end())
364 throw "encountered instruction with undefined instruction type";
374 if(
pc->targets.empty())
375 throw "taken goto without target";
377 if(
pc->targets.size()>=2)
378 throw "non-deterministic goto encountered";
387 const irep_idt &statement =
pc->get_other().get_statement();
388 if(statement==ID_expression)
391 pc->code.operands().size()==1,
392 "expression statement expected to have one operand");
396 else if(statement==ID_array_set)
402 while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
404 error() <<
"!! failed to obtain rhs (" << rhs.size() <<
" vs. "
405 << size <<
")\n" <<
eom;
416 throw "unexpected OTHER statement: "+
id2string(statement);
439 if(real_type.
id()!=ID_struct)
440 throw "request for member of non-struct";
447 for(
const auto &c : components)
455 throw "access out of struct bounds";
475 if(real_type.
id()==ID_struct)
482 result.reserve_operands(components.size());
486 for(
const auto &c : components)
491 result.copy_to_operands(operand);
496 else if(real_type.
id()==ID_array)
500 const exprt &size_expr=
static_cast<const exprt &
>(type.
find(ID_size));
503 if(size_expr.id()!=ID_constant)
513 result.reserve_operands(numeric_cast_v<std::size_t>(count));
518 offset+i*subtype_size);
519 result.copy_to_operands(operand);
524 use_non_det &&
memory[numeric_cast_v<std::size_t>(offset)].initialized !=
530 rhs.push_back(
memory[numeric_cast_v<std::size_t>(offset)].value);
544 if(real_type.
id()==ID_struct)
551 result.reserve_operands(components.size());
559 result.copy_to_operands(operand);
563 else if(real_type.
id()==ID_array)
566 const exprt &size_expr=
static_cast<const exprt &
>(type.
find(ID_size));
582 result.reserve_operands(numeric_cast_v<std::size_t>(count));
586 offset+i*subtype_size);
587 result.copy_to_operands(operand);
591 else if(real_type.
id()==ID_floatbv)
594 f.
unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
597 else if(real_type.
id()==ID_fixedbv)
600 f.
from_integer(rhs[numeric_cast_v<std::size_t>(offset)]);
603 else if(real_type.
id()==ID_bool)
605 if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
610 else if(real_type.
id()==ID_c_bool)
613 rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
615 else if(real_type.
id() == ID_pointer)
617 if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
620 if(rhs[numeric_cast_v<std::size_t>(offset)] <
memory.
size())
623 mp_integer address = rhs[numeric_cast_v<std::size_t>(offset)];
627 if(offset_from_address == 0)
631 symbol_expr.
type().
id() == ID_struct ||
632 symbol_expr.
type().
id() == ID_struct_tag)
643 error() <<
"interpreter: invalid pointer "
644 << rhs[numeric_cast_v<std::size_t>(offset)] <<
" > object count "
647 throw "interpreter: reading from invalid pointer";
649 else if(real_type.
id()==ID_string)
654 numeric_cast_v<std::size_t>(rhs[numeric_cast_v<std::size_t>(offset)])),
659 return from_integer(rhs[numeric_cast_v<std::size_t>(offset)], type);
677 error() <<
"!! failed to obtain rhs ("
678 << rhs.size() <<
" vs. "
689 else if(code_assign.
rhs().
id()==ID_side_effect)
702 memory[numeric_cast_v<std::size_t>(address + i)].initialized =
725 <<
"]:=" << rhs[numeric_cast_v<std::size_t>(i)] <<
"\n"
728 cell.
value = rhs[numeric_cast_v<std::size_t>(i)];
738 throw "assumption failed";
746 throw "program assertion reached";
748 error() <<
"assertion failed at " <<
pc->location_number
761 throw "function call to NULL";
763 throw "out-of-range function call";
774 const goto_functionst::function_mapt::const_iterator f_it=
778 throw "failed to find function "+
id2string(identifier);
784 return_value_address=
787 return_value_address=0;
790 std::vector<mp_vectort> argument_values;
792 argument_values.resize(function_call.
arguments().size());
794 for(std::size_t i=0; i<function_call.
arguments().size(); i++)
799 if(f_it->second.body_available())
810 std::set<irep_idt> locals;
813 for(
const auto &
id : locals)
820 const auto ¶meter_identifiers = f_it->second.parameter_identifiers;
821 if(argument_values.size() < parameter_identifiers.size())
822 throw "not enough arguments";
824 for(std::size_t i = 0; i < parameter_identifiers.size(); i++)
827 ns.
lookup(parameter_identifiers[i]).symbol_expr();
833 next_pc=f_it->second.body.instructions.begin();
844 PRECONDITION(!it->second.front().return_assignments.empty());
845 evaluate(it->second.front().return_assignments.back().value, value);
846 if(return_value_address>0)
848 assign(return_value_address, value);
850 it->second.pop_front();
881 if(symbol.
type.
id()==ID_code)
893 memory.
resize(numeric_cast_v<std::size_t>(address + size));
902 if(type.
id()==ID_array)
904 const exprt &size_expr=
static_cast<const exprt &
>(type.
find(ID_size));
907 if(computed_size.size()==1 &&
910 result() <<
"Concretized array with size " << computed_size[0]
919 warning() <<
"Failed to concretize variable array" <<
eom;
938 if(size<=current_size)
949 memory.
resize(numeric_cast_v<std::size_t>(address + size));
953 std::pair<const irep_idt, typet>(symbol_expr.
get_identifier(), alloc_type));
960 if(type.
id()==ID_array)
963 if(size.
id()==ID_infinity)
967 else if(type.
id()==ID_struct)
970 if(st.components().empty())
986 if(type.
id()==ID_struct)
993 for(
const auto &comp : components)
995 const typet &sub_type=comp.type();
997 if(sub_type.
id()!=ID_code)
1003 else if(type.
id()==ID_union)
1010 for(
const auto &comp : components)
1012 const typet &sub_type=comp.type();
1014 if(sub_type.
id()!=ID_code)
1015 max_size=std::max(max_size,
get_size(sub_type));
1020 else if(type.
id()==ID_array)
1022 const exprt &size_expr=
static_cast<const exprt &
>(type.
find(ID_size));
1033 const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
1034 return subtype_size*size_mp;
1036 return subtype_size;
1038 else if(type.
id() == ID_struct_tag)
1068 for(
const auto &cell_address :
memory)
1074 debug() << identifier <<
"[" << offset <<
"]"
mp_integer base_address_to_actual_size(const mp_integer &address) const
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void show_state()
displays the current position of the pc and corresponding code
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & subtype() const
void from_integer(const mp_integer &i)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
void output(std::ostream &out) const
The type of an expression, extends irept.
mstreamt & status() const
void execute_goto()
executes a goto instruction
goto_programt::const_targett pc
typet type
Type of symbol.
const symbol_tablet & symbol_table
void assign(const mp_integer &address, const mp_vectort &rhs)
sets the memory at address with the given rhs value (up to sizeof(rhs))
const irept & find(const irep_namet &name) const
void unpack(const mp_integer &i)
symbol_exprt address_to_symbol(const mp_integer &address) const
bool evaluate_boolean(const exprt &expr)
Unbounded, signed integers (mathematical integers, not bitvectors)
bool unbounded_size(const typet &)
Interpreter for GOTO Programs.
struct_typet::componentt get_component(const irep_idt &object, const mp_integer &offset)
retrieves the member at offset
Base class for all expressions.
std::vector< componentt > componentst
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Step of the trace of a GOTO program.
goto_programt::const_targett next_pc
side_effect_exprt & to_side_effect_expr(exprt &expr)
function_mapt function_map
Expression to hold a symbol (variable)
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
constant_exprt to_expr() const
std::size_t safe_string2size_t(const std::string &str, int base)
void print_memory(bool input_flags)
Prints the current state of the memory map Since messaget mdofifies class members,...
dynamic_typest dynamic_types
void build_memory_map()
Creates a memory map of all static symbols in the program.
mp_integer base_address_to_alloc_size(const mp_integer &address) const
Struct constructor from list of elements.
const exprt & size() const
typet & type()
Return the type of the expression.
Interpreter for GOTO Programs.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
goto_functionst::function_mapt::const_iterator function
mstreamt & result() const
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
void execute_other()
executes side effects of 'other' instructions
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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
virtual void command()
reads a user command and executes it.
The null pointer constant.
const std::string & id2string(const irep_idt &d)
void step()
executes a single step and updates the program counter
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
goto_programt::const_targett pc
mp_integer old_stack_pointer
void execute_function_call()
const goto_functionst & goto_functions
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
typet get_type(const irep_idt &id) const
returns the type object corresponding to id
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void resize(uint64_t new_size)
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::vector< mp_integer > mp_vectort
The Boolean constant false.
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
typet concretize_type(const typet &type)
turns a variable length array type into a fixed array type
Replace function returns by assignments to global variables.
const irep_idt & get_statement() const
void execute_assign()
executes the assign statement at the current pc value
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
Extract member of struct or union.
bool can_cast_expr< code_outputt >(const exprt &base)
Structure type, corresponds to C style structs.
goto_functionst goto_functions
GOTO functions.
const code_assignt & to_code_assign(const codet &code)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
mp_integer return_value_address
inverse_memory_mapt inverse_memory_map
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
void clear_input_flags()
Clears memoy r/w flag initialization.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
constant_exprt to_expr() const
mp_integer address_to_offset(const mp_integer &address) const
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
goto_functionst::function_mapt::const_iterator return_function
Operator to return the address of an object.
A codet representing an assignment in the program.
The Boolean constant true.
A constant literal expression.
list_input_varst function_input_vars
mstreamt & warning() const
API to expression classes.
goto_programt::const_targett target_assert
symbol_tablet symbol_table
Symbol table.
Array constructor from list of elements.
irep_idt name
The unique identifier.
An expression containing a side effect.
void add_step(const goto_trace_stept &step)
Add a step at the end of the trace.
goto_programt::const_targett return_pc
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
string_containert & get_string_container()
Get a reference to the global string container.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
void initialize(bool init)
Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing...