From fb1be5d8495b3d3dd53925d2cbe79b4c710d791d Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Wed, 19 Sep 2018 16:51:48 +0100 Subject: [PATCH] Add additional exception classes and introduce base exception This adds a number of new exception classes that are meant to be used to replace unstructured throws in other parts of the code. The exception types have been selected according to what we already determined we are going to need. Further, this has a slight fix in the format for invalid_user_input_exceptiont (it did previously not add a separator between the reason and the suggestion on how to fix the error). This also adds a cprover_exception_baset which is mean to avoid unnecessary overhead when adding new exception types - without it, all driver programs would have to updated to explicitly catch the new exception type whenever we introduce one. Also removes some dead code parse_options_baset (there was a final return that cannot be reached because all ancestor statements are returns). --- src/goto-cc/goto_cc_mode.cpp | 6 +++ src/util/exception_utils.cpp | 67 +++++++++++++++++++++++++--- src/util/exception_utils.h | 86 +++++++++++++++++++++++++++++++++--- src/util/parse_options.cpp | 8 +++- 4 files changed, 154 insertions(+), 13 deletions(-) diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp index a971c954af5..59cebe82e2f 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/src/goto-cc/goto_cc_mode.cpp @@ -22,6 +22,7 @@ Author: CM Wintersteiger, 2006 #include #endif +#include #include #include @@ -106,6 +107,11 @@ int goto_cc_modet::main(int argc, const char **argv) error() << "Out of memory" << eom; return EX_SOFTWARE; } + catch(const cprover_exception_baset &e) + { + error() << e.what() << eom; + return EX_SOFTWARE; + } } /// prints a message informing the user about incorrect options diff --git a/src/util/exception_utils.cpp b/src/util/exception_utils.cpp index 148ddc742cd..d43ccba01d8 100644 --- a/src/util/exception_utils.cpp +++ b/src/util/exception_utils.cpp @@ -7,14 +7,71 @@ Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com \*******************************************************************/ #include "exception_utils.h" +#include -std::string invalid_user_input_exceptiont::what() const noexcept +std::string invalid_user_input_exceptiont::what() const { std::string res; - res += "\nInvalid User Input\n"; - res += "Option: " + option + "\n"; - res += "Reason: " + reason; + res += "Invalid User Input"; + res += "\nOption: " + option; + res += "\nReason: " + reason; // Print an optional correct usage message assuming correct input parameters have been passed - res += correct_input + "\n"; + if(!correct_input.empty()) + { + res += "\nSuggestion: " + correct_input; + } return res; } + +invalid_user_input_exceptiont::invalid_user_input_exceptiont( + std::string reason, + std::string option, + std::string correct_input) + : reason(std::move(reason)), + option(std::move(option)), + correct_input(std::move(correct_input)) +{ +} + +system_exceptiont::system_exceptiont(std::string message) + : message(std::move(message)) +{ +} + +std::string system_exceptiont::what() const +{ + return message; +} + +deserialization_exceptiont::deserialization_exceptiont(std::string message) + : message(std::move(message)) +{ +} + +std::string deserialization_exceptiont::what() const +{ + return message; +} + +incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont( + std::string message, + source_locationt source_location) + : message(std::move(message)), source_location(std::move(source_location)) +{ +} + +unsupported_operation_exceptiont::unsupported_operation_exceptiont( + std::string message) + : message(std::move(message)) +{ +} + +std::string incorrect_goto_program_exceptiont::what() const +{ + return message + " (at: " + source_location.as_string() + ")"; +} + +std::string unsupported_operation_exceptiont::what() const +{ + return message; +} diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h index 4c871b94fbf..163284cf2ca 100644 --- a/src/util/exception_utils.h +++ b/src/util/exception_utils.h @@ -11,7 +11,24 @@ Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com #include -class invalid_user_input_exceptiont +#include "source_location.h" + +/// 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. +class cprover_exception_baset +{ +public: + /// A human readable description of what went wrong. + /// For readability, implementors should not add a leading + /// or trailing newline to this description. + virtual std::string what() const = 0; +}; + +/// Thrown when users pass incorrect command line arguments, +/// for example passing no files to analysis or setting +/// two mutually exclusive flags +class invalid_user_input_exceptiont : public cprover_exception_baset { /// The reason this exception was generated. std::string reason; @@ -25,12 +42,69 @@ class invalid_user_input_exceptiont invalid_user_input_exceptiont( std::string reason, std::string option, - std::string correct_input = "") - : reason(reason), option(option), correct_input(correct_input) - { - } + std::string correct_input = ""); + + std::string what() const override; +}; + +/// Thrown when some external system fails unexpectedly. +/// Examples are IO exceptions (files not present, or we don't +/// have the right permissions to interact with them), timeouts for +/// external processes etc +class system_exceptiont : public cprover_exception_baset +{ +public: + explicit system_exceptiont(std::string message); + std::string what() const override; + +private: + std::string message; +}; + +/// Thrown when failing to deserialize a value from some +/// low level format, like JSON or raw bytes +class deserialization_exceptiont : public cprover_exception_baset +{ +public: + explicit deserialization_exceptiont(std::string message); + + std::string what() const override; + +private: + std::string message; +}; + +/// Thrown when a goto program that's being processed is in an invalid format, +/// for example passing the wrong number of arguments to functions. +/// Note that this only applies to goto programs that are user provided, +/// that internal transformations on goto programs don't produce invalid +/// programs should be guarded by invariants instead. +/// \see invariant.h +class incorrect_goto_program_exceptiont : public cprover_exception_baset +{ +public: + incorrect_goto_program_exceptiont( + std::string message, + source_locationt source_location); + std::string what() const override; + +private: + std::string message; + source_locationt source_location; +}; + +/// Thrown when we encounter an instruction, parameters to an instruction etc. +/// in a goto program that has some theoretically valid semantics, +/// but that we don't presently have any support for. +class unsupported_operation_exceptiont : public cprover_exception_baset +{ +public: + explicit unsupported_operation_exceptiont(std::string message); + std::string what() const override; - std::string what() const noexcept; +private: + /// The unsupported operation causing this fault to occur. + std::string message; }; #endif // CPROVER_UTIL_EXCEPTION_UTILS_H diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index b5a1b7e9b1f..770bb4ac31a 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -71,12 +71,16 @@ int parse_options_baset::main() return doit(); } - catch(invalid_user_input_exceptiont &e) + catch(const invalid_user_input_exceptiont &e) { std::cerr << e.what() << "\n"; return CPROVER_EXIT_USAGE_ERROR; } - return CPROVER_EXIT_SUCCESS; + catch(const cprover_exception_baset &e) + { + std::cerr << e.what() << '\n'; + return CPROVER_EXIT_EXCEPTION; + } } std::string