src/main/util.cpp

   1 /*********************                                                        */
   2 /*! \file util.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Utilities for the main driver.
  15  **
  16  ** Utilities for the main driver.
  17  **/
  18
  19 #include <cstdio>
  20 #include <cstdlib>
  21 #include <cerrno>
  22 #include <exception>
  23 #include <string.h>
  24 #include <signal.h>
  25
  26 #include "util/exception.h"
  27 #include "util/options.h"
  28 #include "util/Assert.h"
  29 #include "util/stats.h"
  30
  31 #include "cvc4autoconfig.h"
  32 #include "main.h"
  33
  34 using CVC4::Exception;
  35 using namespace std;
  36
  37 namespace CVC4 {
  38 namespace main {
  39
  40 /**
  41  * If true, will not spin on segfault even when CVC4_DEBUG is on.
  42  * Useful for nightly regressions, noninteractive performance runs
  43  * etc.
  44  */
  45 bool segvNoSpin = false;
  46
  47 /** Handler for SIGXCPU, i.e., timeout. */
  48 void timeout_handler(int sig, siginfo_t* info, void*) {
  49   fprintf(stderr, "CVC4 interrupted by timeout.\n");
  50   if(options.statistics) {
  51     StatisticsRegistry::flushStatistics(cerr);
  52   }
  53   abort();
  54 }
  55
  56 /** Handler for SIGINT, i.e., when the user hits control C. */
  57 void sigint_handler(int sig, siginfo_t* info, void*) {
  58   fprintf(stderr, "CVC4 interrupted by user.\n");
  59   if(options.statistics) {
  60     StatisticsRegistry::flushStatistics(cerr);
  61   }
  62   abort();
  63 }
  64
  65 /** Handler for SIGSEGV (segfault). */
  66 void segv_handler(int sig, siginfo_t* info, void*) {
  67 #ifdef CVC4_DEBUG
  68   fprintf(stderr, "CVC4 suffered a segfault in DEBUG mode.\n");
  69   if(segvNoSpin) {
  70     fprintf(stderr, "No-spin requested, aborting...\n");
  71     abort();
  72   } else {
  73     fprintf(stderr, "Spinning so that a debugger can be connected.\n");
  74     fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
  75     for(;;) {
  76       sleep(60);
  77     }
  78   }
  79 #else /* CVC4_DEBUG */
  80   fprintf(stderr, "CVC4 suffered a segfault.\n");
  81   if(options.statistics) {
  82     StatisticsRegistry::flushStatistics(cerr);
  83   }
  84   abort();
  85 #endif /* CVC4_DEBUG */
  86 }
  87
  88 /** Handler for SIGILL (illegal instruction). */
  89 void ill_handler(int sig, siginfo_t* info, void*) {
  90 #ifdef CVC4_DEBUG
  91   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
  92   if(segvNoSpin) {
  93     fprintf(stderr, "No-spin requested, aborting...\n");
  94     if(options.statistics) {
  95       StatisticsRegistry::flushStatistics(cerr);
  96     }
  97     abort();
  98   } else {
  99     fprintf(stderr, "Spinning so that a debugger can be connected.\n");
 100     fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
 101     for(;;) {
 102       sleep(60);
 103     }
 104   }
 105 #else /* CVC4_DEBUG */
 106   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
 107   if(options.statistics) {
 108     StatisticsRegistry::flushStatistics(cerr);
 109   }
 110   abort();
 111 #endif /* CVC4_DEBUG */
 112 }
 113
 114 static terminate_handler default_terminator;
 115
 116 void cvc4unexpected() {
 117 #ifdef CVC4_DEBUG
 118   fprintf(stderr, "\n"
 119           "CVC4 threw an \"unexpected\" exception (one that wasn't properly "
 120           "specified\nin the throws() specifier for the throwing function)."
 121           "\n\n");
 122   if(CVC4::s_debugLastException == NULL) {
 123     fprintf(stderr,
 124             "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
 125   } else {
 126     fprintf(stderr, "The exception is:\n%s\n\n",
 127             static_cast<const char*>(CVC4::s_debugLastException));
 128   }
 129   if(segvNoSpin) {
 130     fprintf(stderr, "No-spin requested.\n");
 131     if(options.statistics) {
 132       StatisticsRegistry::flushStatistics(cerr);
 133     }
 134     set_terminate(default_terminator);
 135   } else {
 136     fprintf(stderr, "Spinning so that a debugger can be connected.\n");
 137     fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
 138     for(;;) {
 139       sleep(60);
 140     }
 141   }
 142 #else /* CVC4_DEBUG */
 143   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
 144   if(options.statistics) {
 145     StatisticsRegistry::flushStatistics(cerr);
 146   }
 147   set_terminate(default_terminator);
 148 #endif /* CVC4_DEBUG */
 149 }
 150
 151 void cvc4terminate() {
 152 #ifdef CVC4_DEBUG
 153   fprintf(stderr, "\n"
 154           "CVC4 was terminated by the C++ runtime.\n"
 155           "Perhaps an exception was thrown during stack unwinding.  "
 156           "(Don't do that.)\n");
 157   if(options.statistics) {
 158     StatisticsRegistry::flushStatistics(cerr);
 159   }
 160   default_terminator();
 161 #else /* CVC4_DEBUG */
 162   fprintf(stderr,
 163           "CVC4 was terminated by the C++ runtime.\n"
 164           "Perhaps an exception was thrown during stack unwinding.\n");
 165   if(options.statistics) {
 166     StatisticsRegistry::flushStatistics(cerr);
 167   }
 168   default_terminator();
 169 #endif /* CVC4_DEBUG */
 170 }
 171
 172 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 173 void cvc4_init() throw() {
 174   struct sigaction act1;
 175   act1.sa_sigaction = sigint_handler;
 176   act1.sa_flags = SA_SIGINFO;
 177   sigemptyset(&act1.sa_mask);
 178   if(sigaction(SIGINT, &act1, NULL)) {
 179     throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno));
 180   }
 181
 182   struct sigaction act2;
 183   act2.sa_sigaction = timeout_handler;
 184   act2.sa_flags = SA_SIGINFO;
 185   sigemptyset(&act2.sa_mask);
 186   if(sigaction(SIGXCPU, &act2, NULL)) {
 187     throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno));
 188   }
 189
 190   struct sigaction act3;
 191   act3.sa_sigaction = segv_handler;
 192   act3.sa_flags = SA_SIGINFO;
 193   sigemptyset(&act3.sa_mask);
 194   if(sigaction(SIGSEGV, &act3, NULL)) {
 195     throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
 196   }
 197
 198   struct sigaction act4;
 199   act4.sa_sigaction = segv_handler;
 200   act4.sa_flags = SA_SIGINFO;
 201   sigemptyset(&act4.sa_mask);
 202   if(sigaction(SIGILL, &act4, NULL)) {
 203     throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno));
 204   }
 205
 206   set_unexpected(cvc4unexpected);
 207   default_terminator = set_terminate(cvc4terminate);
 208 }
 209
 210 }/* CVC4::main namespace */
 211 }/* CVC4 namespace */