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 |
|
totalTime.reset(); |
61 |
|
pExecutor->printStatisticsSafe(STDERR_FILENO); |
62 |
|
} |
63 |
|
} |
64 |
|
|
65 |
|
void timeout_handler() |
66 |
|
{ |
67 |
|
safe_print(STDERR_FILENO, "cvc5 interrupted by timeout.\n"); |
68 |
|
print_statistics(); |
69 |
|
abort(); |
70 |
|
} |
71 |
|
|
72 |
|
#ifndef __WIN32__ |
73 |
|
|
74 |
|
#ifdef HAVE_SIGALTSTACK |
75 |
|
size_t stackSize; |
76 |
|
void* stackBase; |
77 |
|
#endif /* HAVE_SIGALTSTACK */ |
78 |
|
|
79 |
|
/** Handler for SIGXCPU and SIGALRM, i.e., timeout. */ |
80 |
|
void timeout_handler(int sig, siginfo_t* info, void*) { timeout_handler(); } |
81 |
|
|
82 |
|
/** Handler for SIGTERM. */ |
83 |
|
void sigterm_handler(int sig, siginfo_t* info, void*) |
84 |
|
{ |
85 |
|
safe_print(STDERR_FILENO, "cvc5 interrupted by SIGTERM.\n"); |
86 |
|
print_statistics(); |
87 |
|
signal(sig, SIG_DFL); |
88 |
|
raise(sig); |
89 |
|
} |
90 |
|
|
91 |
|
/** Handler for SIGINT, i.e., when the user hits control C. */ |
92 |
|
void sigint_handler(int sig, siginfo_t* info, void*) |
93 |
|
{ |
94 |
|
safe_print(STDERR_FILENO, "cvc5 interrupted by user.\n"); |
95 |
|
print_statistics(); |
96 |
|
signal(sig, SIG_DFL); |
97 |
|
raise(sig); |
98 |
|
} |
99 |
|
|
100 |
|
#ifdef HAVE_SIGALTSTACK |
101 |
|
/** Handler for SIGSEGV (segfault). */ |
102 |
|
void segv_handler(int sig, siginfo_t* info, void* c) |
103 |
|
{ |
104 |
|
uintptr_t extent = reinterpret_cast<uintptr_t>(stackBase) - stackSize; |
105 |
|
uintptr_t addr = reinterpret_cast<uintptr_t>(info->si_addr); |
106 |
|
#ifdef CVC5_DEBUG |
107 |
|
safe_print(STDERR_FILENO, "cvc5 suffered a segfault in DEBUG mode.\n"); |
108 |
|
safe_print(STDERR_FILENO, "Offending address is "); |
109 |
|
safe_print(STDERR_FILENO, info->si_addr); |
110 |
|
safe_print(STDERR_FILENO, "\n"); |
111 |
|
// cerr << "base is " << (void*)stackBase << endl; |
112 |
|
// cerr << "size is " << stackSize << endl; |
113 |
|
// cerr << "extent is " << (void*)extent << endl; |
114 |
|
if (addr >= extent && addr <= extent + 10 * 1024) |
115 |
|
{ |
116 |
|
safe_print(STDERR_FILENO, |
117 |
|
"Looks like this is likely due to stack overflow.\n"); |
118 |
|
safe_print(STDERR_FILENO, |
119 |
|
"You might consider increasing the limit with `ulimit -s' or " |
120 |
|
"equivalent.\n"); |
121 |
|
} |
122 |
|
else if (addr < 10 * 1024) |
123 |
|
{ |
124 |
|
safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n"); |
125 |
|
} |
126 |
|
|
127 |
|
if (!segvSpin) |
128 |
|
{ |
129 |
|
print_statistics(); |
130 |
|
signal(sig, SIG_DFL); |
131 |
|
raise(sig); |
132 |
|
} |
133 |
|
else |
134 |
|
{ |
135 |
|
safe_print(STDERR_FILENO, |
136 |
|
"Spinning so that a debugger can be connected.\n"); |
137 |
|
safe_print(STDERR_FILENO, "Try: gdb "); |
138 |
|
safe_print(STDERR_FILENO, progName); |
139 |
|
safe_print(STDERR_FILENO, " "); |
140 |
|
safe_print<int64_t>(STDERR_FILENO, getpid()); |
141 |
|
safe_print(STDERR_FILENO, "\n"); |
142 |
|
safe_print(STDERR_FILENO, " or: gdb --pid="); |
143 |
|
safe_print<int64_t>(STDERR_FILENO, getpid()); |
144 |
|
safe_print(STDERR_FILENO, " "); |
145 |
|
safe_print(STDERR_FILENO, progName); |
146 |
|
safe_print(STDERR_FILENO, "\n"); |
147 |
|
for (;;) |
148 |
|
{ |
149 |
|
sleep(60); |
150 |
|
} |
151 |
|
} |
152 |
|
#else /* CVC5_DEBUG */ |
153 |
|
safe_print(STDERR_FILENO, "cvc5 suffered a segfault.\n"); |
154 |
|
safe_print(STDERR_FILENO, "Offending address is "); |
155 |
|
safe_print(STDERR_FILENO, info->si_addr); |
156 |
|
safe_print(STDERR_FILENO, "\n"); |
157 |
|
if (addr >= extent && addr <= extent + 10 * 1024) |
158 |
|
{ |
159 |
|
safe_print(STDERR_FILENO, |
160 |
|
"Looks like this is likely due to stack overflow.\n"); |
161 |
|
safe_print(STDERR_FILENO, |
162 |
|
"You might consider increasing the limit with `ulimit -s' or " |
163 |
|
"equivalent.\n"); |
164 |
|
} |
165 |
|
else if (addr < 10 * 1024) |
166 |
|
{ |
167 |
|
safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n"); |
168 |
|
} |
169 |
|
print_statistics(); |
170 |
|
signal(sig, SIG_DFL); |
171 |
|
raise(sig); |
172 |
|
#endif /* CVC5_DEBUG */ |
173 |
|
} |
174 |
|
#endif /* HAVE_SIGALTSTACK */ |
175 |
|
|
176 |
|
/** Handler for SIGILL (illegal instruction). */ |
177 |
|
void ill_handler(int sig, siginfo_t* info, void*) |
178 |
|
{ |
179 |
|
#ifdef CVC5_DEBUG |
180 |
|
safe_print(STDERR_FILENO, |
181 |
|
"cvc5 executed an illegal instruction in DEBUG mode.\n"); |
182 |
|
if (!segvSpin) |
183 |
|
{ |
184 |
|
print_statistics(); |
185 |
|
signal(sig, SIG_DFL); |
186 |
|
raise(sig); |
187 |
|
} |
188 |
|
else |
189 |
|
{ |
190 |
|
safe_print(STDERR_FILENO, |
191 |
|
"Spinning so that a debugger can be connected.\n"); |
192 |
|
safe_print(STDERR_FILENO, "Try: gdb "); |
193 |
|
safe_print(STDERR_FILENO, progName); |
194 |
|
safe_print(STDERR_FILENO, " "); |
195 |
|
safe_print<int64_t>(STDERR_FILENO, getpid()); |
196 |
|
safe_print(STDERR_FILENO, "\n"); |
197 |
|
safe_print(STDERR_FILENO, " or: gdb --pid="); |
198 |
|
safe_print<int64_t>(STDERR_FILENO, getpid()); |
199 |
|
safe_print(STDERR_FILENO, " "); |
200 |
|
safe_print(STDERR_FILENO, progName); |
201 |
|
safe_print(STDERR_FILENO, "\n"); |
202 |
|
for (;;) |
203 |
|
{ |
204 |
|
sleep(60); |
205 |
|
} |
206 |
|
} |
207 |
|
#else /* CVC5_DEBUG */ |
208 |
|
safe_print(STDERR_FILENO, "cvc5 executed an illegal instruction.\n"); |
209 |
|
print_statistics(); |
210 |
|
signal(sig, SIG_DFL); |
211 |
|
raise(sig); |
212 |
|
#endif /* CVC5_DEBUG */ |
213 |
|
} |
214 |
|
|
215 |
|
#endif /* __WIN32__ */ |
216 |
|
|
217 |
|
static terminate_handler default_terminator; |
218 |
|
|
219 |
|
void cvc5terminate() |
220 |
|
{ |
221 |
|
set_terminate(default_terminator); |
222 |
|
#ifdef CVC5_DEBUG |
223 |
|
LastExceptionBuffer* current = LastExceptionBuffer::getCurrent(); |
224 |
|
LastExceptionBuffer::setCurrent(NULL); |
225 |
|
delete current; |
226 |
|
|
227 |
|
safe_print(STDERR_FILENO, |
228 |
|
"\n" |
229 |
|
"cvc5 was terminated by the C++ runtime.\n" |
230 |
|
"Perhaps an exception was thrown during stack unwinding. " |
231 |
|
"(Don't do that.)\n"); |
232 |
|
print_statistics(); |
233 |
|
default_terminator(); |
234 |
|
#else /* CVC5_DEBUG */ |
235 |
|
safe_print(STDERR_FILENO, |
236 |
|
"cvc5 was terminated by the C++ runtime.\n" |
237 |
|
"Perhaps an exception was thrown during stack unwinding.\n"); |
238 |
|
print_statistics(); |
239 |
|
default_terminator(); |
240 |
|
#endif /* CVC5_DEBUG */ |
241 |
|
} |
242 |
|
|
243 |
8734 |
void install() |
244 |
|
{ |
245 |
|
#ifdef CVC5_DEBUG |
246 |
8734 |
LastExceptionBuffer::setCurrent(new LastExceptionBuffer()); |
247 |
|
#endif |
248 |
|
|
249 |
|
#ifndef __WIN32__ |
250 |
|
struct rlimit limit; |
251 |
8734 |
if (getrlimit(RLIMIT_STACK, &limit)) |
252 |
|
{ |
253 |
|
throw Exception(string("getrlimit() failure: ") + strerror(errno)); |
254 |
|
} |
255 |
8734 |
if (limit.rlim_cur != limit.rlim_max) |
256 |
|
{ |
257 |
|
limit.rlim_cur = limit.rlim_max; |
258 |
|
if (setrlimit(RLIMIT_STACK, &limit)) |
259 |
|
{ |
260 |
|
throw Exception(string("setrlimit() failure: ") + strerror(errno)); |
261 |
|
} |
262 |
|
if (getrlimit(RLIMIT_STACK, &limit)) |
263 |
|
{ |
264 |
|
throw Exception(string("getrlimit() failure: ") + strerror(errno)); |
265 |
|
} |
266 |
|
} |
267 |
|
|
268 |
|
struct sigaction act1; |
269 |
8734 |
act1.sa_sigaction = sigint_handler; |
270 |
8734 |
act1.sa_flags = SA_SIGINFO; |
271 |
8734 |
sigemptyset(&act1.sa_mask); |
272 |
8734 |
if (sigaction(SIGINT, &act1, NULL)) |
273 |
|
{ |
274 |
|
throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno)); |
275 |
|
} |
276 |
|
|
277 |
|
struct sigaction act2; |
278 |
8734 |
act2.sa_sigaction = timeout_handler; |
279 |
8734 |
act2.sa_flags = SA_SIGINFO; |
280 |
8734 |
sigemptyset(&act2.sa_mask); |
281 |
8734 |
if (sigaction(SIGXCPU, &act2, NULL)) |
282 |
|
{ |
283 |
|
throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno)); |
284 |
|
} |
285 |
|
|
286 |
|
struct sigaction act3; |
287 |
8734 |
act3.sa_sigaction = ill_handler; |
288 |
8734 |
act3.sa_flags = SA_SIGINFO; |
289 |
8734 |
sigemptyset(&act3.sa_mask); |
290 |
8734 |
if (sigaction(SIGILL, &act3, NULL)) |
291 |
|
{ |
292 |
|
throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno)); |
293 |
|
} |
294 |
|
|
295 |
|
#ifdef HAVE_SIGALTSTACK |
296 |
|
stack_t ss; |
297 |
8734 |
ss.ss_sp = (char*)malloc(SIGSTKSZ); |
298 |
8734 |
if (ss.ss_sp == NULL) |
299 |
|
{ |
300 |
|
throw Exception("Can't malloc() space for a signal stack"); |
301 |
|
} |
302 |
8734 |
ss.ss_size = SIGSTKSZ; |
303 |
8734 |
ss.ss_flags = 0; |
304 |
8734 |
if (sigaltstack(&ss, NULL) == -1) |
305 |
|
{ |
306 |
|
throw Exception(string("sigaltstack() failure: ") + strerror(errno)); |
307 |
|
} |
308 |
|
|
309 |
8734 |
stackSize = limit.rlim_cur; |
310 |
8734 |
stackBase = ss.ss_sp; |
311 |
|
|
312 |
|
struct sigaction act4; |
313 |
8734 |
act4.sa_sigaction = segv_handler; |
314 |
8734 |
act4.sa_flags = SA_SIGINFO | SA_ONSTACK; |
315 |
8734 |
sigemptyset(&act4.sa_mask); |
316 |
8734 |
if (sigaction(SIGSEGV, &act4, NULL)) |
317 |
|
{ |
318 |
|
throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); |
319 |
|
} |
320 |
|
#endif /* HAVE_SIGALTSTACK */ |
321 |
|
|
322 |
|
struct sigaction act5; |
323 |
8734 |
act5.sa_sigaction = sigterm_handler; |
324 |
8734 |
act5.sa_flags = SA_SIGINFO; |
325 |
8734 |
sigemptyset(&act5.sa_mask); |
326 |
8734 |
if (sigaction(SIGTERM, &act5, NULL)) |
327 |
|
{ |
328 |
|
throw Exception(string("sigaction(SIGTERM) failure: ") + strerror(errno)); |
329 |
|
} |
330 |
|
|
331 |
|
#endif /* __WIN32__ */ |
332 |
|
|
333 |
8734 |
default_terminator = set_terminate(cvc5terminate); |
334 |
8734 |
} |
335 |
|
|
336 |
6111 |
void cleanup() noexcept |
337 |
|
{ |
338 |
|
#ifndef __WIN32__ |
339 |
|
#ifdef HAVE_SIGALTSTACK |
340 |
6111 |
free(stackBase); |
341 |
6111 |
stackBase = nullptr; |
342 |
6111 |
stackSize = 0; |
343 |
|
#endif /* HAVE_SIGALTSTACK */ |
344 |
|
#endif /* __WIN32__ */ |
345 |
6111 |
} |
346 |
|
|
347 |
|
} // namespace signal_handlers |
348 |
|
} // namespace main |
349 |
9344 |
} // namespace cvc5 |