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