better exception wording, assertion-handling in multiple-exception case; resolves bug 175. also newer URL for config/pkg.m4

2 files changed, 73 insertions, 25 deletions

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index dbf292108..7856b3da4 100644
--- 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 0809257bf..62375daff 100644
--- 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) )) {                                   \