Adding a new class LastExceptionBuffer for the purpose of owning the memory for the...

diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp
index 6e51845dd11dcf904713cc2908049ee82bd51ae1..efc71c986f5e1161cf35ed7418de5f26b5638408 100644 (file)
--- 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 6b47de8ccf2300d416ca07a4af22a4f35e6c2aa2..63ed6d53e3b4e5a5acd37863d349b21b22dd057e 100644 (file)
--- 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 87bdfcfa5bc5998ab16954b7ca10bf93ec5584a1..e1486e5bc687b401b4d3d9036d941a3581f57cd6 100644 (file)
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -16,10 +16,11 @@
 
 #include "base/exception.h"
 
-#include <string>
+#include <cstdarg>
 #include <cstdio>
 #include <cstdlib>
-#include <cstdarg>
+#include <cstring>
+#include <string>
 
 #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 84872b9b14a31fd240c7fc5a9497c52f47ec7445..02384b6cbbc20c21593d7aae72c5f50fc9f9c89a 100644 (file)
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -27,6 +27,8 @@
 #include <stdexcept>
 #include <string>
 
+#include "base/tls.h"
+
 namespace CVC4 {
 
 class CVC4_PUBLIC Exception : public std::exception {
@@ -136,6 +138,30 @@ template <class T> 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 2b5c0a2c8e86e6ce2a46754b8c3b3a34c874b392..cf9a772b7f098960c13f05d20a62a7c28b6c9d71 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -18,6 +18,7 @@
 #include <iostream>
 #include <cstring>
 
+#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 ce4e4509d8f04f4c97df8b019aac7d078a6e44bc..bc3d45287bf16a8085e91cbd016980bc8876bb79 100644 (file)
--- 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<const char*>(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);