src/util/Assert.h

   1 /*********************                                                        */
   2 /*! \file Assert.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   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, exceptions, and macros.
  15  **
  16  ** Assertion utility classes, functions, exceptions, and macros.
  17  **/
  18
  19 #include "cvc4_public.h"
  20
  21 #ifndef __CVC4__ASSERT_H
  22 #define __CVC4__ASSERT_H
  23
  24 #include <string>
  25 #include <sstream>
  26 #include <cstdio>
  27 #include <cstdlib>
  28 #include <cstdarg>
  29
  30 #include "util/exception.h"
  31 #include "util/output.h"
  32 #include "util/tls.h"
  33
  34 namespace CVC4 {
  35
  36 class CVC4_PUBLIC AssertionException : public Exception {
  37 protected:
  38   void construct(const char* header, const char* extra,
  39                  const char* function, const char* file,
  40                  unsigned line, const char* fmt, ...) {
  41     va_list args;
  42     va_start(args, fmt);
  43     construct(header, extra, function, file, line, fmt, args);
  44     va_end(args);
  45   }
  46
  47   void construct(const char* header, const char* extra,
  48                  const char* function, const char* file,
  49                  unsigned line, const char* fmt, va_list args);
  50
  51   void construct(const char* header, const char* extra,
  52                  const char* function, const char* file,
  53                  unsigned line);
  54
  55   AssertionException() : Exception() {}
  56
  57 public:
  58   AssertionException(const char* extra, const char* function,
  59                      const char* file, unsigned line,
  60                      const char* fmt, ...) :
  61     Exception() {
  62     va_list args;
  63     va_start(args, fmt);
  64     construct("Assertion failure", extra, function, file, line, fmt, args);
  65     va_end(args);
  66   }
  67
  68   AssertionException(const char* extra, const char* function,
  69                      const char* file, unsigned line) :
  70     Exception() {
  71     construct("Assertion failure", extra, function, file, line);
  72   }
  73 };/* class AssertionException */
  74
  75 class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
  76 protected:
  77   UnreachableCodeException() : AssertionException() {}
  78
  79 public:
  80   UnreachableCodeException(const char* function, const char* file,
  81                            unsigned line, const char* fmt, ...) :
  82     AssertionException() {
  83     va_list args;
  84     va_start(args, fmt);
  85     construct("Unreachable code reached",
  86               NULL, function, file, line, fmt, args);
  87     va_end(args);
  88   }
  89
  90   UnreachableCodeException(const char* function, const char* file,
  91                            unsigned line) :
  92     AssertionException() {
  93     construct("Unreachable code reached", NULL, function, file, line);
  94   }
  95 };/* class UnreachableCodeException */
  96
  97 class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
  98 protected:
  99   UnhandledCaseException() : UnreachableCodeException() {}
 100
 101 public:
 102   UnhandledCaseException(const char* function, const char* file,
 103                          unsigned line, const char* fmt, ...) :
 104     UnreachableCodeException() {
 105     va_list args;
 106     va_start(args, fmt);
 107     construct("Unhandled case encountered",
 108               NULL, function, file, line, fmt, args);
 109     va_end(args);
 110   }
 111
 112   template <class T>
 113   UnhandledCaseException(const char* function, const char* file,
 114                          unsigned line, T theCase) :
 115     UnreachableCodeException() {
 116     std::stringstream sb;
 117     sb << theCase;
 118     construct("Unhandled case encountered",
 119               NULL, function, file, line, "The case was: %s", sb.str().c_str());
 120   }
 121
 122   UnhandledCaseException(const char* function, const char* file,
 123                          unsigned line) :
 124     UnreachableCodeException() {
 125     construct("Unhandled case encountered", NULL, function, file, line);
 126   }
 127 };/* class UnhandledCaseException */
 128
 129 class CVC4_PUBLIC UnimplementedOperationException : public AssertionException {
 130 protected:
 131   UnimplementedOperationException() : AssertionException() {}
 132
 133 public:
 134   UnimplementedOperationException(const char* function, const char* file,
 135                                   unsigned line, const char* fmt, ...) :
 136     AssertionException() {
 137     va_list args;
 138     va_start(args, fmt);
 139     construct("Unimplemented code encountered",
 140               NULL, function, file, line, fmt, args);
 141     va_end(args);
 142   }
 143
 144   UnimplementedOperationException(const char* function, const char* file,
 145                                   unsigned line) :
 146     AssertionException() {
 147     construct("Unimplemented code encountered", NULL, function, file, line);
 148   }
 149 };/* class UnimplementedOperationException */
 150
 151 class CVC4_PUBLIC IllegalArgumentException : public AssertionException {
 152 protected:
 153   IllegalArgumentException() : AssertionException() {}
 154
 155 public:
 156   IllegalArgumentException(const char* argDesc, const char* function,
 157                            const char* file, unsigned line,
 158                            const char* fmt, ...) :
 159     AssertionException() {
 160     va_list args;
 161     va_start(args, fmt);
 162     construct("Illegal argument detected",
 163               ( std::string(argDesc) + " invalid" ).c_str(),
 164               function, file, line, fmt, args);
 165     va_end(args);
 166   }
 167
 168   IllegalArgumentException(const char* argDesc, const char* function,
 169                            const char* file, unsigned line) :
 170     AssertionException() {
 171     construct("Illegal argument detected",
 172               ( std::string(argDesc) + " invalid" ).c_str(),
 173               function, file, line);
 174   }
 175
 176   IllegalArgumentException(const char* condStr, const char* argDesc,
 177                            const char* function, const char* file,
 178                            unsigned line, const char* fmt, ...) :
 179     AssertionException() {
 180     va_list args;
 181     va_start(args, fmt);
 182     construct("Illegal argument detected",
 183               ( std::string(argDesc) + " invalid; expected " +
 184                 condStr + " to hold" ).c_str(),
 185               function, file, line, fmt, args);
 186     va_end(args);
 187   }
 188
 189   IllegalArgumentException(const char* condStr, const char* argDesc,
 190                            const char* function, const char* file,
 191                            unsigned line) :
 192     AssertionException() {
 193     construct("Illegal argument detected",
 194               ( std::string(argDesc) + " invalid; expected " +
 195                 condStr + " to hold" ).c_str(),
 196               function, file, line);
 197   }
 198 };/* class IllegalArgumentException */
 199
 200 #ifdef CVC4_DEBUG
 201
 202 #ifdef CVC4_DEBUG
 203 extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException;
 204 #endif /* CVC4_DEBUG */
 205
 206 /**
 207  * Special assertion failure handling in debug mode; in non-debug
 208  * builds, the exception is thrown from the macro.  We factor out this
 209  * additional logic so as not to bloat the code at every Assert()
 210  * expansion.
 211  *
 212  * Note this name is prefixed with "debug" because it is included in
 213  * debug builds only; in debug builds, it handles all assertion
 214  * failures (even those that exist in non-debug builds).
 215  */
 216 void debugAssertionFailed(const AssertionException& thisException,
 217                           const char* lastException) CVC4_PUBLIC;
 218
 219 // If we're currently handling an exception, print a warning instead;
 220 // otherwise std::terminate() is called by the runtime and we lose
 221 // details of the exception
 222 #  define AlwaysAssert(cond, msg...)                                    \
 223     do {                                                                \
 224       if(EXPECT_FALSE( ! (cond) )) {                                    \
 225         /* save the last assertion failure */                           \
 226         const char* lastException = s_debugLastException;               \
 227         AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
 228         debugAssertionFailed(exception, lastException);                 \
 229       }                                                                 \
 230     } while(0)
 231
 232 #else /* CVC4_DEBUG */
 233 // These simpler (but less useful) versions for non-debug builds fails
 234 // will terminate() if thrown during stack unwinding.
 235 #  define AlwaysAssert(cond, msg...)                                    \
 236      do {                                                               \
 237        if(EXPECT_FALSE( ! (cond) )) {                                   \
 238          throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
 239        }                                                                \
 240      } while(0)
 241 #endif /* CVC4_DEBUG */
 242
 243 #define Unreachable(msg...) \
 244   throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 245 #define Unhandled(msg...) \
 246   throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 247 #define Unimplemented(msg...) \
 248   throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 249 #define IllegalArgument(arg, msg...) \
 250   throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 251 #define CheckArgument(cond, arg, msg...)         \
 252   AlwaysAssertArgument(cond, arg, ## msg)
 253 #define AlwaysAssertArgument(cond, arg, msg...)  \
 254   do { \
 255     if(EXPECT_FALSE( ! (cond) )) { \
 256       throw IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
 257     } \
 258   } while(0)
 259
 260 #ifdef CVC4_ASSERTIONS
 261 #  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
 262 #  define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
 263 #else /* ! CVC4_ASSERTIONS */
 264 #  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
 265 #  define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
 266 #endif /* CVC4_ASSERTIONS */
 267
 268 }/* CVC4 namespace */
 269
 270 #endif /* __CVC4__ASSERT_H */