From: Morgan Deters Date: Sun, 31 Oct 2010 15:22:38 +0000 (+0000) Subject: maximize stack limit, handle SEGV signals on an alternate signal stack, and try to... X-Git-Tag: cvc5-1.0.0~8755 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d4bfaa103d56d5c0172bf1457343a75ddea8a9b5;p=cvc5.git maximize stack limit, handle SEGV signals on an alternate signal stack, and try to diagnose stack overflow --- 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 #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 #include #include +#include #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(cvc4StackBase) - cvc4StackSize; + uintptr_t addr = reinterpret_cast(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));