From: Andres Notzli <andres.noetzli@gmail.com>
Date: Fri, 31 Mar 2017 21:27:05 +0000 (-0700)
Subject: Make signal handlers safer
X-Git-Tag: cvc5-1.0.0~5806
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=31681c7ff2a1469f5efc325fc1b3a406e3a85949;p=cvc5.git

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
---

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 82cabbd3e..cb8ad710f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1039,6 +1039,10 @@ SExpr ExprManager::getStatistic(const std::string& name) const throw() {
   return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
 }
 
+void ExprManager::safeFlushStatistics(int fd) const {
+  d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd);
+}
+
 namespace expr {
 
 Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 9e962d970..07ace173c 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -545,7 +545,7 @@ public:
    * @param type the type for the new bound variable
    */
   Expr mkBoundVar(Type type);
-  
+
   /**
    * Create unique variable of type 
    */
@@ -557,6 +557,12 @@ public:
   /** Get a reference to the statistics registry for this ExprManager */
   SExpr getStatistic(const std::string& name) const throw();
 
+  /**
+   * Flushes statistics for this ExprManager to a file descriptor. Safe to use
+   * in a signal handler.
+   */
+  void safeFlushStatistics(int fd) const;
+
   /** Export an expr to a different ExprManager */
   //static Expr exportExpr(const Expr& e, ExprManager* em);
   /** Export a type to a different ExprManager */
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 */
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4e75a7937..b5fbecf7d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5573,6 +5573,10 @@ SExpr SmtEngine::getStatistic(std::string name) const throw() {
   return d_statisticsRegistry->getStatistic(name);
 }
 
+void SmtEngine::safeFlushStatistics(int fd) const {
+  d_statisticsRegistry->safeFlushInformation(fd);
+}
+
 void SmtEngine::setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value) {
   SmtScope smts(this);
   std::vector<Node> node_values;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c3cb54685..a27259ff4 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -721,6 +721,11 @@ public:
    */
   SExpr getStatistic(std::string name) const throw();
 
+  /**
+   * Flush statistic from this SmtEngine. Safe to use in a signal handler.
+   */
+  void safeFlushStatistics(int fd) const;
+
   /**
    * Returns the most recent result of checkSat/query or (set-info :status).
    */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index a8e37c93c..cd6f0e11c 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -44,6 +44,8 @@ libutil_la_SOURCES = \
 	resource_manager.h \
 	result.cpp \
 	result.h \
+	safe_print.cpp \
+	safe_print.h \
 	sexpr.cpp \
 	sexpr.h \
 	smt2_quote_string.cpp \
diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp
new file mode 100644
index 000000000..ff5a7aa7e
--- /dev/null
+++ b/src/util/safe_print.cpp
@@ -0,0 +1,215 @@
+/*********************                                                        */
+/*! \file safe_print.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** 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
+ **
+ ** \brief Definition of print functions that are safe to use in a signal
+ ** handler.
+ **
+ ** Signal handlers only allow a very limited set of operations, e.g. dynamic
+ ** memory allocation is not possible. This set of functions can be used to
+ ** print information from a signal handler. All output is written to file
+ ** descriptors using the async-signal-safe write() function.
+ **/
+
+#include "safe_print.h"
+
+#include <unistd.h>
+
+/* Size of buffers used */
+#define BUFFER_SIZE 20
+
+namespace CVC4 {
+
+template <>
+void safe_print(int fd, const std::string& msg) {
+  // Print characters one by one instead of using
+  // string::data()/string::c_str() to avoid allocations (pre-c++11)
+  for (size_t i = 0; i < msg.length(); i++) {
+    if (write(fd, &(msg[i]), 1) != 1) {
+      abort();
+    }
+  }
+}
+
+template <>
+void safe_print(int fd, const int64_t& _i) {
+  char buf[BUFFER_SIZE];
+  int64_t i = _i;
+
+  if (i == 0) {
+    safe_print(fd, "0");
+    return;
+  } else if (i < 0) {
+    safe_print(fd, "-");
+    i *= -1;
+  }
+
+  // This loop fills the buffer from the end. The number of elements in the
+  // buffer is BUFER_SIZE - idx - 1 and they start at position idx + 1.
+  ssize_t idx = BUFFER_SIZE - 1;
+  while (i != 0 && idx >= 0) {
+    buf[idx] = '0' + i % 10;
+    i /= 10;
+    idx--;
+  }
+
+  ssize_t nbyte = BUFFER_SIZE - idx - 1;
+  if (write(fd, buf + idx + 1, nbyte) != nbyte) {
+    abort();
+  }
+}
+
+template <>
+void safe_print(int fd, const int32_t& i) {
+  safe_print<int64_t>(fd, i);
+}
+
+template <>
+void safe_print(int fd, const uint64_t& _i) {
+  char buf[BUFFER_SIZE];
+  uint64_t i = _i;
+
+  if (i == 0) {
+    safe_print(fd, "0");
+    return;
+  }
+
+  // This loop fills the buffer from the end. The number of elements in the
+  // buffer is BUFER_SIZE - idx - 1 and they start at position idx + 1.
+  ssize_t idx = BUFFER_SIZE - 1;
+  while (i != 0 && idx >= 0) {
+    buf[idx] = '0' + i % 10;
+    i /= 10;
+    idx--;
+  }
+
+  ssize_t nbyte = BUFFER_SIZE - idx - 1;
+  if (write(fd, buf + idx + 1, nbyte) != nbyte) {
+    abort();
+  }
+}
+
+template <>
+void safe_print(int fd, const uint32_t& i) {
+  safe_print<uint64_t>(fd, i);
+}
+
+template <>
+void safe_print(int fd, const double& _d) {
+  // Note: this print function for floating-point values is optimized for
+  // simplicity, not correctness or performance.
+  char buf[BUFFER_SIZE];
+  double d = _d;
+
+  ssize_t i = 0;
+  int64_t v = static_cast<int64_t>(d);
+  d -= v;
+
+  if (d < 0.0) {
+    d *= -1.0;
+  }
+
+  safe_print<int64_t>(fd, v);
+  safe_print(fd, ".");
+
+  // Print decimal digits as long as the remaining value is larger than zero
+  // and print at least one digit.
+  while (i == 0 || (d > 0.0 && i < BUFFER_SIZE)) {
+    d *= 10.0;
+    char c = static_cast<char>(d);
+    buf[i] = '0' + c;
+    d -= c;
+    i++;
+  }
+  if (i == 0) {
+    safe_print(fd, "0");
+  } else if (write(fd, buf, i) != i) {
+    abort();
+  }
+}
+
+template <>
+void safe_print(int fd, const float& f) {
+  safe_print<double>(fd, (double)f);
+}
+
+template <>
+void safe_print(int fd, const bool& b) {
+  if (b) {
+    safe_print(fd, "true");
+  } else {
+    safe_print(fd, "false");
+  }
+}
+
+template <>
+void safe_print(int fd, void* const& addr) {
+  safe_print_hex(fd, (uint64_t)addr);
+}
+
+template <>
+void safe_print(int fd, const timespec& t) {
+  safe_print<uint64_t>(fd, t.tv_sec);
+  safe_print(fd, ".");
+  safe_print_right_aligned(fd, t.tv_nsec, 9);
+}
+
+void safe_print_hex(int fd, uint64_t i) {
+  char buf[BUFFER_SIZE];
+
+  safe_print(fd, "0x");
+  if (i == 0) {
+    safe_print(fd, "0");
+    return;
+  }
+
+  // This loop fills the buffer from the end. The number of elements in the
+  // buffer is BUFER_SIZE - idx - 1 and they start at position idx + 1.
+  size_t idx = BUFFER_SIZE - 1;
+  while (i != 0 && idx >= 0) {
+    char current = i % 16;
+    if (current <= 9) {
+      buf[idx] = '0' + current;
+    } else {
+      buf[idx] = 'a' + current - 10;
+    }
+    i /= 16;
+    idx--;
+  }
+
+  ssize_t nbyte = BUFFER_SIZE - idx - 1;
+  if (write(fd, buf + idx + 1, nbyte) != nbyte) {
+    abort();
+  }
+}
+
+void safe_print_right_aligned(int fd, uint64_t i, ssize_t width) {
+  char buf[BUFFER_SIZE];
+
+  // Make sure that the result fits in the buffer
+  width = (width < BUFFER_SIZE) ? width : BUFFER_SIZE;
+
+  for (ssize_t j = 0; j < width; j++) {
+    buf[j] = '0';
+  }
+
+  ssize_t idx = width - 1;
+  while (i != 0 && idx >= 0) {
+    buf[idx] = '0' + i % 10;
+    i /= 10;
+    idx--;
+  }
+
+  if (write(fd, buf, width) != width) {
+    abort();
+  }
+}
+
+} /* CVC4 namespace */
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
new file mode 100644
index 000000000..637d00d00
--- /dev/null
+++ b/src/util/safe_print.h
@@ -0,0 +1,99 @@
+/*********************                                                        */
+/*! \file safe_print.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** 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
+ **
+ ** \brief Print functions that are safe to use in a signal handler.
+ **
+ ** Signal handlers only allow a very limited set of operations, e.g. dynamic
+ ** memory allocation is not possible. This set of functions can be used to
+ ** print information from a signal handler.
+ **
+ ** The safe_print function takes a template parameter T and prints an argument
+ ** of type const T& to avoid copying, e.g. when printing std::strings. For
+ ** consistency, we also pass primitive types by reference (otherwise, functions
+ ** in statistics_registry.h would require specialization or we would have to
+ ** use function overloading).
+ **
+ ** This header is a "cvc4_private_library.h" header because it is private but
+ ** the safe_print functions are used in the driver. See also the description
+ ** of "statistics_registry.h" for more information on
+ ** "cvc4_private_library.h".
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef __CVC4__SAFE_PRINT_H
+#define __CVC4__SAFE_PRINT_H
+
+#if __cplusplus >= 201103L
+// For c++11 and newer
+#include <cstdint>
+#else
+#include <stdint.h>
+#endif
+
+#include <unistd.h>
+
+#include "lib/clock_gettime.h"
+#include "util/result.h"
+
+namespace CVC4 {
+
+/**
+ * Prints arrays of chars (e.g. string literals) of length N. Safe to use in a
+ * signal handler.
+ */
+template <size_t N>
+void CVC4_PUBLIC safe_print(int fd, const char (&msg)[N]) {
+  ssize_t nb = N - 1;
+  if (write(fd, msg, nb) != nb) {
+    abort();
+  }
+}
+
+/** Prints a variable of type T. Safe to use in a signal handler. */
+template <typename T>
+void CVC4_PUBLIC safe_print(int fd, const T& msg) {
+  safe_print(fd, "<unsupported>");
+}
+
+template <>
+void CVC4_PUBLIC safe_print(int fd, const std::string& msg);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const int64_t& _i);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const int32_t& i);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const uint64_t& _i);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const uint32_t& i);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const double& _d);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const float& f);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const bool& b);
+template <>
+void CVC4_PUBLIC safe_print(int fd, void* const& addr);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const timespec& t);
+
+/** Prints an integer in hexadecimal. Safe to use in a signal handler. */
+void safe_print_hex(int fd, uint64_t i);
+
+/**
+ * Prints a right aligned number. Fills up remaining space with zeros. Safe to
+ * use in a signal handler.
+ */
+void safe_print_right_aligned(int fd, uint64_t i, ssize_t width);
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__SAFE_PRINT_H */
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 368335f7e..73ea5b1b1 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -19,6 +19,7 @@
 
 #include <typeinfo>
 
+#include "util/safe_print.h"
 #include "util/statistics_registry.h" // for details about class Stat
 
 
@@ -116,6 +117,20 @@ void StatisticsBase::flushInformation(std::ostream &out) const {
 #endif /* CVC4_STATISTICS_ON */
 }
 
+void StatisticsBase::safeFlushInformation(int fd) const {
+#ifdef CVC4_STATISTICS_ON
+  for (StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
+    Stat* s = *i;
+    if (d_prefix.size() != 0) {
+      safe_print(fd, d_prefix.c_str());
+      safe_print(fd, s_regDelim.c_str());
+    }
+    s->safeFlushStat(fd);
+    safe_print(fd, "\n");
+  }
+#endif /* CVC4_STATISTICS_ON */
+}
+
 SExpr StatisticsBase::getStatistic(std::string name) const {
   SExpr value;
   IntStat s(name, 0);
diff --git a/src/util/statistics.h b/src/util/statistics.h
index 663d2071b..bdc8ad6a2 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -84,6 +84,12 @@ public:
   /** Flush all statistics to the given output stream. */
   void flushInformation(std::ostream& out) const;
 
+  /**
+   * Flush all statistics to the given file descriptor. Safe to use in a signal
+   * handler.
+   */
+  void safeFlushInformation(int fd) const;
+
   /** Get the value of a named statistic. */
   SExpr getStatistic(std::string name) const;
 
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index cb8e1ce90..4b0626048 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -182,6 +182,12 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const {
 #endif /* CVC4_STATISTICS_ON */
 }
 
+void StatisticsRegistry::safeFlushInformation(int fd) const {
+#ifdef CVC4_STATISTICS_ON
+  this->StatisticsBase::safeFlushInformation(fd);
+#endif /* CVC4_STATISTICS_ON */
+}
+
 void TimerStat::start() {
   if(__CVC4_USE_STATISTICS) {
     PrettyCheckArgument(!d_running, *this, "timer already running");
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 4f2c356e8..1206a3e4a 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -47,6 +47,7 @@
 
 #include "base/exception.h"
 #include "lib/clock_gettime.h"
+#include "util/safe_print.h"
 #include "util/statistics.h"
 
 namespace CVC4 {
@@ -108,6 +109,13 @@ public:
    */
   virtual void flushInformation(std::ostream& out) const = 0;
 
+  /**
+   * Flush the value of this statistic to a file descriptor. Should finish the
+   * output with an end-of-line character. Should be safe to use in a signal
+   * handler.
+   */
+  virtual void safeFlushInformation(int fd) const = 0;
+
   /**
    * Flush the name,value pair of this statistic to an output stream.
    * Uses the statistic delimiter string between name and value.
@@ -121,6 +129,20 @@ public:
     }
   }
 
+  /**
+   * Flush the name,value pair of this statistic to a file descriptor. Uses the
+   * statistic delimiter string between name and value.
+   *
+   * May be redefined by a child class
+   */
+  virtual void safeFlushStat(int fd) const {
+    if (__CVC4_USE_STATISTICS) {
+      safe_print(fd, d_name.c_str());
+      safe_print(fd, ", ");
+      safeFlushInformation(fd);
+    }
+  }
+
   /** Get the name of this statistic. */
   const std::string& getName() const {
     return d_name;
@@ -210,6 +232,12 @@ public:
     }
   }
 
+  virtual void safeFlushInformation(int fd) const {
+    if (__CVC4_USE_STATISTICS) {
+      safe_print<T>(fd, getData());
+    }
+  }
+
   SExpr getValue() const {
     return mkSExpr(getData());
   }
@@ -298,7 +326,6 @@ public:
 
 };/* class ReferenceStat<T> */
 
-
 /**
  * A data statistic that keeps a T and sets it with setData().
  *
@@ -340,7 +367,6 @@ public:
 
 };/* class BackedStat<T> */
 
-
 /**
  * A wrapper Stat for another Stat.
  *
@@ -455,6 +481,10 @@ public:
     out << d_sized.size();
   }
 
+  void safeFlushInformation(int fd) const {
+    safe_print<uint64_t>(fd, d_sized.size());
+  }
+
   SExpr getValue() const {
     return SExpr(Integer(d_sized.size()));
   }
@@ -522,50 +552,18 @@ public:
     out << d_data << std::endl;
   }
 
+  virtual void safeFlushInformation(int fd) const {
+    // SExprStat is only used in statistics.cpp in copyFrom, which we cannot
+    // do in a signal handler anyway.
+    safe_print(fd, "<unsupported>");
+  }
+
   SExpr getValue() const {
     return d_data;
   }
 
 };/* class SExprStat */
 
-template <class T>
-class ListStat : public Stat {
-private:
-  typedef std::vector<T> List;
-  List d_list;
-public:
-
-  /**
-   * Construct an integer-valued statistic with the given name and
-   * initial value.
-   */
-  ListStat(const std::string& name) : Stat(name) {}
-  ~ListStat() {}
-
-  void flushInformation(std::ostream& out) const{
-    if(__CVC4_USE_STATISTICS) {
-      typename List::const_iterator i = d_list.begin(), end =  d_list.end();
-      out << "[";
-      if(i != end){
-        out << *i;
-        ++i;
-        for(; i != end; ++i){
-          out << ", " << *i;
-        }
-      }
-      out << "]";
-    }
-  }
-
-  ListStat& operator<<(const T& val){
-    if(__CVC4_USE_STATISTICS) {
-      d_list.push_back(val);
-    }
-    return (*this);
-  }
-
-};/* class ListStat */
-
 template <class T>
 class HistogramStat : public Stat {
 private:
@@ -595,6 +593,28 @@ public:
     }
   }
 
+  virtual void safeFlushInformation(int fd) const {
+    if (__CVC4_USE_STATISTICS) {
+      typename Histogram::const_iterator i = d_hist.begin();
+      typename Histogram::const_iterator end = d_hist.end();
+      safe_print(fd, "[");
+      while (i != end) {
+        const T& key = (*i).first;
+        unsigned int count = (*i).second;
+        safe_print(fd, "(");
+        safe_print<T>(fd, key);
+        safe_print(fd, " : ");
+        safe_print<uint64_t>(fd, count);
+        safe_print(fd, ")");
+        ++i;
+        if (i != end) {
+          safe_print(fd, ", ");
+        }
+      }
+      safe_print(fd, "]");
+    }
+  }
+
   HistogramStat& operator<<(const T& val){
     if(__CVC4_USE_STATISTICS) {
       if(d_hist.find(val) == d_hist.end()){
@@ -643,6 +663,8 @@ public:
 
   virtual void flushInformation(std::ostream& out) const;
 
+  virtual void safeFlushInformation(int fd) const;
+
   SExpr getValue() const {
     std::vector<SExpr> v;
     for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
@@ -708,6 +730,10 @@ public:
 
   timespec getData() const;
 
+  virtual void safeFlushInformation(int fd) const {
+    safe_print<timespec>(fd, d_data);
+  }
+
   SExpr getValue() const;
 
 };/* class TimerStat */
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index c5b0d46bb..9f06b469f 100644
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -15,9 +15,10 @@
  **/
 
 #include <cxxtest/TestSuite.h>
+#include <fcntl.h>
+#include <ctime>
 #include <sstream>
 #include <string>
-#include <ctime>
 
 #include "lib/clock_gettime.h"
 #include "util/statistics_registry.h"
@@ -62,6 +63,22 @@ public:
     // getData
     // operator=
 
+    BackedStat<double> backedDouble("backedDouble", 16.5);
+    BackedStat<double> backedNegDouble("backedNegDouble", -16.5);
+    BackedStat<double> backedDoubleNoDec("backedDoubleNoDec", 2.0);
+    BackedStat<bool> backedBool("backedBool", true);
+    BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
+    HistogramStat<int64_t> histStat("hist");
+    histStat << 5;
+    histStat << 6;
+    histStat << 5;
+    histStat << 10;
+    histStat << 10;
+    histStat << 0;
+
+    // A statistic with no safe_print support
+    BackedStat<string*> backedUnsupported("backedUnsupported", &bar);
+
     IntStat sInt("my int", 10);
     TimerStat sTimer("a timer ! for measuring time");
 
@@ -104,6 +121,63 @@ public:
     sstr.str("");
     sTimer.flushInformation(sstr);
     TS_ASSERT_EQUALS(sstr.str(), "0.000000000");
+
+    // Test safeFlushInformation (and safe_print functions)
+    char tmp_filename[] = "testXXXXXX";
+    int fd = mkstemp(tmp_filename);
+    TS_ASSERT_DIFFERS(fd, -1);
+    refStr.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    refStr2.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    backedStr.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    sInt.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    sTimer.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    backedDouble.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    backedNegDouble.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    backedDoubleNoDec.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    backedAddr.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    backedBool.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    histStat.safeFlushInformation(fd);
+    safe_print(fd, "\n");
+    backedUnsupported.safeFlushInformation(fd);
+    off_t file_size = lseek(fd, 0, SEEK_CUR);
+    close(fd);
+
+    char* buf = new char[file_size];
+    fd = open(tmp_filename, O_RDONLY);
+    TS_ASSERT_DIFFERS(fd, -1);
+    ssize_t n_read = pread(fd, buf, file_size, 0);
+    TS_ASSERT_EQUALS(n_read, file_size);
+    close(fd);
+
+    const char* expected =
+        "a different string\n"
+        "bar and with an addition\n"
+        "baz\n"
+        "100\n"
+        "0.000000000\n"
+        "16.5\n"
+        "-16.5\n"
+        "2.0\n"
+        "0xdeadbeef\n"
+        "true\n"
+        "[(0 : 1), (5 : 2), (6 : 1), (10 : 2)]\n"
+        "<unsupported>";
+    std::cout << buf << std::endl;
+    TS_ASSERT(strncmp(expected, buf, file_size) == 0);
+    delete[] buf;
+
+    int ret = remove(tmp_filename);
+    TS_ASSERT_EQUALS(ret, 0);
 #endif /* CVC4_STATISTICS_ON */
   }