better exception wording, assertion-handling in multiple-exception case; resolves...

diff --git a/src/main/util.cpp b/src/main/util.cpp
index eb7b56b19155d242650e039e982b8b4cbee9f59a..c685766fa88f60a7daee476601a1f5631fff6017 100644 (file)
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -72,14 +72,15 @@ static terminate_handler default_terminator;
 
 void cvc4unexpected() {
 #ifdef CVC4_DEBUG
-  fprintf(stderr,
-          "\n"
-          "CVC4 threw an \"unexpected\" exception (one that wasn't properly specified\n"
-          "in the throws() specifier for the throwing function).\n\n");
-  if(CVC4::s_debugAssertionFailure == NULL) {
-    fprintf(stderr, "The exception is unknown.\n\n");
+  fprintf(stderr, "\n"
+          "CVC4 threw an \"unexpected\" exception (one that wasn't properly "
+          "specified\nin the throws() specifier for the throwing function)."
+          "\n\n");
+  if(CVC4::s_debugLastException == NULL) {
+    fprintf(stderr,
+            "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
   } else {
-    fprintf(stderr, "The exception is:\n%s\n\n", CVC4::s_debugAssertionFailure);
+    fprintf(stderr, "The exception is:\n%s\n\n", CVC4::s_debugLastException);
   }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
@@ -99,10 +100,10 @@ void cvc4unexpected() {
 
 void cvc4terminate() {
 #ifdef CVC4_DEBUG
-  fprintf(stderr,
-          "\n"
+  fprintf(stderr, "\n"
           "CVC4 was terminated by the C++ runtime.\n"
-          "Perhaps an exception was thrown during stack unwinding.  (Don't do that.)\n");
+          "Perhaps an exception was thrown during stack unwinding.  "
+          "(Don't do that.)\n");
   default_terminator();
 #else /* CVC4_DEBUG */
   fprintf(stderr,

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index dbf2921081bd7cf92173c9b341178976e03ce30c..7856b3da4cf96fa1135bdb108a3e54521b1a86a1 100644 (file)
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -28,7 +28,7 @@ using namespace std;
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG
-__thread CVC4_PUBLIC const char* s_debugAssertionFailure = NULL;
+__thread CVC4_PUBLIC const char* s_debugLastException = NULL;
 #endif /* CVC4_DEBUG */
 
 void AssertionException::construct(const char* header, const char* extra,
@@ -73,9 +73,9 @@ void AssertionException::construct(const char* header, const char* extra,
   setMessage(string(buf));
 
 #ifdef CVC4_DEBUG
-  if(s_debugAssertionFailure == NULL) {
+  if(s_debugLastException == NULL) {
     // we leak buf[] but only in debug mode with assertions failing
-    s_debugAssertionFailure = buf;
+    s_debugLastException = buf;
   }
 #else /* CVC4_DEBUG */
   delete [] buf;
@@ -115,12 +115,54 @@ void AssertionException::construct(const char* header, const char* extra,
 
 #ifdef CVC4_DEBUG
   // we leak buf[] but only in debug mode with assertions failing
-  if(s_debugAssertionFailure == NULL) {
-    s_debugAssertionFailure = buf;
+  if(s_debugLastException == NULL) {
+    s_debugLastException = buf;
   }
 #else /* CVC4_DEBUG */
   delete [] buf;
 #endif /* CVC4_DEBUG */
 }
 
+#ifdef CVC4_DEBUG
+
+/**
+ * Special assertion failure handling in debug mode; in non-debug
+ * builds, the exception is thrown from the macro.  We factor out this
+ * additional logic so as not to bloat the code at every Assert()
+ * expansion.
+ *
+ * Note this name is prefixed with "debug" because it is included in
+ * debug builds only; in debug builds, it handles all assertion
+ * failures (even those that exist in non-debug builds).
+ */
+void debugAssertionFailed(const AssertionException& thisException,
+                          const char* propagatingException) {
+  static __thread bool alreadyFired = false;
+
+  if(EXPECT_TRUE( !std::uncaught_exception() ) || alreadyFired) {
+    throw thisException;
+  }
+
+  alreadyFired = true;
+
+  // propagatingException is the propagating exception, but can be
+  // NULL if the propagating exception is not a CVC4::Exception.
+  Warning() << "===========================================" << std::endl
+            << "An assertion failed during stack unwinding:" << std::endl;
+  if(propagatingException != NULL) {
+    Warning() << "The propagating exception is:" << std::endl
+              << propagatingException << std::endl
+              << "===========================================" << std::endl;
+    Warning() << "The newly-thrown exception is:" << std::endl;
+  } else {
+    Warning() << "The propagating exception is unknown." << std::endl;
+  }
+  Warning() << thisException << std::endl
+            << "===========================================" << std::endl;
+
+  terminate();
+}
+
+#endif /* CVC4_DEBUG */
+
 }/* CVC4 namespace */

diff --git a/src/util/Assert.h b/src/util/Assert.h
index 0809257bf3dfc23e8d63e121bbd58ca427f444a9..62375daffd9db27cd3aca06be7553bfd1fb19017 100644 (file)
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -198,33 +198,39 @@ public:
 
 #ifdef CVC4_DEBUG
 
-extern __thread CVC4_PUBLIC const char* s_debugAssertionFailure;
+#ifdef CVC4_DEBUG
+extern __thread CVC4_PUBLIC const char* s_debugLastException;
+#endif /* CVC4_DEBUG */
+
+/**
+ * Special assertion failure handling in debug mode; in non-debug
+ * builds, the exception is thrown from the macro.  We factor out this
+ * additional logic so as not to bloat the code at every Assert()
+ * expansion.
+ *
+ * Note this name is prefixed with "debug" because it is included in
+ * debug builds only; in debug builds, it handles all assertion
+ * failures (even those that exist in non-debug builds).
+ */
+void debugAssertionFailed(const AssertionException& thisException,
+                          const char* lastException) CVC4_PUBLIC;
 
 // If we're currently handling an exception, print a warning instead;
 // otherwise std::terminate() is called by the runtime and we lose
 // details of the exception
-#define AlwaysAssert(cond, msg...)                                      \
-  do {                                                                  \
-    if(EXPECT_FALSE( ! (cond) )) {                                      \
-      if(EXPECT_FALSE( std::uncaught_exception() )) {                   \
-        Warning() << "===========================================" << std::endl \
-                  << "An assertion failed during stack unwinding:" << std::endl \
-                  << AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) << std::endl \
-                  << "===========================================" << std::endl; \
-        if(s_debugAssertionFailure != NULL) {                           \
-          Warning() << "The propagating exception is:" << std::endl     \
-                    << s_debugAssertionFailure << std::endl             \
-                    << "===========================================" << std::endl; \
-          s_debugAssertionFailure = NULL;                               \
-        }                                                               \
-      } else {                                                          \
-        throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+#  define AlwaysAssert(cond, msg...)                                    \
+    do {                                                                \
+      if(EXPECT_FALSE( ! (cond) )) {                                    \
+        /* save the last assertion failure */                           \
+        const char* lastException = s_debugLastException;               \
+        AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+        debugAssertionFailed(exception, lastException);                 \
       }                                                                 \
-    }                                                                   \
-  } while(0)
+    } while(0)
+
 #else /* CVC4_DEBUG */
 // These simpler (but less useful) versions for non-debug builds fails
-// with terminate() if thrown during stack unwinding.
+// will terminate() if thrown during stack unwinding.
 #  define AlwaysAssert(cond, msg...)                                    \
      do {                                                               \
        if(EXPECT_FALSE( ! (cond) )) {                                   \