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