Add additional exception classes and introduce base exception

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