1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andres Noetzli |
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 |
|
* Definition of print functions that are safe to use in a signal |
14 |
|
* handler. |
15 |
|
* |
16 |
|
* Signal handlers only allow a very limited set of operations, e.g. dynamic |
17 |
|
* memory allocation is not possible. This set of functions can be used to |
18 |
|
* print information from a signal handler. All output is written to file |
19 |
|
* descriptors using the async-signal-safe write() function. |
20 |
|
*/ |
21 |
|
|
22 |
|
#include "safe_print.h" |
23 |
|
|
24 |
|
#include <time.h> |
25 |
|
#include <unistd.h> |
26 |
|
|
27 |
|
#include <cstdlib> |
28 |
|
|
29 |
|
/* Size of buffers used */ |
30 |
|
#define BUFFER_SIZE 20 |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
|
34 |
|
template <> |
35 |
|
void safe_print(int fd, const std::string& msg) { |
36 |
|
// Print characters one by one instead of using |
37 |
|
// string::data()/string::c_str() to avoid allocations (pre-c++11) |
38 |
|
for (size_t i = 0; i < msg.length(); i++) { |
39 |
|
if (write(fd, &(msg[i]), 1) != 1) { |
40 |
|
abort(); |
41 |
|
} |
42 |
|
} |
43 |
|
} |
44 |
|
|
45 |
|
template <> |
46 |
|
void safe_print(int fd, const int64_t& _i) { |
47 |
|
char buf[BUFFER_SIZE]; |
48 |
|
int64_t i = _i; |
49 |
|
|
50 |
|
if (i == 0) { |
51 |
|
safe_print(fd, "0"); |
52 |
|
return; |
53 |
|
} else if (i < 0) { |
54 |
|
safe_print(fd, "-"); |
55 |
|
i *= -1; |
56 |
|
} |
57 |
|
|
58 |
|
// This loop fills the buffer from the end. The number of elements in the |
59 |
|
// buffer is BUFER_SIZE - idx - 1 and they start at position idx + 1. |
60 |
|
ssize_t idx = BUFFER_SIZE - 1; |
61 |
|
while (i != 0 && idx >= 0) { |
62 |
|
buf[idx] = '0' + i % 10; |
63 |
|
i /= 10; |
64 |
|
idx--; |
65 |
|
} |
66 |
|
|
67 |
|
ssize_t nbyte = BUFFER_SIZE - idx - 1; |
68 |
|
if (write(fd, buf + idx + 1, nbyte) != nbyte) { |
69 |
|
abort(); |
70 |
|
} |
71 |
|
} |
72 |
|
|
73 |
|
template <> |
74 |
|
void safe_print(int fd, const int32_t& i) { |
75 |
|
safe_print<int64_t>(fd, i); |
76 |
|
} |
77 |
|
|
78 |
|
template <> |
79 |
|
void safe_print(int fd, const uint64_t& _i) { |
80 |
|
char buf[BUFFER_SIZE]; |
81 |
|
uint64_t i = _i; |
82 |
|
|
83 |
|
if (i == 0) { |
84 |
|
safe_print(fd, "0"); |
85 |
|
return; |
86 |
|
} |
87 |
|
|
88 |
|
// This loop fills the buffer from the end. The number of elements in the |
89 |
|
// buffer is BUFER_SIZE - idx - 1 and they start at position idx + 1. |
90 |
|
ssize_t idx = BUFFER_SIZE - 1; |
91 |
|
while (i != 0 && idx >= 0) { |
92 |
|
buf[idx] = '0' + i % 10; |
93 |
|
i /= 10; |
94 |
|
idx--; |
95 |
|
} |
96 |
|
|
97 |
|
ssize_t nbyte = BUFFER_SIZE - idx - 1; |
98 |
|
if (write(fd, buf + idx + 1, nbyte) != nbyte) { |
99 |
|
abort(); |
100 |
|
} |
101 |
|
} |
102 |
|
|
103 |
|
template <> |
104 |
|
void safe_print(int fd, const uint32_t& i) { |
105 |
|
safe_print<uint64_t>(fd, i); |
106 |
|
} |
107 |
|
|
108 |
|
template <> |
109 |
|
void safe_print(int fd, const double& _d) { |
110 |
|
// Note: this print function for floating-point values is optimized for |
111 |
|
// simplicity, not correctness or performance. |
112 |
|
char buf[BUFFER_SIZE]; |
113 |
|
double d = _d; |
114 |
|
|
115 |
|
ssize_t i = 0; |
116 |
|
int64_t v = static_cast<int64_t>(d); |
117 |
|
d -= v; |
118 |
|
|
119 |
|
if (d < 0.0) { |
120 |
|
d *= -1.0; |
121 |
|
} |
122 |
|
|
123 |
|
safe_print<int64_t>(fd, v); |
124 |
|
safe_print(fd, "."); |
125 |
|
|
126 |
|
// Print decimal digits as long as the remaining value is larger than zero |
127 |
|
// and print at least one digit. |
128 |
|
while (i == 0 || (d > 0.0 && i < BUFFER_SIZE)) { |
129 |
|
d *= 10.0; |
130 |
|
char c = static_cast<char>(d); |
131 |
|
buf[i] = '0' + c; |
132 |
|
d -= c; |
133 |
|
i++; |
134 |
|
} |
135 |
|
|
136 |
|
if (write(fd, buf, i) != i) { |
137 |
|
abort(); |
138 |
|
} |
139 |
|
} |
140 |
|
|
141 |
|
template <> |
142 |
|
void safe_print(int fd, const float& f) { |
143 |
|
safe_print<double>(fd, (double)f); |
144 |
|
} |
145 |
|
|
146 |
|
template <> |
147 |
|
void safe_print(int fd, const bool& b) { |
148 |
|
if (b) { |
149 |
|
safe_print(fd, "true"); |
150 |
|
} else { |
151 |
|
safe_print(fd, "false"); |
152 |
|
} |
153 |
|
} |
154 |
|
|
155 |
|
template <> |
156 |
|
void safe_print(int fd, void* const& addr) { |
157 |
|
safe_print_hex(fd, (uint64_t)addr); |
158 |
|
} |
159 |
|
|
160 |
|
template <> |
161 |
|
void safe_print(int fd, const timespec& t) { |
162 |
|
safe_print<uint64_t>(fd, t.tv_sec); |
163 |
|
safe_print(fd, "."); |
164 |
|
safe_print_right_aligned(fd, t.tv_nsec, 9); |
165 |
|
} |
166 |
|
|
167 |
|
void safe_print_hex(int fd, uint64_t i) { |
168 |
|
char buf[BUFFER_SIZE]; |
169 |
|
|
170 |
|
safe_print(fd, "0x"); |
171 |
|
if (i == 0) { |
172 |
|
safe_print(fd, "0"); |
173 |
|
return; |
174 |
|
} |
175 |
|
|
176 |
|
// This loop fills the buffer from the end. The number of elements in the |
177 |
|
// buffer is BUFER_SIZE - idx - 1 and they start at position idx + 1. |
178 |
|
ssize_t idx = BUFFER_SIZE - 1; |
179 |
|
while (i != 0 && idx >= 0) { |
180 |
|
char current = i % 16; |
181 |
|
if (current <= 9) { |
182 |
|
buf[idx] = '0' + current; |
183 |
|
} else { |
184 |
|
buf[idx] = 'a' + current - 10; |
185 |
|
} |
186 |
|
i /= 16; |
187 |
|
idx--; |
188 |
|
} |
189 |
|
|
190 |
|
ssize_t nbyte = BUFFER_SIZE - idx - 1; |
191 |
|
if (write(fd, buf + idx + 1, nbyte) != nbyte) { |
192 |
|
abort(); |
193 |
|
} |
194 |
|
} |
195 |
|
|
196 |
|
void safe_print_right_aligned(int fd, uint64_t i, ssize_t width) { |
197 |
|
char buf[BUFFER_SIZE]; |
198 |
|
|
199 |
|
// Make sure that the result fits in the buffer |
200 |
|
width = (width < BUFFER_SIZE) ? width : BUFFER_SIZE; |
201 |
|
|
202 |
|
for (ssize_t j = 0; j < width; j++) { |
203 |
|
buf[j] = '0'; |
204 |
|
} |
205 |
|
|
206 |
|
ssize_t idx = width - 1; |
207 |
|
while (i != 0 && idx >= 0) { |
208 |
|
buf[idx] = '0' + i % 10; |
209 |
|
i /= 10; |
210 |
|
idx--; |
211 |
|
} |
212 |
|
|
213 |
|
if (write(fd, buf, width) != width) { |
214 |
|
abort(); |
215 |
|
} |
216 |
|
} |
217 |
|
|
218 |
|
} // namespace cvc5 |