From d6946221a041070e6e956901300df73747104920 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Apr 2023 11:05:37 +0000 Subject: [PATCH] Reading/writing goto binaries: consistently use return values Always use the return value to communicate errors, not a mix of return values and exceptions. --- src/goto-analyzer/static_simplifier.cpp | 5 ++--- src/goto-cc/compile.cpp | 2 +- .../goto_harness_parse_options.cpp | 9 ++++++-- src/goto-programs/read_bin_goto_object.h | 3 +++ src/goto-programs/read_goto_binary.h | 6 +++-- src/goto-programs/write_goto_binary.cpp | 22 ++++++++++++------- src/goto-programs/write_goto_binary.h | 9 +++++++- src/symtab2gb/symtab2gb_parse_options.cpp | 2 +- 8 files changed, 40 insertions(+), 18 deletions(-) diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index 046081038ea..8765bbf759d 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -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); } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 613e17bd94a..988dadf3af4 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -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); diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index 427283eaa2b..c45f3337414 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -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; diff --git a/src/goto-programs/read_bin_goto_object.h b/src/goto-programs/read_bin_goto_object.h index 6b0d9361787..4419749214a 100644 --- a/src/goto-programs/read_bin_goto_object.h +++ b/src/goto-programs/read_bin_goto_object.h @@ -14,6 +14,8 @@ Date: May 2007 #ifndef CPROVER_GOTO_PROGRAMS_READ_BIN_GOTO_OBJECT_H #define CPROVER_GOTO_PROGRAMS_READ_BIN_GOTO_OBJECT_H +#include + #include #include @@ -21,6 +23,7 @@ class symbol_table_baset; class goto_functionst; class message_handlert; +NODISCARD bool read_bin_goto_object( std::istream &in, const std::string &filename, diff --git a/src/goto-programs/read_goto_binary.h b/src/goto-programs/read_goto_binary.h index 462657df8b6..0d2fe903258 100644 --- a/src/goto-programs/read_goto_binary.h +++ b/src/goto-programs/read_goto_binary.h @@ -12,11 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H #define CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H +#include +#include + #include #include -#include - class goto_modelt; class message_handlert; @@ -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 &file_names, goto_modelt &dest, diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index cb7d43de9e8..1b4ba794344 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -13,7 +13,6 @@ Author: CM Wintersteiger #include -#include #include #include @@ -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); } @@ -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 @@ -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; } 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; @@ -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); } diff --git a/src/goto-programs/write_goto_binary.h b/src/goto-programs/write_goto_binary.h index d0f61c5eccf..1c2ac69ca19 100644 --- a/src/goto-programs/write_goto_binary.h +++ b/src/goto-programs/write_goto_binary.h @@ -14,6 +14,8 @@ Author: CM Wintersteiger #define GOTO_BINARY_VERSION 5 +#include + #include #include @@ -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 &, diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp index eead2e33eae..8c6191803c4 100644 --- a/src/symtab2gb/symtab2gb_parse_options.cpp +++ b/src/symtab2gb/symtab2gb_parse_options.cpp @@ -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}; }