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

2 files changed, 11 insertions, 1 deletions

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