1 /********************* */ 2 /*! \file cvc4_assert.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Tim King 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Assertion utility classes, functions, exceptions, and macros. 13 ** 14 ** Assertion utility classes, functions, exceptions, and macros. 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__ASSERT_H 20 #define __CVC4__ASSERT_H 21 22 #include <cstdarg> 23 #include <cstdio> 24 #include <cstdlib> 25 #include <sstream> 26 #include <string> 27 28 #include "base/exception.h" 29 30 // output.h not strictly needed for this header, but it _is_ needed to 31 // actually _use_ anything in this header, so let's include it. 32 // Tim : Disabling this and moving it into cvc4_assert.cpp 33 //#include "util/output.h" 34 35 namespace CVC4 { 36 37 class AssertionException : public Exception { 38 protected: construct(const char * header,const char * extra,const char * function,const char * file,unsigned line,const char * fmt,...)39 void construct(const char* header, const char* extra, const char* function, 40 const char* file, 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, const char* function, 48 const char* file, unsigned line, const char* fmt, 49 va_list args); 50 51 void construct(const char* header, const char* extra, const char* function, 52 const char* file, unsigned line); 53 AssertionException()54 AssertionException() : Exception() {} 55 56 public: AssertionException(const char * extra,const char * function,const char * file,unsigned line,const char * fmt,...)57 AssertionException(const char* extra, const char* function, const char* file, 58 unsigned line, const char* fmt, ...) 59 : Exception() { 60 va_list args; 61 va_start(args, fmt); 62 construct("Assertion failure", extra, function, file, line, fmt, args); 63 va_end(args); 64 } 65 AssertionException(const char * extra,const char * function,const char * file,unsigned line)66 AssertionException(const char* extra, const char* function, const char* file, 67 unsigned line) 68 : Exception() { 69 construct("Assertion failure", extra, function, file, line); 70 } 71 }; /* class AssertionException */ 72 73 class UnreachableCodeException : public AssertionException { 74 protected: UnreachableCodeException()75 UnreachableCodeException() : AssertionException() {} 76 77 public: UnreachableCodeException(const char * function,const char * file,unsigned line,const char * fmt,...)78 UnreachableCodeException(const char* function, const char* file, 79 unsigned line, const char* fmt, ...) 80 : AssertionException() { 81 va_list args; 82 va_start(args, fmt); 83 construct("Unreachable code reached", NULL, function, file, line, fmt, 84 args); 85 va_end(args); 86 } 87 UnreachableCodeException(const char * function,const char * file,unsigned line)88 UnreachableCodeException(const char* function, const char* file, 89 unsigned line) 90 : AssertionException() { 91 construct("Unreachable code reached", NULL, function, file, line); 92 } 93 }; /* class UnreachableCodeException */ 94 95 class UnhandledCaseException : public UnreachableCodeException { 96 protected: UnhandledCaseException()97 UnhandledCaseException() : UnreachableCodeException() {} 98 99 public: UnhandledCaseException(const char * function,const char * file,unsigned line,const char * fmt,...)100 UnhandledCaseException(const char* function, const char* file, unsigned line, 101 const char* fmt, ...) 102 : UnreachableCodeException() { 103 va_list args; 104 va_start(args, fmt); 105 construct("Unhandled case encountered", NULL, function, file, line, fmt, 106 args); 107 va_end(args); 108 } 109 110 template <class T> UnhandledCaseException(const char * function,const char * file,unsigned line,T theCase)111 UnhandledCaseException(const char* function, const char* file, unsigned line, 112 T theCase) 113 : UnreachableCodeException() { 114 std::stringstream sb; 115 sb << theCase; 116 construct("Unhandled case encountered", NULL, function, file, line, 117 "The case was: %s", sb.str().c_str()); 118 } 119 UnhandledCaseException(const char * function,const char * file,unsigned line)120 UnhandledCaseException(const char* function, const char* file, unsigned line) 121 : UnreachableCodeException() { 122 construct("Unhandled case encountered", NULL, function, file, line); 123 } 124 }; /* class UnhandledCaseException */ 125 126 class UnimplementedOperationException : public AssertionException { 127 protected: UnimplementedOperationException()128 UnimplementedOperationException() : AssertionException() {} 129 130 public: UnimplementedOperationException(const char * function,const char * file,unsigned line,const char * fmt,...)131 UnimplementedOperationException(const char* function, const char* file, 132 unsigned line, const char* fmt, ...) 133 : AssertionException() { 134 va_list args; 135 va_start(args, fmt); 136 construct("Unimplemented code encountered", NULL, function, file, line, fmt, 137 args); 138 va_end(args); 139 } 140 UnimplementedOperationException(const char * function,const char * file,unsigned line)141 UnimplementedOperationException(const char* function, const char* file, 142 unsigned line) 143 : AssertionException() { 144 construct("Unimplemented code encountered", NULL, function, file, line); 145 } 146 }; /* class UnimplementedOperationException */ 147 148 class AssertArgumentException : public AssertionException { 149 protected: AssertArgumentException()150 AssertArgumentException() : AssertionException() {} 151 152 public: AssertArgumentException(const char * argDesc,const char * function,const char * file,unsigned line,const char * fmt,...)153 AssertArgumentException(const char* argDesc, const char* function, 154 const char* file, unsigned line, const char* fmt, ...) 155 : AssertionException() { 156 va_list args; 157 va_start(args, fmt); 158 construct("Illegal argument detected", 159 (std::string("`") + argDesc + "' is a bad argument").c_str(), 160 function, file, line, fmt, args); 161 va_end(args); 162 } 163 AssertArgumentException(const char * argDesc,const char * function,const char * file,unsigned line)164 AssertArgumentException(const char* argDesc, const char* function, 165 const char* file, unsigned line) 166 : AssertionException() { 167 construct("Illegal argument detected", 168 (std::string("`") + argDesc + "' is a bad argument").c_str(), 169 function, file, line); 170 } 171 AssertArgumentException(const char * condStr,const char * argDesc,const char * function,const char * file,unsigned line,const char * fmt,...)172 AssertArgumentException(const char* condStr, const char* argDesc, 173 const char* function, const char* file, unsigned line, 174 const char* fmt, ...) 175 : AssertionException() { 176 va_list args; 177 va_start(args, fmt); 178 construct("Illegal argument detected", 179 (std::string("`") + argDesc + "' is a bad argument; expected " + 180 condStr + " to hold") 181 .c_str(), 182 function, file, line, fmt, args); 183 va_end(args); 184 } 185 AssertArgumentException(const char * condStr,const char * argDesc,const char * function,const char * file,unsigned line)186 AssertArgumentException(const char* condStr, const char* argDesc, 187 const char* function, const char* file, unsigned line) 188 : AssertionException() { 189 construct("Illegal argument detected", 190 (std::string("`") + argDesc + "' is a bad argument; expected " + 191 condStr + " to hold") 192 .c_str(), 193 function, file, line); 194 } 195 }; /* class AssertArgumentException */ 196 197 class InternalErrorException : public AssertionException { 198 protected: InternalErrorException()199 InternalErrorException() : AssertionException() {} 200 201 public: InternalErrorException(const char * function,const char * file,unsigned line)202 InternalErrorException(const char* function, const char* file, unsigned line) 203 : AssertionException() { 204 construct("Internal error detected", "", function, file, line); 205 } 206 InternalErrorException(const char * function,const char * file,unsigned line,const char * fmt,...)207 InternalErrorException(const char* function, const char* file, unsigned line, 208 const char* fmt, ...) 209 : AssertionException() { 210 va_list args; 211 va_start(args, fmt); 212 construct("Internal error detected", "", function, file, line, fmt, args); 213 va_end(args); 214 } 215 InternalErrorException(const char * function,const char * file,unsigned line,std::string fmt,...)216 InternalErrorException(const char* function, const char* file, unsigned line, 217 std::string fmt, ...) 218 : AssertionException() { 219 va_list args; 220 va_start(args, fmt); 221 construct("Internal error detected", "", function, file, line, fmt.c_str(), 222 args); 223 va_end(args); 224 } 225 226 }; /* class InternalErrorException */ 227 228 #ifdef CVC4_DEBUG 229 230 /** 231 * Special assertion failure handling in debug mode; in non-debug 232 * builds, the exception is thrown from the macro. We factor out this 233 * additional logic so as not to bloat the code at every Assert() 234 * expansion. 235 * 236 * Note this name is prefixed with "debug" because it is included in 237 * debug builds only; in debug builds, it handles all assertion 238 * failures (even those that exist in non-debug builds). 239 */ 240 void debugAssertionFailed(const AssertionException& thisException, 241 const char* lastException); 242 243 // If we're currently handling an exception, print a warning instead; 244 // otherwise std::terminate() is called by the runtime and we lose 245 // details of the exception 246 #define AlwaysAssert(cond, msg...) \ 247 do { \ 248 if (__builtin_expect((!(cond)), false)) { \ 249 /* save the last assertion failure */ \ 250 ::CVC4::LastExceptionBuffer* buffer = \ 251 ::CVC4::LastExceptionBuffer::getCurrent(); \ 252 const char* lastException = \ 253 (buffer == NULL) ? NULL : buffer->getContents(); \ 254 ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, \ 255 __FILE__, __LINE__, ##msg); \ 256 ::CVC4::debugAssertionFailed(exception, lastException); \ 257 } \ 258 } while (0) 259 260 #else /* CVC4_DEBUG */ 261 // These simpler (but less useful) versions for non-debug builds fails 262 // will terminate() if thrown during stack unwinding. 263 #define AlwaysAssert(cond, msg...) \ 264 do { \ 265 if (__builtin_expect((!(cond)), false)) { \ 266 throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, \ 267 __LINE__, ##msg); \ 268 } \ 269 } while (0) 270 #endif /* CVC4_DEBUG */ 271 272 #define Unreachable(msg...) \ 273 throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, \ 274 __LINE__, ##msg) 275 #define Unhandled(msg...) \ 276 throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, \ 277 __LINE__, ##msg) 278 #define Unimplemented(msg...) \ 279 throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, \ 280 __LINE__, ##msg) 281 #define InternalError(msg...) \ 282 throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, \ 283 __LINE__, ##msg) 284 #define IllegalArgument(arg, msg...) \ 285 throw ::CVC4::IllegalArgumentException( \ 286 "", #arg, __PRETTY_FUNCTION__, \ 287 ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); 288 // This cannot use check argument directly as this forces 289 // CheckArgument to use a va_list. This is unsupported in Swig. 290 #define PrettyCheckArgument(cond, arg, msg...) \ 291 do { \ 292 if (__builtin_expect((!(cond)), false)) { \ 293 throw ::CVC4::IllegalArgumentException( \ 294 #cond, #arg, __PRETTY_FUNCTION__, \ 295 ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \ 296 } \ 297 } while (0) 298 #define AlwaysAssertArgument(cond, arg, msg...) \ 299 do { \ 300 if (__builtin_expect((!(cond)), false)) { \ 301 throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \ 302 __FILE__, __LINE__, ##msg); \ 303 } \ 304 } while (0) 305 306 #ifdef CVC4_ASSERTIONS 307 #define Assert(cond, msg...) AlwaysAssert(cond, ##msg) 308 #define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ##msg) 309 #define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ##msg) 310 #else /* ! CVC4_ASSERTIONS */ 311 #define Assert(cond, msg...) /*__builtin_expect( ( cond ), true )*/ 312 #define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true \ 313 )*/ 314 #define DebugCheckArgument(cond, arg, \ 315 msg...) /*__builtin_expect( ( cond ), true )*/ 316 #endif /* CVC4_ASSERTIONS */ 317 318 } /* CVC4 namespace */ 319 320 #endif /* __CVC4__ASSERT_H */ 321