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