Skip to content

interpretert isn't a messaget #5595

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Nov 16, 2020
Merged

interpretert isn't a messaget #5595

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
101 changes: 50 additions & 51 deletions src/goto-programs/interpreter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,20 +39,20 @@ const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();

void interpretert::operator()()
{
status() << "0- Initialize:" << eom;
output.status() << "0- Initialize:" << messaget::eom;
initialize(true);
try
{
status() << "Type h for help\n" << eom;
output.status() << "Type h for help\n" << messaget::eom;

while(!done)
command();

status() << total_steps << "- Program End.\n" << eom;
output.status() << total_steps << "- Program End.\n" << messaget::eom;
}
catch (const char *e)
{
error() << e << "\n" << eom;
output.error() << e << "\n" << messaget::eom;
}

while(!done)
Expand Down Expand Up @@ -113,22 +113,19 @@ void interpretert::show_state()
{
if(!show)
return;
status() << "\n"
<< total_steps+1
<< " ----------------------------------------------------\n";
output.status() << "\n"
<< total_steps + 1
<< " ----------------------------------------------------\n";

if(pc==function->second.body.instructions.end())
{
status() << "End of function '" << function->first << "'\n";
output.status() << "End of function '" << function->first << "'\n";
}
else
function->second.body.output_instruction(
ns,
function->first,
status(),
*pc);
ns, function->first, output.status(), *pc);

status() << eom;
output.status() << messaget::eom;
}

/// reads a user command and executes it.
Expand All @@ -147,18 +144,18 @@ void interpretert::command()
done=true;
else if(ch=='h')
{
status() << "Interpreter help\n"
<< "h: display this menu\n"
<< "j: output json trace\n"
<< "m: output memory dump\n"
<< "o: output goto trace\n"
<< "q: quit\n"
<< "r: run up to entry point\n"
<< "s#: step a number of instructions\n"
<< "sa: step across a function\n"
<< "so: step out of a function\n"
<< "se: step until end of program\n"
<< eom;
output.status() << "Interpreter help\n"
<< "h: display this menu\n"
<< "j: output json trace\n"
<< "m: output memory dump\n"
<< "o: output goto trace\n"
<< "q: quit\n"
<< "r: run up to entry point\n"
<< "s#: step a number of instructions\n"
<< "sa: step across a function\n"
<< "so: step out of a function\n"
<< "se: step until end of program\n"
<< messaget::eom;
}
else if(ch=='j')
{
Expand All @@ -176,7 +173,7 @@ void interpretert::command()
return;
}
}
json_steps.output(result());
json_steps.output(output.result());
}
else if(ch=='m')
{
Expand All @@ -197,7 +194,7 @@ void interpretert::command()
return;
}
}
steps.output(ns, result());
steps.output(ns, output.result());
}
else if(ch=='r')
{
Expand Down Expand Up @@ -408,8 +405,9 @@ void interpretert::execute_other()
mp_integer size=get_size(pc->code.op0().type());
while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
if(size!=rhs.size())
error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
<< size << ")\n" << eom;
output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
<< size << ")\n"
<< messaget::eom;
else
{
assign(address, rhs);
Expand Down Expand Up @@ -637,9 +635,9 @@ exprt interpretert::get_value(
symbol_expr, from_integer(offset_from_address, integer_typet()));
}

error() << "interpreter: invalid pointer "
<< rhs[numeric_cast_v<std::size_t>(offset)] << " > object count "
<< memory.size() << eom;
output.error() << "interpreter: invalid pointer "
<< rhs[numeric_cast_v<std::size_t>(offset)]
<< " > object count " << memory.size() << messaget::eom;

throw "interpreter: reading from invalid pointer";
}
Expand Down Expand Up @@ -671,10 +669,9 @@ void interpretert::execute_assign()
mp_integer size=get_size(code_assign.lhs().type());

if(size!=rhs.size())
error() << "!! failed to obtain rhs ("
<< rhs.size() << " vs. "
<< size << ")\n"
<< eom;
output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
<< size << ")\n"
<< messaget::eom;
else
{
goto_trace_stept &trace_step=steps.get_last_step();
Expand Down Expand Up @@ -716,11 +713,11 @@ void interpretert::assign(
memory_cellt &cell = memory[numeric_cast_v<std::size_t>(address_val)];
if(show)
{
status() << total_steps << " ** assigning "
<< address_to_symbol(address_val).get_identifier() << "["
<< address_to_offset(address_val)
<< "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
<< eom;
output.status() << total_steps << " ** assigning "
<< address_to_symbol(address_val).get_identifier()
<< "[" << address_to_offset(address_val)
<< "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
<< messaget::eom;
}
cell.value = rhs[numeric_cast_v<std::size_t>(i)];
if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
Expand All @@ -740,8 +737,8 @@ void interpretert::execute_assert()
if(!evaluate_boolean(pc->get_condition()))
{
if(show)
error() << "assertion failed at " << pc->location_number
<< "\n" << eom;
output.error() << "assertion failed at " << pc->location_number << "\n"
<< messaget::eom;
}
}

Expand Down Expand Up @@ -847,7 +844,7 @@ void interpretert::execute_function_call()
}

if(show)
error() << "no body for "+id2string(identifier) << eom;
output.error() << "no body for " << identifier << messaget::eom;
}
}

Expand Down Expand Up @@ -903,16 +900,17 @@ typet interpretert::concretize_type(const typet &type)
if(computed_size.size()==1 &&
computed_size[0]>=0)
{
result() << "Concretized array with size " << computed_size[0]
<< eom;
output.result() << "Concretized array with size " << computed_size[0]
<< messaget::eom;
return
array_typet(
type.subtype(),
from_integer(computed_size[0], integer_typet()));
}
else
{
warning() << "Failed to concretize variable array" << eom;
output.warning() << "Failed to concretize variable array"
<< messaget::eom;
}
}
return type;
Expand Down Expand Up @@ -1067,11 +1065,12 @@ void interpretert::print_memory(bool input_flags)
const memory_cellt &cell=cell_address.second;
const auto identifier = address_to_symbol(i).get_identifier();
const auto offset=address_to_offset(i);
status() << identifier << "[" << offset << "]"
<< "=" << cell.value << eom;
output.status() << identifier << "[" << offset << "]"
<< "=" << cell.value << messaget::eom;
if(input_flags)
status() << "(" << static_cast<int>(cell.initialized) << ")" << eom;
status() << eom;
output.status() << "(" << static_cast<int>(cell.initialized) << ")"
<< messaget::eom;
output.status() << messaget::eom;
}
}

Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/interpreter.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,10 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_GOTO_PROGRAMS_INTERPRETER_H
#define CPROVER_GOTO_PROGRAMS_INTERPRETER_H

#include <util/message.h>

#include "goto_model.h"

class message_handlert;

void interpreter(
const goto_modelt &,
message_handlert &);
Expand Down
5 changes: 3 additions & 2 deletions src/goto-programs/interpreter_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,14 +24,14 @@ Author: Daniel Kroening, [email protected]
#include "goto_trace.h"
#include "json_goto_trace.h"

class interpretert:public messaget
class interpretert
{
public:
interpretert(
const symbol_tablet &_symbol_table,
const goto_functionst &_goto_functions,
message_handlert &_message_handler)
: messaget(_message_handler),
: output(_message_handler),
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this called output rather than log here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The interpreter necessarily provides user-facing output, i.e., is not useful if not printing some of the messages. So I thought "output" may be a better choice than "log" on this occasion. But I might well be wrong?

symbol_table(_symbol_table),
ns(_symbol_table),
goto_functions(_goto_functions),
Expand Down Expand Up @@ -97,6 +97,7 @@ class interpretert:public messaget
const dynamic_typest &get_dynamic_types() { return dynamic_types; }

protected:
messaget output;
const symbol_tablet &symbol_table;

// This is a cache so that we don't have to create it when a call needs it
Expand Down
31 changes: 14 additions & 17 deletions src/goto-programs/interpreter_evaluate.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -404,8 +404,8 @@ void interpretert::evaluate(
{
const std::string &value = id2string(to_constant_expr(expr).get_value());
if(show)
warning() << "string decoding not fully implemented "
<< value.size() + 1 << eom;
output.warning() << "string decoding not fully implemented "
<< value.size() + 1 << messaget::eom;
dest.push_back(get_string_container()[value]);
return;
}
Expand Down Expand Up @@ -457,15 +457,14 @@ void interpretert::evaluate(
if(side_effect.get_statement()==ID_nondet)
{
if(show)
error() << "nondet not implemented" << eom;
output.error() << "nondet not implemented" << messaget::eom;
return;
}
else if(side_effect.get_statement()==ID_allocate)
{
if(show)
error() << "heap memory allocation not fully implemented "
<< expr.type().subtype().pretty()
<< eom;
output.error() << "heap memory allocation not fully implemented "
<< expr.type().subtype().pretty() << messaget::eom;
std::stringstream buffer;
num_dynamic_objects++;
buffer << "interpreter::dynamic_object" << num_dynamic_objects;
Expand All @@ -478,9 +477,8 @@ void interpretert::evaluate(
return;
}
if(show)
error() << "side effect not implemented "
<< side_effect.get_statement()
<< eom;
output.error() << "side effect not implemented "
<< side_effect.get_statement() << messaget::eom;
}
else if(expr.id()==ID_bitor)
{
Expand Down Expand Up @@ -1041,14 +1039,14 @@ void interpretert::evaluate(
{
if(expr.type().id()==ID_signedbv)
{
warning() << "Infinite size arrays not supported" << eom;
output.warning() << "Infinite size arrays not supported" << messaget::eom;
return;
}
}
error() << "!! failed to evaluate expression: "
<< from_expr(ns, function->first, expr) << "\n"
<< expr.id() << "[" << expr.type().id() << "]"
<< eom;
output.error() << "!! failed to evaluate expression: "
<< from_expr(ns, function->first, expr) << "\n"
<< expr.id() << "[" << expr.type().id() << "]"
<< messaget::eom;
}

mp_integer interpretert::evaluate_address(
Expand Down Expand Up @@ -1157,9 +1155,8 @@ mp_integer interpretert::evaluate_address(

if(!fail_quietly)
{
error() << "!! failed to evaluate address: "
<< from_expr(ns, function->first, expr)
<< eom;
output.error() << "!! failed to evaluate address: "
<< from_expr(ns, function->first, expr) << messaget::eom;
}

return 0;
Expand Down