1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Morgan Deters, Gereon Kremer, Andres Noetzli |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* Implementation of signal handlers. |
14 |
|
* |
15 |
|
* It is important to only call async-signal-safe functions from signal |
16 |
|
* handlers. See: http://man7.org/linux/man-pages/man7/signal-safety.7.html for |
17 |
|
* a list of async-signal-safe POSIX.1 functions. |
18 |
|
*/ |
19 |
|
|
20 |
|
#include <string.h> |
21 |
|
|
22 |
|
#include <cerrno> |
23 |
|
#include <cstdio> |
24 |
|
#include <cstdlib> |
25 |
|
#include <exception> |
26 |
|
|
27 |
|
#ifndef __WIN32__ |
28 |
|
|
29 |
|
#include <signal.h> |
30 |
|
#include <sys/resource.h> |
31 |
|
#include <unistd.h> |
32 |
|
|
33 |
|
#endif /* __WIN32__ */ |
34 |
|
|
35 |
|
#include "base/cvc5config.h" |
36 |
|
#include "base/exception.h" |
37 |
|
#include "main/command_executor.h" |
38 |
|
#include "main/main.h" |
39 |
|
#include "util/safe_print.h" |
40 |
|
|
41 |
|
using cvc5::Exception; |
42 |
|
using namespace std; |
43 |
|
|
44 |
|
namespace cvc5 { |
45 |
|
namespace main { |
46 |
|
|
47 |
|
/** |
48 |
|
* If true, will not spin on segfault even when CVC5_DEBUG is on. |
49 |
|
* Useful for nightly regressions, noninteractive performance runs |
50 |
|
* etc. |
51 |
|
*/ |
52 |
|
bool segvSpin = false; |
53 |
|
|
54 |
|
namespace signal_handlers { |
55 |
|
|
56 |
|
void print_statistics() |
57 |
|
{ |
58 |
|
if (pExecutor != nullptr) |
59 |
|
{ |
60 |
|
pExecutor->printStatisticsSafe(STDERR_FILENO); |
61 |
|
} |
62 |
|
} |
63 |
|
|
64 |
|
void timeout_handler() |
65 |
|
{ |
66 |
|
safe_print(STDERR_FILENO, "cvc5 interrupted by timeout.\n"); |
67 |
|
print_statistics(); |
68 |
|
abort(); |
69 |
|
} |
70 |
|
|
71 |
|
#ifndef __WIN32__ |
72 |
|
|
73 |
|
#ifdef HAVE_SIGALTSTACK |
74 |
|
size_t stackSize; |
75 |
|
void* stackBase; |
76 |
|
#endif /* HAVE_SIGALTSTACK */ |
77 |
|
|
78 |
|
/** Handler for SIGXCPU and SIGALRM, i.e., timeout. */ |
79 |
|
void timeout_handler(int sig, siginfo_t* info, void*) { timeout_handler(); } |
80 |
|
|
81 |
|
/** Handler for SIGTERM. */ |
82 |
|
void sigterm_handler(int sig, siginfo_t* info, void*) |
83 |
|
{ |
84 |
|
safe_print(STDERR_FILENO, "cvc5 interrupted by SIGTERM.\n"); |
85 |
|
print_statistics(); |
86 |
|
signal(sig, SIG_DFL); |
87 |
|
raise(sig); |
88 |
|
} |
89 |
|
|
90 |
|
/** Handler for SIGINT, i.e., when the user hits control C. */ |
91 |
|
void sigint_handler(int sig, siginfo_t* info, void*) |
92 |
|
{ |
93 |
|
safe_print(STDERR_FILENO, "cvc5 interrupted by user.\n"); |
94 |
|
print_statistics(); |
95 |
|
signal(sig, SIG_DFL); |
96 |
|
raise(sig); |
97 |
|
} |
98 |
|
|
99 |
|
#ifdef HAVE_SIGALTSTACK |
100 |
|
/** Handler for SIGSEGV (segfault). */ |
101 |
|
void segv_handler(int sig, siginfo_t* info, void* c) |
102 |
|
{ |
103 |
|
uintptr_t extent = reinterpret_cast<uintptr_t>(stackBase) - stackSize; |
104 |
|
uintptr_t addr = reinterpret_cast<uintptr_t>(info->si_addr); |
105 |
|
#ifdef CVC5_DEBUG |
106 |
|
safe_print(STDERR_FILENO, "cvc5 suffered a segfault in DEBUG mode.\n"); |
107 |
|
safe_print(STDERR_FILENO, "Offending address is "); |
108 |
|
safe_print(STDERR_FILENO, info->si_addr); |
109 |
|
safe_print(STDERR_FILENO, "\n"); |
110 |
|
// cerr << "base is " << (void*)stackBase << endl; |
111 |
|
// cerr << "size is " << stackSize << endl; |
112 |
|
// cerr << "extent is " << (void*)extent << endl; |
113 |
|
if (addr >= extent && addr <= extent + 10 * 1024) |
114 |
|
{ |
115 |
|
safe_print(STDERR_FILENO, |
116 |
|
"Looks like this is likely due to stack overflow.\n"); |
117 |
|
safe_print(STDERR_FILENO, |
118 |
|
"You might consider increasing the limit with `ulimit -s' or " |
119 |
|
"equivalent.\n"); |
120 |
|
} |
121 |
|
else if (addr < 10 * 1024) |
122 |
|
{ |
123 |
|
safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n"); |
124 |
|
} |
125 |
|
|
126 |
|
if (!segvSpin) |
127 |
|
{ |
128 |
|
print_statistics(); |
129 |
|
signal(sig, SIG_DFL); |
130 |
|
raise(sig); |
131 |
|
} |
132 |
|
else |
133 |
|
{ |
134 |
|
safe_print(STDERR_FILENO, |
135 |
|
"Spinning so that a debugger can be connected.\n"); |
136 |
|
safe_print(STDERR_FILENO, "Try: gdb "); |
137 |
|
safe_print(STDERR_FILENO, progName); |
138 |
|
safe_print(STDERR_FILENO, " "); |
139 |
|
safe_print<int64_t>(STDERR_FILENO, getpid()); |
140 |
|
safe_print(STDERR_FILENO, "\n"); |
141 |
|
safe_print(STDERR_FILENO, " or: gdb --pid="); |
142 |
|
safe_print<int64_t>(STDERR_FILENO, getpid()); |
143 |
|
safe_print(STDERR_FILENO, " "); |
144 |
|
safe_print(STDERR_FILENO, progName); |
145 |
|
safe_print(STDERR_FILENO, "\n"); |
146 |
|
for (;;) |
147 |
|
{ |
148 |
|
sleep(60); |
149 |
|
} |
150 |
|
} |
151 |
|
#else /* CVC5_DEBUG */ |
152 |
|
safe_print(STDERR_FILENO, "cvc5 suffered a segfault.\n"); |
153 |
|
safe_print(STDERR_FILENO, "Offending address is "); |
154 |
|
safe_print(STDERR_FILENO, info->si_addr); |
155 |
|
safe_print(STDERR_FILENO, "\n"); |
156 |
|
if (addr >= extent && addr <= extent + 10 * 1024) |
157 |
|
{ |
158 |
|
safe_print(STDERR_FILENO, |
159 |
|
"Looks like this is likely due to stack overflow.\n"); |
160 |
|
safe_print(STDERR_FILENO, |
161 |
|
"You might consider increasing the limit with `ulimit -s' or " |
162 |
|
"equivalent.\n"); |
163 |
|
} |
164 |
|
else if (addr < 10 * 1024) |
165 |
|
{ |
166 |
|
safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n"); |
167 |
|
} |
168 |
|
print_statistics(); |
169 |
|
signal(sig, SIG_DFL); |
170 |
|
raise(sig); |
171 |
|
#endif /* CVC5_DEBUG */ |
172 |
|
} |
173 |
|
#endif /* HAVE_SIGALTSTACK */ |
174 |
|
|
175 |
|
/** Handler for SIGILL (illegal instruction). */ |
176 |
|
void ill_handler(int sig, siginfo_t* info, void*) |
177 |
|
{ |
178 |
|
#ifdef CVC5_DEBUG |
179 |
|
safe_print(STDERR_FILENO, |
180 |
|
"cvc5 executed an illegal instruction in DEBUG mode.\n"); |
181 |
|
if (!segvSpin) |
182 |
|
{ |
183 |
|
print_statistics(); |
184 |
|
signal(sig, SIG_DFL); |
185 |
|
raise(sig); |
186 |
|
} |
187 |
|
else |
188 |
|
{ |
189 |
|
safe_print(STDERR_FILENO, |
190 |
|
"Spinning so that a debugger can be connected.\n"); |
191 |
|
safe_print(STDERR_FILENO, "Try: gdb "); |
192 |
|
safe_print(STDERR_FILENO, progName); |
193 |
|
safe_print(STDERR_FILENO, " "); |
194 |
|
safe_print<int64_t>(STDERR_FILENO, getpid()); |
195 |
|
safe_print(STDERR_FILENO, "\n"); |
196 |
|
safe_print(STDERR_FILENO, " or: gdb --pid="); |
197 |
|
safe_print<int64_t>(STDERR_FILENO, getpid()); |
198 |
|
safe_print(STDERR_FILENO, " "); |
199 |
|
safe_print(STDERR_FILENO, progName); |
200 |
|
safe_print(STDERR_FILENO, "\n"); |
201 |
|
for (;;) |
202 |
|
{ |
203 |
|
sleep(60); |
204 |
|
} |
205 |
|
} |
206 |
|
#else /* CVC5_DEBUG */ |
207 |
|
safe_print(STDERR_FILENO, "cvc5 executed an illegal instruction.\n"); |
208 |
|
print_statistics(); |
209 |
|
signal(sig, SIG_DFL); |
210 |
|
raise(sig); |
211 |
|
#endif /* CVC5_DEBUG */ |
212 |
|
} |
213 |
|
|
214 |
|
#endif /* __WIN32__ */ |
215 |
|
|
216 |
|
static terminate_handler default_terminator; |
217 |
|
|
218 |
|
void cvc5terminate() |
219 |
|
{ |
220 |
|
set_terminate(default_terminator); |
221 |
|
#ifdef CVC5_DEBUG |
222 |
|
LastExceptionBuffer* current = LastExceptionBuffer::getCurrent(); |
223 |
|
LastExceptionBuffer::setCurrent(NULL); |
224 |
|
delete current; |
225 |
|
|
226 |
|
safe_print(STDERR_FILENO, |
227 |
|
"\n" |
228 |
|
"cvc5 was terminated by the C++ runtime.\n" |
229 |
|
"Perhaps an exception was thrown during stack unwinding. " |
230 |
|
"(Don't do that.)\n"); |
231 |
|
print_statistics(); |
232 |
|
default_terminator(); |
233 |
|
#else /* CVC5_DEBUG */ |
234 |
|
safe_print(STDERR_FILENO, |
235 |
|
"cvc5 was terminated by the C++ runtime.\n" |
236 |
|
"Perhaps an exception was thrown during stack unwinding.\n"); |
237 |
|
print_statistics(); |
238 |
|
default_terminator(); |
239 |
|
#endif /* CVC5_DEBUG */ |
240 |
|
} |
241 |
|
|
242 |
8800 |
void install() |
243 |
|
{ |
244 |
|
#ifdef CVC5_DEBUG |
245 |
8800 |
LastExceptionBuffer::setCurrent(new LastExceptionBuffer()); |
246 |
|
#endif |
247 |
|
|
248 |
|
#ifndef __WIN32__ |
249 |
|
struct rlimit limit; |
250 |
8800 |
if (getrlimit(RLIMIT_STACK, &limit)) |
251 |
|
{ |
252 |
|
throw Exception(string("getrlimit() failure: ") + strerror(errno)); |
253 |
|
} |
254 |
8800 |
if (limit.rlim_cur != limit.rlim_max) |
255 |
|
{ |
256 |
|
limit.rlim_cur = limit.rlim_max; |
257 |
|
if (setrlimit(RLIMIT_STACK, &limit)) |
258 |
|
{ |
259 |
|
throw Exception(string("setrlimit() failure: ") + strerror(errno)); |
260 |
|
} |
261 |
|
if (getrlimit(RLIMIT_STACK, &limit)) |
262 |
|
{ |
263 |
|
throw Exception(string("getrlimit() failure: ") + strerror(errno)); |
264 |
|
} |
265 |
|
} |
266 |
|
|
267 |
|
struct sigaction act1; |
268 |
8800 |
act1.sa_sigaction = sigint_handler; |
269 |
8800 |
act1.sa_flags = SA_SIGINFO; |
270 |
8800 |
sigemptyset(&act1.sa_mask); |
271 |
8800 |
if (sigaction(SIGINT, &act1, NULL)) |
272 |
|
{ |
273 |
|
throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno)); |
274 |
|
} |
275 |
|
|
276 |
|
struct sigaction act2; |
277 |
8800 |
act2.sa_sigaction = timeout_handler; |
278 |
8800 |
act2.sa_flags = SA_SIGINFO; |
279 |
8800 |
sigemptyset(&act2.sa_mask); |
280 |
8800 |
if (sigaction(SIGXCPU, &act2, NULL)) |
281 |
|
{ |
282 |
|
throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno)); |
283 |
|
} |
284 |
|
|
285 |
|
struct sigaction act3; |
286 |
8800 |
act3.sa_sigaction = ill_handler; |
287 |
8800 |
act3.sa_flags = SA_SIGINFO; |
288 |
8800 |
sigemptyset(&act3.sa_mask); |
289 |
8800 |
if (sigaction(SIGILL, &act3, NULL)) |
290 |
|
{ |
291 |
|
throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno)); |
292 |
|
} |
293 |
|
|
294 |
|
#ifdef HAVE_SIGALTSTACK |
295 |
|
stack_t ss; |
296 |
8800 |
ss.ss_sp = (char*)malloc(SIGSTKSZ); |
297 |
8800 |
if (ss.ss_sp == NULL) |
298 |
|
{ |
299 |
|
throw Exception("Can't malloc() space for a signal stack"); |
300 |
|
} |
301 |
8800 |
ss.ss_size = SIGSTKSZ; |
302 |
8800 |
ss.ss_flags = 0; |
303 |
8800 |
if (sigaltstack(&ss, NULL) == -1) |
304 |
|
{ |
305 |
|
throw Exception(string("sigaltstack() failure: ") + strerror(errno)); |
306 |
|
} |
307 |
|
|
308 |
8800 |
stackSize = limit.rlim_cur; |
309 |
8800 |
stackBase = ss.ss_sp; |
310 |
|
|
311 |
|
struct sigaction act4; |
312 |
8800 |
act4.sa_sigaction = segv_handler; |
313 |
8800 |
act4.sa_flags = SA_SIGINFO | SA_ONSTACK; |
314 |
8800 |
sigemptyset(&act4.sa_mask); |
315 |
8800 |
if (sigaction(SIGSEGV, &act4, NULL)) |
316 |
|
{ |
317 |
|
throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); |
318 |
|
} |
319 |
|
#endif /* HAVE_SIGALTSTACK */ |
320 |
|
|
321 |
|
struct sigaction act5; |
322 |
8800 |
act5.sa_sigaction = sigterm_handler; |
323 |
8800 |
act5.sa_flags = SA_SIGINFO; |
324 |
8800 |
sigemptyset(&act5.sa_mask); |
325 |
8800 |
if (sigaction(SIGTERM, &act5, NULL)) |
326 |
|
{ |
327 |
|
throw Exception(string("sigaction(SIGTERM) failure: ") + strerror(errno)); |
328 |
|
} |
329 |
|
|
330 |
|
#endif /* __WIN32__ */ |
331 |
|
|
332 |
8800 |
default_terminator = set_terminate(cvc5terminate); |
333 |
8800 |
} |
334 |
|
|
335 |
6153 |
void cleanup() noexcept |
336 |
|
{ |
337 |
|
#ifndef __WIN32__ |
338 |
|
#ifdef HAVE_SIGALTSTACK |
339 |
6153 |
free(stackBase); |
340 |
6153 |
stackBase = nullptr; |
341 |
6153 |
stackSize = 0; |
342 |
|
#endif /* HAVE_SIGALTSTACK */ |
343 |
|
#endif /* __WIN32__ */ |
344 |
6153 |
} |
345 |
|
|
346 |
|
} // namespace signal_handlers |
347 |
|
} // namespace main |
348 |
9416 |
} // namespace cvc5 |