GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/signal_handlers.cpp Lines: 39 131 29.8 %
Date: 2021-05-22 Branches: 15 112 13.4 %

Line Exec Source
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
8385
void install()
245
{
246
#ifdef CVC5_DEBUG
247
8385
  LastExceptionBuffer::setCurrent(new LastExceptionBuffer());
248
#endif
249
250
#ifndef __WIN32__
251
  struct rlimit limit;
252
8385
  if (getrlimit(RLIMIT_STACK, &limit))
253
  {
254
    throw Exception(string("getrlimit() failure: ") + strerror(errno));
255
  }
256
8385
  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
8385
  act1.sa_sigaction = sigint_handler;
271
8385
  act1.sa_flags = SA_SIGINFO;
272
8385
  sigemptyset(&act1.sa_mask);
273
8385
  if (sigaction(SIGINT, &act1, NULL))
274
  {
275
    throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno));
276
  }
277
278
  struct sigaction act2;
279
8385
  act2.sa_sigaction = timeout_handler;
280
8385
  act2.sa_flags = SA_SIGINFO;
281
8385
  sigemptyset(&act2.sa_mask);
282
8385
  if (sigaction(SIGXCPU, &act2, NULL))
283
  {
284
    throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno));
285
  }
286
287
  struct sigaction act3;
288
8385
  act3.sa_sigaction = ill_handler;
289
8385
  act3.sa_flags = SA_SIGINFO;
290
8385
  sigemptyset(&act3.sa_mask);
291
8385
  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
8385
  ss.ss_sp = (char*)malloc(SIGSTKSZ);
299
8385
  if (ss.ss_sp == NULL)
300
  {
301
    throw Exception("Can't malloc() space for a signal stack");
302
  }
303
8385
  ss.ss_size = SIGSTKSZ;
304
8385
  ss.ss_flags = 0;
305
8385
  if (sigaltstack(&ss, NULL) == -1)
306
  {
307
    throw Exception(string("sigaltstack() failure: ") + strerror(errno));
308
  }
309
310
8385
  stackSize = limit.rlim_cur;
311
8385
  stackBase = ss.ss_sp;
312
313
  struct sigaction act4;
314
8385
  act4.sa_sigaction = segv_handler;
315
8385
  act4.sa_flags = SA_SIGINFO | SA_ONSTACK;
316
8385
  sigemptyset(&act4.sa_mask);
317
8385
  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
8385
  act5.sa_sigaction = sigterm_handler;
325
8385
  act5.sa_flags = SA_SIGINFO;
326
8385
  sigemptyset(&act5.sa_mask);
327
8385
  if (sigaction(SIGTERM, &act5, NULL))
328
  {
329
    throw Exception(string("sigaction(SIGTERM) failure: ") + strerror(errno));
330
  }
331
332
#endif /* __WIN32__ */
333
334
8385
  default_terminator = set_terminate(cvc5terminate);
335
8385
}
336
337
5860
void cleanup() noexcept
338
{
339
#ifndef __WIN32__
340
#ifdef HAVE_SIGALTSTACK
341
5860
  free(stackBase);
342
5860
  stackBase = nullptr;
343
5860
  stackSize = 0;
344
#endif /* HAVE_SIGALTSTACK */
345
#endif /* __WIN32__ */
346
5860
}
347
348
}  // namespace signal_handlers
349
}  // namespace main
350
37164
}  // namespace cvc5