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).

Author: hannes-steffenhagen-diffblue

src/goto-cc/goto_cc_mode.cpp

@@ -22,6 +22,7 @@ Author: CM Wintersteiger, 2006
 #include <sysexits.h>
 #endif
 
+#include <util/exception_utils.h>
 #include <util/parse_options.h>
 #include <util/version.h>
 
@@ -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

src/util/exception_utils.cpp

@@ -7,14 +7,71 @@ Author: Fotis Koutoulakis, [email protected]
 \*******************************************************************/
 
 #include "exception_utils.h"
+#include <utility>
 
-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;
+}

src/util/exception_utils.h

@@ -11,7 +11,24 @@ Author: Fotis Koutoulakis, [email protected]
 
 #include <string>
 
-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

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