diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 1403b04f403..42aa3afdd56 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -40,7 +40,7 @@ std::string invalid_function_contract_pair_exceptiont::what() const std::string res; res += "Invalid function-contract mapping"; - res += "\nReason: " + reason; + res += "\nReason: " + reason(); if(!correct_format.empty()) { diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index ec7a01fa037..02f407d26a5 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -98,7 +98,7 @@ std::string invalid_restriction_exceptiont::what() const std::string res; res += "Invalid restriction"; - res += "\nReason: " + reason; + res += "\nReason: " + reason(); if(!correct_format.empty()) { diff --git a/src/solvers/smt2/smt2_tokenizer.h b/src/solvers/smt2/smt2_tokenizer.h index 6cfd4dc2e81..39b5d553f87 100644 --- a/src/solvers/smt2/smt2_tokenizer.h +++ b/src/solvers/smt2/smt2_tokenizer.h @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H #define CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H +#include + #include #include #include @@ -27,48 +29,26 @@ class smt2_tokenizert } /// Exception thrown by the tokenizer (and the parser built on top of - /// it) to report a syntactic error at a known source line. Holds an - /// `std::ostringstream` so that callers can assemble the diagnostic - /// piecewise via `operator<<`. - class smt2_errort + /// it) to report a syntactic error at a known source line. + class smt2_errort : public cprover_exception_baset { public: - smt2_errort(smt2_errort &&) = default; - - smt2_errort(const smt2_errort &other) - { - // ostringstream does not have a copy constructor - message << other.message.str(); - line_no = other.line_no; - } - smt2_errort(const std::string &_message, unsigned _line_no) : line_no(_line_no) { - message << _message; + _reason << _message; } explicit smt2_errort(unsigned _line_no) : line_no(_line_no) { } - std::string what() const - { - return message.str(); - } - unsigned get_line_no() const { return line_no; } - std::ostringstream &message_ostream() - { - return message; - } - protected: - std::ostringstream message; unsigned line_no; }; @@ -199,15 +179,6 @@ class smt2_tokenizert tokent read_token(); }; -/// add to the diagnostic information in the given smt2_tokenizer exception -template -smt2_tokenizert::smt2_errort -operator<<(smt2_tokenizert::smt2_errort &&e, const T &message) -{ - e.message_ostream() << message; - return std::move(e); -} - bool is_smt2_simple_symbol_character(char); #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H diff --git a/src/util/exception_utils.cpp b/src/util/exception_utils.cpp index 234af0c396c..57ad4cd038f 100644 --- a/src/util/exception_utils.cpp +++ b/src/util/exception_utils.cpp @@ -11,7 +11,7 @@ Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com std::string cprover_exception_baset::what() const { - return reason; + return reason(); } std::string invalid_command_line_argument_exceptiont::what() const @@ -19,7 +19,7 @@ std::string invalid_command_line_argument_exceptiont::what() const std::string res; res += "Invalid User Input"; res += "\nOption: " + option; - res += "\nReason: " + reason; + res += "\nReason: " + reason(); // Print an optional correct usage message assuming correct input parameters have been passed if(!correct_input.empty()) { @@ -58,7 +58,7 @@ incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont( std::string incorrect_goto_program_exceptiont::what() const { - std::string ret(reason); + std::string ret(reason()); if(!source_location.is_nil()) ret += " (at: " + source_location.as_string() + ")"; @@ -95,5 +95,5 @@ invalid_source_file_exceptiont::invalid_source_file_exceptiont( std::string invalid_source_file_exceptiont::what() const { - return source_location.as_string() + ": " + reason; + return source_location.as_string() + ": " + reason(); } diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h index e48438516ca..c6f9f951936 100644 --- a/src/util/exception_utils.h +++ b/src/util/exception_utils.h @@ -9,11 +9,14 @@ Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com #ifndef CPROVER_UTIL_EXCEPTION_UTILS_H #define CPROVER_UTIL_EXCEPTION_UTILS_H -#include - #include "invariant.h" #include "source_location.h" +#include +#include +#include +#include + /// Base class for exceptions thrown in the cprover project. /// Intended to be used as a convenient way to have a /// "catch all and report errors" from application entry points. @@ -30,20 +33,58 @@ class cprover_exception_baset virtual std::string what() const; virtual ~cprover_exception_baset() = default; + cprover_exception_baset() = default; + + cprover_exception_baset(cprover_exception_baset &&) = default; + + // std::ostringstream does not have a copy constructor + cprover_exception_baset(const cprover_exception_baset &src) + { + _reason << src.reason(); + } + + std::string reason() const + { + return _reason.str(); + } + protected: /// This constructor is marked protected to ensure this class isn't used /// directly. Deriving classes should be used to more precisely describe the /// problem that occurred. explicit cprover_exception_baset(std::string reason) - : reason(std::move(reason)) { + // ostringstream does not have an appropriate constructor + _reason << reason; } /// The reason this exception was generated. This is the string returned by - /// `what()` unless that method is overridden - std::string reason; + /// `what()` unless that method is overridden. This is an ostringstream + /// to enable efficient appending with <<. + std::ostringstream _reason; + + // to provide access to the _reason field + template + friend std::enable_if_t< + std::is_base_of>::value, + E &&> + operator<<(E &&, const T &); }; +/// add to the diagnostic information in the given +/// cprover_exception_baset exception; the type of the +/// exception is preserved, enabling +/// `throw some_exceptiont{...} << "text"` +template +std::enable_if_t< + std::is_base_of>::value, + E &&> +operator<<(E &&e, const T &message) +{ + e._reason << message; + return std::forward(e); +} + /// Thrown when users pass incorrect command line arguments, /// for example passing no files to analysis or setting /// two mutually exclusive flags @@ -176,9 +217,10 @@ class invalid_source_file_exceptiont : public invalid_input_exceptiont source_locationt source_location); std::string what() const override; - const std::string &get_reason() const + // This method will go away, in favor of cprover_exception_baset::reason + std::string get_reason() const { - return reason; + return reason(); } const source_locationt &get_source_location() const diff --git a/unit/Makefile b/unit/Makefile index e7c008c4539..15663628523 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -150,6 +150,7 @@ SRC += analyses/ai/ai.cpp \ util/dense_integer_map.cpp \ util/dstring.cpp \ util/edit_distance.cpp \ + util/exception_utils.cpp \ util/expr_cast/expr_cast.cpp \ util/expr_initializer.cpp \ util/expr.cpp \ diff --git a/unit/util/exception_utils.cpp b/unit/util/exception_utils.cpp new file mode 100644 index 00000000000..a05ceee0f45 --- /dev/null +++ b/unit/util/exception_utils.cpp @@ -0,0 +1,59 @@ +/*******************************************************************\ + +Module: Unit tests for cprover_exception_baset + +Author: Daniel Kroening + +\*******************************************************************/ + +#include + +#include + +TEST_CASE( + "cprover_exception_baset default construction", + "[core][util][exception_utils]") +{ + cprover_exception_baset e; + CHECK(e.reason().empty()); +} + +TEST_CASE( + "cprover_exception_baset with message via operator<<", + "[core][util][exception_utils]") +{ + auto e = cprover_exception_baset{} << "something went wrong"; + CHECK(e.what() == "something went wrong"); +} + +TEST_CASE( + "cprover_exception_baset streaming multiple values", + "[core][util][exception_utils]") +{ + auto e = cprover_exception_baset{} << "error " << 42 << " occurred"; + CHECK(e.what() == "error 42 occurred"); +} + +TEST_CASE( + "operator<< preserves the exception type", + "[core][util][exception_utils]") +{ + // must not slice to cprover_exception_baset + REQUIRE_THROWS_AS( + throw system_exceptiont{"file"} << " not found", system_exceptiont); +} + +TEST_CASE( + "cprover_exception_baset copy constructor", + "[core][util][exception_utils]") +{ + auto original = cprover_exception_baset{} << "copy test"; + + cprover_exception_baset copy(original); + CHECK(copy.what() == "copy test"); + + // Modifying the copy doesn't affect the original + copy << " extra"; + CHECK(copy.what() == "copy test extra"); + CHECK(original.what() == "copy test"); +}