diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/CMakeLists.txt | 6 | ||||
-rw-r--r-- | src/base/check.cpp | 212 | ||||
-rw-r--r-- | src/base/check.h | 240 | ||||
-rw-r--r-- | src/base/cvc4_assert.cpp | 171 | ||||
-rw-r--r-- | src/base/cvc4_assert.h | 320 | ||||
-rw-r--r-- | src/base/cvc4_check.cpp | 44 | ||||
-rw-r--r-- | src/base/cvc4_check.h | 149 | ||||
-rw-r--r-- | src/base/exception.cpp | 2 | ||||
-rw-r--r-- | src/base/listener.cpp | 2 | ||||
-rw-r--r-- | src/base/map_util.h | 4 |
10 files changed, 458 insertions, 692 deletions
diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt index 8df40a6ff..000aa331c 100644 --- a/src/base/CMakeLists.txt +++ b/src/base/CMakeLists.txt @@ -10,13 +10,11 @@ add_custom_target(gen-gitinfo #-----------------------------------------------------------------------------# libcvc4_add_sources( + check.cpp + check.h configuration.cpp configuration.h configuration_private.h - cvc4_assert.cpp - cvc4_assert.h - cvc4_check.cpp - cvc4_check.h exception.cpp exception.h listener.cpp diff --git a/src/base/check.cpp b/src/base/check.cpp new file mode 100644 index 000000000..10ecad191 --- /dev/null +++ b/src/base/check.cpp @@ -0,0 +1,212 @@ +/********************* */ +/*! \file check.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Assertion utility classes, functions and macros. + ** + ** Implementation of assertion utility classes, functions and macros. + **/ + +#include "base/check.h" + +#include <cstdlib> +#include <iostream> + +namespace CVC4 { + +FatalStream::FatalStream(const char* function, const char* file, int line) +{ + stream() << "Fatal failure within " << function << " at " << file << ":" + << line << "\n"; +} + +FatalStream::~FatalStream() +{ + Flush(); + abort(); +} + +std::ostream& FatalStream::stream() { return std::cerr; } + +void FatalStream::Flush() +{ + stream() << std::endl; + stream().flush(); +} + +void AssertArgumentException::construct(const char* header, + const char* extra, + const char* function, + const char* file, + unsigned line, + const char* fmt, + va_list args) +{ + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 512; + char* buf; + buf = new char[n]; + + for (;;) + { + int size; + if (extra == NULL) + { + size = snprintf(buf, n, "%s\n%s\n%s:%d\n", header, function, file, line); + } + else + { + size = snprintf(buf, + n, + "%s\n%s\n%s:%d:\n\n %s\n", + header, + function, + file, + line, + extra); + } + + if (size < n) + { + va_list args_copy; + va_copy(args_copy, args); + size += vsnprintf(buf + size, n - size, fmt, args_copy); + va_end(args_copy); + + if (size < n) + { + break; + } + } + + if (size >= n) + { + // try again with a buffer that's large enough + n = size + 1; + delete[] buf; + buf = new char[n]; + } + } + + setMessage(std::string(buf)); + +#ifdef CVC4_DEBUG + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if (buffer != NULL) + { + if (buffer->getContents() == NULL) + { + buffer->setContents(buf); + } + } +#endif /* CVC4_DEBUG */ + delete[] buf; +} + +void AssertArgumentException::construct(const char* header, + const char* extra, + const char* function, + const char* file, + unsigned line) +{ + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for (;;) + { + buf = new char[n]; + + int size; + if (extra == NULL) + { + size = snprintf(buf, n, "%s.\n%s\n%s:%d\n", header, function, file, line); + } + else + { + size = snprintf(buf, + n, + "%s.\n%s\n%s:%d:\n\n %s\n", + header, + function, + file, + line, + extra); + } + + if (size < n) + { + break; + } + else + { + // try again with a buffer that's large enough + n = size + 1; + delete[] buf; + } + } + + setMessage(std::string(buf)); + +#ifdef CVC4_DEBUG + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if (buffer != NULL) + { + if (buffer->getContents() == NULL) + { + buffer->setContents(buf); + } + } +#endif /* CVC4_DEBUG */ + delete[] buf; +} + +AssertArgumentException::AssertArgumentException(const char* condStr, + const char* argDesc, + const char* function, + const char* file, + unsigned line, + const char* fmt, + ...) + : Exception() +{ + 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::AssertArgumentException(const char* condStr, + const char* argDesc, + const char* function, + const char* file, + unsigned line) + : Exception() +{ + construct("Illegal argument detected", + (std::string("`") + argDesc + "' is a bad argument; expected " + + condStr + " to hold") + .c_str(), + function, + file, + line); +} + +} // namespace CVC4 diff --git a/src/base/check.h b/src/base/check.h new file mode 100644 index 000000000..915f6e4cb --- /dev/null +++ b/src/base/check.h @@ -0,0 +1,240 @@ +/********************* */ +/*! \file check.h + ** \verbatim + ** Top contributors (to current version): + ** Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Assertion utility classes, functions and macros. + ** + ** The AlwaysAssert utility classes, functions and macros. + ** + ** The main usage in the file is the AlwaysAssert macros. The AlwaysAssert + ** macros assert a condition and aborts()'s the process if the condition is + ** not satisfied. The macro leaves a hanging ostream for the user to specify + ** additional information about the failure. Example usage: + ** AlwaysAssert(x >= 0) << "x must be positive."; + ** + ** Assert is a AlwaysAssert that is only enabled in debug builds. + ** Assert(pointer != nullptr); + ** + ** CVC4_FATAL() can be used to indicate unreachable code. + ** + ** The AlwaysAssert and Assert macros are not safe for use in + ** signal-handling code. In future, a a signal-handling safe version of + ** AlwaysAssert may be added. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__CHECK_H +#define CVC4__CHECK_H + +#include <cstdarg> +#include <ostream> + +#include "base/exception.h" + +// Define CVC4_NO_RETURN macro replacement for [[noreturn]]. +#if defined(SWIG) +#define CVC4_NO_RETURN +// SWIG does not yet support [[noreturn]] so emit nothing instead. +#else +#define CVC4_NO_RETURN [[noreturn]] +// Not checking for whether the compiler supports [[noreturn]] using +// __has_cpp_attribute as GCC 4.8 is too widespread and does not support this. +// We instead assume this is C++11 (or later) and [[noreturn]] is available. +#endif // defined(SWIG) + +// Define CVC4_PREDICT_FALSE(x) that helps the compiler predict that x will be +// false (if there is compiler support). +#ifdef __has_builtin +#if __has_builtin(__builtin_expect) +#define CVC4_PREDICT_FALSE(x) (__builtin_expect(x, false)) +#define CVC4_PREDICT_TRUE(x) (__builtin_expect(x, true)) +#else +#define CVC4_PREDICT_FALSE(x) x +#define CVC4_PREDICT_TRUE(x) x +#endif +#else +#define CVC4_PREDICT_FALSE(x) x +#define CVC4_PREDICT_TRUE(x) x +#endif + +namespace CVC4 { + +// Implementation notes: +// To understand FatalStream and OStreamVoider, it is useful to understand +// how a AlwaysAssert is structured. AlwaysAssert(cond) is roughly the following +// pattern: +// cond ? (void)0 : OstreamVoider() & FatalStream().stream() +// This is a carefully crafted message to achieve a hanging ostream using +// operator precedence. The line `AlwaysAssert(cond) << foo << bar;` will bind +// as follows: +// `cond ? ((void)0) : (OSV() & ((FS().stream() << foo) << bar));` +// Once the expression is evaluated, the destructor ~FatalStream() of the +// temporary object is then run, which abort()'s the process. The role of the +// OStreamVoider() is to match the void type of the true branch. + +// Class that provides an ostream and whose destructor aborts! Direct usage of +// this class is discouraged. +class FatalStream +{ + public: + FatalStream(const char* function, const char* file, int line); + CVC4_NO_RETURN ~FatalStream(); + + std::ostream& stream(); + + private: + void Flush(); +}; + +// Helper class that changes the type of an std::ostream& into a void. See +// "Implementation notes" for more information. +class OstreamVoider +{ + public: + OstreamVoider() {} + // The operator precedence between operator& and operator<< is critical here. + void operator&(std::ostream&) {} +}; + +// CVC4_FATAL() always aborts a function and provides a convenient way of +// formatting error messages. This can be used instead of a return type. +// +// Example function that returns a type Foo: +// Foo bar(T t) { +// switch(t.type()) { +// ... +// default: +// CVC4_FATAL() << "Unknown T type " << t.enum(); +// } +// } +#define CVC4_FATAL() \ + FatalStream(__PRETTY_FUNCTION__, __FILE__, __LINE__).stream() + +/* GCC <= 9.2 ignores CVC4_NO_RETURN of ~FatalStream() if + * used in template classes (e.g., CDHashMap::save()). As a workaround we + * explicitly call abort() to let the compiler know that the + * corresponding function call will not return. */ +#define SuppressWrongNoReturnWarning abort() + +// If `cond` is true, log an error message and abort the process. +// Otherwise, does nothing. This leaves a hanging std::ostream& that can be +// inserted into. +#define CVC4_FATAL_IF(cond, function, file, line) \ + CVC4_PREDICT_FALSE(!(cond)) \ + ? (void)0 : OstreamVoider() & FatalStream(function, file, line).stream() + +// If `cond` is false, log an error message and abort()'s the process. +// Otherwise, does nothing. This leaves a hanging std::ostream& that can be +// inserted into using operator<<. Example usages: +// AlwaysAssert(x >= 0); +// AlwaysAssert(x >= 0) << "x must be positive"; +// AlwaysAssert(x >= 0) << "expected a positive value. Got " << x << " +// instead"; +#define AlwaysAssert(cond) \ + CVC4_FATAL_IF(!(cond), __PRETTY_FUNCTION__, __FILE__, __LINE__) \ + << "Check failure\n\n " << #cond << "\n" + +// Assert is a variant of AlwaysAssert() that is only checked when +// CVC4_ASSERTIONS is defined. We rely on the optimizer to remove the deadcode. +#ifdef CVC4_ASSERTIONS +#define Assert(cond) AlwaysAssert(cond) +#else +#define Assert(cond) \ + CVC4_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__) +#endif /* CVC4_DEBUG */ + +class AssertArgumentException : public Exception +{ + protected: + AssertArgumentException() : Exception() {} + + 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); + + public: + AssertArgumentException(const char* condStr, + const char* argDesc, + const char* function, + const char* file, + unsigned line, + const char* fmt, + ...); + + AssertArgumentException(const char* condStr, + const char* argDesc, + const char* function, + const char* file, + unsigned line); + +}; /* class AssertArgumentException */ + +#define Unreachable() CVC4_FATAL() << "Unreachable code reached" + +#define Unhandled() CVC4_FATAL() << "Unhandled case encountered" + +#define Unimplemented() CVC4_FATAL() << "Unimplemented code encountered" + +#define InternalError() CVC4_FATAL() << "Internal error detected" + +#define IllegalArgument(arg, msg...) \ + throw ::CVC4::IllegalArgumentException( \ + "", \ + #arg, \ + __PRETTY_FUNCTION__, \ + ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); +// This cannot use check argument directly as this forces +// CheckArgument to use a va_list. This is unsupported in Swig. +#define PrettyCheckArgument(cond, arg, msg...) \ + do \ + { \ + if (__builtin_expect((!(cond)), false)) \ + { \ + throw ::CVC4::IllegalArgumentException( \ + #cond, \ + #arg, \ + __PRETTY_FUNCTION__, \ + ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \ + } \ + } while (0) +#define AlwaysAssertArgument(cond, arg, msg...) \ + do \ + { \ + if (__builtin_expect((!(cond)), false)) \ + { \ + throw ::CVC4::AssertArgumentException( \ + #cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ##msg); \ + } \ + } while (0) + +#ifdef CVC4_ASSERTIONS +#define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ##msg) +#define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ##msg) +#else /* ! CVC4_ASSERTIONS */ +#define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true \ + )*/ +#define DebugCheckArgument( \ + cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/ +#endif /* CVC4_ASSERTIONS */ + +} // namespace CVC4 + +#endif /* CVC4__CHECK_H */ diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp deleted file mode 100644 index 1150f41f1..000000000 --- a/src/base/cvc4_assert.cpp +++ /dev/null @@ -1,171 +0,0 @@ -/********************* */ -/*! \file cvc4_assert.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Chad Brewbaker - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Assertion utility classes, functions, and exceptions. - ** - ** Assertion utility classes, functions, and exceptions. Implementation. - **/ - -#include <new> -#include <cstdarg> -#include <cstdio> - -#include "base/cvc4_assert.h" -#include "base/output.h" - -using namespace std; - -namespace CVC4 { - -#ifdef CVC4_DEBUG -//thread_local const char* s_debugLastException = NULL; -#endif /* CVC4_DEBUG */ - - -void AssertionException::construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line, const char* fmt, - va_list args) { - // try building the exception msg with a smallish buffer first, - // then with a larger one if sprintf tells us to. - int n = 512; - char* buf; - buf = new char[n]; - - for(;;) { - - int size; - if(extra == NULL) { - size = snprintf(buf, n, "%s\n%s\n%s:%d\n", - header, function, file, line); - } else { - size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n %s\n", - header, function, file, line, extra); - } - - if(size < n) { - va_list args_copy; - va_copy(args_copy, args); - size += vsnprintf(buf + size, n - size, fmt, args_copy); - va_end(args_copy); - - if(size < n) { - break; - } - } - - if(size >= n) { - // try again with a buffer that's large enough - n = size + 1; - delete [] buf; - buf = new char[n]; - } - } - - setMessage(string(buf)); - -#ifdef CVC4_DEBUG - LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); - if(buffer != NULL){ - if(buffer->getContents() == NULL) { - buffer->setContents(buf); - } - } -#endif /* CVC4_DEBUG */ - delete [] buf; -} - -void AssertionException::construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line) { - // try building the exception msg with a smallish buffer first, - // then with a larger one if sprintf tells us to. - int n = 256; - char* buf; - - for(;;) { - buf = new char[n]; - - int size; - if(extra == NULL) { - size = snprintf(buf, n, "%s.\n%s\n%s:%d\n", - header, function, file, line); - } else { - size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n %s\n", - header, function, file, line, extra); - } - - if(size < n) { - break; - } else { - // try again with a buffer that's large enough - n = size + 1; - delete [] buf; - } - } - - setMessage(string(buf)); - - -#ifdef CVC4_DEBUG - LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); - if(buffer != NULL){ - if(buffer->getContents() == NULL) { - buffer->setContents(buf); - } - } -#endif /* CVC4_DEBUG */ - delete [] buf; -} - -#ifdef CVC4_DEBUG - -/** - * 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* propagatingException) { - static thread_local bool alreadyFired = false; - - if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) { - throw thisException; - } - - alreadyFired = true; - - // propagatingException is the propagating exception, but can be - // NULL if the propagating exception is not a CVC4::Exception. - Warning() << "===========================================" << std::endl - << "An assertion failed during stack unwinding:" << std::endl; - if(propagatingException != NULL) { - Warning() << "The propagating exception is:" << std::endl - << propagatingException << std::endl - << "===========================================" << std::endl; - Warning() << "The newly-thrown exception is:" << std::endl; - } else { - Warning() << "The propagating exception is unknown." << std::endl; - } - Warning() << thisException << std::endl - << "===========================================" << std::endl; - - terminate(); -} - -#endif /* CVC4_DEBUG */ - -}/* CVC4 namespace */ diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h deleted file mode 100644 index a29e6f545..000000000 --- a/src/base/cvc4_assert.h +++ /dev/null @@ -1,320 +0,0 @@ -/********************* */ -/*! \file cvc4_assert.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 <cstdarg> -#include <cstdio> -#include <cstdlib> -#include <sstream> -#include <string> - -#include "base/exception.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. -// Tim : Disabling this and moving it into cvc4_assert.cpp -//#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 - -/** - * 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 (__builtin_expect((!(cond)), false)) { \ - /* save the last assertion failure */ \ - ::CVC4::LastExceptionBuffer* buffer = \ - ::CVC4::LastExceptionBuffer::getCurrent(); \ - const char* lastException = \ - (buffer == NULL) ? NULL : buffer->getContents(); \ - ::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 (__builtin_expect((!(cond)), false)) { \ - 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__, \ - ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); -// This cannot use check argument directly as this forces -// CheckArgument to use a va_list. This is unsupported in Swig. -#define PrettyCheckArgument(cond, arg, msg...) \ - do { \ - if (__builtin_expect((!(cond)), false)) { \ - throw ::CVC4::IllegalArgumentException( \ - #cond, #arg, __PRETTY_FUNCTION__, \ - ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \ - } \ - } while (0) -#define AlwaysAssertArgument(cond, arg, msg...) \ - do { \ - if (__builtin_expect((!(cond)), false)) { \ - 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...) /*__builtin_expect( ( cond ), true )*/ -#define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true \ - )*/ -#define DebugCheckArgument(cond, arg, \ - msg...) /*__builtin_expect( ( cond ), true )*/ -#endif /* CVC4_ASSERTIONS */ - -} /* CVC4 namespace */ - -#endif /* CVC4__ASSERT_H */ diff --git a/src/base/cvc4_check.cpp b/src/base/cvc4_check.cpp deleted file mode 100644 index f0b602849..000000000 --- a/src/base/cvc4_check.cpp +++ /dev/null @@ -1,44 +0,0 @@ -/********************* */ -/*! \file cvc4_check.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Assertion utility classes, functions and macros. - ** - ** Implementation of assertion utility classes, functions and macros. - **/ - -#include "base/cvc4_check.h" - -#include <cstdlib> -#include <iostream> - -namespace CVC4 { - -FatalStream::FatalStream(const char* function, const char* file, int line) -{ - stream() << "Fatal failure within " << function << " at " << file << ":" - << line << "\n"; -} - -FatalStream::~FatalStream() -{ - Flush(); - abort(); -} - -std::ostream& FatalStream::stream() { return std::cerr; } - -void FatalStream::Flush() -{ - stream() << std::endl; - stream().flush(); -} - -} // namespace CVC4 diff --git a/src/base/cvc4_check.h b/src/base/cvc4_check.h deleted file mode 100644 index b18e62303..000000000 --- a/src/base/cvc4_check.h +++ /dev/null @@ -1,149 +0,0 @@ -/********************* */ -/*! \file cvc4_check.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Assertion utility classes, functions and macros. - ** - ** The CVC4_CHECK utility classes, functions and macros are related to the - ** Assert() macros defined in base/cvc4_assert.h. The major distinguishing - ** attribute is the CVC4_CHECK's abort() the process on failures while - ** Assert() statements throw C++ exceptions. - ** - ** The main usage in the file is the CVC4_CHECK macros. The CVC4_CHECK macros - ** assert a condition and aborts()'s the process if the condition is not - ** satisfied. The macro leaves a hanging ostream for the user to specify - ** additional information about the failure. Example usage: - ** CVC4_CHECK(x >= 0) << "x must be positive."; - ** - ** CVC4_DCHECK is a CVC4_CHECK that is only enabled in debug builds. - ** CVC4_DCHECK(pointer != nullptr); - ** - ** CVC4_FATAL() can be used to indicate unreachable code. - ** - ** The CVC4_CHECK and CVC4_DCHECK macros are not safe for use in - ** signal-handling code. In future, a a signal-handling safe version of - ** CVC4_CHECK may be added. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__CHECK_H -#define CVC4__CHECK_H - -#include <ostream> - -// Define CVC4_NO_RETURN macro replacement for [[noreturn]]. -#if defined(SWIG) -#define CVC4_NO_RETURN -// SWIG does not yet support [[noreturn]] so emit nothing instead. -#else -#define CVC4_NO_RETURN [[noreturn]] -// Not checking for whether the compiler supports [[noreturn]] using -// __has_cpp_attribute as GCC 4.8 is too widespread and does not support this. -// We instead assume this is C++11 (or later) and [[noreturn]] is available. -#endif // defined(SWIG) - -// Define CVC4_PREDICT_FALSE(x) that helps the compiler predict that x will be -// false (if there is compiler support). -#ifdef __has_builtin -#if __has_builtin(__builtin_expect) -#define CVC4_PREDICT_FALSE(x) (__builtin_expect(x, false)) -#define CVC4_PREDICT_TRUE(x) (__builtin_expect(x, true)) -#else -#define CVC4_PREDICT_FALSE(x) x -#define CVC4_PREDICT_TRUE(x) x -#endif -#else -#define CVC4_PREDICT_FALSE(x) x -#define CVC4_PREDICT_TRUE(x) x -#endif - -namespace CVC4 { - -// Implementation notes: -// To understand FatalStream and OStreamVoider, it is useful to understand -// how a CVC4_CHECK is structured. CVC4_CHECK(cond) is roughly the following -// pattern: -// cond ? (void)0 : OstreamVoider() & FatalStream().stream() -// This is a carefully crafted message to achieve a hanging ostream using -// operator precedence. The line `CVC4_CHECK(cond) << foo << bar;` will bind as -// follows: -// `cond ? ((void)0) : (OSV() & ((FS().stream() << foo) << bar));` -// Once the expression is evaluated, the destructor ~FatalStream() of the -// temporary object is then run, which abort()'s the process. The role of the -// OStreamVoider() is to match the void type of the true branch. - -// Class that provides an ostream and whose destructor aborts! Direct usage of -// this class is discouraged. -class FatalStream -{ - public: - FatalStream(const char* function, const char* file, int line); - CVC4_NO_RETURN ~FatalStream(); - - std::ostream& stream(); - - private: - void Flush(); -}; - -// Helper class that changes the type of an std::ostream& into a void. See -// "Implementation notes" for more information. -class OstreamVoider -{ - public: - OstreamVoider() {} - // The operator precedence between operator& and operator<< is critical here. - void operator&(std::ostream&) {} -}; - -// CVC4_FATAL() always aborts a function and provides a convenient way of -// formatting error messages. This can be used instead of a return type. -// -// Example function that returns a type Foo: -// Foo bar(T t) { -// switch(t.type()) { -// ... -// default: -// CVC4_FATAL() << "Unknown T type " << t.enum(); -// } -// } -#define CVC4_FATAL() \ - FatalStream(__PRETTY_FUNCTION__, __FILE__, __LINE__).stream() - -// If `cond` is true, log an error message and abort the process. -// Otherwise, does nothing. This leaves a hanging std::ostream& that can be -// inserted into. -#define CVC4_FATAL_IF(cond, function, file, line) \ - CVC4_PREDICT_FALSE(!(cond)) \ - ? (void)0 : OstreamVoider() & FatalStream(function, file, line).stream() - -// If `cond` is false, log an error message and abort()'s the process. -// Otherwise, does nothing. This leaves a hanging std::ostream& that can be -// inserted into using operator<<. Example usages: -// CVC4_CHECK(x >= 0); -// CVC4_CHECK(x >= 0) << "x must be positive"; -// CVC4_CHECK(x >= 0) << "expected a positive value. Got " << x << " instead"; -#define CVC4_CHECK(cond) \ - CVC4_FATAL_IF(!(cond), __PRETTY_FUNCTION__, __FILE__, __LINE__) \ - << "Check failure\n\n " << #cond << "\n" - -// CVC4_DCHECK is a variant of CVC4_CHECK() that is only checked when -// CVC4_ASSERTIONS is defined. We rely on the optimizer to remove the deadcode. -#ifdef CVC4_ASSERTIONS -#define CVC4_DCHECK(cond) CVC4_CHECK(cond) -#else -#define CVC4_DCHECK(cond) \ - CVC4_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__) -#endif /* CVC4_DEBUG */ - -} // namespace CVC4 - -#endif /* CVC4__CHECK_H */ diff --git a/src/base/exception.cpp b/src/base/exception.cpp index 44d9b10bc..cd10f9eb8 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -22,7 +22,7 @@ #include <cstring> #include <string> -#include "base/cvc4_assert.h" +#include "base/check.h" using namespace std; diff --git a/src/base/listener.cpp b/src/base/listener.cpp index 44e5563e7..4a59058e6 100644 --- a/src/base/listener.cpp +++ b/src/base/listener.cpp @@ -18,7 +18,7 @@ #include <list> -#include "base/cvc4_assert.h" +#include "base/check.h" namespace CVC4 { diff --git a/src/base/map_util.h b/src/base/map_util.h index 786e22ae0..67f369ce7 100644 --- a/src/base/map_util.h +++ b/src/base/map_util.h @@ -38,7 +38,7 @@ #ifndef CVC4__BASE__MAP_UTIL_H #define CVC4__BASE__MAP_UTIL_H -#include "base/cvc4_check.h" +#include "base/check.h" namespace CVC4 { @@ -88,7 +88,7 @@ template <class M> const MapMappedTypeT<M>& FindOrDie(const M& map, const MapKeyTypeT<M>& key) { auto it = map.find(key); - CVC4_CHECK(it != map.end()) << "The map does not contain the key."; + AlwaysAssert(it != map.end()) << "The map does not contain the key."; return (*it).second; } |