1 /* IEC 559 floating point format related functions.
2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4
5 This file is part of the Parma Polyhedra Library (PPL).
6
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23
24 #ifndef PPL_Float_inlines_hh
25 #define PPL_Float_inlines_hh 1
26
27 #include "Variable_defs.hh"
28 #include "Linear_Form_defs.hh"
29 #include "assertions.hh"
30 #include <climits>
31
32 namespace Parma_Polyhedra_Library {
33
34 inline int
inf_sign() const35 float_ieee754_half::inf_sign() const {
36 if (word == NEG_INF) {
37 return -1;
38 }
39 if (word == POS_INF) {
40 return 1;
41 }
42 return 0;
43 }
44
45 inline bool
is_nan() const46 float_ieee754_half::is_nan() const {
47 return (word & ~SGN_MASK) > POS_INF;
48 }
49
50 inline int
zero_sign() const51 float_ieee754_half::zero_sign() const {
52 if (word == NEG_ZERO) {
53 return -1;
54 }
55 if (word == POS_ZERO) {
56 return 1;
57 }
58 return 0;
59 }
60
61 inline void
negate()62 float_ieee754_half::negate() {
63 word ^= SGN_MASK;
64 }
65
66 inline bool
sign_bit() const67 float_ieee754_half::sign_bit() const {
68 return (word & SGN_MASK) != 0;
69 }
70
71 inline void
dec()72 float_ieee754_half::dec() {
73 --word;
74 }
75
76 inline void
inc()77 float_ieee754_half::inc() {
78 ++word;
79 }
80
81 inline void
set_max(bool negative)82 float_ieee754_half::set_max(bool negative) {
83 word = WRD_MAX;
84 if (negative) {
85 word |= SGN_MASK;
86 }
87 }
88
89 inline void
build(bool negative,mpz_t mantissa,int exponent)90 float_ieee754_half::build(bool negative, mpz_t mantissa, int exponent) {
91 word = static_cast<uint16_t>(mpz_get_ui(mantissa)
92 & ((1UL << MANTISSA_BITS) - 1));
93 if (negative) {
94 word |= SGN_MASK;
95 }
96 const int exponent_repr = exponent + EXPONENT_BIAS;
97 PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
98 word |= static_cast<uint16_t>(exponent_repr) << MANTISSA_BITS;
99 }
100
101 inline int
inf_sign() const102 float_ieee754_single::inf_sign() const {
103 if (word == NEG_INF) {
104 return -1;
105 }
106 if (word == POS_INF) {
107 return 1;
108 }
109 return 0;
110 }
111
112 inline bool
is_nan() const113 float_ieee754_single::is_nan() const {
114 return (word & ~SGN_MASK) > POS_INF;
115 }
116
117 inline int
zero_sign() const118 float_ieee754_single::zero_sign() const {
119 if (word == NEG_ZERO) {
120 return -1;
121 }
122 if (word == POS_ZERO) {
123 return 1;
124 }
125 return 0;
126 }
127
128 inline void
negate()129 float_ieee754_single::negate() {
130 word ^= SGN_MASK;
131 }
132
133 inline bool
sign_bit() const134 float_ieee754_single::sign_bit() const {
135 return (word & SGN_MASK) != 0;
136 }
137
138 inline void
dec()139 float_ieee754_single::dec() {
140 --word;
141 }
142
143 inline void
inc()144 float_ieee754_single::inc() {
145 ++word;
146 }
147
148 inline void
set_max(bool negative)149 float_ieee754_single::set_max(bool negative) {
150 word = WRD_MAX;
151 if (negative) {
152 word |= SGN_MASK;
153 }
154 }
155
156 inline void
build(bool negative,mpz_t mantissa,int exponent)157 float_ieee754_single::build(bool negative, mpz_t mantissa, int exponent) {
158 word = static_cast<uint32_t>(mpz_get_ui(mantissa)
159 & ((1UL << MANTISSA_BITS) - 1));
160 if (negative) {
161 word |= SGN_MASK;
162 }
163 const int exponent_repr = exponent + EXPONENT_BIAS;
164 PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
165 word |= static_cast<uint32_t>(exponent_repr) << MANTISSA_BITS;
166 }
167
168 inline int
inf_sign() const169 float_ieee754_double::inf_sign() const {
170 if (lsp != LSP_INF) {
171 return 0;
172 }
173 if (msp == MSP_NEG_INF) {
174 return -1;
175 }
176 if (msp == MSP_POS_INF) {
177 return 1;
178 }
179 return 0;
180 }
181
182 inline bool
is_nan() const183 float_ieee754_double::is_nan() const {
184 const uint32_t a = msp & ~MSP_SGN_MASK;
185 return a > MSP_POS_INF || (a == MSP_POS_INF && lsp != LSP_INF);
186 }
187
188 inline int
zero_sign() const189 float_ieee754_double::zero_sign() const {
190 if (lsp != LSP_ZERO) {
191 return 0;
192 }
193 if (msp == MSP_NEG_ZERO) {
194 return -1;
195 }
196 if (msp == MSP_POS_ZERO) {
197 return 1;
198 }
199 return 0;
200 }
201
202 inline void
negate()203 float_ieee754_double::negate() {
204 msp ^= MSP_SGN_MASK;
205 }
206
207 inline bool
sign_bit() const208 float_ieee754_double::sign_bit() const {
209 return (msp & MSP_SGN_MASK) != 0;
210 }
211
212 inline void
dec()213 float_ieee754_double::dec() {
214 if (lsp == 0) {
215 --msp;
216 lsp = LSP_MAX;
217 }
218 else {
219 --lsp;
220 }
221 }
222
223 inline void
inc()224 float_ieee754_double::inc() {
225 if (lsp == LSP_MAX) {
226 ++msp;
227 lsp = 0;
228 }
229 else {
230 ++lsp;
231 }
232 }
233
234 inline void
set_max(bool negative)235 float_ieee754_double::set_max(bool negative) {
236 msp = MSP_MAX;
237 lsp = LSP_MAX;
238 if (negative) {
239 msp |= MSP_SGN_MASK;
240 }
241 }
242
243 inline void
build(bool negative,mpz_t mantissa,int exponent)244 float_ieee754_double::build(bool negative, mpz_t mantissa, int exponent) {
245 unsigned long m;
246 #if ULONG_MAX == 0xffffffffUL
247 lsp = mpz_get_ui(mantissa);
248 mpz_tdiv_q_2exp(mantissa, mantissa, 32);
249 m = mpz_get_ui(mantissa);
250 #else
251 m = mpz_get_ui(mantissa);
252 lsp = static_cast<uint32_t>(m & LSP_MAX);
253 m >>= 32;
254 #endif
255 msp = static_cast<uint32_t>(m & ((1UL << (MANTISSA_BITS - 32)) - 1));
256 if (negative) {
257 msp |= MSP_SGN_MASK;
258 }
259 const int exponent_repr = exponent + EXPONENT_BIAS;
260 PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
261 msp |= static_cast<uint32_t>(exponent_repr) << (MANTISSA_BITS - 32);
262 }
263
264 inline int
inf_sign() const265 float_ibm_single::inf_sign() const {
266 if (word == NEG_INF) {
267 return -1;
268 }
269 if (word == POS_INF) {
270 return 1;
271 }
272 return 0;
273 }
274
275 inline bool
is_nan() const276 float_ibm_single::is_nan() const {
277 return (word & ~SGN_MASK) > POS_INF;
278 }
279
280 inline int
zero_sign() const281 float_ibm_single::zero_sign() const {
282 if (word == NEG_ZERO) {
283 return -1;
284 }
285 if (word == POS_ZERO) {
286 return 1;
287 }
288 return 0;
289 }
290
291 inline void
negate()292 float_ibm_single::negate() {
293 word ^= SGN_MASK;
294 }
295
296 inline bool
sign_bit() const297 float_ibm_single::sign_bit() const {
298 return (word & SGN_MASK) != 0;
299 }
300
301 inline void
dec()302 float_ibm_single::dec() {
303 --word;
304 }
305
306 inline void
inc()307 float_ibm_single::inc() {
308 ++word;
309 }
310
311 inline void
set_max(bool negative)312 float_ibm_single::set_max(bool negative) {
313 word = WRD_MAX;
314 if (negative) {
315 word |= SGN_MASK;
316 }
317 }
318
319 inline void
build(bool negative,mpz_t mantissa,int exponent)320 float_ibm_single::build(bool negative, mpz_t mantissa, int exponent) {
321 word = static_cast<uint32_t>(mpz_get_ui(mantissa)
322 & ((1UL << MANTISSA_BITS) - 1));
323 if (negative) {
324 word |= SGN_MASK;
325 }
326 const int exponent_repr = exponent + EXPONENT_BIAS;
327 PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
328 word |= static_cast<uint32_t>(exponent_repr) << MANTISSA_BITS;
329 }
330
331 inline int
inf_sign() const332 float_intel_double_extended::inf_sign() const {
333 if (lsp != LSP_INF) {
334 return 0;
335 }
336 const uint32_t a = msp & MSP_NEG_INF;
337 if (a == MSP_NEG_INF) {
338 return -1;
339 }
340 if (a == MSP_POS_INF) {
341 return 1;
342 }
343 return 0;
344 }
345
346 inline bool
is_nan() const347 float_intel_double_extended::is_nan() const {
348 return (msp & MSP_POS_INF) == MSP_POS_INF
349 && lsp != LSP_INF;
350 }
351
352 inline int
zero_sign() const353 float_intel_double_extended::zero_sign() const {
354 if (lsp != LSP_ZERO) {
355 return 0;
356 }
357 const uint32_t a = msp & MSP_NEG_INF;
358 if (a == MSP_NEG_ZERO) {
359 return -1;
360 }
361 if (a == MSP_POS_ZERO) {
362 return 1;
363 }
364 return 0;
365 }
366
367 inline void
negate()368 float_intel_double_extended::negate() {
369 msp ^= MSP_SGN_MASK;
370 }
371
372 inline bool
sign_bit() const373 float_intel_double_extended::sign_bit() const {
374 return (msp & MSP_SGN_MASK) != 0;
375 }
376
377 inline void
dec()378 float_intel_double_extended::dec() {
379 if ((lsp & LSP_DMAX) == 0) {
380 --msp;
381 lsp = ((msp & MSP_NEG_INF) == 0) ? LSP_DMAX : LSP_NMAX;
382 }
383 else {
384 --lsp;
385 }
386 }
387
388 inline void
inc()389 float_intel_double_extended::inc() {
390 if ((lsp & LSP_DMAX) == LSP_DMAX) {
391 ++msp;
392 lsp = LSP_DMAX + 1;
393 }
394 else {
395 ++lsp;
396 }
397 }
398
399 inline void
set_max(bool negative)400 float_intel_double_extended::set_max(bool negative) {
401 msp = MSP_MAX;
402 lsp = LSP_NMAX;
403 if (negative) {
404 msp |= MSP_SGN_MASK;
405 }
406 }
407
408 inline void
build(bool negative,mpz_t mantissa,int exponent)409 float_intel_double_extended::build(bool negative,
410 mpz_t mantissa, int exponent) {
411 #if ULONG_MAX == 0xffffffffUL
412 mpz_export(&lsp, 0, -1, sizeof(lsp), 0, 0, mantissa);
413 #else
414 lsp = mpz_get_ui(mantissa);
415 #endif
416 msp = (negative ? MSP_SGN_MASK : 0);
417 const int exponent_repr = exponent + EXPONENT_BIAS;
418 PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
419 msp |= static_cast<uint32_t>(exponent_repr);
420 }
421
422 inline int
inf_sign() const423 float_ieee754_quad::inf_sign() const {
424 if (lsp != LSP_INF) {
425 return 0;
426 }
427 if (msp == MSP_NEG_INF) {
428 return -1;
429 }
430 if (msp == MSP_POS_INF) {
431 return 1;
432 }
433 return 0;
434 }
435
436 inline bool
is_nan() const437 float_ieee754_quad::is_nan() const {
438 return (msp & ~MSP_SGN_MASK) == MSP_POS_INF
439 && lsp != LSP_INF;
440 }
441
442 inline int
zero_sign() const443 float_ieee754_quad::zero_sign() const {
444 if (lsp != LSP_ZERO) {
445 return 0;
446 }
447 if (msp == MSP_NEG_ZERO) {
448 return -1;
449 }
450 if (msp == MSP_POS_ZERO) {
451 return 1;
452 }
453 return 0;
454 }
455
456 inline void
negate()457 float_ieee754_quad::negate() {
458 msp ^= MSP_SGN_MASK;
459 }
460
461 inline bool
sign_bit() const462 float_ieee754_quad::sign_bit() const {
463 return (msp & MSP_SGN_MASK) != 0;
464 }
465
466 inline void
dec()467 float_ieee754_quad::dec() {
468 if (lsp == 0) {
469 --msp;
470 lsp = LSP_MAX;
471 }
472 else {
473 --lsp;
474 }
475 }
476
477 inline void
inc()478 float_ieee754_quad::inc() {
479 if (lsp == LSP_MAX) {
480 ++msp;
481 lsp = 0;
482 }
483 else {
484 ++lsp;
485 }
486 }
487
488 inline void
set_max(bool negative)489 float_ieee754_quad::set_max(bool negative) {
490 msp = MSP_MAX;
491 lsp = LSP_MAX;
492 if (negative) {
493 msp |= MSP_SGN_MASK;
494 }
495 }
496
497 inline void
build(bool negative,mpz_t mantissa,int exponent)498 float_ieee754_quad::build(bool negative, mpz_t mantissa, int exponent) {
499 uint64_t parts[2];
500 mpz_export(parts, 0, -1, sizeof(parts[0]), 0, 0, mantissa);
501 lsp = parts[0];
502 msp = parts[1];
503 msp &= ((static_cast<uint64_t>(1) << (MANTISSA_BITS - 64)) - 1);
504 if (negative) {
505 msp |= MSP_SGN_MASK;
506 }
507 const int exponent_repr = exponent + EXPONENT_BIAS;
508 PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
509 msp |= static_cast<uint64_t>(exponent_repr) << (MANTISSA_BITS - 64);
510 }
511
512 inline bool
is_less_precise_than(Floating_Point_Format f1,Floating_Point_Format f2)513 is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2) {
514 return f1 < f2;
515 }
516
517 inline unsigned int
msb_position(unsigned long long v)518 msb_position(unsigned long long v) {
519 return static_cast<unsigned int>(sizeof_to_bits(sizeof(v))) - 1U - clz(v);
520 }
521
522 template <typename FP_Interval_Type>
523 inline void
affine_form_image(std::map<dimension_type,Linear_Form<FP_Interval_Type>> & lf_store,const Variable var,const Linear_Form<FP_Interval_Type> & lf)524 affine_form_image(std::map<dimension_type,
525 Linear_Form<FP_Interval_Type> >& lf_store,
526 const Variable var,
527 const Linear_Form<FP_Interval_Type>& lf) {
528 // Assign the new linear form for var.
529 lf_store[var.id()] = lf;
530 // Now invalidate all linear forms in which var occurs.
531 discard_occurrences(lf_store, var);
532 }
533
534 #if PPL_SUPPORTED_FLOAT
535 inline
Float()536 Float<float>::Float() {
537 }
538
539 inline
Float(float v)540 Float<float>::Float(float v) {
541 u.number = v;
542 }
543
544 inline float
value()545 Float<float>::value() {
546 return u.number;
547 }
548 #endif
549
550 #if PPL_SUPPORTED_DOUBLE
551 inline
Float()552 Float<double>::Float() {
553 }
554
555 inline
Float(double v)556 Float<double>::Float(double v) {
557 u.number = v;
558 }
559
560 inline double
value()561 Float<double>::value() {
562 return u.number;
563 }
564 #endif
565
566 #if PPL_SUPPORTED_LONG_DOUBLE
567 inline
Float()568 Float<long double>::Float() {
569 }
570
571 inline
Float(long double v)572 Float<long double>::Float(long double v) {
573 u.number = v;
574 }
575
576 inline long double
value()577 Float<long double>::value() {
578 return u.number;
579 }
580 #endif
581
582 } // namespace Parma_Polyhedra_Library
583
584 #endif // !defined(PPL_Float_inlines_hh)
585