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