Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Mathias Preiner, Tim King, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Assertion utility classes, functions and macros.
14 : : *
15 : : * Assertion macros assert a condition and aborts() the process if the
16 : : * condition is not satisfied. These macro leave a hanging ostream for the user
17 : : * to specify additional information about the failure.
18 : : *
19 : : * Example usage:
20 : : * AlwaysAssert(x >= 0) << "x must be positive.";
21 : : *
22 : : * Assert is an AlwaysAssert that is only enabled in debug builds.
23 : : * Assert(pointer != nullptr);
24 : : *
25 : : * CVC5_FATAL() can be used to indicate unreachable code.
26 : : *
27 : : * Note: The AlwaysAssert and Assert macros are not safe for use in
28 : : * signal-handling code.
29 : : */
30 : :
31 : : #include "cvc5_private_library.h"
32 : :
33 : : #ifndef CVC5__CHECK_H
34 : : #define CVC5__CHECK_H
35 : :
36 : : #include <cvc5/cvc5_export.h>
37 : :
38 : : #include <cstdarg>
39 : : #include <ostream>
40 : :
41 : : #include "base/exception.h"
42 : :
43 : : namespace cvc5::internal {
44 : :
45 : : // Implementation notes:
46 : : // To understand FatalStream and OStreamVoider, it is useful to understand
47 : : // how a AlwaysAssert is structured. AlwaysAssert(cond) is roughly the following
48 : : // pattern:
49 : : // cond ? (void)0 : OstreamVoider() & FatalStream().stream()
50 : : // This is a carefully crafted message to achieve a hanging ostream using
51 : : // operator precedence. The line `AlwaysAssert(cond) << foo << bar;` will bind
52 : : // as follows:
53 : : // `cond ? ((void)0) : (OSV() & ((FS().stream() << foo) << bar));`
54 : : // Once the expression is evaluated, the destructor ~FatalStream() of the
55 : : // temporary object is then run, which abort()'s the process. The role of the
56 : : // OStreamVoider() is to match the void type of the true branch.
57 : :
58 : : // Class that provides an ostream and whose destructor aborts! Direct usage of
59 : : // this class is discouraged.
60 : : class CVC5_EXPORT FatalStream
61 : : {
62 : : public:
63 : : FatalStream(const char* function, const char* file, int line);
64 : : [[noreturn]] ~FatalStream();
65 : :
66 : : std::ostream& stream();
67 : :
68 : : private:
69 : : void Flush();
70 : : };
71 : :
72 : : // Helper class that changes the type of an std::ostream& into a void. See
73 : : // "Implementation notes" for more information.
74 : : class OstreamVoider
75 : : {
76 : : public:
77 : 2553 : OstreamVoider() {}
78 : : // The operator precedence between operator& and operator<< is critical here.
79 : 2553 : void operator&(std::ostream&) {}
80 : : };
81 : :
82 : : // CVC5_FATAL() always aborts a function and provides a convenient way of
83 : : // formatting error messages. This can be used instead of a return type.
84 : : //
85 : : // Example function that returns a type Foo:
86 : : // Foo bar(T t) {
87 : : // switch(t.type()) {
88 : : // ...
89 : : // default:
90 : : // CVC5_FATAL() << "Unknown T type " << t.enum();
91 : : // }
92 : : // }
93 : : #define CVC5_FATAL() \
94 : : internal::FatalStream(__PRETTY_FUNCTION__, __FILE__, __LINE__).stream()
95 : :
96 : : /* GCC <= 9.2 ignores CVC5_NO_RETURN of ~FatalStream() if
97 : : * used in template classes (e.g., CDHashMap::save()). As a workaround we
98 : : * explicitly call abort() to let the compiler know that the
99 : : * corresponding function call will not return. */
100 : : #define SuppressWrongNoReturnWarning abort()
101 : :
102 : : // If `cond` is true, log an error message and abort the process.
103 : : // Otherwise, does nothing. This leaves a hanging std::ostream& that can be
104 : : // inserted into.
105 : : #define CVC5_FATAL_IF(cond, function, file, line) \
106 : : CVC5_PREDICT_FALSE(!(cond)) \
107 : : ? (void)0 \
108 : : : cvc5::internal::OstreamVoider() \
109 : : & cvc5::internal::FatalStream(function, file, line).stream()
110 : :
111 : : // If `cond` is false, log an error message and abort()'s the process.
112 : : // Otherwise, does nothing. This leaves a hanging std::ostream& that can be
113 : : // inserted into using operator<<. Example usages:
114 : : // AlwaysAssert(x >= 0);
115 : : // AlwaysAssert(x >= 0) << "x must be positive";
116 : : // AlwaysAssert(x >= 0) << "expected a positive value. Got " << x << "
117 : : // instead";
118 : : #define AlwaysAssert(cond) \
119 : : CVC5_FATAL_IF(!(cond), __PRETTY_FUNCTION__, __FILE__, __LINE__) \
120 : : << "Check failure\n\n " << #cond << "\n"
121 : :
122 : : // Assert is a variant of AlwaysAssert() that is only checked when
123 : : // CVC5_ASSERTIONS is defined. We rely on the optimizer to remove the deadcode.
124 : : #ifdef CVC5_ASSERTIONS
125 : : #define Assert(cond) AlwaysAssert(cond)
126 : : #else
127 : : #define Assert(cond) \
128 : : CVC5_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__)
129 : : #endif
130 : :
131 : : class AssertArgumentException : public Exception
132 : : {
133 : : protected:
134 : : AssertArgumentException() : Exception() {}
135 : :
136 : : void construct(const char* header,
137 : : const char* extra,
138 : : const char* function,
139 : : const char* file,
140 : : unsigned line,
141 : : const char* fmt,
142 : : va_list args);
143 : :
144 : : void construct(const char* header,
145 : : const char* extra,
146 : : const char* function,
147 : : const char* file,
148 : : unsigned line);
149 : :
150 : : public:
151 : : AssertArgumentException(const char* condStr,
152 : : const char* argDesc,
153 : : const char* function,
154 : : const char* file,
155 : : unsigned line,
156 : : const char* fmt,
157 : : ...);
158 : :
159 : : AssertArgumentException(const char* condStr,
160 : : const char* argDesc,
161 : : const char* function,
162 : : const char* file,
163 : : unsigned line);
164 : :
165 : : }; /* class AssertArgumentException */
166 : :
167 : : #define Unreachable() CVC5_FATAL() << "Unreachable code reached "
168 : :
169 : : #define Unhandled() CVC5_FATAL() << "Unhandled case encountered "
170 : :
171 : : #define Unimplemented() CVC5_FATAL() << "Unimplemented code encountered "
172 : :
173 : : #define InternalError() CVC5_FATAL() << "Internal error detected "
174 : :
175 : : #define IllegalArgument(arg, msg...) \
176 : : throw cvc5::internal::IllegalArgumentException( \
177 : : "", \
178 : : #arg, \
179 : : __PRETTY_FUNCTION__, \
180 : : cvc5::internal::IllegalArgumentException::formatVariadic(msg).c_str());
181 : : // This cannot use check argument directly as this forces
182 : : // CheckArgument to use a va_list. This is unsupported in Swig.
183 : : #define PrettyCheckArgument(cond, arg, msg...) \
184 : : do \
185 : : { \
186 : : if (__builtin_expect((!(cond)), false)) \
187 : : { \
188 : : throw cvc5::internal::IllegalArgumentException( \
189 : : #cond, \
190 : : #arg, \
191 : : __PRETTY_FUNCTION__, \
192 : : cvc5::internal::IllegalArgumentException::formatVariadic(msg) \
193 : : .c_str()); \
194 : : } \
195 : : } while (0)
196 : : #define AlwaysAssertArgument(cond, arg, msg...) \
197 : : do \
198 : : { \
199 : : if (__builtin_expect((!(cond)), false)) \
200 : : { \
201 : : throw cvc5::internal::AssertArgumentException( \
202 : : #cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ##msg); \
203 : : } \
204 : : } while (0)
205 : :
206 : : #ifdef CVC5_ASSERTIONS
207 : : #define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ##msg)
208 : : #define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ##msg)
209 : : #else /* ! CVC5_ASSERTIONS */
210 : : #define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true \
211 : : )*/
212 : : #define DebugCheckArgument( \
213 : : cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/
214 : : #endif /* CVC5_ASSERTIONS */
215 : :
216 : : } // namespace cvc5::internal
217 : :
218 : : #endif /* CVC5__CHECK_H */
|
