diff options
| -rw-r--r-- | src/main/util.cpp | 21 | ||||
| -rw-r--r-- | src/util/Assert.cpp | 52 | ||||
| -rw-r--r-- | src/util/Assert.h | 46 |
3 files changed, 84 insertions, 35 deletions
diff --git a/src/main/util.cpp b/src/main/util.cpp index eb7b56b19..c685766fa 100644 --- 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 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) )) { \ |