Skip to content

Invariant cleanup goto programs jr #2967

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.

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
Show file tree
Hide file tree
Changes from all commits
Commits
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
4 changes: 2 additions & 2 deletions regression/goto-instrument/replace-calls-03/test.desc
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
main.c
--replace-calls f:g
Functions f and g are not type-compatible
^EXIT=11$
functions f and g are not type-compatible
^EXIT=1$
^SIGNAL=0$
--
^warning: ignoring
4 changes: 2 additions & 2 deletions regression/goto-instrument/replace-calls-04/test.desc
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
main.c
--replace-calls f:g
Functions f and g are not type-compatible
^EXIT=11$
functions f and g are not type-compatible
^EXIT=1$
^SIGNAL=0$
--
^warning: ignoring
4 changes: 2 additions & 2 deletions regression/goto-instrument/replace-calls-05/test.desc
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
main.c
--replace-calls f:g --replace-calls h:f
Function f cannot both be replaced and be a replacement
^EXIT=11$
function f cannot both be replaced and be a replacement
^EXIT=1$
^SIGNAL=0$
--
^warning: ignoring
36 changes: 19 additions & 17 deletions src/goto-programs/lazy_goto_model.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@

#include <util/cmdline.h>
#include <util/config.h>
#include <util/exception_utils.h>
#include <util/journalling_symbol_table.h>
#include <util/unicode.h>

Expand Down Expand Up @@ -96,8 +97,11 @@ void lazy_goto_modelt::initialize(
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(
"no program provided",
"source file names",
"one or more paths to a goto binary or a source file in a supported "
"language");
}

std::vector<std::string> binaries, sources;
Expand All @@ -124,21 +128,17 @@ void lazy_goto_modelt::initialize(

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

Choose a reason for hiding this comment

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

Isn't this (most likely) also an invalid_user_input_exceptiont. It's of course possible that your file system is somehow hosed, but in almost all cases the user will be the one who got it wrong.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It's quite possible that the root cause is because the user passed in the wrong filename. Or it could fail for other reasons. The only thing we know at this point is that we can't open the file, so we report that as such here.

}

language_filet &lf=add_language_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 + '\'');
}

languaget &language=*lf.language;
Expand All @@ -149,8 +149,7 @@ void lazy_goto_modelt::initialize(

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 @@ -160,8 +159,7 @@ void lazy_goto_modelt::initialize(

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

Expand All @@ -170,7 +168,12 @@ void lazy_goto_modelt::initialize(
msg.status() << "Reading GOTO program from file" << messaget::eom;

if(read_object_and_link(file, *goto_model, message_handler))
throw 0;
{
source_locationt source_location;
source_location.set_file(file);
throw incorrect_goto_program_exceptiont(
"failed to read/link goto model", source_location);
}
}

bool binaries_provided_start =
Expand Down Expand Up @@ -205,8 +208,7 @@ void lazy_goto_modelt::initialize(

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

// stupid hack
Expand Down
24 changes: 14 additions & 10 deletions src/goto-programs/link_goto_model.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ Author: Michael Tautschnig, Daniel Kroening
#include <util/rename_symbol.h>

#include <linking/linking_class.h>
#include <util/exception_utils.h>

#include "goto_model.h"

Expand Down Expand Up @@ -171,15 +172,18 @@ void link_goto_model(
message_handler);

if(linking.typecheck_main())
throw 0;

{
throw invalid_source_file_exceptiont("typechecking main failed");
}
if(link_functions(
dest.symbol_table,
dest.goto_functions,
src.symbol_table,
src.goto_functions,
linking.rename_symbol,
weak_symbols,
linking.object_type_updates))
throw 0;
dest.symbol_table,
dest.goto_functions,
src.symbol_table,
src.goto_functions,
linking.rename_symbol,
weak_symbols,
linking.object_type_updates))
{
throw invalid_source_file_exceptiont("linking failed");
}
}
2 changes: 1 addition & 1 deletion src/goto-programs/loop_ids.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ void show_loop_ids_json(
const goto_programt &goto_program,
json_arrayt &loops)
{
assert(ui==ui_message_handlert::uit::JSON_UI); // use function above
PRECONDITION(ui == ui_message_handlert::uit::JSON_UI); // use function above

forall_goto_program_instructions(it, goto_program)
{
Expand Down
19 changes: 11 additions & 8 deletions src/goto-programs/osx_fat_reader.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,9 @@ Module: Read Mach-O

#include "osx_fat_reader.h"

#include <cassert>
#include <cstdlib>
#include <util/exception_utils.h>
#include <util/invariant.h>

#ifdef __APPLE__
#include <mach-o/fat.h>
Expand Down Expand Up @@ -46,12 +47,13 @@ osx_fat_readert::osx_fat_readert(std::ifstream &in) :
in.read(reinterpret_cast<char*>(&fh), sizeof(struct fat_header));

if(!in)
throw "failed to read OSX fat header";
throw system_exceptiont("failed to read OSX fat header");

if(!is_osx_fat_magic(reinterpret_cast<char*>(&(fh.magic))))
throw "OSX fat header malformed (magic)"; // NOLINT(readability/throw)
throw deserialization_exceptiont("OSX fat header malformed (magic)");

assert(sizeof(fh.nfat_arch)==4);
static_assert(
sizeof(fh.nfat_arch) == 4, "fat_header::nfat_arch is of type uint32_t");
unsigned narch=__builtin_bswap32(fh.nfat_arch);

for(unsigned i=0; !has_gb_arch && i<narch; ++i)
Expand All @@ -61,9 +63,10 @@ osx_fat_readert::osx_fat_readert(std::ifstream &in) :
// NOLINTNEXTLINE(readability/identifiers)
in.read(reinterpret_cast<char*>(&fa), sizeof(struct fat_arch));

assert(sizeof(fa.cputype)==4 &&
sizeof(fa.cpusubtype)==4 &&
sizeof(fa.size)==4);
static_assert(
sizeof(fa.cputype) == 4 && sizeof(fa.cpusubtype) == 4 &&
sizeof(fa.size) == 4,
"This requires a specific fat architecture");
int cputype=__builtin_bswap32(fa.cputype);
int cpusubtype=__builtin_bswap32(fa.cpusubtype);
unsigned size=__builtin_bswap32(fa.size);
Expand All @@ -79,7 +82,7 @@ bool osx_fat_readert::extract_gb(
const std::string &source,
const std::string &dest) const
{
assert(has_gb_arch);
PRECONDITION(has_gb_arch);

return run("lipo", {"lipo", "-thin", "hppa7100LC", "-output", dest, source});
}
2 changes: 1 addition & 1 deletion src/goto-programs/parameter_assignments.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ void parameter_assignmentst::do_function_calls(

// add x=y for f(y) where x is the parameter

assert(function_call.function().id()==ID_symbol);
PRECONDITION(function_call.function().id() == ID_symbol);

const irep_idt &identifier=
to_symbol_expr(function_call.function()).get_identifier();
Expand Down
27 changes: 14 additions & 13 deletions src/goto-programs/pointer_arithmetic.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -32,32 +32,33 @@ void pointer_arithmetict::read(const exprt &src)
}
else if(src.id()==ID_minus)
{
assert(src.operands().size()==2);
read(src.op0());
const unary_minus_exprt o(src.op1(), src.op1().type());
add_to_offset(o);
auto const &minus_src = to_minus_expr(src);
read(minus_src.op0());
const unary_minus_exprt unary_minus(
minus_src.op1(), minus_src.op1().type());
add_to_offset(unary_minus);
}
else if(src.id()==ID_address_of)
{
assert(src.operands().size()==1);
if(src.op0().id()==ID_index)
auto const &address_of_src = to_address_of_expr(src);
if(address_of_src.op().id() == ID_index)
{
const index_exprt &index_expr=
to_index_expr(src.op0());
const index_exprt &index_expr = to_index_expr(address_of_src.op());

if(index_expr.index().is_zero())
make_pointer(src);
make_pointer(address_of_src);
else
{
add_to_offset(index_expr.index());
// produce &x[0] + i instead of &x[i]
exprt new_src=src;
new_src.op0().op1()=from_integer(0, index_expr.index().type());
make_pointer(new_src);
auto new_address_of_src = address_of_src;
new_address_of_src.op().op1() =
from_integer(0, index_expr.index().type());
make_pointer(new_address_of_src);
}
}
else
make_pointer(src);
make_pointer(address_of_src);
}
else
make_pointer(src);
Expand Down
1 change: 0 additions & 1 deletion src/goto-programs/printf_formatter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]

#include "printf_formatter.h"

#include <cassert>
#include <sstream>

#include <util/c_types.h>
Expand Down
5 changes: 4 additions & 1 deletion src/goto-programs/read_bin_goto_object.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,10 @@ static bool read_bin_goto_object_v4(
{
unsigned n=*nit;
rev_target_mapt::const_iterator entry=rev_target_map.find(n);
assert(entry!=rev_target_map.end());
INVARIANT(
entry != rev_target_map.end(),
"something from the target map should also be in the reverse target "
"map");
ins->targets.push_back(entry->second);
}
}
Expand Down
Loading