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