Support async-signal-safe printing of inferences (#4148)

Commit c9b7c3d introduced code for
counting the number of string inferences done per type of inference.
However, it did not add support for printing the inference names in an
async-signal-safe manner via safe_print() (note that printing in
signal handlers is done differently from the regular stats printing).
This commit adds the corresponding code, s.t. we get the inference names
when printing the stats when CVC4 is interrupted or crashes.

3 files changed, 92 insertions, 19 deletions

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index aa7fe8974..cdf764aa8 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -14,30 +14,33 @@
 
 #include "theory/strings/infer_info.h"
 
-using namespace CVC4::kind;
-
 namespace CVC4 {
 namespace theory {
 namespace strings {
 
-std::ostream& operator<<(std::ostream& out, Inference i)
+const char* toString(Inference i)
 {
   switch (i)
   {
-    case Inference::N_ENDPOINT_EMP: out << "N_EndpointEmp"; break;
-    case Inference::N_UNIFY: out << "N_Unify"; break;
-    case Inference::N_ENDPOINT_EQ: out << "N_EndpointEq"; break;
-    case Inference::N_CONST: out << "N_Const"; break;
-    case Inference::INFER_EMP: out << "Infer-Emp"; break;
-    case Inference::SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
-    case Inference::SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
-    case Inference::LEN_SPLIT: out << "Len-Split(Len)"; break;
-    case Inference::LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
-    case Inference::SSPLIT_CST: out << "S-Split(CST-P)"; break;
-    case Inference::SSPLIT_VAR: out << "S-Split(VAR)"; break;
-    case Inference::FLOOP: out << "F-Loop"; break;
-    default: out << "?"; break;
+    case Inference::N_ENDPOINT_EMP: return "N_EndpointEmp";
+    case Inference::N_UNIFY: return "N_Unify";
+    case Inference::N_ENDPOINT_EQ: return "N_EndpointEq";
+    case Inference::N_CONST: return "N_Const";
+    case Inference::INFER_EMP: return "Infer-Emp";
+    case Inference::SSPLIT_CST_PROP: return "S-Split(CST-P)-prop";
+    case Inference::SSPLIT_VAR_PROP: return "S-Split(VAR)-prop";
+    case Inference::LEN_SPLIT: return "Len-Split(Len)";
+    case Inference::LEN_SPLIT_EMP: return "Len-Split(Emp)";
+    case Inference::SSPLIT_CST: return "S-Split(CST-P)";
+    case Inference::SSPLIT_VAR: return "S-Split(VAR)";
+    case Inference::FLOOP: return "F-Loop";
+    default: return "?";
   }
+}
+
+std::ostream& operator<<(std::ostream& out, Inference i)
+{
+  out << toString(i);
   return out;
 }
 
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 9d2f71b53..cfabe5c51 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -19,7 +19,9 @@
 
 #include <map>
 #include <vector>
+
 #include "expr/node.h"
+#include "util/safe_print.h"
 
 namespace CVC4 {
 namespace theory {
@@ -94,6 +96,25 @@ enum class Inference : uint32_t
   FLOOP,
   NONE,
 };
+
+/**
+ * Converts an inference to a string. Note: This function is also used in
+ * `safe_print()`. Changing this functions name or signature will result in
+ * `safe_print()` printing "<unsupported>" instead of the proper strings for
+ * the enum values.
+ *
+ * @param i The inference
+ * @return The name of the inference
+ */
+const char* toString(Inference i);
+
+/**
+ * Writes an inference name to a stream.
+ *
+ * @param out The stream to write to
+ * @param i The inference to write to the stream
+ * @return The stream
+ */
 std::ostream& operator<<(std::ostream& out, Inference i);
 
 /**
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
index 75a517b18..fa9430f2c 100644
--- a/src/util/safe_print.h
+++ b/src/util/safe_print.h
@@ -21,6 +21,11 @@
  ** in statistics_registry.h would require specialization or we would have to
  ** use function overloading).
  **
+ ** If there exists a function `toString(obj)` for a given object, it will be
+ ** used automatically. This is useful for printing enum values for example.
+ ** IMPORTANT: The `toString(obj)` function *must not* perform any allocations
+ ** or call other functions that are not async-signal-safe.
+ **
  ** 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
@@ -41,6 +46,9 @@
 
 #include <unistd.h>
 
+#include <cstring>
+#include <type_traits>
+
 #include "lib/clock_gettime.h"
 #include "util/result.h"
 
@@ -58,10 +66,51 @@ void CVC4_PUBLIC safe_print(int fd, const char (&msg)[N]) {
   }
 }
 
-/** Prints a variable of type T. Safe to use in a signal handler. */
+/**
+ * The default method for converting an object to a string for safe printing.
+ * This method simply returns "<unsupported>". The `long` argument is used to
+ * indicate that we do not prefer this method over the version that calls
+ * `toString()`.
+ */
+template <typename T>
+const char* toStringImpl(const T& obj, long)
+{
+  return "<unsupported>";
+}
+
+/**
+ * Returns the result of calling `toString(obj)`. This method is only defined
+ * if such an overload of `toString()` exists. To detect the existence of such
+ * a method, we use SFINAE and a trailing return type. The trailing return type
+ * is necessary because it allows us to refer to `obj`. The `int` argument is
+ * used to prefer this version of the function instead of the one that prints
+ * "<unsupported>".
+ */
+template <typename T>
+auto toStringImpl(const T& obj, int) -> decltype(toString(obj))
+{
+  return toString(obj);
+}
+
+/**
+ * Prints a variable of type T. Safe to use in a signal handler. The default
+ * implementation either prints "<unsupported>" or the result of calling
+ * `toString(obj)` if such a method exists (this is useful for printing enum
+ * values for example without implementing a template specialization here).
+ *
+ * @param fd The file descriptor to print to
+ * @param obj The object to print
+ */
 template <typename T>
-void CVC4_PUBLIC safe_print(int fd, const T& msg) {
-  safe_print(fd, "<unsupported>");
+void CVC4_PUBLIC safe_print(int fd, const T& obj)
+{
+  const char* s =
+      toStringImpl(obj, /* prefer the method that uses `toString()` */ 0);
+  ssize_t slen = static_cast<ssize_t>(strlen(s));
+  if (write(fd, s, slen) != slen)
+  {
+    abort();
+  }
 }
 
 template <>