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 =
696 zero_extend_exprt{unpacked1.fraction, new_fraction_type};
697 const exprt fraction2 =
698 zero_extend_exprt{unpacked2.fraction, new_fraction_type};
699
700 // multiply the fractions
701 unbiased_floatt result;
702 result.fraction=mult_exprt(fraction1, fraction2);
703
704 // extend exponents to account for overflow
705 // add two bits, as we do extra arithmetic on it later
706 typet new_exponent_type=signedbv_typet(spec.e+2);
707 const exprt exponent1=typecast_exprt(unpacked1.exponent, new_exponent_type);
708 const exprt exponent2=typecast_exprt(unpacked2.exponent, new_exponent_type);
709
710 const plus_exprt added_exponent(exponent1, exponent2);
711
712 // Adjust exponent; we are thowing in an extra fraction bit,
713 // it has been extended above.
714 result.exponent=
715 plus_exprt(added_exponent, from_integer(1, new_exponent_type));
716
717 // new sign
718 result.sign=notequal_exprt(unpacked1.sign, unpacked2.sign);
719
720 // infinity?
721 result.infinity=or_exprt(unpacked1.infinity, unpacked2.infinity);
722
723 // NaN?
724 result.NaN = disjunction(
725 {isnan(src1, spec),
726 isnan(src2, spec),
727 // infinity * 0 is NaN!
728 and_exprt(unpacked1.zero, unpacked2.infinity),
729 and_exprt(unpacked2.zero, unpacked1.infinity)});
730
731 return rounder(result, rm, spec);
732}
733
735 const exprt &src1,
736 const exprt &src2,
737 const exprt &rm,
738 const ieee_float_spect &spec) const
739{
740 // unpack
741 const unbiased_floatt unpacked1=unpack(src1, spec);
742 const unbiased_floatt unpacked2=unpack(src2, spec);
743
744 std::size_t fraction_width=
746 std::size_t div_width=fraction_width*2+1;
747
748 // pad fraction1 with zeros
749 const concatenation_exprt fraction1(
750 unpacked1.fraction,
751 from_integer(0, unsignedbv_typet(div_width - fraction_width)),
752 unsignedbv_typet(div_width));
753
754 // zero-extend fraction2 to match fraction1
755 const zero_extend_exprt fraction2{unpacked2.fraction, fraction1.type()};
756
757 // divide fractions
758 unbiased_floatt result;
759 exprt rem;
760
761 // the below should be merged somehow
762 result.fraction=div_exprt(fraction1, fraction2);
763 rem=mod_exprt(fraction1, fraction2);
764
765 // is there a remainder?
766 const notequal_exprt have_remainder(rem, from_integer(0, rem.type()));
767
768 // we throw this into the result, as least-significant bit,
769 // to get the right rounding decision
770 result.fraction=
772 result.fraction, have_remainder, unsignedbv_typet(div_width+1));
773
774 // We will subtract the exponents;
775 // to account for overflow, we add a bit.
776 const typecast_exprt exponent1(
777 unpacked1.exponent, signedbv_typet(spec.e + 1));
778 const typecast_exprt exponent2(
779 unpacked2.exponent, signedbv_typet(spec.e + 1));
780
781 // subtract exponents
782 const minus_exprt added_exponent(exponent1, exponent2);
783
784 // adjust, as we have thown in extra fraction bits
785 result.exponent=plus_exprt(
786 added_exponent,
787 from_integer(spec.f, added_exponent.type()));
788
789 // new sign
790 result.sign=notequal_exprt(unpacked1.sign, unpacked2.sign);
791
792 // Infinity? This happens when
793 // 1) dividing a non-nan/non-zero by zero, or
794 // 2) first operand is inf and second is non-nan and non-zero
795 // In particular, inf/0=inf.
796 result.infinity=
797 or_exprt(
798 and_exprt(not_exprt(unpacked1.zero),
799 and_exprt(not_exprt(unpacked1.NaN),
800 unpacked2.zero)),
801 and_exprt(unpacked1.infinity,
802 and_exprt(not_exprt(unpacked2.NaN),
803 not_exprt(unpacked2.zero))));
804
805 // NaN?
806 result.NaN=or_exprt(unpacked1.NaN,
807 or_exprt(unpacked2.NaN,
808 or_exprt(and_exprt(unpacked1.zero, unpacked2.zero),
809 and_exprt(unpacked1.infinity, unpacked2.infinity))));
810
811 // Division by infinity produces zero, unless we have NaN
812 const and_exprt force_zero(not_exprt(unpacked1.NaN), unpacked2.infinity);
813
814 result.fraction=
815 if_exprt(
816 force_zero,
817 from_integer(0, result.fraction.type()),
818 result.fraction);
819
820 return rounder(result, rm, spec);
821}
822
824 const exprt &src1,
825 relt rel,
826 const exprt &src2,
827 const ieee_float_spect &spec)
828{
829 if(rel==relt::GT)
830 return relation(src2, relt::LT, src1, spec); // swapped
831 else if(rel==relt::GE)
832 return relation(src2, relt::LE, src1, spec); // swapped
833
834 INVARIANT(
835 rel == relt::EQ || rel == relt::LT || rel == relt::LE,
836 "relation should be equality, less-than, or less-or-equal");
837
838 // special cases: -0 and 0 are equal
839 const exprt is_zero1 = is_zero(src1);
840 const exprt is_zero2 = is_zero(src2);
841 const and_exprt both_zero(is_zero1, is_zero2);
842
843 // NaN compares to nothing
844 exprt isnan1=isnan(src1, spec);
845 exprt isnan2=isnan(src2, spec);
846 const or_exprt nan(isnan1, isnan2);
847
848 if(rel==relt::LT || rel==relt::LE)
849 {
850 const equal_exprt bitwise_equal(src1, src2);
851
852 // signs different? trivial! Unless Zero.
853
854 const notequal_exprt signs_different(sign_bit(src1), sign_bit(src2));
855
856 // as long as the signs match: compare like unsigned numbers
857
858 // this works due to the BIAS
859 const binary_relation_exprt less_than1(
861 typecast_exprt(src1, bv_typet(spec.width())),
862 unsignedbv_typet(spec.width())),
863 ID_lt,
865 typecast_exprt(src2, bv_typet(spec.width())),
866 unsignedbv_typet(spec.width())));
867
868 // if both are negative (and not the same), need to turn around!
869 const notequal_exprt less_than2(
870 less_than1, and_exprt(sign_bit(src1), sign_bit(src2)));
871
872 const if_exprt less_than3(signs_different, sign_bit(src1), less_than2);
873
874 if(rel==relt::LT)
875 {
876 and_exprt and_bv{{less_than3,
877 // for the case of two negative numbers
878 not_exprt(bitwise_equal),
879 not_exprt(both_zero),
880 not_exprt(nan)}};
881
882 return std::move(and_bv);
883 }
884 else if(rel==relt::LE)
885 {
886 or_exprt or_bv{{less_than3, both_zero, bitwise_equal}};
887
888 return and_exprt(or_bv, not_exprt(nan));
889 }
890 else
892 }
893 else if(rel==relt::EQ)
894 {
895 const equal_exprt bitwise_equal(src1, src2);
896
897 return and_exprt(
898 or_exprt(bitwise_equal, both_zero),
899 not_exprt(nan));
900 }
901
903 return false_exprt();
904}
905
907 const exprt &src,
908 const ieee_float_spect &spec)
909{
910 return and_exprt(
911 exponent_all_ones(src, spec),
912 fraction_all_zeros(src, spec));
913}
914
916 const exprt &src,
917 const ieee_float_spect &spec)
918{
919 return not_exprt(or_exprt(isinf(src, spec), isnan(src, spec)));
920}
921
924 const exprt &src,
925 const ieee_float_spect &spec)
926{
927 return extractbits_exprt(src, spec.f, unsignedbv_typet(spec.e));
928}
929
932 const exprt &src,
933 const ieee_float_spect &spec)
934{
935 return extractbits_exprt(src, 0, unsignedbv_typet(spec.f));
936}
937
939 const exprt &src,
940 const ieee_float_spect &spec)
941{
942 return and_exprt(exponent_all_ones(src, spec),
943 not_exprt(fraction_all_zeros(src, spec)));
944}
945
948 exprt &fraction,
949 exprt &exponent)
950{
951 // n-log-n alignment shifter.
952 // The worst-case shift is the number of fraction
953 // bits minus one, in case the fraction is one exactly.
954 std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
955 std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
956 PRECONDITION(fraction_bits != 0);
957
958 std::size_t depth = address_bits(fraction_bits - 1);
959
960 exponent = typecast_exprt(
961 exponent, signedbv_typet(std::max(depth, exponent_bits + 1)));
962
963 exprt exponent_delta=from_integer(0, exponent.type());
964
965 for(int d=depth-1; d>=0; d--)
966 {
967 unsigned distance=(1<<d);
968 INVARIANT(
969 fraction_bits > distance,
970 "distance must be within the range of fraction bits");
971
972 // check if first 'distance'-many bits are zeros
973 const extractbits_exprt prefix(
974 fraction, fraction_bits - distance, unsignedbv_typet(distance));
975 const equal_exprt prefix_is_zero(prefix, from_integer(0, prefix.type()));
976
977 // If so, shift the zeros out left by 'distance'.
978 // Otherwise, leave as is.
979 const shl_exprt shifted(fraction, distance);
980
981 fraction=
982 if_exprt(prefix_is_zero, shifted, fraction);
983
984 // add corresponding weight to exponent
985 INVARIANT(
986 d < (signed int)exponent_bits,
987 "depth must be smaller than exponent bits");
988
989 exponent_delta=
990 bitor_exprt(exponent_delta,
991 shl_exprt(typecast_exprt(prefix_is_zero, exponent_delta.type()), d));
992 }
993
994 exponent=minus_exprt(exponent, exponent_delta);
995}
996
999 exprt &fraction,
1000 exprt &exponent,
1001 const ieee_float_spect &spec)
1002{
1003 mp_integer bias=spec.bias();
1004
1005 // Is the exponent strictly less than -bias+1, i.e., exponent<-bias+1?
1006 // This is transformed to distance=(-bias+1)-exponent
1007 // i.e., distance>0
1008 // Note that 1-bias is the exponent represented by 0...01,
1009 // i.e. the exponent of the smallest normal number and thus the 'base'
1010 // exponent for subnormal numbers.
1011
1012 std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
1013 PRECONDITION(exponent_bits >= spec.e);
1014
1015#if 1
1016 // Need to sign extend to avoid overflow. Note that this is a
1017 // relatively rare problem as the value needs to be close to the top
1018 // of the exponent range and then range must not have been
1019 // previously extended as add, multiply, etc. do. This is primarily
1020 // to handle casting down from larger ranges.
1021 exponent=typecast_exprt(exponent, signedbv_typet(exponent_bits+1));
1022#endif
1023
1024 const minus_exprt distance(
1025 from_integer(-bias + 1, exponent.type()), exponent);
1026
1027 // use sign bit
1028 const and_exprt denormal(
1029 not_exprt(sign_exprt(distance)),
1030 notequal_exprt(distance, from_integer(0, distance.type())));
1031
1032#if 1
1033 // Care must be taken to not loose information required for the
1034 // guard and sticky bits. +3 is for the hidden, guard and sticky bits.
1035 std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
1036
1037 if(fraction_bits < spec.f+3)
1038 {
1039 // Add zeros at the LSB end for the guard bit to shift into
1040 fraction=
1042 fraction, unsignedbv_typet(spec.f + 3 - fraction_bits).zero_expr(),
1043 unsignedbv_typet(spec.f+3));
1044 }
1045
1046 exprt denormalisedFraction = fraction;
1047
1048 exprt sticky_bit = false_exprt();
1049 denormalisedFraction =
1050 sticky_right_shift(fraction, distance, sticky_bit);
1051
1052 denormalisedFraction=
1053 bitor_exprt(denormalisedFraction,
1054 typecast_exprt(sticky_bit, denormalisedFraction.type()));
1055
1056 fraction=
1057 if_exprt(
1058 denormal,
1059 denormalisedFraction,
1060 fraction);
1061
1062#else
1063 fraction=
1064 if_exprt(
1065 denormal,
1066 lshr_exprt(fraction, distance),
1067 fraction);
1068#endif
1069
1070 exponent=
1071 if_exprt(denormal,
1072 from_integer(-bias, exponent.type()),
1073 exponent);
1074}
1075
1077 const unbiased_floatt &src,
1078 const exprt &rm,
1079 const ieee_float_spect &spec) const
1080{
1081 // incoming: some fraction (with explicit 1),
1082 // some exponent without bias
1083 // outgoing: rounded, with right size, with hidden bit, bias
1084
1085 exprt aligned_fraction=src.fraction,
1086 aligned_exponent=src.exponent;
1087
1088 {
1089 std::size_t exponent_bits = std::max(address_bits(spec.f), spec.e) + 1;
1090
1091 // before normalization, make sure exponent is large enough
1092 if(to_signedbv_type(aligned_exponent.type()).get_width()<exponent_bits)
1093 {
1094 // sign extend
1095 aligned_exponent=
1096 typecast_exprt(aligned_exponent, signedbv_typet(exponent_bits));
1097 }
1098 }
1099
1100 // align it!
1101 normalization_shift(aligned_fraction, aligned_exponent);
1102 denormalization_shift(aligned_fraction, aligned_exponent, spec);
1103
1104 unbiased_floatt result;
1105 result.fraction=aligned_fraction;
1106 result.exponent=aligned_exponent;
1107 result.sign=src.sign;
1108 result.NaN=src.NaN;
1109 result.infinity=src.infinity;
1110
1111 rounding_mode_bitst rounding_mode_bits(rm);
1112 round_fraction(result, rounding_mode_bits, spec);
1113 round_exponent(result, rounding_mode_bits, spec);
1114
1115 return pack(bias(result, spec), spec);
1116}
1117
1120 const std::size_t dest_bits,
1121 const exprt sign,
1122 const exprt &fraction,
1123 const rounding_mode_bitst &rounding_mode_bits)
1124{
1125 std::size_t fraction_bits=
1126 to_unsignedbv_type(fraction.type()).get_width();
1127
1128 PRECONDITION(dest_bits < fraction_bits);
1129
1130 // we have too many fraction bits
1131 std::size_t extra_bits=fraction_bits-dest_bits;
1132
1133 // more than two extra bits are superflus, and are
1134 // turned into a sticky bit
1135
1136 exprt sticky_bit=false_exprt();
1137
1138 if(extra_bits>=2)
1139 {
1140 // We keep most-significant bits, and thus the tail is made
1141 // of least-significant bits.
1142 const extractbits_exprt tail(
1143 fraction, 0, unsignedbv_typet(extra_bits - 2 + 1));
1144 sticky_bit=notequal_exprt(tail, from_integer(0, tail.type()));
1145 }
1146
1147 // the rounding bit is the last extra bit
1148 INVARIANT(
1149 extra_bits >= 1, "the extra bits contain at least the rounding bit");
1150 const extractbit_exprt rounding_bit(fraction, extra_bits - 1);
1151
1152 // we get one bit of the fraction for some rounding decisions
1153 const extractbit_exprt rounding_least(fraction, extra_bits);
1154
1155 // round-to-nearest (ties to even)
1156 const and_exprt round_to_even(
1157 rounding_bit, or_exprt(rounding_least, sticky_bit));
1158
1159 // round up
1160 const and_exprt round_to_plus_inf(
1161 not_exprt(sign), or_exprt(rounding_bit, sticky_bit));
1162
1163 // round down
1164 const and_exprt round_to_minus_inf(sign, or_exprt(rounding_bit, sticky_bit));
1165
1166 // round to zero
1167 false_exprt round_to_zero;
1168
1169 // now select appropriate one
1170 return if_exprt(rounding_mode_bits.round_to_even, round_to_even,
1171 if_exprt(rounding_mode_bits.round_to_plus_inf, round_to_plus_inf,
1172 if_exprt(rounding_mode_bits.round_to_minus_inf, round_to_minus_inf,
1173 if_exprt(rounding_mode_bits.round_to_zero, round_to_zero,
1174 false_exprt())))); // otherwise zero
1175}
1176
1178 unbiased_floatt &result,
1179 const rounding_mode_bitst &rounding_mode_bits,
1180 const ieee_float_spect &spec)
1181{
1182 std::size_t fraction_size=spec.f+1;
1183 std::size_t result_fraction_size=
1185
1186 // do we need to enlarge the fraction?
1187 if(result_fraction_size<fraction_size)
1188 {
1189 // pad with zeros at bottom
1190 std::size_t padding=fraction_size-result_fraction_size;
1191
1193 result.fraction,
1194 unsignedbv_typet(padding).zero_expr(),
1195 unsignedbv_typet(fraction_size));
1196 }
1197 else if(result_fraction_size==fraction_size) // it stays
1198 {
1199 // do nothing
1200 }
1201 else // fraction gets smaller -- rounding
1202 {
1203 std::size_t extra_bits=result_fraction_size-fraction_size;
1204 INVARIANT(
1205 extra_bits >= 1, "the extra bits include at least the rounding bit");
1206
1207 // this computes the rounding decision
1209 fraction_size, result.sign, result.fraction, rounding_mode_bits);
1210
1211 // chop off all the extra bits
1212 result.fraction = extractbits_exprt(
1213 result.fraction, extra_bits, unsignedbv_typet(fraction_size));
1214
1215#if 0
1216 // *** does not catch when the overflow goes subnormal -> normal ***
1217 // incrementing the fraction might result in an overflow
1218 result.fraction=
1219 bv_utils.zero_extension(result.fraction, result.fraction.size()+1);
1220
1221 result.fraction=bv_utils.incrementer(result.fraction, increment);
1222
1223 exprt overflow=result.fraction.back();
1224
1225 // In case of an overflow, the exponent has to be incremented.
1226 // "Post normalization" is then required.
1227 result.exponent=
1228 bv_utils.incrementer(result.exponent, overflow);
1229
1230 // post normalization of the fraction
1231 exprt integer_part1=result.fraction.back();
1232 exprt integer_part0=result.fraction[result.fraction.size()-2];
1233 const or_exprt new_integer_part(integer_part1, integer_part0);
1234
1235 result.fraction.resize(result.fraction.size()-1);
1236 result.fraction.back()=new_integer_part;
1237
1238#else
1239 // When incrementing due to rounding there are two edge
1240 // cases we need to be aware of:
1241 // 1. If the number is normal, the increment can overflow.
1242 // In this case we need to increment the exponent and
1243 // set the MSB of the fraction to 1.
1244 // 2. If the number is the largest subnormal, the increment
1245 // can change the MSB making it normal. Thus the exponent
1246 // must be incremented but the fraction will be OK.
1247 const extractbit_exprt old_msb(result.fraction, fraction_size - 1);
1248
1249 // increment if 'increment' is true
1250 result.fraction=
1251 plus_exprt(result.fraction,
1252 typecast_exprt(increment, result.fraction.type()));
1253
1254 // Normal overflow when old MSB == 1 and new MSB == 0
1255 const extractbit_exprt new_msb(result.fraction, fraction_size - 1);
1256 const and_exprt overflow(old_msb, not_exprt(new_msb));
1257
1258 // Subnormal to normal transition when old MSB == 0 and new MSB == 1
1259 const and_exprt subnormal_to_normal(not_exprt(old_msb), new_msb);
1260
1261 // In case of an overflow or subnormal to normal conversion,
1262 // the exponent has to be incremented.
1263 result.exponent=
1264 plus_exprt(
1265 result.exponent,
1266 if_exprt(
1267 or_exprt(overflow, subnormal_to_normal),
1268 from_integer(1, result.exponent.type()),
1269 from_integer(0, result.exponent.type())));
1270
1271 // post normalization of the fraction
1272 // In the case of overflow, set the MSB to 1
1273 // The subnormal case will have (only) the MSB set to 1
1274 result.fraction=bitor_exprt(
1275 result.fraction,
1276 if_exprt(overflow,
1277 from_integer(1<<(fraction_size-1), result.fraction.type()),
1278 from_integer(0, result.fraction.type())));
1279#endif
1280 }
1281}
1282
1284 unbiased_floatt &result,
1285 const rounding_mode_bitst &rounding_mode_bits,
1286 const ieee_float_spect &spec)
1287{
1288 std::size_t result_exponent_size=
1290
1291 PRECONDITION(result_exponent_size >= spec.e);
1292
1293 // do we need to enlarge the exponent?
1294 if(result_exponent_size == spec.e) // it stays
1295 {
1296 // do nothing
1297 }
1298 else // exponent gets smaller -- chop off top bits
1299 {
1300 exprt old_exponent=result.exponent;
1301 result.exponent =
1302 extractbits_exprt(result.exponent, 0, signedbv_typet(spec.e));
1303
1304 // max_exponent is the maximum representable
1305 // i.e. 1 higher than the maximum possible for a normal number
1306 exprt max_exponent=
1308 spec.max_exponent()-spec.bias(), old_exponent.type());
1309
1310 // the exponent is garbage if the fractional is zero
1311
1312 const and_exprt exponent_too_large(
1313 binary_relation_exprt(old_exponent, ID_ge, max_exponent),
1314 notequal_exprt(result.fraction, from_integer(0, result.fraction.type())));
1315
1316#if 1
1317 // Directed rounding modes round overflow to the maximum normal
1318 // depending on the particular mode and the sign
1319 const or_exprt overflow_to_inf(
1320 rounding_mode_bits.round_to_even,
1321 or_exprt(
1322 and_exprt(rounding_mode_bits.round_to_plus_inf, not_exprt(result.sign)),
1323 and_exprt(rounding_mode_bits.round_to_minus_inf, result.sign)));
1324
1325 const and_exprt set_to_max(exponent_too_large, not_exprt(overflow_to_inf));
1326
1327 exprt largest_normal_exponent=
1329 spec.max_exponent()-(spec.bias() + 1), result.exponent.type());
1330
1331 result.exponent=
1332 if_exprt(set_to_max, largest_normal_exponent, result.exponent);
1333
1334 result.fraction=
1335 if_exprt(set_to_max,
1337 result.fraction);
1338
1339 result.infinity=or_exprt(result.infinity,
1340 and_exprt(exponent_too_large,
1341 overflow_to_inf));
1342#else
1343 result.infinity=or_exprt(result.infinity, exponent_too_large);
1344#endif
1345 }
1346}
1347
1350 const unbiased_floatt &src,
1351 const ieee_float_spect &spec)
1352{
1353 biased_floatt result;
1354
1355 result.sign=src.sign;
1356 result.NaN=src.NaN;
1357 result.infinity=src.infinity;
1358
1359 // we need to bias the new exponent
1360 result.exponent=add_bias(src.exponent, spec);
1361
1362 // strip off the hidden bit
1364 to_unsignedbv_type(src.fraction.type()).get_width() == spec.f + 1);
1365
1366 const extractbit_exprt hidden_bit(src.fraction, spec.f);
1367 const not_exprt denormal(hidden_bit);
1368
1369 result.fraction =
1371
1372 // make exponent zero if its denormal
1373 // (includes zero)
1374 result.exponent=
1375 if_exprt(denormal, from_integer(0, result.exponent.type()),
1376 result.exponent);
1377
1378 return result;
1379}
1380
1382 const exprt &src,
1383 const ieee_float_spect &spec)
1384{
1385 typet t=unsignedbv_typet(spec.e);
1386 return plus_exprt(
1387 typecast_exprt(src, t),
1388 from_integer(spec.bias(), t));
1389}
1390
1392 const exprt &src,
1393 const ieee_float_spect &spec)
1394{
1395 typet t=signedbv_typet(spec.e);
1396 return minus_exprt(
1397 typecast_exprt(src, t),
1398 from_integer(spec.bias(), t));
1399}
1400
1402 const exprt &src,
1403 const ieee_float_spect &spec)
1404{
1405 unbiased_floatt result;
1406
1407 result.sign=sign_bit(src);
1408
1409 result.fraction=get_fraction(src, spec);
1410
1411 // add hidden bit
1412 exprt hidden_bit=isnormal(src, spec);
1413 result.fraction=
1414 concatenation_exprt(hidden_bit, result.fraction,
1415 unsignedbv_typet(spec.f+1));
1416
1417 result.exponent=get_exponent(src, spec);
1418
1419 // unbias the exponent
1420 exprt denormal=exponent_all_zeros(src, spec);
1421
1422 result.exponent=
1423 if_exprt(denormal,
1424 from_integer(-spec.bias()+1, signedbv_typet(spec.e)),
1425 sub_bias(result.exponent, spec));
1426
1427 result.infinity=isinf(src, spec);
1428 result.zero = is_zero(src);
1429 result.NaN=isnan(src, spec);
1430
1431 return result;
1432}
1433
1435 const biased_floatt &src,
1436 const ieee_float_spect &spec)
1437{
1440
1441 // do sign -- we make this 'false' for NaN
1442 const if_exprt sign_bit(src.NaN, false_exprt(), src.sign);
1443
1444 // the fraction is zero in case of infinity,
1445 // and one in case of NaN
1446 const if_exprt fraction(
1447 src.NaN,
1448 from_integer(1, src.fraction.type()),
1449 if_exprt(src.infinity, from_integer(0, src.fraction.type()), src.fraction));
1450
1451 const or_exprt infinity_or_NaN(src.NaN, src.infinity);
1452
1453 // do exponent
1454 const if_exprt exponent(
1455 infinity_or_NaN, from_integer(-1, src.exponent.type()), src.exponent);
1456
1457 // stitch all three together
1458 return typecast_exprt(
1460 {std::move(sign_bit), std::move(exponent), std::move(fraction)},
1461 bv_typet(spec.f + spec.e + 1)),
1462 spec.to_type());
1463}
1464
1466 const exprt &op,
1467 const exprt &dist,
1468 exprt &sticky)
1469{
1470 std::size_t d=1, width=to_unsignedbv_type(op.type()).get_width();
1471 exprt result=op;
1472 sticky=false_exprt();
1473
1474 std::size_t dist_width=to_bitvector_type(dist.type()).get_width();
1475
1476 for(std::size_t stage=0; stage<dist_width; stage++)
1477 {
1478 const lshr_exprt tmp(result, d);
1479
1480 exprt lost_bits;
1481
1482 if(d<=width)
1483 lost_bits = extractbits_exprt(result, 0, unsignedbv_typet(d));
1484 else
1485 lost_bits=result;
1486
1487 const extractbit_exprt dist_bit(dist, stage);
1488
1489 sticky=
1490 or_exprt(
1491 and_exprt(
1492 dist_bit,
1493 notequal_exprt(lost_bits, from_integer(0, lost_bits.type()))),
1494 sticky);
1495
1496 result=if_exprt(dist_bit, tmp, result);
1497
1498 d=d<<1;
1499 }
1500
1501 return result;
1502}
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:2125
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:925
Bit-wise XOR.
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:2995
Division.
Definition std_expr.h:1157
Equality.
Definition std_expr.h:1366
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:3077
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:947
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:931
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:915
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:938
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:923
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:998
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:734
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:823
static exprt isinf(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:906
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:2375
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:1228
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
The NIL expression.
Definition std_expr.h:3086
Boolean negation.
Definition std_expr.h:2332
Disequality.
Definition std_expr.h:1425
Boolean OR.
Definition std_expr.h:2233
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:2073
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.
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
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.
const std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::mask
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:71
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:2107
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