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