Skip to content

Reading/writing goto binaries: consistently use return values #7643

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

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Reading/writing goto binaries: consistently use return values #7643

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
5 changes: 2 additions & 3 deletions src/goto-analyzer/static_simplifier.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,6 @@ bool static_simplifier(
goto_model.goto_functions.update();

m.status() << "Writing goto binary" << messaget::eom;
return write_goto_binary(out,
ns.get_symbol_table(),
goto_model.goto_functions);
return write_goto_binary(
out, ns.get_symbol_table(), goto_model.goto_functions, message_handler);
}
2 changes: 1 addition & 1 deletion src/goto-cc/compile.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -601,7 +601,7 @@ bool compilet::write_bin_object_file(
return true;
}

if(write_goto_binary(outfile, src_goto_model))
if(write_goto_binary(outfile, src_goto_model, message_handler))
return true;

const auto cnt = function_body_count(src_goto_model.goto_functions);
Expand Down
9 changes: 7 additions & 2 deletions src/goto-harness/goto_harness_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,8 +163,13 @@ int goto_harness_parse_optionst::doit()
}
else
{
write_goto_binary(
got_harness_config.out_file, goto_model, log.get_message_handler());
if(write_goto_binary(
got_harness_config.out_file, goto_model, log.get_message_handler()))
{
throw deserialization_exceptiont{
"failed to write goto program to file '" + got_harness_config.out_file +
"'"};
}
}

return CPROVER_EXIT_SUCCESS;
Expand Down
3 changes: 3 additions & 0 deletions src/goto-programs/read_bin_goto_object.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,13 +14,16 @@ Date: May 2007
#ifndef CPROVER_GOTO_PROGRAMS_READ_BIN_GOTO_OBJECT_H
#define CPROVER_GOTO_PROGRAMS_READ_BIN_GOTO_OBJECT_H

#include <util/nodiscard.h>

#include <iosfwd>
#include <string>

class symbol_table_baset;
class goto_functionst;
class message_handlert;

NODISCARD
bool read_bin_goto_object(
std::istream &in,
const std::string &filename,
Expand Down
6 changes: 4 additions & 2 deletions src/goto-programs/read_goto_binary.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,12 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H
#define CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H

#include <util/nodiscard.h>
#include <util/optional.h>

#include <list>
#include <string>

#include <util/optional.h>

class goto_modelt;
class message_handlert;

Expand All @@ -30,6 +31,7 @@ bool is_goto_binary(const std::string &filename, message_handlert &);
/// \param [out] dest: GOTO model to update.
/// \param message_handler: for diagnostics
/// \return True on error, false otherwise
NODISCARD
bool read_objects_and_link(
const std::list<std::string> &file_names,
goto_modelt &dest,
Expand Down
22 changes: 14 additions & 8 deletions src/goto-programs/write_goto_binary.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ Author: CM Wintersteiger

#include <fstream>

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

Expand Down Expand Up @@ -144,12 +143,14 @@ static void write_goto_binary(
bool write_goto_binary(
std::ostream &out,
const goto_modelt &goto_model,
message_handlert &message_handler,
int version)
{
return write_goto_binary(
out,
goto_model.symbol_table,
goto_model.goto_functions,
message_handler,
version);
}

Expand All @@ -158,6 +159,7 @@ bool write_goto_binary(
std::ostream &out,
const symbol_table_baset &symbol_table,
const goto_functionst &goto_functions,
message_handlert &message_handler,
int version)
{
// header
Expand All @@ -169,15 +171,19 @@ bool write_goto_binary(

if(version < GOTO_BINARY_VERSION)
{
throw invalid_command_line_argument_exceptiont(
"version " + std::to_string(version) + " no longer supported",
"supported version = " + std::to_string(GOTO_BINARY_VERSION));
messaget message{message_handler};
message.error() << "version " << version << " no longer supported; "
<< "supported version = " << GOTO_BINARY_VERSION
<< messaget::eom;
return true;
Copy link
Member

Choose a reason for hiding this comment

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

Is this an improvement?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Using return values rather than exceptions? I'd argue yes for two reasons:

  1. It is consistent across reading (which already did this) and writing (which now does this) goto binaries.
  2. Using return values to communicate errors makes it easier to build (cross-language) APIs.

}
if(version > GOTO_BINARY_VERSION)
{
throw invalid_command_line_argument_exceptiont(
"unknown goto binary version " + std::to_string(version),
"supported version = " + std::to_string(GOTO_BINARY_VERSION));
messaget message{message_handler};
message.error() << "unknown goto binary version " << version << "; "
<< "supported version = " << GOTO_BINARY_VERSION
<< messaget::eom;
return true;
}
write_goto_binary(out, symbol_table, goto_functions, irepconverter);
return false;
Expand All @@ -198,5 +204,5 @@ bool write_goto_binary(
return true;
}

return write_goto_binary(out, goto_model);
return write_goto_binary(out, goto_model, message_handler);
}
9 changes: 8 additions & 1 deletion src/goto-programs/write_goto_binary.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ Author: CM Wintersteiger

#define GOTO_BINARY_VERSION 5

#include <util/nodiscard.h>

#include <iosfwd>
#include <string>

Expand All @@ -22,17 +24,22 @@ class goto_modelt;
class message_handlert;
class symbol_table_baset;

NODISCARD
bool write_goto_binary(
std::ostream &out,
const goto_modelt &,
int version=GOTO_BINARY_VERSION);
message_handlert &,
int version = GOTO_BINARY_VERSION);

NODISCARD
bool write_goto_binary(
std::ostream &out,
const symbol_table_baset &,
const goto_functionst &,
message_handlert &,
int version = GOTO_BINARY_VERSION);

NODISCARD
bool write_goto_binary(
const std::string &filename,
const goto_modelt &,
Expand Down
2 changes: 1 addition & 1 deletion src/symtab2gb/symtab2gb_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ static void run_symtab2gb(
linked_goto_model.symbol_table.swap(linked_symbol_table);
goto_convert(linked_goto_model, message_handler);

if(failed(write_goto_binary(out_file, linked_goto_model)))
if(failed(write_goto_binary(out_file, linked_goto_model, message_handler)))
{
throw system_exceptiont{"failed to write goto binary to " + gb_filename};
}
Expand Down