From: Tim King Date: Tue, 5 Jan 2016 19:36:30 +0000 (-0800) Subject: Adding a new class LastExceptionBuffer for the purpose of owning the memory for the... X-Git-Tag: cvc5-1.0.0~6121 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b717513e2a1d956c4456d13e0625957fc84c2449;p=cvc5.git Adding a new class LastExceptionBuffer for the purpose of owning the memory for the last exception C string. This replaces s_debugLastException. --- diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp index 6e51845dd..efc71c986 100644 --- a/src/base/cvc4_assert.cpp +++ b/src/base/cvc4_assert.cpp @@ -26,9 +26,10 @@ using namespace std; namespace CVC4 { #ifdef CVC4_DEBUG -CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; +//CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; #endif /* CVC4_DEBUG */ + void AssertionException::construct(const char* header, const char* extra, const char* function, const char* file, unsigned line, const char* fmt, @@ -71,13 +72,14 @@ void AssertionException::construct(const char* header, const char* extra, setMessage(string(buf)); #ifdef CVC4_DEBUG - if(s_debugLastException == NULL) { - // we leak buf[] but only in debug mode with assertions failing - s_debugLastException = buf; + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if(buffer != NULL){ + if(buffer->getContents() == NULL) { + buffer->setContents(buf); + } } -#else /* CVC4_DEBUG */ - delete [] buf; #endif /* CVC4_DEBUG */ + delete [] buf; } void AssertionException::construct(const char* header, const char* extra, @@ -111,14 +113,16 @@ void AssertionException::construct(const char* header, const char* extra, setMessage(string(buf)); + #ifdef CVC4_DEBUG - // we leak buf[] but only in debug mode with assertions failing - if(s_debugLastException == NULL) { - s_debugLastException = buf; + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if(buffer != NULL){ + if(buffer->getContents() == NULL) { + buffer->setContents(buf); + } } -#else /* CVC4_DEBUG */ - delete [] buf; #endif /* CVC4_DEBUG */ + delete [] buf; } #ifdef CVC4_DEBUG diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h index 6b47de8cc..63ed6d53e 100644 --- a/src/base/cvc4_assert.h +++ b/src/base/cvc4_assert.h @@ -235,8 +235,6 @@ public: #ifdef CVC4_DEBUG -extern CVC4_THREADLOCAL(const char*) s_debugLastException; - /** * Special assertion failure handling in debug mode; in non-debug * builds, the exception is thrown from the macro. We factor out this @@ -254,9 +252,12 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l // details of the exception # define AlwaysAssert(cond, msg...) \ do { \ - if(__builtin_expect( ( ! (cond) ), false )) { \ + if(__builtin_expect( ( ! (cond) ), false )) { \ /* save the last assertion failure */ \ - const char* lastException = ::CVC4::s_debugLastException; \ + ::CVC4::LastExceptionBuffer* buffer = \ + ::CVC4::LastExceptionBuffer::getCurrent(); \ + const char* lastException = (buffer == NULL) ? \ + NULL : buffer->getContents(); \ ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ ::CVC4::debugAssertionFailed(exception, lastException); \ } \ diff --git a/src/base/exception.cpp b/src/base/exception.cpp index 87bdfcfa5..e1486e5bc 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -16,10 +16,11 @@ #include "base/exception.h" -#include +#include #include #include -#include +#include +#include #include "base/cvc4_assert.h" @@ -27,6 +28,28 @@ using namespace std; namespace CVC4 { +CVC4_THREADLOCAL(LastExceptionBuffer*) LastExceptionBuffer::s_currentBuffer = NULL; + +LastExceptionBuffer::LastExceptionBuffer() : d_contents(NULL) {} + +LastExceptionBuffer::~LastExceptionBuffer() { + if(d_contents != NULL){ + free(d_contents); + d_contents = NULL; + } +} + +void LastExceptionBuffer::setContents(const char* string) { + if(d_contents != NULL){ + free(d_contents); + d_contents = NULL; + } + + if(string != NULL){ + d_contents = strdup(string); + } +} + char* IllegalArgumentException::s_header = "Illegal argument detected"; std::string IllegalArgumentException::formatVariadic() { @@ -107,13 +130,14 @@ void IllegalArgumentException::construct(const char* header, const char* extra, setMessage(string(buf)); #ifdef CVC4_DEBUG - if(s_debugLastException == NULL) { - // we leak buf[] but only in debug mode with assertions failing - s_debugLastException = buf; + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if(buffer != NULL){ + if(buffer->getContents() == NULL) { + buffer->setContents(buf); + } } -#else /* CVC4_DEBUG */ - delete [] buf; #endif /* CVC4_DEBUG */ + delete [] buf; } void IllegalArgumentException::construct(const char* header, const char* extra, @@ -147,13 +171,14 @@ void IllegalArgumentException::construct(const char* header, const char* extra, setMessage(string(buf)); #ifdef CVC4_DEBUG - if(s_debugLastException == NULL) { - // we leak buf[] but only in debug mode with assertions failing - s_debugLastException = buf; + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if(buffer != NULL){ + if(buffer->getContents() == NULL) { + buffer->setContents(buf); + } } -#else /* CVC4_DEBUG */ - delete [] buf; #endif /* CVC4_DEBUG */ + delete [] buf; } } /* namespace CVC4 */ diff --git a/src/base/exception.h b/src/base/exception.h index 84872b9b1..02384b6cb 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -27,6 +27,8 @@ #include #include +#include "base/tls.h" + namespace CVC4 { class CVC4_PUBLIC Exception : public std::exception { @@ -136,6 +138,30 @@ template inline void CheckArgument(bool cond, const T& arg) { } \ } +class CVC4_PUBLIC LastExceptionBuffer { +public: + LastExceptionBuffer(); + ~LastExceptionBuffer(); + + void setContents(const char* string); + const char* getContents() const { return d_contents; } + + static LastExceptionBuffer* getCurrent() { return s_currentBuffer; } + static void setCurrent(LastExceptionBuffer* buffer) { s_currentBuffer = buffer; } + + static const char* currentContents() { + return (getCurrent() == NULL) ? NULL : getCurrent()->getContents(); + } + +private: + /* Disallow copies */ + LastExceptionBuffer(const LastExceptionBuffer&) CVC4_UNUSED; + LastExceptionBuffer& operator=(const LastExceptionBuffer&) CVC4_UNUSED; + + char* d_contents; + + static CVC4_THREADLOCAL(LastExceptionBuffer*) s_currentBuffer; +}; /* class LastExceptionBuffer */ }/* CVC4 namespace */ diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 2b5c0a2c8..cf9a772b7 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -18,6 +18,7 @@ #include #include +#include "base/exception.h" #include "base/output.h" #include "expr/attribute.h" @@ -31,8 +32,10 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, Exception(message), d_node(new Node(node)) { #ifdef CVC4_DEBUG - // yes, this leaks memory, but only in debug modes with exceptions occurring - s_debugLastException = strdup(toString().c_str()); + LastExceptionBuffer* current = LastExceptionBuffer::getCurrent(); + if(current != NULL){ + current->setContents(toString().c_str()); + } #endif /* CVC4_DEBUG */ } diff --git a/src/main/util.cpp b/src/main/util.cpp index ce4e4509d..bc3d45287 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -44,7 +44,7 @@ using namespace std; namespace CVC4 { #ifdef CVC4_DEBUG - extern CVC4_THREADLOCAL(const char*) s_debugLastException; +//extern CVC4_THREADLOCAL(const char*) s_debugLastException; #endif /* CVC4_DEBUG */ namespace main { @@ -167,12 +167,14 @@ void cvc4unexpected() { "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) { + + const char* lastContents = LastExceptionBuffer::currentContents(); + + if(lastContents == 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", - static_cast(CVC4::s_debugLastException)); + fprintf(stderr, "The exception is:\n%s\n\n", lastContents); } if(!segvSpin) { if((*pOptions)[options::statistics] && pExecutor != NULL) { @@ -201,6 +203,10 @@ void cvc4unexpected() { void cvc4terminate() { set_terminate(default_terminator); #ifdef CVC4_DEBUG + LastExceptionBuffer* current = LastExceptionBuffer::getCurrent(); + LastExceptionBuffer::setCurrent(NULL); + delete current; + fprintf(stderr, "\n" "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding. " @@ -224,6 +230,10 @@ void cvc4terminate() { /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw(Exception) { +#ifdef CVC4_DEBUG + LastExceptionBuffer::setCurrent(new LastExceptionBuffer()); +#endif + #ifndef __WIN32__ stack_t ss; ss.ss_sp = malloc(SIGSTKSZ);