introduce << on cprover_exception_baset

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())
   {

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())
   {

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 <util/exception_utils.h>
+
 #include <optional>
 #include <sstream>
 #include <string>
@@ -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 <typename T>
-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

src/util/exception_utils.cpp

@@ -11,15 +11,15 @@ 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
 {
   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();
 }

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 <string>
-
 #include "invariant.h"
 #include "source_location.h"
 
+#include <sstream>
+#include <string>
+#include <type_traits>
+#include <utility>
+
 /// 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 <typename E, typename T>
+  friend std::enable_if_t<
+    std::is_base_of<cprover_exception_baset, std::decay_t<E>>::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 <typename E, typename T>
+std::enable_if_t<
+  std::is_base_of<cprover_exception_baset, std::decay_t<E>>::value,
+  E &&>
+operator<<(E &&e, const T &message)
+{
+  e._reason << message;
+  return std::forward<E>(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

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 \

unit/util/exception_utils.cpp

@@ -0,0 +1,59 @@
+/*******************************************************************\
+
+Module: Unit tests for cprover_exception_baset
+
+Author: Daniel Kroening
+
+\*******************************************************************/
+
+#include <util/exception_utils.h>
+
+#include <testing-utils/use_catch.h>
+
+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");
+}