Branch data Line data Source code
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-2024 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::internal {
33 : :
34 : : template <>
35 : 28 : 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 [ + + ]: 299 : for (size_t i = 0; i < msg.length(); i++) {
39 [ - + ]: 271 : if (write(fd, &(msg[i]), 1) != 1) {
40 : 0 : abort();
41 : : }
42 : : }
43 : 28 : }
44 : :
45 : : template <>
46 : 0 : void safe_print(int fd, const int64_t& _i) {
47 : : char buf[BUFFER_SIZE];
48 : 0 : int64_t i = _i;
49 : :
50 [ - - ]: 0 : if (i == 0) {
51 : 0 : safe_print(fd, "0");
52 : 0 : return;
53 [ - - ]: 0 : } else if (i < 0) {
54 : 0 : safe_print(fd, "-");
55 : 0 : 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 : 0 : ssize_t idx = BUFFER_SIZE - 1;
61 [ - - ][ - - ]: 0 : while (i != 0 && idx >= 0) {
62 : 0 : buf[idx] = '0' + i % 10;
63 : 0 : i /= 10;
64 : 0 : idx--;
65 : : }
66 : :
67 : 0 : ssize_t nbyte = BUFFER_SIZE - idx - 1;
68 [ - - ]: 0 : if (write(fd, buf + idx + 1, nbyte) != nbyte) {
69 : 0 : abort();
70 : : }
71 : : }
72 : :
73 : : template <>
74 : 0 : void safe_print(int fd, const int32_t& i) {
75 : 0 : safe_print<int64_t>(fd, i);
76 : 0 : }
77 : :
78 : : template <>
79 : 16 : void safe_print(int fd, const uint64_t& _i) {
80 : : char buf[BUFFER_SIZE];
81 : 16 : uint64_t i = _i;
82 : :
83 [ + + ]: 16 : if (i == 0) {
84 : 12 : safe_print(fd, "0");
85 : 12 : 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 : 4 : ssize_t idx = BUFFER_SIZE - 1;
91 [ + + ][ + - ]: 9 : while (i != 0 && idx >= 0) {
92 : 5 : buf[idx] = '0' + i % 10;
93 : 5 : i /= 10;
94 : 5 : idx--;
95 : : }
96 : :
97 : 4 : ssize_t nbyte = BUFFER_SIZE - idx - 1;
98 [ - + ]: 4 : if (write(fd, buf + idx + 1, nbyte) != nbyte) {
99 : 0 : abort();
100 : : }
101 : : }
102 : :
103 : : template <>
104 : 0 : void safe_print(int fd, const uint32_t& i) {
105 : 0 : safe_print<uint64_t>(fd, i);
106 : 0 : }
107 : :
108 : : template <>
109 : 0 : 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 : 0 : double d = _d;
114 : :
115 : 0 : ssize_t i = 0;
116 : 0 : int64_t v = static_cast<int64_t>(d);
117 : 0 : d -= v;
118 : :
119 [ - - ]: 0 : if (d < 0.0) {
120 : 0 : d *= -1.0;
121 : : }
122 : :
123 : 0 : safe_print<int64_t>(fd, v);
124 : 0 : 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 [ - - ][ - - ]: 0 : while (i == 0 || (d > 0.0 && i < BUFFER_SIZE)) {
[ - - ]
129 : 0 : d *= 10.0;
130 : 0 : char c = static_cast<char>(d);
131 : 0 : buf[i] = '0' + c;
132 : 0 : d -= c;
133 : 0 : i++;
134 : : }
135 : :
136 [ - - ]: 0 : if (write(fd, buf, i) != i) {
137 : 0 : abort();
138 : : }
139 : 0 : }
140 : :
141 : : template <>
142 : 0 : void safe_print(int fd, const float& f) {
143 : 0 : safe_print<double>(fd, (double)f);
144 : 0 : }
145 : :
146 : : template <>
147 : 0 : void safe_print(int fd, const bool& b) {
148 [ - - ]: 0 : if (b) {
149 : 0 : safe_print(fd, "true");
150 : : } else {
151 : 0 : safe_print(fd, "false");
152 : : }
153 : 0 : }
154 : :
155 : : template <>
156 : 0 : void safe_print(int fd, void* const& addr) {
157 : 0 : safe_print_hex(fd, (uint64_t)addr);
158 : 0 : }
159 : :
160 : : template <>
161 : 0 : void safe_print(int fd, const timespec& t) {
162 : 0 : safe_print<uint64_t>(fd, t.tv_sec);
163 : 0 : safe_print(fd, ".");
164 : 0 : safe_print_right_aligned(fd, t.tv_nsec, 9);
165 : 0 : }
166 : :
167 : 0 : void safe_print_hex(int fd, uint64_t i) {
168 : : char buf[BUFFER_SIZE];
169 : :
170 : 0 : safe_print(fd, "0x");
171 [ - - ]: 0 : if (i == 0) {
172 : 0 : safe_print(fd, "0");
173 : 0 : 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 : 0 : ssize_t idx = BUFFER_SIZE - 1;
179 [ - - ][ - - ]: 0 : while (i != 0 && idx >= 0) {
180 : 0 : char current = i % 16;
181 [ - - ]: 0 : if (current <= 9) {
182 : 0 : buf[idx] = '0' + current;
183 : : } else {
184 : 0 : buf[idx] = 'a' + current - 10;
185 : : }
186 : 0 : i /= 16;
187 : 0 : idx--;
188 : : }
189 : :
190 : 0 : ssize_t nbyte = BUFFER_SIZE - idx - 1;
191 [ - - ]: 0 : if (write(fd, buf + idx + 1, nbyte) != nbyte) {
192 : 0 : abort();
193 : : }
194 : : }
195 : :
196 : 0 : 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 : 0 : width = (width < BUFFER_SIZE) ? width : BUFFER_SIZE;
201 : :
202 [ - - ]: 0 : for (ssize_t j = 0; j < width; j++) {
203 : 0 : buf[j] = '0';
204 : : }
205 : :
206 : 0 : ssize_t idx = width - 1;
207 [ - - ][ - - ]: 0 : while (i != 0 && idx >= 0) {
208 : 0 : buf[idx] = '0' + i % 10;
209 : 0 : i /= 10;
210 : 0 : idx--;
211 : : }
212 : :
213 [ - - ]: 0 : if (write(fd, buf, width) != width) {
214 : 0 : abort();
215 : : }
216 : 0 : }
217 : :
218 : : } // namespace cvc5::internal
|
