diff options
Diffstat (limited to 'src/util/cvc4_assert.h')
| -rw-r--r-- | src/util/cvc4_assert.h | 311 |
1 files changed, 311 insertions, 0 deletions
diff --git a/src/util/cvc4_assert.h b/src/util/cvc4_assert.h new file mode 100644 index 000000000..4a6fe4d3a --- /dev/null +++ b/src/util/cvc4_assert.h @@ -0,0 +1,311 @@ +/********************* */ +/*! \file Assert.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): acsys + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Assertion utility classes, functions, exceptions, and macros. + ** + ** Assertion utility classes, functions, exceptions, and macros. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__ASSERT_H +#define __CVC4__ASSERT_H + +#include <string> +#include <sstream> +#include <cstdio> +#include <cstdlib> +#include <cstdarg> + +#include "util/exception.h" +#include "util/tls.h" + +// output.h not strictly needed for this header, but it _is_ needed to +// actually _use_ anything in this header, so let's include it. +#include "util/output.h" + +namespace CVC4 { + +class AssertionException : public Exception { +protected: + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, ...) { + va_list args; + va_start(args, fmt); + construct(header, extra, function, file, line, fmt, args); + va_end(args); + } + + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, va_list args); + + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line); + + AssertionException() : Exception() {} + +public: + AssertionException(const char* extra, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : + Exception() { + va_list args; + va_start(args, fmt); + construct("Assertion failure", extra, function, file, line, fmt, args); + va_end(args); + } + + AssertionException(const char* extra, const char* function, + const char* file, unsigned line) : + Exception() { + construct("Assertion failure", extra, function, file, line); + } +};/* class AssertionException */ + +class UnreachableCodeException : public AssertionException { +protected: + UnreachableCodeException() : AssertionException() {} + +public: + UnreachableCodeException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Unreachable code reached", + NULL, function, file, line, fmt, args); + va_end(args); + } + + UnreachableCodeException(const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Unreachable code reached", NULL, function, file, line); + } +};/* class UnreachableCodeException */ + +class UnhandledCaseException : public UnreachableCodeException { +protected: + UnhandledCaseException() : UnreachableCodeException() {} + +public: + UnhandledCaseException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + UnreachableCodeException() { + va_list args; + va_start(args, fmt); + construct("Unhandled case encountered", + NULL, function, file, line, fmt, args); + va_end(args); + } + + template <class T> + UnhandledCaseException(const char* function, const char* file, + unsigned line, T theCase) : + UnreachableCodeException() { + std::stringstream sb; + sb << theCase; + construct("Unhandled case encountered", + NULL, function, file, line, "The case was: %s", sb.str().c_str()); + } + + UnhandledCaseException(const char* function, const char* file, + unsigned line) : + UnreachableCodeException() { + construct("Unhandled case encountered", NULL, function, file, line); + } +};/* class UnhandledCaseException */ + +class UnimplementedOperationException : public AssertionException { +protected: + UnimplementedOperationException() : AssertionException() {} + +public: + UnimplementedOperationException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Unimplemented code encountered", + NULL, function, file, line, fmt, args); + va_end(args); + } + + UnimplementedOperationException(const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Unimplemented code encountered", NULL, function, file, line); + } +};/* class UnimplementedOperationException */ + +class AssertArgumentException : public AssertionException { +protected: + AssertArgumentException() : AssertionException() {} + +public: + AssertArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), + function, file, line, fmt, args); + va_end(args); + } + + AssertArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line) : + AssertionException() { + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), + function, file, line); + } + + AssertArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument; expected " + + condStr + " to hold" ).c_str(), + function, file, line, fmt, args); + va_end(args); + } + + AssertArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument; expected " + + condStr + " to hold" ).c_str(), + function, file, line); + } +};/* class AssertArgumentException */ + +class InternalErrorException : public AssertionException { +protected: + InternalErrorException() : AssertionException() {} + +public: + InternalErrorException(const char* function, const char* file, unsigned line) : + AssertionException() { + construct("Internal error detected", "", + function, file, line); + } + + InternalErrorException(const char* function, const char* file, unsigned line, + const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Internal error detected", "", + function, file, line, fmt, args); + va_end(args); + } + + InternalErrorException(const char* function, const char* file, unsigned line, + std::string fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Internal error detected", "", + function, file, line, fmt.c_str(), args); + va_end(args); + } + +};/* class InternalErrorException */ + +#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 + * additional logic so as not to bloat the code at every Assert() + * expansion. + * + * Note this name is prefixed with "debug" because it is included in + * debug builds only; in debug builds, it handles all assertion + * failures (even those that exist in non-debug builds). + */ +void debugAssertionFailed(const AssertionException& thisException, const char* lastException); + +// If we're currently handling an exception, print a warning instead; +// otherwise std::terminate() is called by the runtime and we lose +// details of the exception +# define AlwaysAssert(cond, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + /* save the last assertion failure */ \ + const char* lastException = ::CVC4::s_debugLastException; \ + ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + ::CVC4::debugAssertionFailed(exception, lastException); \ + } \ + } while(0) + +#else /* CVC4_DEBUG */ +// These simpler (but less useful) versions for non-debug builds fails +// will terminate() if thrown during stack unwinding. +# define AlwaysAssert(cond, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + } \ + } while(0) +#endif /* CVC4_DEBUG */ + +#define Unreachable(msg...) \ + throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define Unhandled(msg...) \ + throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define Unimplemented(msg...) \ + throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define InternalError(msg...) \ + throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define IllegalArgument(arg, msg...) \ + throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg) +#define CheckArgument(cond, arg, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \ + } \ + } while(0) +#define AlwaysAssertArgument(cond, arg, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + } \ + } while(0) + +#ifdef CVC4_ASSERTIONS +# define Assert(cond, msg...) AlwaysAssert(cond, ## msg) +# define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) +# define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg) +#else /* ! CVC4_ASSERTIONS */ +# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +# define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ +# define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ +#endif /* CVC4_ASSERTIONS */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__ASSERT_H */ |