cprover
Loading...
Searching...
No Matches
float_bv.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "float_bv.h"
10
11#include <algorithm>
12
13#include <util/arith_tools.h>
14#include <util/bitvector_expr.h>
16#include <util/floatbv_expr.h>
17#include <util/std_expr.h>
18
19exprt float_bvt::convert(const exprt &expr) const
20{
21 if(expr.id()==ID_abs)
22 return abs(to_abs_expr(expr).op(), get_spec(expr));
23 else if(expr.id()==ID_unary_minus)
24 return negation(to_unary_minus_expr(expr).op(), get_spec(expr));
25 else if(expr.id()==ID_ieee_float_equal)
26 {
27 const auto &equal_expr = to_ieee_float_equal_expr(expr);
28 return is_equal(
29 equal_expr.lhs(), equal_expr.rhs(), get_spec(equal_expr.lhs()));
30 }
31 else if(expr.id()==ID_ieee_float_notequal)
32 {
33 const auto &notequal_expr = to_ieee_float_notequal_expr(expr);
34 return not_exprt(is_equal(
35 notequal_expr.lhs(), notequal_expr.rhs(), get_spec(notequal_expr.lhs())));
36 }
37 else if(expr.id()==ID_floatbv_typecast)
38 {
39 const auto &floatbv_typecast_expr = to_floatbv_typecast_expr(expr);
40 const auto &op = floatbv_typecast_expr.op();
41 const typet &src_type = floatbv_typecast_expr.op().type();
42 const typet &dest_type = floatbv_typecast_expr.type();
43 const auto &rounding_mode = floatbv_typecast_expr.rounding_mode();
44
45 if(dest_type.id()==ID_signedbv &&
46 src_type.id()==ID_floatbv) // float -> signed
47 return to_signed_integer(
48 op,
49 to_signedbv_type(dest_type).get_width(),
50 rounding_mode,
51 get_spec(op));
52 else if(dest_type.id()==ID_unsignedbv &&
53 src_type.id()==ID_floatbv) // float -> unsigned
55 op,
56 to_unsignedbv_type(dest_type).get_width(),
57 rounding_mode,
58 get_spec(op));
59 else if(src_type.id()==ID_signedbv &&
60 dest_type.id()==ID_floatbv) // signed -> float
61 return from_signed_integer(op, rounding_mode, get_spec(expr));
62 else if(src_type.id()==ID_unsignedbv &&
63 dest_type.id()==ID_floatbv) // unsigned -> float
64 {
65 return from_unsigned_integer(op, rounding_mode, get_spec(expr));
66 }
67 else if(dest_type.id()==ID_floatbv &&
68 src_type.id()==ID_floatbv) // float -> float
69 {
70 return conversion(op, rounding_mode, get_spec(op), get_spec(expr));
71 }
72 else
73 return nil_exprt();
74 }
75 else if(
76 expr.id() == ID_typecast && expr.is_boolean() &&
77 to_typecast_expr(expr).op().type().id() == ID_floatbv) // float -> bool
78 {
79 return not_exprt(is_zero(to_typecast_expr(expr).op()));
80 }
81 else if(
82 expr.id() == ID_typecast && expr.type().id() == ID_bv &&
83 to_typecast_expr(expr).op().type().id() == ID_floatbv) // float -> raw bv
84 {
85 const typecast_exprt &tc = to_typecast_expr(expr);
86 const bitvector_typet &dest_type = to_bitvector_type(expr.type());
87 const floatbv_typet &src_type = to_floatbv_type(tc.op().type());
88 if(
89 dest_type.get_width() != src_type.get_width() ||
90 dest_type.get_width() == 0)
91 {
92 return nil_exprt{};
93 }
94
95 return extractbits_exprt{to_typecast_expr(expr).op(), 0, dest_type};
96 }
97 else if(expr.id()==ID_floatbv_plus)
98 {
99 const auto &float_expr = to_ieee_float_op_expr(expr);
100 return add_sub(
101 false,
102 float_expr.lhs(),
103 float_expr.rhs(),
104 float_expr.rounding_mode(),
105 get_spec(expr));
106 }
107 else if(expr.id()==ID_floatbv_minus)
108 {
109 const auto &float_expr = to_ieee_float_op_expr(expr);
110 return add_sub(
111 true,
112 float_expr.lhs(),
113 float_expr.rhs(),
114 float_expr.rounding_mode(),
115 get_spec(expr));
116 }
117 else if(expr.id()==ID_floatbv_mult)
118 {
119 const auto &float_expr = to_ieee_float_op_expr(expr);
120 return mul(
121 float_expr.lhs(),
122 float_expr.rhs(),
123 float_expr.rounding_mode(),
124 get_spec(expr));
125 }
126 else if(expr.id()==ID_floatbv_div)
127 {
128 const auto &float_expr = to_ieee_float_op_expr(expr);
129 return div(
130 float_expr.lhs(),
131 float_expr.rhs(),
132 float_expr.rounding_mode(),
133 get_spec(expr));
134 }
135 else if(expr.id()==ID_isnan)
136 {
137 const auto &op = to_unary_expr(expr).op();
138 return isnan(op, get_spec(op));
139 }
140 else if(expr.id()==ID_isfinite)
141 {
142 const auto &op = to_unary_expr(expr).op();
143 return isfinite(op, get_spec(op));
144 }
145 else if(expr.id()==ID_isinf)
146 {
147 const auto &op = to_unary_expr(expr).op();
148 return isinf(op, get_spec(op));
149 }
150 else if(expr.id()==ID_isnormal)
151 {
152 const auto &op = to_unary_expr(expr).op();
153 return isnormal(op, get_spec(op));
154 }
155 else if(expr.id()==ID_lt)
156 {
157 const auto &rel_expr = to_binary_relation_expr(expr);
158 return relation(
159 rel_expr.lhs(), relt::LT, rel_expr.rhs(), get_spec(rel_expr.lhs()));
160 }
161 else if(expr.id()==ID_gt)
162 {
163 const auto &rel_expr = to_binary_relation_expr(expr);
164 return relation(
165 rel_expr.lhs(), relt::GT, rel_expr.rhs(), get_spec(rel_expr.lhs()));
166 }
167 else if(expr.id()==ID_le)
168 {
169 const auto &rel_expr = to_binary_relation_expr(expr);
170 return relation(
171 rel_expr.lhs(), relt::LE, rel_expr.rhs(), get_spec(rel_expr.lhs()));
172 }
173 else if(expr.id()==ID_ge)
174 {
175 const auto &rel_expr = to_binary_relation_expr(expr);
176 return relation(
177 rel_expr.lhs(), relt::GE, rel_expr.rhs(), get_spec(rel_expr.lhs()));
178 }
179 else if(expr.id()==ID_sign)
180 return sign_bit(to_unary_expr(expr).op());
181
182 return nil_exprt();
183}
184
186{
187 const floatbv_typet &type=to_floatbv_type(expr.type());
188 return ieee_float_spect(type);
189}
190
192{
193 // we mask away the sign bit, which is the most significant bit
194 const mp_integer v = power(2, spec.width() - 1) - 1;
195
196 const constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
197
198 return bitand_exprt(op, mask);
199}
200
202{
203 // we flip the sign bit with an xor
204 const mp_integer v = power(2, spec.width() - 1);
205
206 constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
207
208 return bitxor_exprt(op, mask);
209}
210
212 const exprt &src0,
213 const exprt &src1,
214 const ieee_float_spect &spec)
215{
216 // special cases: -0 and 0 are equal
217 const exprt is_zero0 = is_zero(src0);
218 const exprt is_zero1 = is_zero(src1);
219 const and_exprt both_zero(is_zero0, is_zero1);
220
221 // NaN compares to nothing
222 exprt isnan0=isnan(src0, spec);
223 exprt isnan1=isnan(src1, spec);
224 const or_exprt nan(isnan0, isnan1);
225
226 const equal_exprt bitwise_equal(src0, src1);
227
228 return and_exprt(
229 or_exprt(bitwise_equal, both_zero),
230 not_exprt(nan));
231}
232
234{
235 // we mask away the sign bit, which is the most significant bit
236 const floatbv_typet &type=to_floatbv_type(src.type());
237 std::size_t width=type.get_width();
238
239 const mp_integer v = power(2, width - 1) - 1;
240
241 constant_exprt mask(integer2bvrep(v, width), src.type());
242
243 ieee_floatt z(type);
244 z.make_zero();
245
246 return equal_exprt(bitand_exprt(src, mask), z.to_expr());
247}
248
250 const exprt &src,
251 const ieee_float_spect &spec)
252{
253 exprt exponent=get_exponent(src, spec);
254 exprt all_ones=to_unsignedbv_type(exponent.type()).largest_expr();
255 return equal_exprt(exponent, all_ones);
256}
257
259 const exprt &src,
260 const ieee_float_spect &spec)
261{
262 exprt exponent=get_exponent(src, spec);
263 exprt all_zeros=to_unsignedbv_type(exponent.type()).zero_expr();
264 return equal_exprt(exponent, all_zeros);
265}
266
268 const exprt &src,
269 const ieee_float_spect &spec)
270{
271 // does not include hidden bit
272 exprt fraction=get_fraction(src, spec);
273 exprt all_zeros=to_unsignedbv_type(fraction.type()).zero_expr();
274 return equal_exprt(fraction, all_zeros);
275}
276
278{
279 exprt round_to_even_const=from_integer(ieee_floatt::ROUND_TO_EVEN, rm.type());
280 exprt round_to_plus_inf_const=
282 exprt round_to_minus_inf_const=
284 exprt round_to_zero_const=from_integer(ieee_floatt::ROUND_TO_ZERO, rm.type());
285
286 round_to_even=equal_exprt(rm, round_to_even_const);
287 round_to_plus_inf=equal_exprt(rm, round_to_plus_inf_const);
288 round_to_minus_inf=equal_exprt(rm, round_to_minus_inf_const);
289 round_to_zero=equal_exprt(rm, round_to_zero_const);
290}
291
293{
294 const bitvector_typet &bv_type=to_bitvector_type(op.type());
295 std::size_t width=bv_type.get_width();
296 return extractbit_exprt(op, width-1);
297}
298
300 const exprt &src,
301 const exprt &rm,
302 const ieee_float_spect &spec) const
303{
304 std::size_t src_width=to_signedbv_type(src.type()).get_width();
305
306 unbiased_floatt result;
307
308 // we need to adjust for negative integers
309 result.sign=sign_bit(src);
310
311 result.fraction=
312 typecast_exprt(abs_exprt(src), unsignedbv_typet(src_width));
313
314 // build an exponent (unbiased) -- this is signed!
315 result.exponent=
317 src_width-1,
318 signedbv_typet(address_bits(src_width - 1) + 1));
319
320 return rounder(result, rm, spec);
321}
322
324 const exprt &src,
325 const exprt &rm,
326 const ieee_float_spect &spec) const
327{
328 unbiased_floatt result;
329
330 result.fraction=src;
331
332 std::size_t src_width=to_unsignedbv_type(src.type()).get_width();
333
334 // build an exponent (unbiased) -- this is signed!
335 result.exponent=
337 src_width-1,
338 signedbv_typet(address_bits(src_width - 1) + 1));
339
340 result.sign=false_exprt();
341
342 return rounder(result, rm, spec);
343}
344
346 const exprt &src,
347 std::size_t dest_width,
348 const exprt &rm,
349 const ieee_float_spect &spec)
350{
351 return to_integer(src, dest_width, true, rm, spec);
352}
353
355 const exprt &src,
356 std::size_t dest_width,
357 const exprt &rm,
358 const ieee_float_spect &spec)
359{
360 return to_integer(src, dest_width, false, rm, spec);
361}
362
364 const exprt &src,
365 std::size_t dest_width,
366 bool is_signed,
367 const exprt &rm,
368 const ieee_float_spect &spec)
369{
370 const unbiased_floatt unpacked=unpack(src, spec);
371
372 rounding_mode_bitst rounding_mode_bits(rm);
373
374 // Right now hard-wired to round-to-zero, which is
375 // the usual case in ANSI-C.
376
377 // if the exponent is positive, shift right
378 exprt offset=from_integer(spec.f, signedbv_typet(spec.e));
379 const minus_exprt distance(offset, unpacked.exponent);
380 const lshr_exprt shift_result(unpacked.fraction, distance);
381
382 // if the exponent is negative, we have zero anyways
383 exprt result=shift_result;
384 const sign_exprt exponent_sign(unpacked.exponent);
385
386 result=
387 if_exprt(exponent_sign, from_integer(0, result.type()), result);
388
389 // chop out the right number of bits from the result
390 typet result_type=
391 is_signed?static_cast<typet>(signedbv_typet(dest_width)):
392 static_cast<typet>(unsignedbv_typet(dest_width));
393
394 result=typecast_exprt(result, result_type);
395
396 // if signed, apply sign.
397 if(is_signed)
398 {
399 result=if_exprt(
400 unpacked.sign, unary_minus_exprt(result), result);
401 }
402 else
403 {
404 // It's unclear what the behaviour for negative floats
405 // to integer shall be.
406 }
407
408 return result;
409}
410
412 const exprt &src,
413 const exprt &rm,
414 const ieee_float_spect &src_spec,
415 const ieee_float_spect &dest_spec) const
416{
417 // Catch the special case in which we extend,
418 // e.g. single to double.
419 // In this case, rounding can be avoided,
420 // but a denormal number may be come normal.
421 // Be careful to exclude the difficult case
422 // when denormalised numbers in the old format
423 // can be converted to denormalised numbers in the
424 // new format. Note that this is rare and will only
425 // happen with very non-standard formats.
426
427 int sourceSmallestNormalExponent = -((1 << (src_spec.e - 1)) - 1);
428 int sourceSmallestDenormalExponent =
429 sourceSmallestNormalExponent - src_spec.f;
430
431 // Using the fact that f doesn't include the hidden bit
432
433 int destSmallestNormalExponent = -((1 << (dest_spec.e - 1)) - 1);
434
435 if(dest_spec.e>=src_spec.e &&
436 dest_spec.f>=src_spec.f &&
437 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
438 {
439 unbiased_floatt unpacked_src=unpack(src, src_spec);
440 unbiased_floatt result;
441
442 // the fraction gets zero-padded
443 std::size_t padding=dest_spec.f-src_spec.f;
444 result.fraction=
446 unpacked_src.fraction,
447 from_integer(0, unsignedbv_typet(padding)),
448 unsignedbv_typet(dest_spec.f+1));
449
450 // the exponent gets sign-extended
451 INVARIANT(
452 unpacked_src.exponent.type().id() == ID_signedbv,
453 "the exponent needs to have a signed type");
454 result.exponent=
455 typecast_exprt(unpacked_src.exponent, signedbv_typet(dest_spec.e));
456
457 // if the number was denormal and is normal in the new format,
458 // normalise it!
459 if(dest_spec.e > src_spec.e)
460 {
461 normalization_shift(result.fraction, result.exponent);
462 // normalization_shift unconditionally extends the exponent size to avoid
463 // arithmetic overflow, but this cannot have happened here as the exponent
464 // had already been extended to dest_spec's size
465 result.exponent =
466 typecast_exprt(result.exponent, signedbv_typet(dest_spec.e));
467 }
468
469 // the flags get copied
470 result.sign=unpacked_src.sign;
471 result.NaN=unpacked_src.NaN;
472 result.infinity=unpacked_src.infinity;
473
474 // no rounding needed!
475 return pack(bias(result, dest_spec), dest_spec);
476 }
477 else
478 {
479 // we actually need to round
480 unbiased_floatt result=unpack(src, src_spec);
481 return rounder(result, rm, dest_spec);
482 }
483}
484
486 const exprt &src,
487 const ieee_float_spect &spec)
488{
489 return and_exprt(
490 not_exprt(exponent_all_zeros(src, spec)),
491 not_exprt(exponent_all_ones(src, spec)));
492}
493
496 const unbiased_floatt &src1,
497 const unbiased_floatt &src2)
498{
499 // extend both by one bit
500 std::size_t old_width1=to_signedbv_type(src1.exponent.type()).get_width();
501 std::size_t old_width2=to_signedbv_type(src2.exponent.type()).get_width();
502 PRECONDITION(old_width1 == old_width2);
503
504 const typecast_exprt extended_exponent1(
505 src1.exponent, signedbv_typet(old_width1 + 1));
506
507 const typecast_exprt extended_exponent2(
508 src2.exponent, signedbv_typet(old_width2 + 1));
509
510 // compute shift distance (here is the subtraction)
511 return minus_exprt(extended_exponent1, extended_exponent2);
512}
513
515 bool subtract,
516 const exprt &op0,
517 const exprt &op1,
518 const exprt &rm,
519 const ieee_float_spect &spec) const
520{
521 unbiased_floatt unpacked1=unpack(op0, spec);
522 unbiased_floatt unpacked2=unpack(op1, spec);
523
524 // subtract?
525 if(subtract)
526 unpacked2.sign=not_exprt(unpacked2.sign);
527
528 // figure out which operand has the bigger exponent
529 const exprt exponent_difference=subtract_exponents(unpacked1, unpacked2);
530 const sign_exprt src2_bigger(exponent_difference);
531
532 const exprt bigger_exponent=
533 if_exprt(src2_bigger, unpacked2.exponent, unpacked1.exponent);
534
535 // swap fractions as needed
536 const exprt new_fraction1=
537 if_exprt(src2_bigger, unpacked2.fraction, unpacked1.fraction);
538
539 const exprt new_fraction2=
540 if_exprt(src2_bigger, unpacked1.fraction, unpacked2.fraction);
541
542 // compute distance
543 const exprt distance=
544 typecast_exprt(abs_exprt(exponent_difference), unsignedbv_typet(spec.e));
545
546 // limit the distance: shifting more than f+3 bits is unnecessary
547 const exprt limited_dist=limit_distance(distance, spec.f+3);
548
549 // pad fractions with 3 zeros from below
550 exprt three_zeros=from_integer(0, unsignedbv_typet(3));
551 // add 4 to spec.f because unpacked new_fraction has the hidden bit
552 const exprt fraction1_padded=
553 concatenation_exprt(new_fraction1, three_zeros, unsignedbv_typet(spec.f+4));
554 const exprt fraction2_padded=
555 concatenation_exprt(new_fraction2, three_zeros, unsignedbv_typet(spec.f+4));
556
557 // shift new_fraction2
558 exprt sticky_bit;
559 const exprt fraction1_shifted=fraction1_padded;
560 const exprt fraction2_shifted=sticky_right_shift(
561 fraction2_padded, limited_dist, sticky_bit);
562
563 // sticky bit: 'or' of the bits lost by the right-shift
564 const bitor_exprt fraction2_stickied(
565 fraction2_shifted,
567 from_integer(0, unsignedbv_typet(spec.f + 3)),
568 sticky_bit,
569 fraction2_shifted.type()));
570
571 // need to have two extra fraction bits for addition and rounding
572 const exprt fraction1_ext=
573 typecast_exprt(fraction1_shifted, unsignedbv_typet(spec.f+4+2));
574 const exprt fraction2_ext=
575 typecast_exprt(fraction2_stickied, unsignedbv_typet(spec.f+4+2));
576
577 unbiased_floatt result;
578
579 // now add/sub them
580 const notequal_exprt subtract_lit(unpacked1.sign, unpacked2.sign);
581
582 result.fraction=
583 if_exprt(subtract_lit,
584 minus_exprt(fraction1_ext, fraction2_ext),
585 plus_exprt(fraction1_ext, fraction2_ext));
586
587 // sign of result
588 std::size_t width=to_bitvector_type(result.fraction.type()).get_width();
589 const sign_exprt fraction_sign(
590 typecast_exprt(result.fraction, signedbv_typet(width)));
591 result.fraction=
594 unsignedbv_typet(width));
595
596 result.exponent=bigger_exponent;
597
598 // adjust the exponent for the fact that we added two bits to the fraction
599 result.exponent=
601 from_integer(2, signedbv_typet(spec.e+1)));
602
603 // NaN?
604 result.NaN=or_exprt(
605 and_exprt(and_exprt(unpacked1.infinity, unpacked2.infinity),
606 notequal_exprt(unpacked1.sign, unpacked2.sign)),
607 or_exprt(unpacked1.NaN, unpacked2.NaN));
608
609 // infinity?
610 result.infinity=and_exprt(
611 not_exprt(result.NaN),
612 or_exprt(unpacked1.infinity, unpacked2.infinity));
613
614 // zero?
615 // Note that:
616 // 1. The zero flag isn't used apart from in divide and
617 // is only set on unpack
618 // 2. Subnormals mean that addition or subtraction can't round to 0,
619 // thus we can perform this test now
620 // 3. The rules for sign are different for zero
621 result.zero=
622 and_exprt(
623 not_exprt(or_exprt(result.infinity, result.NaN)),
625 result.fraction,
626 from_integer(0, result.fraction.type())));
627
628 // sign
629 const notequal_exprt add_sub_sign(
630 if_exprt(src2_bigger, unpacked2.sign, unpacked1.sign), fraction_sign);
631
632 const if_exprt infinity_sign(
633 unpacked1.infinity, unpacked1.sign, unpacked2.sign);
634
635 #if 1
636 rounding_mode_bitst rounding_mode_bits(rm);
637
638 const if_exprt zero_sign(
639 rounding_mode_bits.round_to_minus_inf,
640 or_exprt(unpacked1.sign, unpacked2.sign),
641 and_exprt(unpacked1.sign, unpacked2.sign));
642
643 result.sign=if_exprt(
644 result.infinity,
645 infinity_sign,
646 if_exprt(result.zero,
647 zero_sign,
648 add_sub_sign));
649 #else
650 result.sign=if_exprt(
651 result.infinity,
652 infinity_sign,
653 add_sub_sign);
654 #endif
655
656 return rounder(result, rm, spec);
657}
658
661 const exprt &dist,
662 mp_integer limit)
663{
664 std::size_t nb_bits = address_bits(limit);
665 std::size_t dist_width=to_unsignedbv_type(dist.type()).get_width();
666
667 if(dist_width<=nb_bits)
668 return dist;
669
670 const extractbits_exprt upper_bits(
671 dist, nb_bits, unsignedbv_typet(dist_width - nb_bits));
672 const equal_exprt upper_bits_zero(
673 upper_bits, from_integer(0, upper_bits.type()));
674
675 const extractbits_exprt lower_bits(dist, 0, unsignedbv_typet(nb_bits));
676
677 return if_exprt(
678 upper_bits_zero,
679 lower_bits,
680 unsignedbv_typet(nb_bits).largest_expr());
681}
682
684 const exprt &src1,
685 const exprt &src2,
686 const exprt &rm,
687 const ieee_float_spect &spec) const
688{
689 // unpack
690 const unbiased_floatt unpacked1=unpack(src1, spec);
691 const unbiased_floatt unpacked2=unpack(src2, spec);
692
693 // zero-extend the fractions (unpacked fraction has the hidden bit)
694 typet new_fraction_type=unsignedbv_typet((spec.f+1)*2);
695 const exprt fraction1=typecast_exprt(unpacked1.fraction, new_fraction_type);
696 const exprt fraction2=typecast_exprt(unpacked2.fraction, new_fraction_type);
697
698 // multiply the fractions
699 unbiased_floatt result;
700 result.fraction=mult_exprt(fraction1, fraction2);
701
702 // extend exponents to account for overflow
703 // add two bits, as we do extra arithmetic on it later
704 typet new_exponent_type=signedbv_typet(spec.e+2);
705 const exprt exponent1=typecast_exprt(unpacked1.exponent, new_exponent_type);
706 const exprt exponent2=typecast_exprt(unpacked2.exponent, new_exponent_type);
707
708 const plus_exprt added_exponent(exponent1, exponent2);
709
710 // Adjust exponent; we are thowing in an extra fraction bit,
711 // it has been extended above.
712 result.exponent=
713 plus_exprt(added_exponent, from_integer(1, new_exponent_type));
714
715 // new sign
716 result.sign=notequal_exprt(unpacked1.sign, unpacked2.sign);
717
718 // infinity?
719 result.infinity=or_exprt(unpacked1.infinity, unpacked2.infinity);
720
721 // NaN?
722 result.NaN = disjunction(
723 {isnan(src1, spec),
724 isnan(src2, spec),
725 // infinity * 0 is NaN!
726 and_exprt(unpacked1.zero, unpacked2.infinity),
727 and_exprt(unpacked2.zero, unpacked1.infinity)});
728
729 return rounder(result, rm, spec);
730}
731
733 const exprt &src1,
734 const exprt &src2,
735 const exprt &rm,
736 const ieee_float_spect &spec) const
737{
738 // unpack
739 const unbiased_floatt unpacked1=unpack(src1, spec);
740 const unbiased_floatt unpacked2=unpack(src2, spec);
741
742 std::size_t fraction_width=
744 std::size_t div_width=fraction_width*2+1;
745
746 // pad fraction1 with zeros
747 const concatenation_exprt fraction1(
748 unpacked1.fraction,
749 from_integer(0, unsignedbv_typet(div_width - fraction_width)),
750 unsignedbv_typet(div_width));
751
752 // zero-extend fraction2 to match fraction1
753 const typecast_exprt fraction2(unpacked2.fraction, fraction1.type());
754
755 // divide fractions
756 unbiased_floatt result;
757 exprt rem;
758
759 // the below should be merged somehow
760 result.fraction=div_exprt(fraction1, fraction2);
761 rem=mod_exprt(fraction1, fraction2);
762
763 // is there a remainder?
764 const notequal_exprt have_remainder(rem, from_integer(0, rem.type()));
765
766 // we throw this into the result, as least-significant bit,
767 // to get the right rounding decision
768 result.fraction=
770 result.fraction, have_remainder, unsignedbv_typet(div_width+1));
771
772 // We will subtract the exponents;
773 // to account for overflow, we add a bit.
774 const typecast_exprt exponent1(
775 unpacked1.exponent, signedbv_typet(spec.e + 1));
776 const typecast_exprt exponent2(
777 unpacked2.exponent, signedbv_typet(spec.e + 1));
778
779 // subtract exponents
780 const minus_exprt added_exponent(exponent1, exponent2);
781
782 // adjust, as we have thown in extra fraction bits
783 result.exponent=plus_exprt(
784 added_exponent,
785 from_integer(spec.f, added_exponent.type()));
786
787 // new sign
788 result.sign=notequal_exprt(unpacked1.sign, unpacked2.sign);
789
790 // Infinity? This happens when
791 // 1) dividing a non-nan/non-zero by zero, or
792 // 2) first operand is inf and second is non-nan and non-zero
793 // In particular, inf/0=inf.
794 result.infinity=
795 or_exprt(
796 and_exprt(not_exprt(unpacked1.zero),
797 and_exprt(not_exprt(unpacked1.NaN),
798 unpacked2.zero)),
799 and_exprt(unpacked1.infinity,
800 and_exprt(not_exprt(unpacked2.NaN),
801 not_exprt(unpacked2.zero))));
802
803 // NaN?
804 result.NaN=or_exprt(unpacked1.NaN,
805 or_exprt(unpacked2.NaN,
806 or_exprt(and_exprt(unpacked1.zero, unpacked2.zero),
807 and_exprt(unpacked1.infinity, unpacked2.infinity))));
808
809 // Division by infinity produces zero, unless we have NaN
810 const and_exprt force_zero(not_exprt(unpacked1.NaN), unpacked2.infinity);
811
812 result.fraction=
813 if_exprt(
814 force_zero,
815 from_integer(0, result.fraction.type()),
816 result.fraction);
817
818 return rounder(result, rm, spec);
819}
820
822 const exprt &src1,
823 relt rel,
824 const exprt &src2,
825 const ieee_float_spect &spec)
826{
827 if(rel==relt::GT)
828 return relation(src2, relt::LT, src1, spec); // swapped
829 else if(rel==relt::GE)
830 return relation(src2, relt::LE, src1, spec); // swapped
831
832 INVARIANT(
833 rel == relt::EQ || rel == relt::LT || rel == relt::LE,
834 "relation should be equality, less-than, or less-or-equal");
835
836 // special cases: -0 and 0 are equal
837 const exprt is_zero1 = is_zero(src1);
838 const exprt is_zero2 = is_zero(src2);
839 const and_exprt both_zero(is_zero1, is_zero2);
840
841 // NaN compares to nothing
842 exprt isnan1=isnan(src1, spec);
843 exprt isnan2=isnan(src2, spec);
844 const or_exprt nan(isnan1, isnan2);
845
846 if(rel==relt::LT || rel==relt::LE)
847 {
848 const equal_exprt bitwise_equal(src1, src2);
849
850 // signs different? trivial! Unless Zero.
851
852 const notequal_exprt signs_different(sign_bit(src1), sign_bit(src2));
853
854 // as long as the signs match: compare like unsigned numbers
855
856 // this works due to the BIAS
857 const binary_relation_exprt less_than1(
859 typecast_exprt(src1, bv_typet(spec.width())),
860 unsignedbv_typet(spec.width())),
861 ID_lt,
863 typecast_exprt(src2, bv_typet(spec.width())),
864 unsignedbv_typet(spec.width())));
865
866 // if both are negative (and not the same), need to turn around!
867 const notequal_exprt less_than2(
868 less_than1, and_exprt(sign_bit(src1), sign_bit(src2)));
869
870 const if_exprt less_than3(signs_different, sign_bit(src1), less_than2);
871
872 if(rel==relt::LT)
873 {
874 and_exprt and_bv{{less_than3,
875 // for the case of two negative numbers
876 not_exprt(bitwise_equal),
877 not_exprt(both_zero),
878 not_exprt(nan)}};
879
880 return std::move(and_bv);
881 }
882 else if(rel==relt::LE)
883 {
884 or_exprt or_bv{{less_than3, both_zero, bitwise_equal}};
885
886 return and_exprt(or_bv, not_exprt(nan));
887 }
888 else
890 }
891 else if(rel==relt::EQ)
892 {
893 const equal_exprt bitwise_equal(src1, src2);
894
895 return and_exprt(
896 or_exprt(bitwise_equal, both_zero),
897 not_exprt(nan));
898 }
899
901 return false_exprt();
902}
903
905 const exprt &src,
906 const ieee_float_spect &spec)
907{
908 return and_exprt(
909 exponent_all_ones(src, spec),
910 fraction_all_zeros(src, spec));
911}
912
914 const exprt &src,
915 const ieee_float_spect &spec)
916{
917 return not_exprt(or_exprt(isinf(src, spec), isnan(src, spec)));
918}
919
922 const exprt &src,
923 const ieee_float_spect &spec)
924{
925 return extractbits_exprt(src, spec.f, unsignedbv_typet(spec.e));
926}
927
930 const exprt &src,
931 const ieee_float_spect &spec)
932{
933 return extractbits_exprt(src, 0, unsignedbv_typet(spec.f));
934}
935
937 const exprt &src,
938 const ieee_float_spect &spec)
939{
940 return and_exprt(exponent_all_ones(src, spec),
941 not_exprt(fraction_all_zeros(src, spec)));
942}
943
946 exprt &fraction,
947 exprt &exponent)
948{
949 // n-log-n alignment shifter.
950 // The worst-case shift is the number of fraction
951 // bits minus one, in case the fraction is one exactly.
952 std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
953 std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
954 PRECONDITION(fraction_bits != 0);
955
956 std::size_t depth = address_bits(fraction_bits - 1);
957
958 exponent = typecast_exprt(
959 exponent, signedbv_typet(std::max(depth, exponent_bits + 1)));
960
961 exprt exponent_delta=from_integer(0, exponent.type());
962
963 for(int d=depth-1; d>=0; d--)
964 {
965 unsigned distance=(1<<d);
966 INVARIANT(
967 fraction_bits > distance,
968 "distance must be within the range of fraction bits");
969
970 // check if first 'distance'-many bits are zeros
971 const extractbits_exprt prefix(
972 fraction, fraction_bits - distance, unsignedbv_typet(distance));
973 const equal_exprt prefix_is_zero(prefix, from_integer(0, prefix.type()));
974
975 // If so, shift the zeros out left by 'distance'.
976 // Otherwise, leave as is.
977 const shl_exprt shifted(fraction, distance);
978
979 fraction=
980 if_exprt(prefix_is_zero, shifted, fraction);
981
982 // add corresponding weight to exponent
983 INVARIANT(
984 d < (signed int)exponent_bits,
985 "depth must be smaller than exponent bits");
986
987 exponent_delta=
988 bitor_exprt(exponent_delta,
989 shl_exprt(typecast_exprt(prefix_is_zero, exponent_delta.type()), d));
990 }
991
992 exponent=minus_exprt(exponent, exponent_delta);
993}
994
997 exprt &fraction,
998 exprt &exponent,
999 const ieee_float_spect &spec)
1000{
1001 mp_integer bias=spec.bias();
1002
1003 // Is the exponent strictly less than -bias+1, i.e., exponent<-bias+1?
1004 // This is transformed to distance=(-bias+1)-exponent
1005 // i.e., distance>0
1006 // Note that 1-bias is the exponent represented by 0...01,
1007 // i.e. the exponent of the smallest normal number and thus the 'base'
1008 // exponent for subnormal numbers.
1009
1010 std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
1011 PRECONDITION(exponent_bits >= spec.e);
1012
1013#if 1
1014 // Need to sign extend to avoid overflow. Note that this is a
1015 // relatively rare problem as the value needs to be close to the top
1016 // of the exponent range and then range must not have been
1017 // previously extended as add, multiply, etc. do. This is primarily
1018 // to handle casting down from larger ranges.
1019 exponent=typecast_exprt(exponent, signedbv_typet(exponent_bits+1));
1020#endif
1021
1022 const minus_exprt distance(
1023 from_integer(-bias + 1, exponent.type()), exponent);
1024
1025 // use sign bit
1026 const and_exprt denormal(
1027 not_exprt(sign_exprt(distance)),
1028 notequal_exprt(distance, from_integer(0, distance.type())));
1029
1030#if 1
1031 // Care must be taken to not loose information required for the
1032 // guard and sticky bits. +3 is for the hidden, guard and sticky bits.
1033 std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
1034
1035 if(fraction_bits < spec.f+3)
1036 {
1037 // Add zeros at the LSB end for the guard bit to shift into
1038 fraction=
1040 fraction, unsignedbv_typet(spec.f + 3 - fraction_bits).zero_expr(),
1041 unsignedbv_typet(spec.f+3));
1042 }
1043
1044 exprt denormalisedFraction = fraction;
1045
1046 exprt sticky_bit = false_exprt();
1047 denormalisedFraction =
1048 sticky_right_shift(fraction, distance, sticky_bit);
1049
1050 denormalisedFraction=
1051 bitor_exprt(denormalisedFraction,
1052 typecast_exprt(sticky_bit, denormalisedFraction.type()));
1053
1054 fraction=
1055 if_exprt(
1056 denormal,
1057 denormalisedFraction,
1058 fraction);
1059
1060#else
1061 fraction=
1062 if_exprt(
1063 denormal,
1064 lshr_exprt(fraction, distance),
1065 fraction);
1066#endif
1067
1068 exponent=
1069 if_exprt(denormal,
1070 from_integer(-bias, exponent.type()),
1071 exponent);
1072}
1073
1075 const unbiased_floatt &src,
1076 const exprt &rm,
1077 const ieee_float_spect &spec) const
1078{
1079 // incoming: some fraction (with explicit 1),
1080 // some exponent without bias
1081 // outgoing: rounded, with right size, with hidden bit, bias
1082
1083 exprt aligned_fraction=src.fraction,
1084 aligned_exponent=src.exponent;
1085
1086 {
1087 std::size_t exponent_bits = std::max(address_bits(spec.f), spec.e) + 1;
1088
1089 // before normalization, make sure exponent is large enough
1090 if(to_signedbv_type(aligned_exponent.type()).get_width()<exponent_bits)
1091 {
1092 // sign extend
1093 aligned_exponent=
1094 typecast_exprt(aligned_exponent, signedbv_typet(exponent_bits));
1095 }
1096 }
1097
1098 // align it!
1099 normalization_shift(aligned_fraction, aligned_exponent);
1100 denormalization_shift(aligned_fraction, aligned_exponent, spec);
1101
1102 unbiased_floatt result;
1103 result.fraction=aligned_fraction;
1104 result.exponent=aligned_exponent;
1105 result.sign=src.sign;
1106 result.NaN=src.NaN;
1107 result.infinity=src.infinity;
1108
1109 rounding_mode_bitst rounding_mode_bits(rm);
1110 round_fraction(result, rounding_mode_bits, spec);
1111 round_exponent(result, rounding_mode_bits, spec);
1112
1113 return pack(bias(result, spec), spec);
1114}
1115
1118 const std::size_t dest_bits,
1119 const exprt sign,
1120 const exprt &fraction,
1121 const rounding_mode_bitst &rounding_mode_bits)
1122{
1123 std::size_t fraction_bits=
1124 to_unsignedbv_type(fraction.type()).get_width();
1125
1126 PRECONDITION(dest_bits < fraction_bits);
1127
1128 // we have too many fraction bits
1129 std::size_t extra_bits=fraction_bits-dest_bits;
1130
1131 // more than two extra bits are superflus, and are
1132 // turned into a sticky bit
1133
1134 exprt sticky_bit=false_exprt();
1135
1136 if(extra_bits>=2)
1137 {
1138 // We keep most-significant bits, and thus the tail is made
1139 // of least-significant bits.
1140 const extractbits_exprt tail(
1141 fraction, 0, unsignedbv_typet(extra_bits - 2 + 1));
1142 sticky_bit=notequal_exprt(tail, from_integer(0, tail.type()));
1143 }
1144
1145 // the rounding bit is the last extra bit
1146 INVARIANT(
1147 extra_bits >= 1, "the extra bits contain at least the rounding bit");
1148 const extractbit_exprt rounding_bit(fraction, extra_bits - 1);
1149
1150 // we get one bit of the fraction for some rounding decisions
1151 const extractbit_exprt rounding_least(fraction, extra_bits);
1152
1153 // round-to-nearest (ties to even)
1154 const and_exprt round_to_even(
1155 rounding_bit, or_exprt(rounding_least, sticky_bit));
1156
1157 // round up
1158 const and_exprt round_to_plus_inf(
1159 not_exprt(sign), or_exprt(rounding_bit, sticky_bit));
1160
1161 // round down
1162 const and_exprt round_to_minus_inf(sign, or_exprt(rounding_bit, sticky_bit));
1163
1164 // round to zero
1165 false_exprt round_to_zero;
1166
1167 // now select appropriate one
1168 return if_exprt(rounding_mode_bits.round_to_even, round_to_even,
1169 if_exprt(rounding_mode_bits.round_to_plus_inf, round_to_plus_inf,
1170 if_exprt(rounding_mode_bits.round_to_minus_inf, round_to_minus_inf,
1171 if_exprt(rounding_mode_bits.round_to_zero, round_to_zero,
1172 false_exprt())))); // otherwise zero
1173}
1174
1176 unbiased_floatt &result,
1177 const rounding_mode_bitst &rounding_mode_bits,
1178 const ieee_float_spect &spec)
1179{
1180 std::size_t fraction_size=spec.f+1;
1181 std::size_t result_fraction_size=
1183
1184 // do we need to enlarge the fraction?
1185 if(result_fraction_size<fraction_size)
1186 {
1187 // pad with zeros at bottom
1188 std::size_t padding=fraction_size-result_fraction_size;
1189
1191 result.fraction,
1192 unsignedbv_typet(padding).zero_expr(),
1193 unsignedbv_typet(fraction_size));
1194 }
1195 else if(result_fraction_size==fraction_size) // it stays
1196 {
1197 // do nothing
1198 }
1199 else // fraction gets smaller -- rounding
1200 {
1201 std::size_t extra_bits=result_fraction_size-fraction_size;
1202 INVARIANT(
1203 extra_bits >= 1, "the extra bits include at least the rounding bit");
1204
1205 // this computes the rounding decision
1207 fraction_size, result.sign, result.fraction, rounding_mode_bits);
1208
1209 // chop off all the extra bits
1210 result.fraction = extractbits_exprt(
1211 result.fraction, extra_bits, unsignedbv_typet(fraction_size));
1212
1213#if 0
1214 // *** does not catch when the overflow goes subnormal -> normal ***
1215 // incrementing the fraction might result in an overflow
1216 result.fraction=
1217 bv_utils.zero_extension(result.fraction, result.fraction.size()+1);
1218
1219 result.fraction=bv_utils.incrementer(result.fraction, increment);
1220
1221 exprt overflow=result.fraction.back();
1222
1223 // In case of an overflow, the exponent has to be incremented.
1224 // "Post normalization" is then required.
1225 result.exponent=
1226 bv_utils.incrementer(result.exponent, overflow);
1227
1228 // post normalization of the fraction
1229 exprt integer_part1=result.fraction.back();
1230 exprt integer_part0=result.fraction[result.fraction.size()-2];
1231 const or_exprt new_integer_part(integer_part1, integer_part0);
1232
1233 result.fraction.resize(result.fraction.size()-1);
1234 result.fraction.back()=new_integer_part;
1235
1236#else
1237 // When incrementing due to rounding there are two edge
1238 // cases we need to be aware of:
1239 // 1. If the number is normal, the increment can overflow.
1240 // In this case we need to increment the exponent and
1241 // set the MSB of the fraction to 1.
1242 // 2. If the number is the largest subnormal, the increment
1243 // can change the MSB making it normal. Thus the exponent
1244 // must be incremented but the fraction will be OK.
1245 const extractbit_exprt old_msb(result.fraction, fraction_size - 1);
1246
1247 // increment if 'increment' is true
1248 result.fraction=
1249 plus_exprt(result.fraction,
1250 typecast_exprt(increment, result.fraction.type()));
1251
1252 // Normal overflow when old MSB == 1 and new MSB == 0
1253 const extractbit_exprt new_msb(result.fraction, fraction_size - 1);
1254 const and_exprt overflow(old_msb, not_exprt(new_msb));
1255
1256 // Subnormal to normal transition when old MSB == 0 and new MSB == 1
1257 const and_exprt subnormal_to_normal(not_exprt(old_msb), new_msb);
1258
1259 // In case of an overflow or subnormal to normal conversion,
1260 // the exponent has to be incremented.
1261 result.exponent=
1262 plus_exprt(
1263 result.exponent,
1264 if_exprt(
1265 or_exprt(overflow, subnormal_to_normal),
1266 from_integer(1, result.exponent.type()),
1267 from_integer(0, result.exponent.type())));
1268
1269 // post normalization of the fraction
1270 // In the case of overflow, set the MSB to 1
1271 // The subnormal case will have (only) the MSB set to 1
1272 result.fraction=bitor_exprt(
1273 result.fraction,
1274 if_exprt(overflow,
1275 from_integer(1<<(fraction_size-1), result.fraction.type()),
1276 from_integer(0, result.fraction.type())));
1277#endif
1278 }
1279}
1280
1282 unbiased_floatt &result,
1283 const rounding_mode_bitst &rounding_mode_bits,
1284 const ieee_float_spect &spec)
1285{
1286 std::size_t result_exponent_size=
1288
1289 PRECONDITION(result_exponent_size >= spec.e);
1290
1291 // do we need to enlarge the exponent?
1292 if(result_exponent_size == spec.e) // it stays
1293 {
1294 // do nothing
1295 }
1296 else // exponent gets smaller -- chop off top bits
1297 {
1298 exprt old_exponent=result.exponent;
1299 result.exponent =
1300 extractbits_exprt(result.exponent, 0, signedbv_typet(spec.e));
1301
1302 // max_exponent is the maximum representable
1303 // i.e. 1 higher than the maximum possible for a normal number
1304 exprt max_exponent=
1306 spec.max_exponent()-spec.bias(), old_exponent.type());
1307
1308 // the exponent is garbage if the fractional is zero
1309
1310 const and_exprt exponent_too_large(
1311 binary_relation_exprt(old_exponent, ID_ge, max_exponent),
1312 notequal_exprt(result.fraction, from_integer(0, result.fraction.type())));
1313
1314#if 1
1315 // Directed rounding modes round overflow to the maximum normal
1316 // depending on the particular mode and the sign
1317 const or_exprt overflow_to_inf(
1318 rounding_mode_bits.round_to_even,
1319 or_exprt(
1320 and_exprt(rounding_mode_bits.round_to_plus_inf, not_exprt(result.sign)),
1321 and_exprt(rounding_mode_bits.round_to_minus_inf, result.sign)));
1322
1323 const and_exprt set_to_max(exponent_too_large, not_exprt(overflow_to_inf));
1324
1325 exprt largest_normal_exponent=
1327 spec.max_exponent()-(spec.bias() + 1), result.exponent.type());
1328
1329 result.exponent=
1330 if_exprt(set_to_max, largest_normal_exponent, result.exponent);
1331
1332 result.fraction=
1333 if_exprt(set_to_max,
1335 result.fraction);
1336
1337 result.infinity=or_exprt(result.infinity,
1338 and_exprt(exponent_too_large,
1339 overflow_to_inf));
1340#else
1341 result.infinity=or_exprt(result.infinity, exponent_too_large);
1342#endif
1343 }
1344}
1345
1348 const unbiased_floatt &src,
1349 const ieee_float_spect &spec)
1350{
1351 biased_floatt result;
1352
1353 result.sign=src.sign;
1354 result.NaN=src.NaN;
1355 result.infinity=src.infinity;
1356
1357 // we need to bias the new exponent
1358 result.exponent=add_bias(src.exponent, spec);
1359
1360 // strip off the hidden bit
1362 to_unsignedbv_type(src.fraction.type()).get_width() == spec.f + 1);
1363
1364 const extractbit_exprt hidden_bit(src.fraction, spec.f);
1365 const not_exprt denormal(hidden_bit);
1366
1367 result.fraction =
1369
1370 // make exponent zero if its denormal
1371 // (includes zero)
1372 result.exponent=
1373 if_exprt(denormal, from_integer(0, result.exponent.type()),
1374 result.exponent);
1375
1376 return result;
1377}
1378
1380 const exprt &src,
1381 const ieee_float_spect &spec)
1382{
1383 typet t=unsignedbv_typet(spec.e);
1384 return plus_exprt(
1385 typecast_exprt(src, t),
1386 from_integer(spec.bias(), t));
1387}
1388
1390 const exprt &src,
1391 const ieee_float_spect &spec)
1392{
1393 typet t=signedbv_typet(spec.e);
1394 return minus_exprt(
1395 typecast_exprt(src, t),
1396 from_integer(spec.bias(), t));
1397}
1398
1400 const exprt &src,
1401 const ieee_float_spect &spec)
1402{
1403 unbiased_floatt result;
1404
1405 result.sign=sign_bit(src);
1406
1407 result.fraction=get_fraction(src, spec);
1408
1409 // add hidden bit
1410 exprt hidden_bit=isnormal(src, spec);
1411 result.fraction=
1412 concatenation_exprt(hidden_bit, result.fraction,
1413 unsignedbv_typet(spec.f+1));
1414
1415 result.exponent=get_exponent(src, spec);
1416
1417 // unbias the exponent
1418 exprt denormal=exponent_all_zeros(src, spec);
1419
1420 result.exponent=
1421 if_exprt(denormal,
1422 from_integer(-spec.bias()+1, signedbv_typet(spec.e)),
1423 sub_bias(result.exponent, spec));
1424
1425 result.infinity=isinf(src, spec);
1426 result.zero = is_zero(src);
1427 result.NaN=isnan(src, spec);
1428
1429 return result;
1430}
1431
1433 const biased_floatt &src,
1434 const ieee_float_spect &spec)
1435{
1438
1439 // do sign -- we make this 'false' for NaN
1440 const if_exprt sign_bit(src.NaN, false_exprt(), src.sign);
1441
1442 // the fraction is zero in case of infinity,
1443 // and one in case of NaN
1444 const if_exprt fraction(
1445 src.NaN,
1446 from_integer(1, src.fraction.type()),
1447 if_exprt(src.infinity, from_integer(0, src.fraction.type()), src.fraction));
1448
1449 const or_exprt infinity_or_NaN(src.NaN, src.infinity);
1450
1451 // do exponent
1452 const if_exprt exponent(
1453 infinity_or_NaN, from_integer(-1, src.exponent.type()), src.exponent);
1454
1455 // stitch all three together
1456 return typecast_exprt(
1458 {std::move(sign_bit), std::move(exponent), std::move(fraction)},
1459 bv_typet(spec.f + spec.e + 1)),
1460 spec.to_type());
1461}
1462
1464 const exprt &op,
1465 const exprt &dist,
1466 exprt &sticky)
1467{
1468 std::size_t d=1, width=to_unsignedbv_type(op.type()).get_width();
1469 exprt result=op;
1470 sticky=false_exprt();
1471
1472 std::size_t dist_width=to_bitvector_type(dist.type()).get_width();
1473
1474 for(std::size_t stage=0; stage<dist_width; stage++)
1475 {
1476 const lshr_exprt tmp(result, d);
1477
1478 exprt lost_bits;
1479
1480 if(d<=width)
1481 lost_bits = extractbits_exprt(result, 0, unsignedbv_typet(d));
1482 else
1483 lost_bits=result;
1484
1485 const extractbit_exprt dist_bit(dist, stage);
1486
1487 sticky=
1488 or_exprt(
1489 and_exprt(
1490 dist_bit,
1491 notequal_exprt(lost_bits, from_integer(0, lost_bits.type()))),
1492 sticky);
1493
1494 result=if_exprt(dist_bit, tmp, result);
1495
1496 d=d<<1;
1497 }
1498
1499 return result;
1500}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
API to expression classes for bitvectors.
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Absolute value.
Definition std_expr.h:442
Boolean AND.
Definition std_expr.h:2120
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Bit-wise AND.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition std_types.h:909
std::size_t get_width() const
Definition std_types.h:920
Bit-wise XOR.
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:2987
Division.
Definition std_expr.h:1152
Equality.
Definition std_expr.h:1361
Base class for all expressions.
Definition expr.h:56
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
typet & type()
Return the type of the expression.
Definition expr.h:84
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition std_expr.h:3064
static unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
static void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
Definition float_bv.cpp:945
static exprt get_fraction(const exprt &, const ieee_float_spect &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition float_bv.cpp:929
static exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
static exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:249
static exprt to_integer(const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:363
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:323
static exprt isfinite(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:913
static exprt isnormal(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:485
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:299
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:514
static exprt is_zero(const exprt &)
Definition float_bv.cpp:233
static exprt abs(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:191
static void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
static exprt fraction_rounding_decision(const std::size_t dest_bits, const exprt sign, const exprt &fraction, const rounding_mode_bitst &)
rounding decision for fraction using sticky bit
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec) const
Definition float_bv.cpp:411
static exprt isnan(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:936
static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
static exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
Definition float_bv.cpp:921
static void denormalization_shift(exprt &fraction, exprt &exponent, const ieee_float_spect &)
make sure exponent is not too small; the exponent is unbiased
Definition float_bv.cpp:996
static exprt add_bias(const exprt &exponent, const ieee_float_spect &)
static exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const
static exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
Definition float_bv.cpp:495
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:732
exprt convert(const exprt &) const
Definition float_bv.cpp:19
static ieee_float_spect get_spec(const exprt &)
Definition float_bv.cpp:185
static exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:354
static exprt negation(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:201
static exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:821
static exprt isinf(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:904
static exprt sign_bit(const exprt &)
Definition float_bv.cpp:292
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:683
static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:267
static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:258
static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:211
static exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:345
static exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition float_bv.cpp:660
static exprt pack(const biased_floatt &, const ieee_float_spect &)
static void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Fixed-width bit-vector with IEEE floating-point interpretation.
class floatbv_typet to_type() const
mp_integer bias() const
mp_integer max_exponent() const
std::size_t f
Definition ieee_float.h:26
std::size_t width() const
Definition ieee_float.h:50
std::size_t e
Definition ieee_float.h:26
constant_exprt to_expr() const
void make_zero()
Definition ieee_float.h:186
The trinary if-then-else operator.
Definition std_expr.h:2370
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
const irep_idt & id() const
Definition irep.h:388
Logical right shift.
Binary minus.
Definition std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1223
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
The NIL expression.
Definition std_expr.h:3073
Boolean negation.
Definition std_expr.h:2327
Disequality.
Definition std_expr.h:1420
Boolean OR.
Definition std_expr.h:2228
The plus expression Associativity is not specified.
Definition std_expr.h:1002
Left shift.
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:596
Fixed-width bit-vector with two's complement interpretation.
Semantic type conversion.
Definition std_expr.h:2068
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
The unary minus expression.
Definition std_expr.h:484
Fixed-width bit-vector with unsigned binary interpretation.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
BigInt mp_integer
Definition smt_terms.h:17
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:54
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2102
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition std_expr.h:466
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:514
void get(const exprt &rm)
Definition float_bv.cpp:277
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45