src/util/Assert.cpp

   1 /*********************                                                        */
   2 /*! \file Assert.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): acsys
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Assertion utility classes, functions, and exceptions.
  15  **
  16  ** Assertion utility classes, functions, and exceptions.  Implementation.
  17  **/
  18
  19 #include <new>
  20 #include <cstdarg>
  21 #include <cstdio>
  22
  23 #include "util/Assert.h"
  24 #include "util/exception.h"
  25 #include "util/tls.h"
  26
  27 using namespace std;
  28
  29 namespace CVC4 {
  30
  31 #ifdef CVC4_DEBUG
  32 CVC4_PUBLIC CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
  33 #endif /* CVC4_DEBUG */
  34
  35 void AssertionException::construct(const char* header, const char* extra,
  36                                    const char* function, const char* file,
  37                                    unsigned line, const char* fmt,
  38                                    va_list args) {
  39   // try building the exception msg with a smallish buffer first,
  40   // then with a larger one if sprintf tells us to.
  41   int n = 512;
  42   char* buf;
  43
  44   for(;;) {
  45     buf = new char[n];
  46
  47     int size;
  48     if(extra == NULL) {
  49       size = snprintf(buf, n, "%s\n%s\n%s:%d\n",
  50                       header, function, file, line);
  51     } else {
  52       size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n  %s\n",
  53                       header, function, file, line, extra);
  54     }
  55
  56     if(size < n) {
  57       va_list args_copy;
  58       va_copy(args_copy, args);
  59       size += vsnprintf(buf + size, n - size, fmt, args);
  60       va_end(args_copy);
  61
  62       if(size < n) {
  63         break;
  64       }
  65     }
  66
  67     if(size >= n) {
  68       // try again with a buffer that's large enough
  69       n = size + 1;
  70       delete [] buf;
  71     }
  72   }
  73
  74   setMessage(string(buf));
  75
  76 #ifdef CVC4_DEBUG
  77   if(s_debugLastException == NULL) {
  78     // we leak buf[] but only in debug mode with assertions failing
  79     s_debugLastException = buf;
  80   }
  81 #else /* CVC4_DEBUG */
  82   delete [] buf;
  83 #endif /* CVC4_DEBUG */
  84 }
  85
  86 void AssertionException::construct(const char* header, const char* extra,
  87                                    const char* function, const char* file,
  88                                    unsigned line) {
  89   // try building the exception msg with a smallish buffer first,
  90   // then with a larger one if sprintf tells us to.
  91   int n = 256;
  92   char* buf;
  93
  94   for(;;) {
  95     buf = new char[n];
  96
  97     int size;
  98     if(extra == NULL) {
  99       size = snprintf(buf, n, "%s.\n%s\n%s:%d\n",
 100                       header, function, file, line);
 101     } else {
 102       size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n  %s\n",
 103                       header, function, file, line, extra);
 104     }
 105
 106     if(size < n) {
 107       break;
 108     } else {
 109       // try again with a buffer that's large enough
 110       n = size + 1;
 111       delete [] buf;
 112     }
 113   }
 114
 115   setMessage(string(buf));
 116
 117 #ifdef CVC4_DEBUG
 118   // we leak buf[] but only in debug mode with assertions failing
 119   if(s_debugLastException == NULL) {
 120     s_debugLastException = buf;
 121   }
 122 #else /* CVC4_DEBUG */
 123   delete [] buf;
 124 #endif /* CVC4_DEBUG */
 125 }
 126
 127 #ifdef CVC4_DEBUG
 128
 129 /**
 130  * Special assertion failure handling in debug mode; in non-debug
 131  * builds, the exception is thrown from the macro.  We factor out this
 132  * additional logic so as not to bloat the code at every Assert()
 133  * expansion.
 134  *
 135  * Note this name is prefixed with "debug" because it is included in
 136  * debug builds only; in debug builds, it handles all assertion
 137  * failures (even those that exist in non-debug builds).
 138  */
 139 void debugAssertionFailed(const AssertionException& thisException,
 140                           const char* propagatingException) {
 141   static CVC4_THREADLOCAL(bool) alreadyFired = false;
 142
 143   if(EXPECT_TRUE( !std::uncaught_exception() ) || alreadyFired) {
 144     throw thisException;
 145   }
 146
 147   alreadyFired = true;
 148
 149   // propagatingException is the propagating exception, but can be
 150   // NULL if the propagating exception is not a CVC4::Exception.
 151   Warning() << "===========================================" << std::endl
 152             << "An assertion failed during stack unwinding:" << std::endl;
 153   if(propagatingException != NULL) {
 154     Warning() << "The propagating exception is:" << std::endl
 155               << propagatingException << std::endl
 156               << "===========================================" << std::endl;
 157     Warning() << "The newly-thrown exception is:" << std::endl;
 158   } else {
 159     Warning() << "The propagating exception is unknown." << std::endl;
 160   }
 161   Warning() << thisException << std::endl
 162             << "===========================================" << std::endl;
 163
 164   terminate();
 165 }
 166
 167 #endif /* CVC4_DEBUG */
 168
 169 }/* CVC4 namespace */