summaryrefslogtreecommitdiff
path: root/src/main/signal_handlers.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/signal_handlers.cpp')
-rw-r--r--src/main/signal_handlers.cpp405
1 files changed, 405 insertions, 0 deletions
diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
new file mode 100644
index 000000000..6f24dfc9b
--- /dev/null
+++ b/src/main/signal_handlers.cpp
@@ -0,0 +1,405 @@
+/********************* */
+/*! \file signal_handlers.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andres Noetzli, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of signal handlers.
+ **
+ ** Implementation of signal handlers.
+ **
+ ** It is important to only call async-signal-safe functions from signal
+ ** handlers. See: http://man7.org/linux/man-pages/man7/signal-safety.7.html for
+ ** a list of async-signal-safe POSIX.1 functions.
+ **/
+
+#include <string.h>
+
+#include <cerrno>
+#include <cstdio>
+#include <cstdlib>
+#include <exception>
+
+#ifndef __WIN32__
+
+#include <signal.h>
+#include <sys/resource.h>
+#include <unistd.h>
+
+#endif /* __WIN32__ */
+
+#include "base/exception.h"
+#include "cvc4autoconfig.h"
+#include "main/command_executor.h"
+#include "main/main.h"
+#include "options/options.h"
+#include "smt/smt_engine.h"
+#include "util/safe_print.h"
+#include "util/statistics.h"
+
+using CVC4::Exception;
+using namespace std;
+
+namespace CVC4 {
+namespace main {
+
+/**
+ * If true, will not spin on segfault even when CVC4_DEBUG is on.
+ * Useful for nightly regressions, noninteractive performance runs
+ * etc.
+ */
+bool segvSpin = false;
+
+namespace signal_handlers {
+
+void print_statistics()
+{
+ if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL)
+ {
+ if (pTotalTime != NULL && pTotalTime->running())
+ {
+ pTotalTime->stop();
+ }
+ pExecutor->safeFlushStatistics(STDERR_FILENO);
+ }
+}
+
+void timeout_handler()
+{
+ safe_print(STDERR_FILENO, "CVC4 interrupted by timeout.\n");
+ print_statistics();
+ abort();
+}
+
+#ifndef __WIN32__
+
+#ifdef HAVE_SIGALTSTACK
+size_t cvc4StackSize;
+void* cvc4StackBase;
+#endif /* HAVE_SIGALTSTACK */
+
+/** Handler for SIGXCPU and SIGALRM, i.e., timeout. */
+void timeout_handler(int sig, siginfo_t* info, void*) { timeout_handler(); }
+
+/** Handler for SIGTERM. */
+void sigterm_handler(int sig, siginfo_t* info, void*)
+{
+ safe_print(STDERR_FILENO, "CVC4 interrupted by SIGTERM.\n");
+ print_statistics();
+ abort();
+}
+
+/** Handler for SIGINT, i.e., when the user hits control C. */
+void sigint_handler(int sig, siginfo_t* info, void*)
+{
+ safe_print(STDERR_FILENO, "CVC4 interrupted by user.\n");
+ print_statistics();
+ abort();
+}
+
+#ifdef HAVE_SIGALTSTACK
+/** Handler for SIGSEGV (segfault). */
+void segv_handler(int sig, siginfo_t* info, void* c)
+{
+ uintptr_t extent = reinterpret_cast<uintptr_t>(cvc4StackBase) - cvc4StackSize;
+ uintptr_t addr = reinterpret_cast<uintptr_t>(info->si_addr);
+#ifdef CVC4_DEBUG
+ safe_print(STDERR_FILENO, "CVC4 suffered a segfault in DEBUG mode.\n");
+ safe_print(STDERR_FILENO, "Offending address is ");
+ safe_print(STDERR_FILENO, info->si_addr);
+ safe_print(STDERR_FILENO, "\n");
+ // cerr << "base is " << (void*)cvc4StackBase << endl;
+ // cerr << "size is " << cvc4StackSize << endl;
+ // cerr << "extent is " << (void*)extent << endl;
+ if (addr >= extent && addr <= extent + 10 * 1024)
+ {
+ safe_print(STDERR_FILENO,
+ "Looks like this is likely due to stack overflow.\n");
+ safe_print(STDERR_FILENO,
+ "You might consider increasing the limit with `ulimit -s' or "
+ "equivalent.\n");
+ }
+ else if (addr < 10 * 1024)
+ {
+ safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n");
+ }
+
+ if (!segvSpin)
+ {
+ print_statistics();
+ abort();
+ }
+ else
+ {
+ safe_print(STDERR_FILENO,
+ "Spinning so that a debugger can be connected.\n");
+ safe_print(STDERR_FILENO, "Try: gdb ");
+ safe_print(STDERR_FILENO, *progName);
+ safe_print(STDERR_FILENO, " ");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, "\n");
+ safe_print(STDERR_FILENO, " or: gdb --pid=");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, " ");
+ safe_print(STDERR_FILENO, *progName);
+ safe_print(STDERR_FILENO, "\n");
+ for (;;)
+ {
+ sleep(60);
+ }
+ }
+#else /* CVC4_DEBUG */
+ safe_print(STDERR_FILENO, "CVC4 suffered a segfault.\n");
+ safe_print(STDERR_FILENO, "Offending address is ");
+ safe_print(STDERR_FILENO, info->si_addr);
+ safe_print(STDERR_FILENO, "\n");
+ if (addr >= extent && addr <= extent + 10 * 1024)
+ {
+ safe_print(STDERR_FILENO,
+ "Looks like this is likely due to stack overflow.\n");
+ safe_print(STDERR_FILENO,
+ "You might consider increasing the limit with `ulimit -s' or "
+ "equivalent.\n");
+ }
+ else if (addr < 10 * 1024)
+ {
+ safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n");
+ }
+ print_statistics();
+ abort();
+#endif /* CVC4_DEBUG */
+}
+#endif /* HAVE_SIGALTSTACK */
+
+/** Handler for SIGILL (illegal instruction). */
+void ill_handler(int sig, siginfo_t* info, void*)
+{
+#ifdef CVC4_DEBUG
+ safe_print(STDERR_FILENO,
+ "CVC4 executed an illegal instruction in DEBUG mode.\n");
+ if (!segvSpin)
+ {
+ print_statistics();
+ abort();
+ }
+ else
+ {
+ safe_print(STDERR_FILENO,
+ "Spinning so that a debugger can be connected.\n");
+ safe_print(STDERR_FILENO, "Try: gdb ");
+ safe_print(STDERR_FILENO, *progName);
+ safe_print(STDERR_FILENO, " ");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, "\n");
+ safe_print(STDERR_FILENO, " or: gdb --pid=");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, " ");
+ safe_print(STDERR_FILENO, *progName);
+ safe_print(STDERR_FILENO, "\n");
+ for (;;)
+ {
+ sleep(60);
+ }
+ }
+#else /* CVC4_DEBUG */
+ safe_print(STDERR_FILENO, "CVC4 executed an illegal instruction.\n");
+ print_statistics();
+ abort();
+#endif /* CVC4_DEBUG */
+}
+
+#endif /* __WIN32__ */
+
+static terminate_handler default_terminator;
+
+void cvc4unexpected()
+{
+#if defined(CVC4_DEBUG) && !defined(__WIN32__)
+ safe_print(STDERR_FILENO,
+ "\n"
+ "CVC4 threw an \"unexpected\" exception (one that wasn't properly "
+ "specified\nin the throws() specifier for the throwing function)."
+ "\n\n");
+
+ const char* lastContents = LastExceptionBuffer::currentContents();
+
+ if (lastContents == NULL)
+ {
+ safe_print(
+ STDERR_FILENO,
+ "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
+ }
+ else
+ {
+ safe_print(STDERR_FILENO, "The exception is:\n");
+ safe_print(STDERR_FILENO, lastContents);
+ safe_print(STDERR_FILENO, "\n\n");
+ }
+ if (!segvSpin)
+ {
+ print_statistics();
+ set_terminate(default_terminator);
+ }
+ else
+ {
+ safe_print(STDERR_FILENO,
+ "Spinning so that a debugger can be connected.\n");
+ safe_print(STDERR_FILENO, "Try: gdb ");
+ safe_print(STDERR_FILENO, *progName);
+ safe_print(STDERR_FILENO, " ");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, "\n");
+ safe_print(STDERR_FILENO, " or: gdb --pid=");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, " ");
+ safe_print(STDERR_FILENO, *progName);
+ safe_print(STDERR_FILENO, "\n");
+ for (;;)
+ {
+ sleep(60);
+ }
+ }
+#else /* CVC4_DEBUG */
+ safe_print(STDERR_FILENO, "CVC4 threw an \"unexpected\" exception.\n");
+ print_statistics();
+ set_terminate(default_terminator);
+#endif /* CVC4_DEBUG */
+}
+
+void cvc4terminate()
+{
+ set_terminate(default_terminator);
+#ifdef CVC4_DEBUG
+ LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
+ LastExceptionBuffer::setCurrent(NULL);
+ delete current;
+
+ safe_print(STDERR_FILENO,
+ "\n"
+ "CVC4 was terminated by the C++ runtime.\n"
+ "Perhaps an exception was thrown during stack unwinding. "
+ "(Don't do that.)\n");
+ print_statistics();
+ default_terminator();
+#else /* CVC4_DEBUG */
+ safe_print(STDERR_FILENO,
+ "CVC4 was terminated by the C++ runtime.\n"
+ "Perhaps an exception was thrown during stack unwinding.\n");
+ print_statistics();
+ default_terminator();
+#endif /* CVC4_DEBUG */
+}
+
+void install()
+{
+#ifdef CVC4_DEBUG
+ LastExceptionBuffer::setCurrent(new LastExceptionBuffer());
+#endif
+
+#ifndef __WIN32__
+ struct rlimit limit;
+ if (getrlimit(RLIMIT_STACK, &limit))
+ {
+ throw Exception(string("getrlimit() failure: ") + strerror(errno));
+ }
+ if (limit.rlim_cur != limit.rlim_max)
+ {
+ limit.rlim_cur = limit.rlim_max;
+ if (setrlimit(RLIMIT_STACK, &limit))
+ {
+ throw Exception(string("setrlimit() failure: ") + strerror(errno));
+ }
+ if (getrlimit(RLIMIT_STACK, &limit))
+ {
+ throw Exception(string("getrlimit() failure: ") + strerror(errno));
+ }
+ }
+
+ struct sigaction act1;
+ act1.sa_sigaction = sigint_handler;
+ act1.sa_flags = SA_SIGINFO;
+ sigemptyset(&act1.sa_mask);
+ if (sigaction(SIGINT, &act1, NULL))
+ {
+ throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno));
+ }
+
+ struct sigaction act2;
+ act2.sa_sigaction = timeout_handler;
+ act2.sa_flags = SA_SIGINFO;
+ sigemptyset(&act2.sa_mask);
+ if (sigaction(SIGXCPU, &act2, NULL))
+ {
+ throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno));
+ }
+
+ struct sigaction act3;
+ act3.sa_sigaction = ill_handler;
+ act3.sa_flags = SA_SIGINFO;
+ sigemptyset(&act3.sa_mask);
+ if (sigaction(SIGILL, &act3, NULL))
+ {
+ throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno));
+ }
+
+#ifdef HAVE_SIGALTSTACK
+ stack_t ss;
+ ss.ss_sp = (char*)malloc(SIGSTKSZ);
+ if (ss.ss_sp == NULL)
+ {
+ throw Exception("Can't malloc() space for a signal stack");
+ }
+ ss.ss_size = SIGSTKSZ;
+ ss.ss_flags = 0;
+ if (sigaltstack(&ss, NULL) == -1)
+ {
+ throw Exception(string("sigaltstack() failure: ") + strerror(errno));
+ }
+
+ cvc4StackSize = limit.rlim_cur;
+ cvc4StackBase = ss.ss_sp;
+
+ struct sigaction act4;
+ act4.sa_sigaction = segv_handler;
+ act4.sa_flags = SA_SIGINFO | SA_ONSTACK;
+ sigemptyset(&act4.sa_mask);
+ if (sigaction(SIGSEGV, &act4, NULL))
+ {
+ throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
+ }
+#endif /* HAVE_SIGALTSTACK */
+
+ struct sigaction act5;
+ act5.sa_sigaction = sigterm_handler;
+ act5.sa_flags = SA_SIGINFO;
+ sigemptyset(&act5.sa_mask);
+ if (sigaction(SIGTERM, &act5, NULL))
+ {
+ throw Exception(string("sigaction(SIGTERM) failure: ") + strerror(errno));
+ }
+
+#endif /* __WIN32__ */
+
+ std::set_unexpected(cvc4unexpected);
+ default_terminator = set_terminate(cvc4terminate);
+}
+
+void cleanup() noexcept
+{
+#ifndef __WIN32__
+#ifdef HAVE_SIGALTSTACK
+ free(cvc4StackBase);
+ cvc4StackBase = NULL;
+ cvc4StackSize = 0;
+#endif /* HAVE_SIGALTSTACK */
+#endif /* __WIN32__ */
+}
+
+} // namespace signal_handlers
+} // namespace main
+} // namespace CVC4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback