GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/main/signal_handlers.cpp Lines: 39 130 30.0 %
Date: 2021-09-15 Branches: 12 106 11.3 %

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