Make signal handlers safer

As reported in bug 769, the signal handlers currently use unsafe
functions such as dynamic memory allocations and fprintf. This commit
fixes the issue by introducing functions for printing statistics in
signal handlers (functions with the `safe` prefix). It also avoids
copying statistics, which further avoids dynamic memory allocation. The
safe printing of statistics has some limitations (it does not support
SExprStats or printing CVC4::Result), which should not matter much in
practice. Printing statistics in a non-signal handler is not affected by
these changes as that uses a separate code path (the functions without
the `safe` prefix).

Additional changes:
- Remove ListStat as it is not used anywhere
- Add unit test for safe printing statistics

3 files changed, 127 insertions, 85 deletions

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 4018aeda1..7a33e1db7 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -69,6 +69,15 @@ public:
     d_stats.flushInformation(out);
   }
 
+  /**
+   * Flushes statistics to a file descriptor. Safe to use in a signal handler.
+   */
+  void safeFlushStatistics(int fd) const {
+    d_exprMgr.safeFlushStatistics(fd);
+    d_smtEngine->safeFlushStatistics(fd);
+    d_stats.safeFlushInformation(fd);
+  }
+
   static void printStatsFilterZeros(std::ostream& out,
                                     const std::string& statsString);
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index efa4f5bd2..6de4f9ff4 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -146,14 +146,20 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   }
 
   // Auto-detect input language by filename extension
-  const char* filename = inputFromStdin ? "<stdin>" : filenames[0].c_str();
+  std::string filenameStr("<stdin>");
+  if (!inputFromStdin) {
+    // Use swap to avoid copying the string
+    // TODO: use std::move() when switching to c++11
+    filenameStr.swap(filenames[0]);
+  }
+  const char* filename = filenameStr.c_str();
 
   if(opts.getInputLanguage() == language::input::LANG_AUTO) {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
       opts.setInputLanguage(language::input::LANG_CVC4);
     } else {
-      unsigned len = strlen(filename);
+      unsigned len = filenameStr.size();
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
         opts.setInputLanguage(language::input::LANG_SMTLIB_V2_5);
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
@@ -264,7 +270,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
                                     pTotalTime);
 
     // Filename statistics
-    ReferenceStat< const char* > s_statFilename("filename", filename);
+    ReferenceStat<std::string> s_statFilename("filename", filenameStr);
     RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
                                       &s_statFilename);
 
diff --git a/src/main/util.cpp b/src/main/util.cpp
index d4c00cad2..744122cc8 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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
@@ -12,13 +12,17 @@
  ** \brief Utilities for the main driver.
  **
  ** Utilities for the main driver.
+ **
+ ** 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 <cerrno>
 #include <exception>
-#include <string.h>
 
 #ifndef __WIN32__
 
@@ -35,6 +39,7 @@
 #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;
@@ -55,23 +60,26 @@ bool segvSpin = false;
 size_t cvc4StackSize;
 void* cvc4StackBase;
 
+void print_statistics() {
+  if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL) {
+    if (pTotalTime != NULL && pTotalTime->running()) {
+      pTotalTime->stop();
+    }
+    pExecutor->safeFlushStatistics(STDERR_FILENO);
+  }
+}
+
 /** Handler for SIGXCPU, i.e., timeout. */
 void timeout_handler(int sig, siginfo_t* info, void*) {
-  fprintf(stderr, "CVC4 interrupted by timeout.\n");
-  if(pOptions->getStatistics() && pExecutor != NULL) {
-    pTotalTime->stop();
-    pExecutor->flushStatistics(cerr);
-  }
+  safe_print(STDERR_FILENO, "CVC4 interrupted by timeout.\n");
+  print_statistics();
   abort();
 }
 
 /** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
-  fprintf(stderr, "CVC4 interrupted by user.\n");
-  if(pOptions->getStatistics() && pExecutor != NULL) {
-    pTotalTime->stop();
-    pExecutor->flushStatistics(cerr);
-  }
+  safe_print(STDERR_FILENO, "CVC4 interrupted by user.\n");
+  print_statistics();
   abort();
 }
 
@@ -80,45 +88,58 @@ 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;
+  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) {
-    cerr << "Looks like this is likely due to stack overflow." << endl
-         << "You might consider increasing the limit with `ulimit -s' or equivalent." << endl;
+    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) {
-    cerr << "Looks like a NULL pointer was dereferenced." << endl;
+    safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n");
   }
 
   if(!segvSpin) {
-    if(pOptions->getStatistics() && pExecutor != NULL) {
-      pTotalTime->stop();
-      pExecutor->flushStatistics(cerr);
-    }
+    print_statistics();
     abort();
   } else {
-    fprintf(stderr, "Spinning so that a debugger can be connected.\n");
-    cerr << "Try:  gdb " << progName << " " << getpid() << endl
-         << " or:  gdb --pid=" << getpid() << " " << progName << endl;
+    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 */
-  fprintf(stderr, "CVC4 suffered a segfault.\n");
-  cerr << "Offending address is " << info->si_addr << endl;
+  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) {
-    cerr << "Looks like this is likely due to stack overflow." << endl
-         << "You might consider increasing the limit with `ulimit -s' or equivalent." << endl;
+    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) {
-    cerr << "Looks like a NULL pointer was dereferenced." << endl;
-  }
-  if(pOptions->getStatistics() && pExecutor != NULL) {
-    pTotalTime->stop();
-    pExecutor->flushStatistics(cerr);
+    safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n");
   }
+  print_statistics();
   abort();
 #endif /* CVC4_DEBUG */
 }
@@ -126,27 +147,31 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
 /** Handler for SIGILL (illegal instruction). */
 void ill_handler(int sig, siginfo_t* info, void*) {
 #ifdef CVC4_DEBUG
-  fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
+  safe_print(STDERR_FILENO,
+             "CVC4 executed an illegal instruction in DEBUG mode.\n");
   if(!segvSpin) {
-    if(pOptions->getStatistics() && pExecutor != NULL) {
-      pTotalTime->stop();
-      pExecutor->flushStatistics(cerr);
-    }
+    print_statistics();
     abort();
   } else {
-    fprintf(stderr, "Spinning so that a debugger can be connected.\n");
-    fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
-    fprintf(stderr, " or:  gdb --pid=%u %s\n", getpid(), progName);
+    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 */
-  fprintf(stderr, "CVC4 executed an illegal instruction.\n");
-  if(pOptions->getStatistics() && pExecutor != NULL) {
-    pTotalTime->stop();
-    pExecutor->flushStatistics(cerr);
-  }
+  safe_print(STDERR_FILENO, "CVC4 executed an illegal instruction.\n");
+  print_statistics();
   abort();
 #endif /* CVC4_DEBUG */
 }
@@ -157,39 +182,46 @@ static terminate_handler default_terminator;
 
 void cvc4unexpected() {
 #if defined(CVC4_DEBUG) && !defined(__WIN32__)
-  fprintf(stderr, "\n"
-          "CVC4 threw an \"unexpected\" exception (one that wasn't properly "
-          "specified\nin the throws() specifier for the throwing function)."
-          "\n\n");
+  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) {
-    fprintf(stderr,
-            "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
+    safe_print(
+        STDERR_FILENO,
+        "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
   } else {
-    fprintf(stderr, "The exception is:\n%s\n\n", lastContents);
+    safe_print(STDERR_FILENO, "The exception is:\n");
+    safe_print(STDERR_FILENO, lastContents);
+    safe_print(STDERR_FILENO, "\n\n");
   }
   if(!segvSpin) {
-    if(pOptions->getStatistics() && pExecutor != NULL) {
-      pTotalTime->stop();
-      pExecutor->flushStatistics(cerr);
-    }
+    print_statistics();
     set_terminate(default_terminator);
   } else {
-    fprintf(stderr, "Spinning so that a debugger can be connected.\n");
-    fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
-    fprintf(stderr, " or:  gdb --pid=%u %s\n", getpid(), progName);
+    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 */
-  fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
-  if(pOptions->getStatistics() && pExecutor != NULL) {
-    pTotalTime->stop();
-    pExecutor->flushStatistics(cerr);
-  }
+  safe_print(STDERR_FILENO, "CVC4 threw an \"unexpected\" exception.\n");
+  print_statistics();
   set_terminate(default_terminator);
 #endif /* CVC4_DEBUG */
 }
@@ -198,26 +230,21 @@ void cvc4terminate() {
   set_terminate(default_terminator);
 #ifdef CVC4_DEBUG
   LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
-   LastExceptionBuffer::setCurrent(NULL);
+  LastExceptionBuffer::setCurrent(NULL);
   delete current;
 
-  fprintf(stderr, "\n"
-          "CVC4 was terminated by the C++ runtime.\n"
-          "Perhaps an exception was thrown during stack unwinding.  "
-          "(Don't do that.)\n");
-  if(pOptions->getStatistics() && pExecutor != NULL) {
-    pTotalTime->stop();
-    pExecutor->flushStatistics(cerr);
-  }
+  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 */
-  fprintf(stderr,
-          "CVC4 was terminated by the C++ runtime.\n"
-          "Perhaps an exception was thrown during stack unwinding.\n");
-  if(pOptions->getStatistics() && pExecutor != NULL) {
-    pTotalTime->stop();
-    pExecutor->flushStatistics(cerr);
-  }
+  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 */
 }