diff options
Diffstat (limited to 'src/util/safe_print.h')
-rw-r--r-- | src/util/safe_print.h | 55 |
1 files changed, 52 insertions, 3 deletions
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 <> |