diff options
-rw-r--r-- | src/theory/strings/infer_info.cpp | 35 | ||||
-rw-r--r-- | src/theory/strings/infer_info.h | 21 | ||||
-rw-r--r-- | src/util/safe_print.h | 55 |
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 <> |