GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/signal_handlers.cpp Lines: 39 124 31.5 %
Date: 2021-03-22 Branches: 15 126 11.9 %

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