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, 215 insertions, 0 deletions

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