Skip to content

Invariant cleanup in goto programs i* #2952

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

Closed
wants to merge 5 commits into from
Closed

Invariant cleanup in goto programs i* #2952

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
4ff7318
Use structured exceptions in initialize_goto_model
hannes-steffenhagen-diffblue Sep 13, 2018
c842c01
Replace throws with structured throws or invariant in interpreter
hannes-steffenhagen-diffblue Sep 13, 2018
d8f8cf3
Add pointer_offset_exprt
hannes-steffenhagen-diffblue Oct 10, 2018
c8329fb
Use structured invariant in interpreter_class.h
hannes-steffenhagen-diffblue Oct 10, 2018
ce7f792
Invariant cleanup in interpreter_evaluate.cpp
hannes-steffenhagen-diffblue Oct 10, 2018
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
36 changes: 17 additions & 19 deletions src/goto-programs/initialize_goto_model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
#include <langapi/language.h>

#include <goto-programs/rebuild_goto_start_function.h>
#include <util/exception_utils.h>

#include "goto_convert_functions.h"
#include "read_goto_binary.h"
Expand All @@ -36,8 +37,10 @@ goto_modelt initialize_goto_model(
const std::vector<std::string> &files=cmdline.args;
if(files.empty())
{
msg.error() << "Please provide a program" << messaget::eom;
throw 0;
throw invalid_command_line_argument_exceptiont(
"missing program argument",
"filename",
"one or more paths to program files");
}

std::vector<std::string> binaries, sources;
Expand Down Expand Up @@ -69,21 +72,17 @@ goto_modelt initialize_goto_model(

if(!infile)
{
msg.error() << "failed to open input file `" << filename
<< '\'' << messaget::eom;
throw 0;
throw system_exceptiont(
"Failed to open input file `" + filename + '\'');
}

language_filet &lf=language_files.add_file(filename);
lf.language=get_language_from_filename(filename);

if(lf.language==nullptr)
{
source_locationt location;
location.set_file(filename);
msg.error().source_location=location;
msg.error() << "failed to figure out type of file" << messaget::eom;
throw 0;
throw invalid_source_file_exceptiont(
"Failed to figure out type of file `" + filename + '\'');
Copy link
Contributor Author

Choose a reason for hiding this comment

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

This should arguably happen before the check whether the file can be opened, but that's a minor point and not really within the spirit of this PR

}

languaget &language=*lf.language;
Expand All @@ -94,8 +93,7 @@ goto_modelt initialize_goto_model(

if(language.parse(infile, filename))
{
msg.error() << "PARSING ERROR" << messaget::eom;
throw 0;
throw invalid_source_file_exceptiont("PARSING ERROR");
}

lf.get_modules();
Expand All @@ -105,8 +103,7 @@ goto_modelt initialize_goto_model(

if(language_files.typecheck(goto_model.symbol_table))
{
msg.error() << "CONVERSION ERROR" << messaget::eom;
throw 0;
throw invalid_source_file_exceptiont("CONVERSION ERROR");
}
}

Expand All @@ -115,7 +112,10 @@ goto_modelt initialize_goto_model(
msg.status() << "Reading GOTO program from file" << messaget::eom;

if(read_object_and_link(file, goto_model, message_handler))
throw 0;
{
throw invalid_source_file_exceptiont(
"failed to read object or link in file `" + file + '\'');
}
}

bool binaries_provided_start=
Expand Down Expand Up @@ -150,14 +150,12 @@ goto_modelt initialize_goto_model(

if(entry_point_generation_failed)
{
msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
throw 0;
throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
}

if(language_files.final(goto_model.symbol_table))
{
msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
throw 0;
throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR");
}

msg.status() << "Generating GOTO Program" << messaget::eom;
Expand Down
63 changes: 36 additions & 27 deletions src/goto-programs/interpreter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,12 +69,12 @@ void interpretert::initialize(bool init)
main_it=goto_functions.function_map.find(goto_functionst::entry_point());

if(main_it==goto_functions.function_map.end())
throw "main not found";
throw analysis_exceptiont("main not found");
Copy link
Collaborator

Choose a reason for hiding this comment

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

Is this actually a structural invariant on goto-programs?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I wasn't sure about this one, because you might have goto programs without an entry point (libraries mostly). I suppose it could be a precondition if we assume that a caller should've checked for an entry point before calling this.

Copy link
Collaborator

Choose a reason for hiding this comment

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

It is getting in to the heart of why we need to check that goto-programs are well formed and to clarify what "normal forms" exist for them. If it has been linked and is a complete goto program then it should have an entry point which is a function in the map. If it is only partially built (goto-cc -c for example) then it may not do. It is not immediately clear to me whose fault it would be to try to interpret a n "object file" rather than an "executable".


const goto_functionst::goto_functiont &goto_function=main_it->second;

if(!goto_function.body_available())
throw "main has no body";
throw analysis_exceptiont("main has no body");
Copy link
Collaborator

Choose a reason for hiding this comment

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

As above.


pc=goto_function.body.instructions.begin();
function=main_it;
Expand Down Expand Up @@ -292,7 +292,10 @@ void interpretert::step()
case RETURN:
trace_step.type=goto_trace_stept::typet::FUNCTION_RETURN;
if(call_stack.empty())
throw "RETURN without call"; // NOLINT(readability/throw)
{
throw analysis_exceptiont(
"RETURN without call"); // NOLINT(readability/throw)
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think this is an INVARIANT as if the interpreter is working as it should, then this should never happen.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I was thinking this could happen in a nonsensical goto program that has returns in unexpected places, such as __CPROVER_initialize. Is that wrong?

Copy link
Collaborator

Choose a reason for hiding this comment

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

If I understand the code correctly (and it is possible I don't) then the INVARIANT is that the number of RETURNS executed should never exceed the number of functions started. So this should always hold.

}

if(pc->code.operands().size()==1 &&
call_stack.top().return_value_address!=0)
Expand All @@ -317,19 +320,23 @@ void interpretert::step()

case START_THREAD:
trace_step.type=goto_trace_stept::typet::SPAWN;
throw "START_THREAD not yet implemented"; // NOLINT(readability/throw)
throw analysis_exceptiont(
"START_THREAD not yet implemented"); // NOLINT(readability/throw)
Copy link
Collaborator

Choose a reason for hiding this comment

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

UNIMPLEMENTED ? Also below.


case END_THREAD:
throw "END_THREAD not yet implemented"; // NOLINT(readability/throw)
throw analysis_exceptiont(
"END_THREAD not yet implemented"); // NOLINT(readability/throw)
break;

case ATOMIC_BEGIN:
trace_step.type=goto_trace_stept::typet::ATOMIC_BEGIN;
throw "ATOMIC_BEGIN not yet implemented"; // NOLINT(readability/throw)
throw analysis_exceptiont(
"ATOMIC_BEGIN not yet implemented"); // NOLINT(readability/throw)

case ATOMIC_END:
trace_step.type=goto_trace_stept::typet::ATOMIC_END;
throw "ATOMIC_END not yet implemented"; // NOLINT(readability/throw)
throw analysis_exceptiont(
"ATOMIC_END not yet implemented"); // NOLINT(readability/throw)

case DEAD:
trace_step.type=goto_trace_stept::typet::DEAD;
Expand Down Expand Up @@ -359,7 +366,7 @@ void interpretert::step()
case CATCH:
break;
default:
throw "encountered instruction with undefined instruction type";
UNREACHABLE; // I'm assuming we'd catch such a thing before this point
Copy link
Collaborator

Choose a reason for hiding this comment

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

Sounds like you're saying it is a consequence of the goto program being well-formed ;-)

}
pc=next_pc;
}
Expand All @@ -369,11 +376,9 @@ void interpretert::execute_goto()
{
if(evaluate_boolean(pc->guard))
{
if(pc->targets.empty())
throw "taken goto without target";

if(pc->targets.size()>=2)
throw "non-deterministic goto encountered";
DATA_INVARIANT(
pc->targets.size() == 1,
"a goto should have exactly one target location");

next_pc=pc->targets.front();
}
Expand All @@ -383,6 +388,10 @@ void interpretert::execute_goto()
void interpretert::execute_other()
{
const irep_idt &statement=pc->code.get_statement();
PRECONDITION(
statement == ID_expression || statement == ID_array_set ||
statement == ID_output);

if(statement==ID_expression)
{
DATA_INVARIANT(
Expand Down Expand Up @@ -410,8 +419,6 @@ void interpretert::execute_other()
{
return;
}
else
throw "unexpected OTHER statement: "+id2string(statement);
}

void interpretert::execute_decl()
Expand All @@ -427,8 +434,7 @@ struct_typet::componentt interpretert::get_component(
{
const symbolt &symbol=ns.lookup(object);
const typet real_type=ns.follow(symbol.type);
if(real_type.id()!=ID_struct)
throw "request for member of non-struct";
PRECONDITION(real_type.id() == ID_struct);

const struct_typet &struct_type=to_struct_type(real_type);
const struct_typet::componentst &components=struct_type.components();
Expand All @@ -443,7 +449,7 @@ struct_typet::componentt interpretert::get_component(
tmp_offset-=get_size(c.type());
}

throw "access out of struct bounds";
throw analysis_exceptiont("access out of struct bounds");
}

/// returns the type object corresponding to id
Expand Down Expand Up @@ -634,7 +640,7 @@ exprt interpretert::get_value(
error() << "interpreter: invalid pointer " << rhs[integer2size_t(offset)]
<< " > object count " << memory.size() << eom;

throw "interpreter: reading from invalid pointer";
throw analysis_exceptiont("interpreter: reading from invalid pointer");
}
else if(real_type.id()==ID_string)
{
Expand Down Expand Up @@ -724,15 +730,15 @@ void interpretert::assign(
void interpretert::execute_assume()
{
if(!evaluate_boolean(pc->guard))
throw "assumption failed";
throw analysis_exceptiont("assumption failed");
Copy link
Collaborator

Choose a reason for hiding this comment

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

Unrelated to this; I'm not sure this is the right way of handling this case. I think it should just terminate correctly.

}

void interpretert::execute_assert()
{
if(!evaluate_boolean(pc->guard))
{
if((target_assert==pc) || stop_on_assertion)
throw "program assertion reached";
throw analysis_exceptiont("program assertion reached");
else if(show)
error() << "assertion failed at " << pc->location_number
<< "\n" << eom;
Expand All @@ -748,9 +754,9 @@ void interpretert::execute_function_call()
mp_integer address=evaluate_address(function_call.function());

if(address==0)
throw "function call to NULL";
throw analysis_exceptiont("function call to NULL");
else if(address>=memory.size())
throw "out-of-range function call";
throw analysis_exceptiont("out-of-range function call");

// Retrieve the empty last trace step struct we pushed for this step
// of the interpreter run to fill it with the corresponding data
Expand All @@ -764,8 +770,9 @@ void interpretert::execute_function_call()
const goto_functionst::function_mapt::const_iterator f_it=
goto_functions.function_map.find(identifier);

if(f_it==goto_functions.function_map.end())
throw "failed to find function "+id2string(identifier);
INVARIANT(
f_it != goto_functions.function_map.end(),
"calls to missing functions should be caught during typechecking");

// return value
mp_integer return_value_address;
Expand Down Expand Up @@ -810,8 +817,10 @@ void interpretert::execute_function_call()
const code_typet::parameterst &parameters=
to_code_type(f_it->second.type).parameters();

if(argument_values.size()<parameters.size())
throw "not enough arguments";
INVARIANT(
argument_values.size() != parameters.size(),
"function calls not matching function signatures should be caught during "
"typechecking");

for(std::size_t i=0; i<parameters.size(); i++)
{
Expand Down
1 change: 1 addition & 0 deletions src/goto-programs/interpreter.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_GOTO_PROGRAMS_INTERPRETER_H
#define CPROVER_GOTO_PROGRAMS_INTERPRETER_H

#include <util/exception_utils.h>
#include <util/message.h>

#include "goto_model.h"
Expand Down
8 changes: 5 additions & 3 deletions src/goto-programs/interpreter_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,11 @@ Author: Daniel Kroening, [email protected]
#include <stack>

#include <util/arith_tools.h>
#include <util/exception_utils.h>
#include <util/invariant.h>
#include <util/std_types.h>
#include <util/sparse_vector.h>
#include <util/message.h>
#include <util/sparse_vector.h>
#include <util/std_types.h>

#include "goto_functions.h"
#include "goto_trace.h"
Expand Down Expand Up @@ -279,8 +280,9 @@ class interpretert:public messaget
{
mp_vectort v;
evaluate(expr, v);
// FIXME not sure if this can happen
if(v.size()!=1)
throw "invalid boolean value";
throw analysis_exceptiont("invalid boolean value");
Copy link
Collaborator

Choose a reason for hiding this comment

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

I would drop the FIXME and turn this into an INVARIANT. People will start complaining if it's not actually an invariant... :-)

return v.front()!=0;
}

Expand Down
Loading