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 : : * cvc5's exception base class and some associated utilities.
11 : : */
12 : :
13 : : #include "base/exception.h"
14 : :
15 : : #include <cstdarg>
16 : : #include <cstdio>
17 : : #include <cstdlib>
18 : : #include <cstring>
19 : : #include <ostream>
20 : : #include <sstream>
21 : : #include <string>
22 : :
23 : : #include "base/check.h"
24 : :
25 : : using namespace std;
26 : :
27 : : namespace cvc5::internal {
28 : :
29 : 3 : std::string Exception::toString() const
30 : : {
31 : 3 : std::stringstream ss;
32 : 3 : toStream(ss);
33 : 6 : return ss.str();
34 : 3 : }
35 : :
36 : 93 : void Exception::toStream(std::ostream& os) const { os << d_msg; }
37 : :
38 : : thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer =
39 : : nullptr;
40 : :
41 : 28355 : LastExceptionBuffer::LastExceptionBuffer() : d_contents(nullptr) {}
42 : :
43 : 0 : LastExceptionBuffer::~LastExceptionBuffer()
44 : : {
45 [ - - ]: 0 : if (d_contents != nullptr)
46 : : {
47 : 0 : free(d_contents);
48 : 0 : d_contents = nullptr;
49 : : }
50 : 0 : }
51 : :
52 : 24 : void LastExceptionBuffer::setContents(const char* string)
53 : : {
54 [ - + ]: 24 : if (d_contents != nullptr)
55 : : {
56 : 0 : free(d_contents);
57 : 0 : d_contents = nullptr;
58 : : }
59 : :
60 [ + - ]: 24 : if (string != nullptr)
61 : : {
62 : 24 : d_contents = strdup(string);
63 : : }
64 : 24 : }
65 : :
66 : : const char* IllegalArgumentException::s_header = "Illegal argument detected";
67 : :
68 : 1 : std::string IllegalArgumentException::formatVariadic() { return std::string(); }
69 : :
70 : 40 : std::string IllegalArgumentException::formatVariadic(const char* format, ...)
71 : : {
72 : : va_list args;
73 : 40 : va_start(args, format);
74 : :
75 : 40 : int n = 512;
76 : 40 : char* buf = nullptr;
77 : :
78 [ + - ]: 40 : for (int i = 0; i < 2; ++i)
79 : : {
80 [ - + ][ - + ]: 40 : Assert(n > 0);
[ - - ]
81 [ - + ]: 40 : delete[] buf;
82 : 40 : buf = new char[n];
83 : :
84 : : va_list args_copy;
85 : 40 : va_copy(args_copy, args);
86 : 40 : int size = vsnprintf(buf, n, format, args);
87 : 40 : va_end(args_copy);
88 : :
89 [ - + ]: 40 : if (size >= n)
90 : : {
91 : 0 : buf[n - 1] = '\0';
92 : 0 : n = size + 1;
93 : : }
94 : : else
95 : : {
96 : 40 : break;
97 : : }
98 : : }
99 : : // buf is not nullptr is an invariant.
100 : : // buf is also 0 terminated.
101 [ - + ][ - + ]: 40 : Assert(buf != nullptr);
[ - - ]
102 : 40 : std::string result(buf);
103 [ + - ]: 40 : delete[] buf;
104 : 40 : va_end(args);
105 : 80 : return result;
106 : : }
107 : :
108 : 42 : std::string IllegalArgumentException::format_extra(const char* condStr,
109 : : const char* argDesc)
110 : : {
111 : 84 : return (std::string("`") + argDesc + "' is a bad argument"
112 : 42 : + (*condStr == '\0'
113 [ + + ]: 124 : ? std::string()
114 : 124 : : (std::string("; expected ") + condStr + " to hold")));
115 : : }
116 : :
117 : 41 : void IllegalArgumentException::construct(const char* header,
118 : : const char* extra,
119 : : const char* function,
120 : : const char* tail)
121 : : {
122 : : // try building the exception msg with a smallish buffer first,
123 : : // then with a larger one if sprintf tells us to.
124 : 41 : int n = 512;
125 : : char* buf;
126 : :
127 : : for (;;)
128 : : {
129 : 41 : buf = new char[n];
130 : :
131 : : int size;
132 [ - + ]: 41 : if (extra == nullptr)
133 : : {
134 : 0 : size = snprintf(buf, n, "%s\n%s\n%s", header, function, tail);
135 : : }
136 : : else
137 : : {
138 : : size =
139 : 41 : snprintf(buf, n, "%s\n%s\n\n %s\n%s", header, function, extra, tail);
140 : : }
141 : :
142 [ + - ]: 41 : if (size < n)
143 : : {
144 : 41 : break;
145 : : }
146 : : else
147 : : {
148 : : // size >= n
149 : : // try again with a buffer that's large enough
150 : 0 : n = size + 1;
151 [ - - ]: 0 : delete[] buf;
152 : : }
153 : 0 : }
154 : :
155 : 41 : setMessage(string(buf));
156 : :
157 : : #ifdef CVC5_DEBUG
158 : 41 : LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
159 [ - + ]: 41 : if (buffer != nullptr)
160 : : {
161 [ - - ]: 0 : if (buffer->getContents() == nullptr)
162 : : {
163 : 0 : buffer->setContents(buf);
164 : : }
165 : : }
166 : : #endif /* CVC5_DEBUG */
167 [ + - ]: 41 : delete[] buf;
168 : 41 : }
169 : :
170 : 1 : void IllegalArgumentException::construct(const char* header,
171 : : const char* extra,
172 : : const char* function)
173 : : {
174 : : // try building the exception msg with a smallish buffer first,
175 : : // then with a larger one if sprintf tells us to.
176 : 1 : int n = 256;
177 : : char* buf;
178 : :
179 : : for (;;)
180 : : {
181 : 1 : buf = new char[n];
182 : :
183 : : int size;
184 [ - + ]: 1 : if (extra == nullptr)
185 : : {
186 : 0 : size = snprintf(buf, n, "%s.\n%s\n", header, function);
187 : : }
188 : : else
189 : : {
190 : 1 : size = snprintf(buf, n, "%s.\n%s\n\n %s\n", header, function, extra);
191 : : }
192 : :
193 [ + - ]: 1 : if (size < n)
194 : : {
195 : 1 : break;
196 : : }
197 : : else
198 : : {
199 : : // try again with a buffer that's large enough
200 : 0 : n = size + 1;
201 [ - - ]: 0 : delete[] buf;
202 : : }
203 : 0 : }
204 : :
205 : 1 : setMessage(string(buf));
206 : :
207 : : #ifdef CVC5_DEBUG
208 : 1 : LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
209 [ - + ]: 1 : if (buffer != nullptr)
210 : : {
211 [ - - ]: 0 : if (buffer->getContents() == nullptr)
212 : : {
213 : 0 : buffer->setContents(buf);
214 : : }
215 : : }
216 : : #endif /* CVC5_DEBUG */
217 [ + - ]: 1 : delete[] buf;
218 : 1 : }
219 : :
220 : : } // namespace cvc5::internal
|
