1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andres Noetzli, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Print functions that are safe to use in a signal handler. |
14 |
|
* |
15 |
|
* Signal handlers only allow a very limited set of operations, e.g. dynamic |
16 |
|
* memory allocation is not possible. This set of functions can be used to |
17 |
|
* print information from a signal handler. |
18 |
|
* |
19 |
|
* The safe_print function takes a template parameter T and prints an argument |
20 |
|
* of type const T& to avoid copying, e.g. when printing std::strings. For |
21 |
|
* consistency, we also pass primitive types by reference (otherwise, functions |
22 |
|
* in statistics_registry.h would require specialization or we would have to |
23 |
|
* use function overloading). |
24 |
|
* |
25 |
|
* If there exists a function `toString(obj)` for a given object, it will be |
26 |
|
* used automatically. This is useful for printing enum values for example. |
27 |
|
* IMPORTANT: The `toString(obj)` function *must not* perform any allocations |
28 |
|
* or call other functions that are not async-signal-safe. |
29 |
|
* |
30 |
|
* This header is a "cvc5_private_library.h" header because it is private but |
31 |
|
* the safe_print functions are used in the driver. See also the description |
32 |
|
* of "statistics_registry.h" for more information on |
33 |
|
* "cvc5_private_library.h". |
34 |
|
*/ |
35 |
|
|
36 |
|
#include "cvc5_private_library.h" |
37 |
|
|
38 |
|
#ifndef CVC5__SAFE_PRINT_H |
39 |
|
#define CVC5__SAFE_PRINT_H |
40 |
|
|
41 |
|
#include <unistd.h> |
42 |
|
|
43 |
|
#include <cstring> |
44 |
|
#include <string> |
45 |
|
|
46 |
|
#include "cvc5_export.h" |
47 |
|
|
48 |
|
namespace cvc5 { |
49 |
|
|
50 |
|
/** |
51 |
|
* Prints arrays of chars (e.g. string literals) of length N. Safe to use in a |
52 |
|
* signal handler. |
53 |
|
*/ |
54 |
|
template <size_t N> |
55 |
|
void CVC5_EXPORT safe_print(int fd, const char (&msg)[N]) |
56 |
|
{ |
57 |
|
ssize_t nb = N - 1; |
58 |
|
if (write(fd, msg, nb) != nb) { |
59 |
|
abort(); |
60 |
|
} |
61 |
|
} |
62 |
|
|
63 |
|
/** |
64 |
|
* The default method for converting an object to a string for safe printing. |
65 |
|
* This method simply returns "<unsupported>". The `long` argument is used to |
66 |
|
* indicate that we do not prefer this method over the version that calls |
67 |
|
* `toString()`. |
68 |
|
*/ |
69 |
|
template <typename T> |
70 |
|
const char* toStringImpl(const T& obj, long) |
71 |
|
{ |
72 |
|
return "<unsupported>"; |
73 |
|
} |
74 |
|
|
75 |
|
/** |
76 |
|
* Returns the result of calling `toString(obj)`. This method is only defined |
77 |
|
* if such an overload of `toString()` exists. To detect the existence of such |
78 |
|
* a method, we use SFINAE and a trailing return type. The trailing return type |
79 |
|
* is necessary because it allows us to refer to `obj`. The `int` argument is |
80 |
|
* used to prefer this version of the function instead of the one that prints |
81 |
|
* "<unsupported>". |
82 |
|
*/ |
83 |
|
template <typename T> |
84 |
|
auto toStringImpl(const T& obj, int) -> decltype(toString(obj)) |
85 |
|
{ |
86 |
|
return toString(obj); |
87 |
|
} |
88 |
|
|
89 |
|
/** |
90 |
|
* Prints a variable of type T. Safe to use in a signal handler. The default |
91 |
|
* implementation either prints "<unsupported>" or the result of calling |
92 |
|
* `toString(obj)` if such a method exists (this is useful for printing enum |
93 |
|
* values for example without implementing a template specialization here). |
94 |
|
* |
95 |
|
* @param fd The file descriptor to print to |
96 |
|
* @param obj The object to print |
97 |
|
*/ |
98 |
|
template <typename T> |
99 |
|
void CVC5_EXPORT safe_print(int fd, const T& obj) |
100 |
|
{ |
101 |
|
const char* s = |
102 |
|
toStringImpl(obj, /* prefer the method that uses `toString()` */ 0); |
103 |
|
ssize_t slen = static_cast<ssize_t>(strlen(s)); |
104 |
|
if (write(fd, s, slen) != slen) |
105 |
|
{ |
106 |
|
abort(); |
107 |
|
} |
108 |
|
} |
109 |
|
|
110 |
|
template <> |
111 |
|
void CVC5_EXPORT safe_print(int fd, const std::string& msg); |
112 |
|
template <> |
113 |
|
void CVC5_EXPORT safe_print(int fd, const int64_t& _i); |
114 |
|
template <> |
115 |
|
void CVC5_EXPORT safe_print(int fd, const int32_t& i); |
116 |
|
template <> |
117 |
|
void CVC5_EXPORT safe_print(int fd, const uint64_t& _i); |
118 |
|
template <> |
119 |
|
void CVC5_EXPORT safe_print(int fd, const uint32_t& i); |
120 |
|
template <> |
121 |
|
void CVC5_EXPORT safe_print(int fd, const double& _d); |
122 |
|
template <> |
123 |
|
void CVC5_EXPORT safe_print(int fd, const float& f); |
124 |
|
template <> |
125 |
|
void CVC5_EXPORT safe_print(int fd, const bool& b); |
126 |
|
template <> |
127 |
|
void CVC5_EXPORT safe_print(int fd, void* const& addr); |
128 |
|
template <> |
129 |
|
void CVC5_EXPORT safe_print(int fd, const timespec& t); |
130 |
|
|
131 |
|
/** Prints an integer in hexadecimal. Safe to use in a signal handler. */ |
132 |
|
void safe_print_hex(int fd, uint64_t i); |
133 |
|
|
134 |
|
/** |
135 |
|
* Prints a right aligned number. Fills up remaining space with zeros. Safe to |
136 |
|
* use in a signal handler. |
137 |
|
*/ |
138 |
|
void safe_print_right_aligned(int fd, uint64_t i, ssize_t width); |
139 |
|
|
140 |
|
} // namespace cvc5 |
141 |
|
|
142 |
|
#endif /* CVC5__SAFE_PRINT_H */ |