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

1 files changed, 66 insertions, 40 deletions

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 {
@@ -109,6 +110,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,6 +552,12 @@ 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;
   }
@@ -529,44 +565,6 @@ public:
 };/* 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:
   typedef std::map<T, unsigned int> Histogram;
@@ -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 */