maximize stack limit, handle SEGV signals on an alternate signal stack, and try to diagnose stack overflow

2 files changed, 58 insertions, 4 deletions

diff --git a/src/main/main.h b/src/main/main.h
index b6a8bcfb1..2c2773a92 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -20,6 +20,7 @@
 #include <string>
 
 #include "util/options.h"
+#include "util/exception.h"
 #include "cvc4autoconfig.h"
 
 #ifndef __CVC4__MAIN__MAIN_H
@@ -45,7 +46,7 @@ extern bool segvNoSpin;
 extern Options options;
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
-void cvc4_init() throw();
+void cvc4_init() throw(Exception);
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 4ec1c1bee..c59e398f5 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -22,6 +22,7 @@
 #include <exception>
 #include <string.h>
 #include <signal.h>
+#include <sys/resource.h>
 
 #include "util/Assert.h"
 #include "util/exception.h"
@@ -37,6 +38,9 @@ using namespace std;
 namespace CVC4 {
 namespace main {
 
+size_t cvc4StackSize;
+void* cvc4StackBase;
+
 /**
  * If true, will not spin on segfault even when CVC4_DEBUG is on.
  * Useful for nightly regressions, noninteractive performance runs
@@ -63,11 +67,27 @@ void sigint_handler(int sig, siginfo_t* info, void*) {
 }
 
 /** Handler for SIGSEGV (segfault). */
-void segv_handler(int sig, siginfo_t* info, void*) {
+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
   fprintf(stderr, "CVC4 suffered a segfault in DEBUG mode.\n");
+  cerr << "Offending address is " << info->si_addr << endl;
+  //cerr << "base is " << (void*)cvc4StackBase << endl;
+  //cerr << "size is " << cvc4StackSize << endl;
+  //cerr << "extent is " << (void*)extent << endl;
+  if(addr >= extent && addr <= extent + 10*1024) {
+    cerr << "Looks like this is likely due to stack overflow." << endl
+         << "You might consider increasing the limit with `ulimit -s' or equivalent." << endl;
+  } else if(addr < 10*1024) {
+    cerr << "Looks like a NULL pointer was dereferenced." << endl;
+  }
+
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
+    if(options.statistics) {
+      StatisticsRegistry::flushStatistics(cerr);
+    }
     abort();
   } else {
     fprintf(stderr, "Spinning so that a debugger can be connected.\n");
@@ -78,6 +98,13 @@ void segv_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 suffered a segfault.\n");
+  cerr << "Offending address is " << info->si_addr << endl;
+  if(addr >= extent && addr <= extent + 10*1024) {
+    cerr << "Looks like this is likely due to stack overflow." << endl
+         << "You might consider increasing the limit with `ulimit -s' or equivalent." << endl;
+  } else if(addr < 10*1024) {
+    cerr << "Looks like a NULL pointer was dereferenced." << endl;
+  }
   if(options.statistics) {
     StatisticsRegistry::flushStatistics(cerr);
   }
@@ -170,7 +197,33 @@ void cvc4terminate() {
 }
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
-void cvc4_init() throw() {
+void cvc4_init() throw(Exception) {
+  stack_t ss;
+  ss.ss_sp = 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));
+  }
+  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));
+    }
+  }
+  cvc4StackSize = limit.rlim_cur;
+  cvc4StackBase = &ss;
+
   struct sigaction act1;
   act1.sa_sigaction = sigint_handler;
   act1.sa_flags = SA_SIGINFO;
@@ -189,7 +242,7 @@ void cvc4_init() throw() {
 
   struct sigaction act3;
   act3.sa_sigaction = segv_handler;
-  act3.sa_flags = SA_SIGINFO;
+  act3.sa_flags = SA_SIGINFO | SA_ONSTACK;
   sigemptyset(&act3.sa_mask);
   if(sigaction(SIGSEGV, &act3, NULL)) {
     throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));