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{
96 to_typecast_expr(expr).op(), dest_type.get_width() - 1, 0, dest_type};
97 }
98 else if(expr.id()==ID_floatbv_plus)
99 {
100 const auto &float_expr = to_ieee_float_op_expr(expr);
101 return add_sub(
102 false,
103 float_expr.lhs(),
104 float_expr.rhs(),
105 float_expr.rounding_mode(),
106 get_spec(expr));
107 }
108 else if(expr.id()==ID_floatbv_minus)
109 {
110 const auto &float_expr = to_ieee_float_op_expr(expr);
111 return add_sub(
112 true,
113 float_expr.lhs(),
114 float_expr.rhs(),
115 float_expr.rounding_mode(),
116 get_spec(expr));
117 }
118 else if(expr.id()==ID_floatbv_mult)
119 {
120 const auto &float_expr = to_ieee_float_op_expr(expr);
121 return mul(
122 float_expr.lhs(),
123 float_expr.rhs(),
124 float_expr.rounding_mode(),
125 get_spec(expr));
126 }
127 else if(expr.id()==ID_floatbv_div)
128 {
129 const auto &float_expr = to_ieee_float_op_expr(expr);
130 return div(
131 float_expr.lhs(),
132 float_expr.rhs(),
133 float_expr.rounding_mode(),
134 get_spec(expr));
135 }
136 else if(expr.id()==ID_isnan)
137 {
138 const auto &op = to_unary_expr(expr).op();
139 return isnan(op, get_spec(op));
140 }
141 else if(expr.id()==ID_isfinite)
142 {
143 const auto &op = to_unary_expr(expr).op();
144 return isfinite(op, get_spec(op));
145 }
146 else if(expr.id()==ID_isinf)
147 {
148 const auto &op = to_unary_expr(expr).op();
149 return isinf(op, get_spec(op));
150 }
151 else if(expr.id()==ID_isnormal)
152 {
153 const auto &op = to_unary_expr(expr).op();
154 return isnormal(op, get_spec(op));
155 }
156 else if(expr.id()==ID_lt)
157 {
158 const auto &rel_expr = to_binary_relation_expr(expr);
159 return relation(
160 rel_expr.lhs(), relt::LT, rel_expr.rhs(), get_spec(rel_expr.lhs()));
161 }
162 else if(expr.id()==ID_gt)
163 {
164 const auto &rel_expr = to_binary_relation_expr(expr);
165 return relation(
166 rel_expr.lhs(), relt::GT, rel_expr.rhs(), get_spec(rel_expr.lhs()));
167 }
168 else if(expr.id()==ID_le)
169 {
170 const auto &rel_expr = to_binary_relation_expr(expr);
171 return relation(
172 rel_expr.lhs(), relt::LE, rel_expr.rhs(), get_spec(rel_expr.lhs()));
173 }
174 else if(expr.id()==ID_ge)
175 {
176 const auto &rel_expr = to_binary_relation_expr(expr);
177 return relation(
178 rel_expr.lhs(), relt::GE, rel_expr.rhs(), get_spec(rel_expr.lhs()));
179 }
180 else if(expr.id()==ID_sign)
181 return sign_bit(to_unary_expr(expr).op());
182
183 return nil_exprt();
184}
185
187{
188 const floatbv_typet &type=to_floatbv_type(expr.type());
189 return ieee_float_spect(type);
190}
191
193{
194 // we mask away the sign bit, which is the most significant bit
195 const mp_integer v = power(2, spec.width() - 1) - 1;
196
197 const constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
198
199 return bitand_exprt(op, mask);
200}
201
203{
204 // we flip the sign bit with an xor
205 const mp_integer v = power(2, spec.width() - 1);
206
207 constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
208
209 return bitxor_exprt(op, mask);
210}
211
213 const exprt &src0,
214 const exprt &src1,
215 const ieee_float_spect &spec)
216{
217 // special cases: -0 and 0 are equal
218 const exprt is_zero0 = is_zero(src0);
219 const exprt is_zero1 = is_zero(src1);
220 const and_exprt both_zero(is_zero0, is_zero1);
221
222 // NaN compares to nothing
223 exprt isnan0=isnan(src0, spec);
224 exprt isnan1=isnan(src1, spec);
225 const or_exprt nan(isnan0, isnan1);
226
227 const equal_exprt bitwise_equal(src0, src1);
228
229 return and_exprt(
230 or_exprt(bitwise_equal, both_zero),
231 not_exprt(nan));
232}
233
235{
236 // we mask away the sign bit, which is the most significant bit
237 const floatbv_typet &type=to_floatbv_type(src.type());
238 std::size_t width=type.get_width();
239
240 const mp_integer v = power(2, width - 1) - 1;
241
242 constant_exprt mask(integer2bvrep(v, width), src.type());
243
244 ieee_floatt z(type);
245 z.make_zero();
246
247 return equal_exprt(bitand_exprt(src, mask), z.to_expr());
248}
249
251 const exprt &src,
252 const ieee_float_spect &spec)
253{
254 exprt exponent=get_exponent(src, spec);
255 exprt all_ones=to_unsignedbv_type(exponent.type()).largest_expr();
256 return equal_exprt(exponent, all_ones);
257}
258
260 const exprt &src,
261 const ieee_float_spect &spec)
262{
263 exprt exponent=get_exponent(src, spec);
264 exprt all_zeros=to_unsignedbv_type(exponent.type()).zero_expr();
265 return equal_exprt(exponent, all_zeros);
266}
267
269 const exprt &src,
270 const ieee_float_spect &spec)
271{
272 // does not include hidden bit
273 exprt fraction=get_fraction(src, spec);
274 exprt all_zeros=to_unsignedbv_type(fraction.type()).zero_expr();
275 return equal_exprt(fraction, all_zeros);
276}
277
279{
280 exprt round_to_even_const=from_integer(ieee_floatt::ROUND_TO_EVEN, rm.type());
281 exprt round_to_plus_inf_const=
283 exprt round_to_minus_inf_const=
285 exprt round_to_zero_const=from_integer(ieee_floatt::ROUND_TO_ZERO, rm.type());
286
287 round_to_even=equal_exprt(rm, round_to_even_const);
288 round_to_plus_inf=equal_exprt(rm, round_to_plus_inf_const);
289 round_to_minus_inf=equal_exprt(rm, round_to_minus_inf_const);
290 round_to_zero=equal_exprt(rm, round_to_zero_const);
291}
292
294{
295 const bitvector_typet &bv_type=to_bitvector_type(op.type());
296 std::size_t width=bv_type.get_width();
297 return extractbit_exprt(op, width-1);
298}
299
301 const exprt &src,
302 const exprt &rm,
303 const ieee_float_spect &spec) const
304{
305 std::size_t src_width=to_signedbv_type(src.type()).get_width();
306
307 unbiased_floatt result;
308
309 // we need to adjust for negative integers
310 result.sign=sign_bit(src);
311
312 result.fraction=
313 typecast_exprt(abs_exprt(src), unsignedbv_typet(src_width));
314
315 // build an exponent (unbiased) -- this is signed!
316 result.exponent=
318 src_width-1,
319 signedbv_typet(address_bits(src_width - 1) + 1));
320
321 return rounder(result, rm, spec);
322}
323
325 const exprt &src,
326 const exprt &rm,
327 const ieee_float_spect &spec) const
328{
329 unbiased_floatt result;
330
331 result.fraction=src;
332
333 std::size_t src_width=to_unsignedbv_type(src.type()).get_width();
334
335 // build an exponent (unbiased) -- this is signed!
336 result.exponent=
338 src_width-1,
339 signedbv_typet(address_bits(src_width - 1) + 1));
340
341 result.sign=false_exprt();
342
343 return rounder(result, rm, spec);
344}
345
347 const exprt &src,
348 std::size_t dest_width,
349 const exprt &rm,
350 const ieee_float_spect &spec)
351{
352 return to_integer(src, dest_width, true, rm, spec);
353}
354
356 const exprt &src,
357 std::size_t dest_width,
358 const exprt &rm,
359 const ieee_float_spect &spec)
360{
361 return to_integer(src, dest_width, false, rm, spec);
362}
363
365 const exprt &src,
366 std::size_t dest_width,
367 bool is_signed,
368 const exprt &rm,
369 const ieee_float_spect &spec)
370{
371 const unbiased_floatt unpacked=unpack(src, spec);
372
373 rounding_mode_bitst rounding_mode_bits(rm);
374
375 // Right now hard-wired to round-to-zero, which is
376 // the usual case in ANSI-C.
377
378 // if the exponent is positive, shift right
379 exprt offset=from_integer(spec.f, signedbv_typet(spec.e));
380 const minus_exprt distance(offset, unpacked.exponent);
381 const lshr_exprt shift_result(unpacked.fraction, distance);
382
383 // if the exponent is negative, we have zero anyways
384 exprt result=shift_result;
385 const sign_exprt exponent_sign(unpacked.exponent);
386
387 result=
388 if_exprt(exponent_sign, from_integer(0, result.type()), result);
389
390 // chop out the right number of bits from the result
391 typet result_type=
392 is_signed?static_cast<typet>(signedbv_typet(dest_width)):
393 static_cast<typet>(unsignedbv_typet(dest_width));
394
395 result=typecast_exprt(result, result_type);
396
397 // if signed, apply sign.
398 if(is_signed)
399 {
400 result=if_exprt(
401 unpacked.sign, unary_minus_exprt(result), result);
402 }
403 else
404 {
405 // It's unclear what the behaviour for negative floats
406 // to integer shall be.
407 }
408
409 return result;
410}
411
413 const exprt &src,
414 const exprt &rm,
415 const ieee_float_spect &src_spec,
416 const ieee_float_spect &dest_spec) const
417{
418 // Catch the special case in which we extend,
419 // e.g. single to double.
420 // In this case, rounding can be avoided,
421 // but a denormal number may be come normal.
422 // Be careful to exclude the difficult case
423 // when denormalised numbers in the old format
424 // can be converted to denormalised numbers in the
425 // new format. Note that this is rare and will only
426 // happen with very non-standard formats.
427
428 int sourceSmallestNormalExponent = -((1 << (src_spec.e - 1)) - 1);
429 int sourceSmallestDenormalExponent =
430 sourceSmallestNormalExponent - src_spec.f;
431
432 // Using the fact that f doesn't include the hidden bit
433
434 int destSmallestNormalExponent = -((1 << (dest_spec.e - 1)) - 1);
435
436 if(dest_spec.e>=src_spec.e &&
437 dest_spec.f>=src_spec.f &&
438 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
439 {
440 unbiased_floatt unpacked_src=unpack(src, src_spec);
441 unbiased_floatt result;
442
443 // the fraction gets zero-padded
444 std::size_t padding=dest_spec.f-src_spec.f;
445 result.fraction=
447 unpacked_src.fraction,
448 from_integer(0, unsignedbv_typet(padding)),
449 unsignedbv_typet(dest_spec.f+1));
450
451 // the exponent gets sign-extended
452 INVARIANT(
453 unpacked_src.exponent.type().id() == ID_signedbv,
454 "the exponent needs to have a signed type");
455 result.exponent=
456 typecast_exprt(unpacked_src.exponent, signedbv_typet(dest_spec.e));
457
458 // if the number was denormal and is normal in the new format,
459 // normalise it!
460 if(dest_spec.e > src_spec.e)
461 {
462 normalization_shift(result.fraction, result.exponent);
463 // normalization_shift unconditionally extends the exponent size to avoid
464 // arithmetic overflow, but this cannot have happened here as the exponent
465 // had already been extended to dest_spec's size
466 result.exponent =
467 typecast_exprt(result.exponent, signedbv_typet(dest_spec.e));
468 }
469
470 // the flags get copied
471 result.sign=unpacked_src.sign;
472 result.NaN=unpacked_src.NaN;
473 result.infinity=unpacked_src.infinity;
474
475 // no rounding needed!
476 return pack(bias(result, dest_spec), dest_spec);
477 }
478 else
479 {
480 // we actually need to round
481 unbiased_floatt result=unpack(src, src_spec);
482 return rounder(result, rm, dest_spec);
483 }
484}
485
487 const exprt &src,
488 const ieee_float_spect &spec)
489{
490 return and_exprt(
491 not_exprt(exponent_all_zeros(src, spec)),
492 not_exprt(exponent_all_ones(src, spec)));
493}
494
497 const unbiased_floatt &src1,
498 const unbiased_floatt &src2)
499{
500 // extend both by one bit
501 std::size_t old_width1=to_signedbv_type(src1.exponent.type()).get_width();
502 std::size_t old_width2=to_signedbv_type(src2.exponent.type()).get_width();
503 PRECONDITION(old_width1 == old_width2);
504
505 const typecast_exprt extended_exponent1(
506 src1.exponent, signedbv_typet(old_width1 + 1));
507
508 const typecast_exprt extended_exponent2(
509 src2.exponent, signedbv_typet(old_width2 + 1));
510
511 // compute shift distance (here is the subtraction)
512 return minus_exprt(extended_exponent1, extended_exponent2);
513}
514
516 bool subtract,
517 const exprt &op0,
518 const exprt &op1,
519 const exprt &rm,
520 const ieee_float_spect &spec) const
521{
522 unbiased_floatt unpacked1=unpack(op0, spec);
523 unbiased_floatt unpacked2=unpack(op1, spec);
524
525 // subtract?
526 if(subtract)
527 unpacked2.sign=not_exprt(unpacked2.sign);
528
529 // figure out which operand has the bigger exponent
530 const exprt exponent_difference=subtract_exponents(unpacked1, unpacked2);
531 const sign_exprt src2_bigger(exponent_difference);
532
533 const exprt bigger_exponent=
534 if_exprt(src2_bigger, unpacked2.exponent, unpacked1.exponent);
535
536 // swap fractions as needed
537 const exprt new_fraction1=
538 if_exprt(src2_bigger, unpacked2.fraction, unpacked1.fraction);
539
540 const exprt new_fraction2=
541 if_exprt(src2_bigger, unpacked1.fraction, unpacked2.fraction);
542
543 // compute distance
544 const exprt distance=
545 typecast_exprt(abs_exprt(exponent_difference), unsignedbv_typet(spec.e));
546
547 // limit the distance: shifting more than f+3 bits is unnecessary
548 const exprt limited_dist=limit_distance(distance, spec.f+3);
549
550 // pad fractions with 3 zeros from below
551 exprt three_zeros=from_integer(0, unsignedbv_typet(3));
552 // add 4 to spec.f because unpacked new_fraction has the hidden bit
553 const exprt fraction1_padded=
554 concatenation_exprt(new_fraction1, three_zeros, unsignedbv_typet(spec.f+4));
555 const exprt fraction2_padded=
556 concatenation_exprt(new_fraction2, three_zeros, unsignedbv_typet(spec.f+4));
557
558 // shift new_fraction2
559 exprt sticky_bit;
560 const exprt fraction1_shifted=fraction1_padded;
561 const exprt fraction2_shifted=sticky_right_shift(
562 fraction2_padded, limited_dist, sticky_bit);
563
564 // sticky bit: 'or' of the bits lost by the right-shift
565 const bitor_exprt fraction2_stickied(
566 fraction2_shifted,
568 from_integer(0, unsignedbv_typet(spec.f + 3)),
569 sticky_bit,
570 fraction2_shifted.type()));
571
572 // need to have two extra fraction bits for addition and rounding
573 const exprt fraction1_ext=
574 typecast_exprt(fraction1_shifted, unsignedbv_typet(spec.f+4+2));
575 const exprt fraction2_ext=
576 typecast_exprt(fraction2_stickied, unsignedbv_typet(spec.f+4+2));
577
578 unbiased_floatt result;
579
580 // now add/sub them
581 const notequal_exprt subtract_lit(unpacked1.sign, unpacked2.sign);
582
583 result.fraction=
584 if_exprt(subtract_lit,
585 minus_exprt(fraction1_ext, fraction2_ext),
586 plus_exprt(fraction1_ext, fraction2_ext));
587
588 // sign of result
589 std::size_t width=to_bitvector_type(result.fraction.type()).get_width();
590 const sign_exprt fraction_sign(
591 typecast_exprt(result.fraction, signedbv_typet(width)));
592 result.fraction=
595 unsignedbv_typet(width));
596
597 result.exponent=bigger_exponent;
598
599 // adjust the exponent for the fact that we added two bits to the fraction
600 result.exponent=
602 from_integer(2, signedbv_typet(spec.e+1)));
603
604 // NaN?
605 result.NaN=or_exprt(
606 and_exprt(and_exprt(unpacked1.infinity, unpacked2.infinity),
607 notequal_exprt(unpacked1.sign, unpacked2.sign)),
608 or_exprt(unpacked1.NaN, unpacked2.NaN));
609
610 // infinity?
611 result.infinity=and_exprt(
612 not_exprt(result.NaN),
613 or_exprt(unpacked1.infinity, unpacked2.infinity));
614
615 // zero?
616 // Note that:
617 // 1. The zero flag isn't used apart from in divide and
618 // is only set on unpack
619 // 2. Subnormals mean that addition or subtraction can't round to 0,
620 // thus we can perform this test now
621 // 3. The rules for sign are different for zero
622 result.zero=
623 and_exprt(
624 not_exprt(or_exprt(result.infinity, result.NaN)),
626 result.fraction,
627 from_integer(0, result.fraction.type())));
628
629 // sign
630 const notequal_exprt add_sub_sign(
631 if_exprt(src2_bigger, unpacked2.sign, unpacked1.sign), fraction_sign);
632
633 const if_exprt infinity_sign(
634 unpacked1.infinity, unpacked1.sign, unpacked2.sign);
635
636 #if 1
637 rounding_mode_bitst rounding_mode_bits(rm);
638
639 const if_exprt zero_sign(
640 rounding_mode_bits.round_to_minus_inf,
641 or_exprt(unpacked1.sign, unpacked2.sign),
642 and_exprt(unpacked1.sign, unpacked2.sign));
643
644 result.sign=if_exprt(
645 result.infinity,
646 infinity_sign,
647 if_exprt(result.zero,
648 zero_sign,
649 add_sub_sign));
650 #else
651 result.sign=if_exprt(
652 result.infinity,
653 infinity_sign,
654 add_sub_sign);
655 #endif
656
657 return rounder(result, rm, spec);
658}
659
662 const exprt &dist,
663 mp_integer limit)
664{
665 std::size_t nb_bits = address_bits(limit);
666 std::size_t dist_width=to_unsignedbv_type(dist.type()).get_width();
667
668 if(dist_width<=nb_bits)
669 return dist;
670
671 const extractbits_exprt upper_bits(
672 dist, dist_width - 1, nb_bits, unsignedbv_typet(dist_width - nb_bits));
673 const equal_exprt upper_bits_zero(
674 upper_bits, from_integer(0, upper_bits.type()));
675
676 const extractbits_exprt lower_bits(
677 dist, nb_bits - 1, 0, unsignedbv_typet(nb_bits));
678
679 return if_exprt(
680 upper_bits_zero,
681 lower_bits,
682 unsignedbv_typet(nb_bits).largest_expr());
683}
684
686 const exprt &src1,
687 const exprt &src2,
688 const exprt &rm,
689 const ieee_float_spect &spec) const
690{
691 // unpack
692 const unbiased_floatt unpacked1=unpack(src1, spec);
693 const unbiased_floatt unpacked2=unpack(src2, spec);
694
695 // zero-extend the fractions (unpacked fraction has the hidden bit)
696 typet new_fraction_type=unsignedbv_typet((spec.f+1)*2);
697 const exprt fraction1=typecast_exprt(unpacked1.fraction, new_fraction_type);
698 const exprt fraction2=typecast_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 typecast_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(
928 src, spec.f+spec.e-1, spec.f,
929 unsignedbv_typet(spec.e));
930}
931
934 const exprt &src,
935 const ieee_float_spect &spec)
936{
937 return extractbits_exprt(
938 src, spec.f-1, 0,
939 unsignedbv_typet(spec.f));
940}
941
943 const exprt &src,
944 const ieee_float_spect &spec)
945{
946 return and_exprt(exponent_all_ones(src, spec),
947 not_exprt(fraction_all_zeros(src, spec)));
948}
949
952 exprt &fraction,
953 exprt &exponent)
954{
955 // n-log-n alignment shifter.
956 // The worst-case shift is the number of fraction
957 // bits minus one, in case the fraction is one exactly.
958 std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
959 std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
960 PRECONDITION(fraction_bits != 0);
961
962 std::size_t depth = address_bits(fraction_bits - 1);
963
964 exponent = typecast_exprt(
965 exponent, signedbv_typet(std::max(depth, exponent_bits + 1)));
966
967 exprt exponent_delta=from_integer(0, exponent.type());
968
969 for(int d=depth-1; d>=0; d--)
970 {
971 unsigned distance=(1<<d);
972 INVARIANT(
973 fraction_bits > distance,
974 "distance must be within the range of fraction bits");
975
976 // check if first 'distance'-many bits are zeros
977 const extractbits_exprt prefix(
978 fraction,
979 fraction_bits - 1,
980 fraction_bits - distance,
981 unsignedbv_typet(distance));
982 const equal_exprt prefix_is_zero(prefix, from_integer(0, prefix.type()));
983
984 // If so, shift the zeros out left by 'distance'.
985 // Otherwise, leave as is.
986 const shl_exprt shifted(fraction, distance);
987
988 fraction=
989 if_exprt(prefix_is_zero, shifted, fraction);
990
991 // add corresponding weight to exponent
992 INVARIANT(
993 d < (signed int)exponent_bits,
994 "depth must be smaller than exponent bits");
995
996 exponent_delta=
997 bitor_exprt(exponent_delta,
998 shl_exprt(typecast_exprt(prefix_is_zero, exponent_delta.type()), d));
999 }
1000
1001 exponent=minus_exprt(exponent, exponent_delta);
1002}
1003
1006 exprt &fraction,
1007 exprt &exponent,
1008 const ieee_float_spect &spec)
1009{
1010 mp_integer bias=spec.bias();
1011
1012 // Is the exponent strictly less than -bias+1, i.e., exponent<-bias+1?
1013 // This is transformed to distance=(-bias+1)-exponent
1014 // i.e., distance>0
1015 // Note that 1-bias is the exponent represented by 0...01,
1016 // i.e. the exponent of the smallest normal number and thus the 'base'
1017 // exponent for subnormal numbers.
1018
1019 std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
1020 PRECONDITION(exponent_bits >= spec.e);
1021
1022#if 1
1023 // Need to sign extend to avoid overflow. Note that this is a
1024 // relatively rare problem as the value needs to be close to the top
1025 // of the exponent range and then range must not have been
1026 // previously extended as add, multiply, etc. do. This is primarily
1027 // to handle casting down from larger ranges.
1028 exponent=typecast_exprt(exponent, signedbv_typet(exponent_bits+1));
1029#endif
1030
1031 const minus_exprt distance(
1032 from_integer(-bias + 1, exponent.type()), exponent);
1033
1034 // use sign bit
1035 const and_exprt denormal(
1036 not_exprt(sign_exprt(distance)),
1037 notequal_exprt(distance, from_integer(0, distance.type())));
1038
1039#if 1
1040 // Care must be taken to not loose information required for the
1041 // guard and sticky bits. +3 is for the hidden, guard and sticky bits.
1042 std::size_t fraction_bits=to_unsignedbv_type(fraction.type()).get_width();
1043
1044 if(fraction_bits < spec.f+3)
1045 {
1046 // Add zeros at the LSB end for the guard bit to shift into
1047 fraction=
1049 fraction, unsignedbv_typet(spec.f + 3 - fraction_bits).zero_expr(),
1050 unsignedbv_typet(spec.f+3));
1051 }
1052
1053 exprt denormalisedFraction = fraction;
1054
1055 exprt sticky_bit = false_exprt();
1056 denormalisedFraction =
1057 sticky_right_shift(fraction, distance, sticky_bit);
1058
1059 denormalisedFraction=
1060 bitor_exprt(denormalisedFraction,
1061 typecast_exprt(sticky_bit, denormalisedFraction.type()));
1062
1063 fraction=
1064 if_exprt(
1065 denormal,
1066 denormalisedFraction,
1067 fraction);
1068
1069#else
1070 fraction=
1071 if_exprt(
1072 denormal,
1073 lshr_exprt(fraction, distance),
1074 fraction);
1075#endif
1076
1077 exponent=
1078 if_exprt(denormal,
1079 from_integer(-bias, exponent.type()),
1080 exponent);
1081}
1082
1084 const unbiased_floatt &src,
1085 const exprt &rm,
1086 const ieee_float_spect &spec) const
1087{
1088 // incoming: some fraction (with explicit 1),
1089 // some exponent without bias
1090 // outgoing: rounded, with right size, with hidden bit, bias
1091
1092 exprt aligned_fraction=src.fraction,
1093 aligned_exponent=src.exponent;
1094
1095 {
1096 std::size_t exponent_bits = std::max(address_bits(spec.f), spec.e) + 1;
1097
1098 // before normalization, make sure exponent is large enough
1099 if(to_signedbv_type(aligned_exponent.type()).get_width()<exponent_bits)
1100 {
1101 // sign extend
1102 aligned_exponent=
1103 typecast_exprt(aligned_exponent, signedbv_typet(exponent_bits));
1104 }
1105 }
1106
1107 // align it!
1108 normalization_shift(aligned_fraction, aligned_exponent);
1109 denormalization_shift(aligned_fraction, aligned_exponent, spec);
1110
1111 unbiased_floatt result;
1112 result.fraction=aligned_fraction;
1113 result.exponent=aligned_exponent;
1114 result.sign=src.sign;
1115 result.NaN=src.NaN;
1116 result.infinity=src.infinity;
1117
1118 rounding_mode_bitst rounding_mode_bits(rm);
1119 round_fraction(result, rounding_mode_bits, spec);
1120 round_exponent(result, rounding_mode_bits, spec);
1121
1122 return pack(bias(result, spec), spec);
1123}
1124
1127 const std::size_t dest_bits,
1128 const exprt sign,
1129 const exprt &fraction,
1130 const rounding_mode_bitst &rounding_mode_bits)
1131{
1132 std::size_t fraction_bits=
1133 to_unsignedbv_type(fraction.type()).get_width();
1134
1135 PRECONDITION(dest_bits < fraction_bits);
1136
1137 // we have too many fraction bits
1138 std::size_t extra_bits=fraction_bits-dest_bits;
1139
1140 // more than two extra bits are superflus, and are
1141 // turned into a sticky bit
1142
1143 exprt sticky_bit=false_exprt();
1144
1145 if(extra_bits>=2)
1146 {
1147 // We keep most-significant bits, and thus the tail is made
1148 // of least-significant bits.
1149 const extractbits_exprt tail(
1150 fraction, extra_bits - 2, 0, unsignedbv_typet(extra_bits - 2 + 1));
1151 sticky_bit=notequal_exprt(tail, from_integer(0, tail.type()));
1152 }
1153
1154 // the rounding bit is the last extra bit
1155 INVARIANT(
1156 extra_bits >= 1, "the extra bits contain at least the rounding bit");
1157 const extractbit_exprt rounding_bit(fraction, extra_bits - 1);
1158
1159 // we get one bit of the fraction for some rounding decisions
1160 const extractbit_exprt rounding_least(fraction, extra_bits);
1161
1162 // round-to-nearest (ties to even)
1163 const and_exprt round_to_even(
1164 rounding_bit, or_exprt(rounding_least, sticky_bit));
1165
1166 // round up
1167 const and_exprt round_to_plus_inf(
1168 not_exprt(sign), or_exprt(rounding_bit, sticky_bit));
1169
1170 // round down
1171 const and_exprt round_to_minus_inf(sign, or_exprt(rounding_bit, sticky_bit));
1172
1173 // round to zero
1174 false_exprt round_to_zero;
1175
1176 // now select appropriate one
1177 return if_exprt(rounding_mode_bits.round_to_even, round_to_even,
1178 if_exprt(rounding_mode_bits.round_to_plus_inf, round_to_plus_inf,
1179 if_exprt(rounding_mode_bits.round_to_minus_inf, round_to_minus_inf,
1180 if_exprt(rounding_mode_bits.round_to_zero, round_to_zero,
1181 false_exprt())))); // otherwise zero
1182}
1183
1185 unbiased_floatt &result,
1186 const rounding_mode_bitst &rounding_mode_bits,
1187 const ieee_float_spect &spec)
1188{
1189 std::size_t fraction_size=spec.f+1;
1190 std::size_t result_fraction_size=
1192
1193 // do we need to enlarge the fraction?
1194 if(result_fraction_size<fraction_size)
1195 {
1196 // pad with zeros at bottom
1197 std::size_t padding=fraction_size-result_fraction_size;
1198
1200 result.fraction,
1201 unsignedbv_typet(padding).zero_expr(),
1202 unsignedbv_typet(fraction_size));
1203 }
1204 else if(result_fraction_size==fraction_size) // it stays
1205 {
1206 // do nothing
1207 }
1208 else // fraction gets smaller -- rounding
1209 {
1210 std::size_t extra_bits=result_fraction_size-fraction_size;
1211 INVARIANT(
1212 extra_bits >= 1, "the extra bits include at least the rounding bit");
1213
1214 // this computes the rounding decision
1216 fraction_size, result.sign, result.fraction, rounding_mode_bits);
1217
1218 // chop off all the extra bits
1220 result.fraction, result_fraction_size-1, extra_bits,
1221 unsignedbv_typet(fraction_size));
1222
1223#if 0
1224 // *** does not catch when the overflow goes subnormal -> normal ***
1225 // incrementing the fraction might result in an overflow
1226 result.fraction=
1227 bv_utils.zero_extension(result.fraction, result.fraction.size()+1);
1228
1229 result.fraction=bv_utils.incrementer(result.fraction, increment);
1230
1231 exprt overflow=result.fraction.back();
1232
1233 // In case of an overflow, the exponent has to be incremented.
1234 // "Post normalization" is then required.
1235 result.exponent=
1236 bv_utils.incrementer(result.exponent, overflow);
1237
1238 // post normalization of the fraction
1239 exprt integer_part1=result.fraction.back();
1240 exprt integer_part0=result.fraction[result.fraction.size()-2];
1241 const or_exprt new_integer_part(integer_part1, integer_part0);
1242
1243 result.fraction.resize(result.fraction.size()-1);
1244 result.fraction.back()=new_integer_part;
1245
1246#else
1247 // When incrementing due to rounding there are two edge
1248 // cases we need to be aware of:
1249 // 1. If the number is normal, the increment can overflow.
1250 // In this case we need to increment the exponent and
1251 // set the MSB of the fraction to 1.
1252 // 2. If the number is the largest subnormal, the increment
1253 // can change the MSB making it normal. Thus the exponent
1254 // must be incremented but the fraction will be OK.
1255 const extractbit_exprt old_msb(result.fraction, fraction_size - 1);
1256
1257 // increment if 'increment' is true
1258 result.fraction=
1259 plus_exprt(result.fraction,
1260 typecast_exprt(increment, result.fraction.type()));
1261
1262 // Normal overflow when old MSB == 1 and new MSB == 0
1263 const extractbit_exprt new_msb(result.fraction, fraction_size - 1);
1264 const and_exprt overflow(old_msb, not_exprt(new_msb));
1265
1266 // Subnormal to normal transition when old MSB == 0 and new MSB == 1
1267 const and_exprt subnormal_to_normal(not_exprt(old_msb), new_msb);
1268
1269 // In case of an overflow or subnormal to normal conversion,
1270 // the exponent has to be incremented.
1271 result.exponent=
1272 plus_exprt(
1273 result.exponent,
1274 if_exprt(
1275 or_exprt(overflow, subnormal_to_normal),
1276 from_integer(1, result.exponent.type()),
1277 from_integer(0, result.exponent.type())));
1278
1279 // post normalization of the fraction
1280 // In the case of overflow, set the MSB to 1
1281 // The subnormal case will have (only) the MSB set to 1
1282 result.fraction=bitor_exprt(
1283 result.fraction,
1284 if_exprt(overflow,
1285 from_integer(1<<(fraction_size-1), result.fraction.type()),
1286 from_integer(0, result.fraction.type())));
1287#endif
1288 }
1289}
1290
1292 unbiased_floatt &result,
1293 const rounding_mode_bitst &rounding_mode_bits,
1294 const ieee_float_spect &spec)
1295{
1296 std::size_t result_exponent_size=
1298
1299 PRECONDITION(result_exponent_size >= spec.e);
1300
1301 // do we need to enlarge the exponent?
1302 if(result_exponent_size == spec.e) // it stays
1303 {
1304 // do nothing
1305 }
1306 else // exponent gets smaller -- chop off top bits
1307 {
1308 exprt old_exponent=result.exponent;
1309 result.exponent=
1310 extractbits_exprt(result.exponent, spec.e-1, 0, signedbv_typet(spec.e));
1311
1312 // max_exponent is the maximum representable
1313 // i.e. 1 higher than the maximum possible for a normal number
1314 exprt max_exponent=
1316 spec.max_exponent()-spec.bias(), old_exponent.type());
1317
1318 // the exponent is garbage if the fractional is zero
1319
1320 const and_exprt exponent_too_large(
1321 binary_relation_exprt(old_exponent, ID_ge, max_exponent),
1322 notequal_exprt(result.fraction, from_integer(0, result.fraction.type())));
1323
1324#if 1
1325 // Directed rounding modes round overflow to the maximum normal
1326 // depending on the particular mode and the sign
1327 const or_exprt overflow_to_inf(
1328 rounding_mode_bits.round_to_even,
1329 or_exprt(
1330 and_exprt(rounding_mode_bits.round_to_plus_inf, not_exprt(result.sign)),
1331 and_exprt(rounding_mode_bits.round_to_minus_inf, result.sign)));
1332
1333 const and_exprt set_to_max(exponent_too_large, not_exprt(overflow_to_inf));
1334
1335 exprt largest_normal_exponent=
1337 spec.max_exponent()-(spec.bias() + 1), result.exponent.type());
1338
1339 result.exponent=
1340 if_exprt(set_to_max, largest_normal_exponent, result.exponent);
1341
1342 result.fraction=
1343 if_exprt(set_to_max,
1345 result.fraction);
1346
1347 result.infinity=or_exprt(result.infinity,
1348 and_exprt(exponent_too_large,
1349 overflow_to_inf));
1350#else
1351 result.infinity=or_exprt(result.infinity, exponent_too_large);
1352#endif
1353 }
1354}
1355
1358 const unbiased_floatt &src,
1359 const ieee_float_spect &spec)
1360{
1361 biased_floatt result;
1362
1363 result.sign=src.sign;
1364 result.NaN=src.NaN;
1365 result.infinity=src.infinity;
1366
1367 // we need to bias the new exponent
1368 result.exponent=add_bias(src.exponent, spec);
1369
1370 // strip off the hidden bit
1372 to_unsignedbv_type(src.fraction.type()).get_width() == spec.f + 1);
1373
1374 const extractbit_exprt hidden_bit(src.fraction, spec.f);
1375 const not_exprt denormal(hidden_bit);
1376
1377 result.fraction=
1379 src.fraction, spec.f-1, 0,
1380 unsignedbv_typet(spec.f));
1381
1382 // make exponent zero if its denormal
1383 // (includes zero)
1384 result.exponent=
1385 if_exprt(denormal, from_integer(0, result.exponent.type()),
1386 result.exponent);
1387
1388 return result;
1389}
1390
1392 const exprt &src,
1393 const ieee_float_spect &spec)
1394{
1395 typet t=unsignedbv_typet(spec.e);
1396 return plus_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 typet t=signedbv_typet(spec.e);
1406 return minus_exprt(
1407 typecast_exprt(src, t),
1408 from_integer(spec.bias(), t));
1409}
1410
1412 const exprt &src,
1413 const ieee_float_spect &spec)
1414{
1415 unbiased_floatt result;
1416
1417 result.sign=sign_bit(src);
1418
1419 result.fraction=get_fraction(src, spec);
1420
1421 // add hidden bit
1422 exprt hidden_bit=isnormal(src, spec);
1423 result.fraction=
1424 concatenation_exprt(hidden_bit, result.fraction,
1425 unsignedbv_typet(spec.f+1));
1426
1427 result.exponent=get_exponent(src, spec);
1428
1429 // unbias the exponent
1430 exprt denormal=exponent_all_zeros(src, spec);
1431
1432 result.exponent=
1433 if_exprt(denormal,
1434 from_integer(-spec.bias()+1, signedbv_typet(spec.e)),
1435 sub_bias(result.exponent, spec));
1436
1437 result.infinity=isinf(src, spec);
1438 result.zero = is_zero(src);
1439 result.NaN=isnan(src, spec);
1440
1441 return result;
1442}
1443
1445 const biased_floatt &src,
1446 const ieee_float_spect &spec)
1447{
1450
1451 // do sign -- we make this 'false' for NaN
1452 const if_exprt sign_bit(src.NaN, false_exprt(), src.sign);
1453
1454 // the fraction is zero in case of infinity,
1455 // and one in case of NaN
1456 const if_exprt fraction(
1457 src.NaN,
1458 from_integer(1, src.fraction.type()),
1459 if_exprt(src.infinity, from_integer(0, src.fraction.type()), src.fraction));
1460
1461 const or_exprt infinity_or_NaN(src.NaN, src.infinity);
1462
1463 // do exponent
1464 const if_exprt exponent(
1465 infinity_or_NaN, from_integer(-1, src.exponent.type()), src.exponent);
1466
1467 // stitch all three together
1468 return typecast_exprt(
1470 {std::move(sign_bit), std::move(exponent), std::move(fraction)},
1471 bv_typet(spec.f + spec.e + 1)),
1472 spec.to_type());
1473}
1474
1476 const exprt &op,
1477 const exprt &dist,
1478 exprt &sticky)
1479{
1480 std::size_t d=1, width=to_unsignedbv_type(op.type()).get_width();
1481 exprt result=op;
1482 sticky=false_exprt();
1483
1484 std::size_t dist_width=to_bitvector_type(dist.type()).get_width();
1485
1486 for(std::size_t stage=0; stage<dist_width; stage++)
1487 {
1488 const lshr_exprt tmp(result, d);
1489
1490 exprt lost_bits;
1491
1492 if(d<=width)
1493 lost_bits=extractbits_exprt(result, d-1, 0, unsignedbv_typet(d));
1494 else
1495 lost_bits=result;
1496
1497 const extractbit_exprt dist_bit(dist, stage);
1498
1499 sticky=
1500 or_exprt(
1501 and_exprt(
1502 dist_bit,
1503 notequal_exprt(lost_bits, from_integer(0, lost_bits.type()))),
1504 sticky);
1505
1506 result=if_exprt(dist_bit, tmp, result);
1507
1508 d=d<<1;
1509 }
1510
1511 return result;
1512}
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:379
Boolean AND.
Definition std_expr.h:2071
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
Bit-wise AND.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition std_types.h:865
std::size_t get_width() const
Definition std_types.h:876
Bit-wise XOR.
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:2942
Division.
Definition std_expr.h:1097
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:216
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:3017
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:951
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:933
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:250
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:364
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:324
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:486
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:300
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:515
static exprt is_zero(const exprt &)
Definition float_bv.cpp:234
static exprt abs(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:192
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:412
static exprt isnan(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:942
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
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:496
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:186
static exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:355
static exprt negation(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:202
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:293
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:685
static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:268
static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:259
static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:212
static exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:346
static exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition float_bv.cpp:661
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:2323
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:396
Logical right shift.
Binary minus.
Definition std_expr.h:1006
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1168
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
The NIL expression.
Definition std_expr.h:3026
Boolean negation.
Definition std_expr.h:2278
Disequality.
Definition std_expr.h:1365
Boolean OR.
Definition std_expr.h:2179
The plus expression Associativity is not specified.
Definition std_expr.h:947
Left shift.
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:539
Fixed-width bit-vector with two's complement interpretation.
Semantic type conversion.
Definition std_expr.h:2017
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:326
The unary minus expression.
Definition std_expr.h:423
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:18
#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:51
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:840
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition std_expr.h:403
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:453
void get(const exprt &rm)
Definition float_bv.cpp:278
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45