cprover
Loading...
Searching...
No Matches
float_utils.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "float_utils.h"
10
11#include <algorithm>
12
13#include <util/arith_tools.h>
14
16{
17 bvt round_to_even=
19 bvt round_to_plus_inf=
21 bvt round_to_minus_inf=
23 bvt round_to_zero=
25
27 rounding_mode_bits.round_to_plus_inf=bv_utils.equal(src, round_to_plus_inf);
28 rounding_mode_bits.round_to_minus_inf=bv_utils.equal(src, round_to_minus_inf);
30}
31
33{
34 unbiased_floatt result;
35
36 // we need to convert negative integers
37 result.sign=sign_bit(src);
38
40
41 // build an exponent (unbiased) -- this is signed!
42 result.exponent=
44 src.size()-1,
45 address_bits(src.size() - 1) + 1);
46
47 return rounder(result);
48}
49
51{
52 unbiased_floatt result;
53
54 result.fraction=src;
55
56 // build an exponent (unbiased) -- this is signed!
57 result.exponent=
59 src.size()-1,
60 address_bits(src.size() - 1) + 1);
61
62 result.sign=const_literal(false);
63
64 return rounder(result);
65}
66
68 const bvt &src,
69 std::size_t dest_width)
70{
71 return to_integer(src, dest_width, true);
72}
73
75 const bvt &src,
76 std::size_t dest_width)
77{
78 return to_integer(src, dest_width, false);
79}
80
82 const bvt &src,
83 std::size_t dest_width,
84 bool is_signed)
85{
86 PRECONDITION(src.size() == spec.width());
87
88 // The following is the usual case in ANSI-C, and we optimize for that.
90
91 const unbiased_floatt unpacked = unpack(src);
92
93 bvt fraction = unpacked.fraction;
94
95 if(dest_width > fraction.size())
96 {
98 bv_utils.build_constant(0U, dest_width - fraction.size());
99 fraction.insert(
100 fraction.begin(), lsb_extension.begin(), lsb_extension.end());
101 }
102
103 // if the exponent is positive, shift right
104 bvt offset =
105 bv_utils.build_constant(fraction.size() - 1, unpacked.exponent.size());
106 bvt distance = bv_utils.sub(offset, unpacked.exponent);
109
110 // if the exponent is negative, we have zero anyways
111 bvt result = shift_result;
112 literalt exponent_sign = unpacked.exponent[unpacked.exponent.size() - 1];
113
114 for(std::size_t i = 0; i < result.size(); i++)
115 result[i] = prop.land(result[i], !exponent_sign);
116
117 // chop out the right number of bits from the result
118 if(result.size() > dest_width)
119 {
120 result.resize(dest_width);
121 }
122
123 INVARIANT(
124 result.size() == dest_width,
125 "result bitvector width should equal the destination bitvector width");
126
127 // if signed, apply sign.
128 if(is_signed)
129 result = bv_utils.cond_negate(result, unpacked.sign);
130 else
131 {
132 // It's unclear what the behaviour for negative floats
133 // to integer shall be.
134 }
135
136 return result;
137}
138
140{
141 unbiased_floatt result;
142
143 result.sign=const_literal(src.get_sign());
144 result.NaN=const_literal(src.is_NaN());
145 result.infinity=const_literal(src.is_infinity());
148
149 return pack(bias(result));
150}
151
153 const bvt &src,
155{
156 PRECONDITION(src.size() == spec.width());
157
158 #if 1
159 // Catch the special case in which we extend,
160 // e.g. single to double.
161 // In this case, rounding can be avoided,
162 // but a denormal number may be come normal.
163 // Be careful to exclude the difficult case
164 // when denormalised numbers in the old format
165 // can be converted to denormalised numbers in the
166 // new format. Note that this is rare and will only
167 // happen with very non-standard formats.
168
169 int sourceSmallestNormalExponent=-((1 << (spec.e - 1)) - 1);
172
173 // Using the fact that f doesn't include the hidden bit
174
175 int destSmallestNormalExponent=-((1 << (dest_spec.e - 1)) - 1);
176
177 if(dest_spec.e>=spec.e &&
178 dest_spec.f>=spec.f &&
180 {
182 unbiased_floatt result;
183
184 // the fraction gets zero-padded
185 std::size_t padding=dest_spec.f-spec.f;
186 result.fraction=
188
189 // the exponent gets sign-extended
190 result.exponent=
192
193 // if the number was denormal and is normal in the new format,
194 // normalise it!
195 if(dest_spec.e > spec.e)
196 {
197 normalization_shift(result.fraction, result.exponent);
198 }
199
200 // the flags get copied
201 result.sign=unpacked_src.sign;
202 result.NaN=unpacked_src.NaN;
203 result.infinity=unpacked_src.infinity;
204
205 // no rounding needed!
207 return pack(bias(result));
208 }
209 else // NOLINT(readability/braces)
210 #endif
211 {
212 // we actually need to round
213 unbiased_floatt result=unpack(src);
215 return rounder(result);
216 }
217}
218
220{
221 return prop.land(
222 !exponent_all_zeros(src),
223 !exponent_all_ones(src));
224}
225
228 const unbiased_floatt &src1,
229 const unbiased_floatt &src2)
230{
231 // extend both
233 bv_utils.sign_extension(src1.exponent, src1.exponent.size()+1);
235 bv_utils.sign_extension(src2.exponent, src2.exponent.size()+1);
236
238
239 // compute shift distance (here is the subtraction)
241}
242
244 const bvt &src1,
245 const bvt &src2,
246 bool subtract)
247{
250
251 // subtract?
252 if(subtract)
253 unpacked2.sign=!unpacked2.sign;
254
255 // figure out which operand has the bigger exponent
258
259 const bvt bigger_exponent=
260 bv_utils.select(src2_bigger, unpacked2.exponent, unpacked1.exponent);
261
262 // swap fractions as needed
263 const bvt new_fraction1=
264 bv_utils.select(src2_bigger, unpacked2.fraction, unpacked1.fraction);
265
266 const bvt new_fraction2=
267 bv_utils.select(src2_bigger, unpacked1.fraction, unpacked2.fraction);
268
269 // compute distance
271
272 // limit the distance: shifting more than f+3 bits is unnecessary
273 const bvt limited_dist=limit_distance(distance, spec.f+3);
274
275 // pad fractions with 2 zeros from below
276 const bvt fraction1_padded=
278 const bvt fraction2_padded=
280
281 // shift new_fraction2
286
287 // sticky bit: or of the bits lost by the right-shift
290
291 // need to have two extra fraction bits for addition and rounding
292 const bvt fraction1_ext=
294 const bvt fraction2_ext=
296
297 unbiased_floatt result;
298
299 // now add/sub them
301 result.fraction=
303
304 // sign of result
305 literalt fraction_sign=result.fraction.back();
307
309
310 // adjust the exponent for the fact that we added two bits to the fraction
311 result.exponent=
313 bv_utils.sign_extension(result.exponent, result.exponent.size()+1),
314 bv_utils.build_constant(2, result.exponent.size()+1));
315
316 // NaN?
317 result.NaN=prop.lor(
318 prop.land(prop.land(unpacked1.infinity, unpacked2.infinity),
319 prop.lxor(unpacked1.sign, unpacked2.sign)),
320 prop.lor(unpacked1.NaN, unpacked2.NaN));
321
322 // infinity?
323 result.infinity=prop.land(
324 !result.NaN,
325 prop.lor(unpacked1.infinity, unpacked2.infinity));
326
327 // zero?
328 // Note that:
329 // 1. The zero flag isn't used apart from in divide and
330 // is only set on unpack
331 // 2. Subnormals mean that addition or subtraction can't round to 0,
332 // thus we can perform this test now
333 // 3. The rules for sign are different for zero
334 result.zero=prop.land(
335 !prop.lor(result.infinity, result.NaN),
336 !prop.lor(result.fraction));
337
338
339 // sign
343
345 prop.lselect(unpacked1.infinity, unpacked1.sign, unpacked2.sign);
346
347 #if 1
350 prop.lor(unpacked1.sign, unpacked2.sign),
351 prop.land(unpacked1.sign, unpacked2.sign));
352
353 result.sign=prop.lselect(
354 result.infinity,
356 prop.lselect(result.zero,
357 zero_sign,
358 add_sub_sign));
359 #else
360 result.sign=prop.lselect(
361 result.infinity,
364 #endif
365
366 #if 0
367 result.sign=const_literal(false);
368 result.fraction.resize(spec.f+1, const_literal(true));
369 result.exponent.resize(spec.e, const_literal(false));
370 result.NaN=const_literal(false);
371 result.infinity=const_literal(false);
372 // for(std::size_t i=0; i<result.fraction.size(); i++)
373 // result.fraction[i]=const_literal(true);
374
375 for(std::size_t i=0; i<result.fraction.size(); i++)
376 result.fraction[i]=new_fraction2[i];
377
378 return pack(bias(result));
379 #endif
380
381 return rounder(result);
382}
383
386 const bvt &dist,
388{
389 std::size_t nb_bits = address_bits(limit);
390
392 upper_bits.erase(upper_bits.begin(), upper_bits.begin()+nb_bits);
394
396 lower_bits.resize(nb_bits);
397
398 bvt result;
399 result.resize(lower_bits.size());
400
401 // bitwise or with or_upper_bits
402 for(std::size_t i=0; i<result.size(); i++)
403 result[i]=prop.lor(lower_bits[i], or_upper_bits);
404
405 return result;
406}
407
409{
410 // unpack
413
414 // zero-extend the fractions
415 const bvt fraction1=
416 bv_utils.zero_extension(unpacked1.fraction, unpacked1.fraction.size()*2);
417 const bvt fraction2=
418 bv_utils.zero_extension(unpacked2.fraction, unpacked2.fraction.size()*2);
419
420 // multiply fractions
421 unbiased_floatt result;
423
424 // extend exponents to account for overflow
425 // add two bits, as we do extra arithmetic on it later
426 const bvt exponent1=
427 bv_utils.sign_extension(unpacked1.exponent, unpacked1.exponent.size()+2);
428 const bvt exponent2=
429 bv_utils.sign_extension(unpacked2.exponent, unpacked2.exponent.size()+2);
430
432
433 // adjust, we are thowing in an extra fraction bit
434 // it has been extended above
436
437 // new sign
438 result.sign=prop.lxor(unpacked1.sign, unpacked2.sign);
439
440 // infinity?
441 result.infinity=prop.lor(unpacked1.infinity, unpacked2.infinity);
442
443 // NaN?
444 {
446
447 NaN_cond.push_back(is_NaN(src1));
448 NaN_cond.push_back(is_NaN(src2));
449
450 // infinity * 0 is NaN!
451 NaN_cond.push_back(prop.land(unpacked1.zero, unpacked2.infinity));
452 NaN_cond.push_back(prop.land(unpacked2.zero, unpacked1.infinity));
453
454 result.NaN=prop.lor(NaN_cond);
455 }
456
457 return rounder(result);
458}
459
461{
462 // unpack
465
466 std::size_t div_width=unpacked1.fraction.size()*2+1;
467
468 // pad fraction1 with zeros
469 bvt fraction1=unpacked1.fraction;
470 fraction1.reserve(div_width);
471 while(fraction1.size()<div_width)
472 fraction1.insert(fraction1.begin(), const_literal(false));
473
474 // zero-extend fraction2
475 const bvt fraction2=
477
478 // divide fractions
479 unbiased_floatt result;
480 bvt rem;
482
483 // is there a remainder?
485
486 // we throw this into the result, as one additional bit,
487 // to get the right rounding decision
488 result.fraction.insert(
489 result.fraction.begin(), have_remainder);
490
491 // We will subtract the exponents;
492 // to account for overflow, we add a bit.
493 // we add a second bit for the adjust by extra fraction bits
494 const bvt exponent1=
495 bv_utils.sign_extension(unpacked1.exponent, unpacked1.exponent.size()+2);
496 const bvt exponent2=
497 bv_utils.sign_extension(unpacked2.exponent, unpacked2.exponent.size()+2);
498
499 // subtract exponents
501
502 // adjust, as we have thown in extra fraction bits
503 result.exponent=bv_utils.add(
506
507 // new sign
508 result.sign=prop.lxor(unpacked1.sign, unpacked2.sign);
509
510 // Infinity? This happens when
511 // 1) dividing a non-nan/non-zero by zero, or
512 // 2) first operand is inf and second is non-nan and non-zero
513 // In particular, inf/0=inf.
514 result.infinity=
515 prop.lor(
516 prop.land(!unpacked1.zero,
517 prop.land(!unpacked1.NaN,
518 unpacked2.zero)),
519 prop.land(unpacked1.infinity,
520 prop.land(!unpacked2.NaN,
521 !unpacked2.zero)));
522
523 // NaN?
524 result.NaN=prop.lor(unpacked1.NaN,
525 prop.lor(unpacked2.NaN,
526 prop.lor(prop.land(unpacked1.zero, unpacked2.zero),
527 prop.land(unpacked1.infinity, unpacked2.infinity))));
528
529 // Division by infinity produces zero, unless we have NaN
531 prop.land(!unpacked1.NaN, unpacked2.infinity);
532
534 bv_utils.zeros(result.fraction.size()), result.fraction);
535
536 return rounder(result);
537}
538
540{
541 /* The semantics of floating-point remainder implemented as below
542 is the sensible one. Unfortunately this is not the one required
543 by IEEE-754 or fmod / remainder. Martin has discussed the
544 'correct' semantics with Christoph and Alberto at length as
545 well as talking to various hardware designers and we still
546 hasn't found a good way to implement them in a solver.
547 We have some approaches that are correct but they really
548 don't scale. */
549
551
552 // stub: do (src2.infinity ? src1 : (src1/src2)*src2))
553 return bv_utils.select(
554 unpacked2.infinity, src1, sub(src1, mul(div(src1, src2), src2)));
555}
556
558{
559 PRECONDITION(!src.empty());
560 bvt result=src;
561 literalt &sign_bit=result[result.size()-1];
563 return result;
564}
565
567{
568 PRECONDITION(!src.empty());
569 bvt result=src;
570 result[result.size()-1]=const_literal(false);
571 return result;
572}
573
575 const bvt &src1,
576 relt rel,
577 const bvt &src2)
578{
579 if(rel==relt::GT)
580 return relation(src2, relt::LT, src1); // swapped
581 else if(rel==relt::GE)
582 return relation(src2, relt::LE, src1); // swapped
583
584 PRECONDITION(rel == relt::EQ || rel == relt::LT || rel == relt::LE);
585
586 // special cases: -0 and 0 are equal
590
591 // NaN compares to nothing
595
596 if(rel==relt::LT || rel==relt::LE)
597 {
599
600 // signs different? trivial! Unless Zero.
601
604
605 // as long as the signs match: compare like unsigned numbers
606
607 // this works due to the BIAS
609
610 // if both are negative (and not the same), need to turn around!
613
616 sign_bit(src1),
617 less_than2);
618
619 if(rel==relt::LT)
620 {
621 bvt and_bv;
622 and_bv.push_back(less_than3);
623 and_bv.push_back(!bitwise_equal); // for the case of two negative numbers
624 and_bv.push_back(!both_zero);
625 and_bv.push_back(!NaN);
626
627 return prop.land(and_bv);
628 }
629 else if(rel==relt::LE)
630 {
631 bvt or_bv;
632 or_bv.push_back(less_than3);
633 or_bv.push_back(both_zero);
634 or_bv.push_back(bitwise_equal);
635
636 return prop.land(prop.lor(or_bv), !NaN);
637 }
638 else
640 }
641 else if(rel==relt::EQ)
642 {
644
645 return prop.land(
647 !NaN);
648 }
649
650 // not reached
652 return const_literal(false);
653}
654
656{
657 PRECONDITION(!src.empty());
659 all_but_sign=src;
660 all_but_sign.resize(all_but_sign.size()-1);
662}
663
665{
666 bvt and_bv;
667 and_bv.push_back(!sign_bit(src));
668 and_bv.push_back(exponent_all_ones(src));
669 and_bv.push_back(fraction_all_zeros(src));
670 return prop.land(and_bv);
671}
672
674{
675 return prop.land(
677 fraction_all_zeros(src));
678}
679
682{
683 return bv_utils.extract(src, spec.f, spec.f+spec.e-1);
684}
685
688{
689 return bv_utils.extract(src, 0, spec.f-1);
690}
691
693{
694 bvt and_bv;
695 and_bv.push_back(sign_bit(src));
696 and_bv.push_back(exponent_all_ones(src));
697 and_bv.push_back(fraction_all_zeros(src));
698 return prop.land(and_bv);
699}
700
702{
703 return prop.land(exponent_all_ones(src),
704 !fraction_all_zeros(src));
705}
706
708{
709 bvt exponent=src;
710
711 // removes the fractional part
712 exponent.erase(exponent.begin(), exponent.begin()+spec.f);
713
714 // removes the sign
715 exponent.resize(spec.e);
716
717 return bv_utils.is_all_ones(exponent);
718}
719
721{
722 bvt exponent=src;
723
724 // removes the fractional part
725 exponent.erase(exponent.begin(), exponent.begin()+spec.f);
726
727 // removes the sign
728 exponent.resize(spec.e);
729
730 return bv_utils.is_zero(exponent);
731}
732
734{
735 PRECONDITION(src.size() == spec.width());
736 // does not include hidden bit
737 bvt tmp=src;
738 tmp.resize(spec.f);
739 return bv_utils.is_zero(tmp);
740}
741
743void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
744{
745 #if 0
746 // this thing is quadratic!
747
748 bvt new_fraction=prop.new_variables(fraction.size());
749 bvt new_exponent=prop.new_variables(exponent.size());
750
751 // i is the shift distance
752 for(std::size_t i=0; i<fraction.size(); i++)
753 {
754 bvt equal;
755
756 // the bits above need to be zero
757 for(std::size_t j=0; j<i; j++)
758 equal.push_back(
759 !fraction[fraction.size()-1-j]);
760
761 // this one needs to be one
762 equal.push_back(fraction[fraction.size()-1-i]);
763
764 // iff all of that holds, we shift here!
765 literalt shift=prop.land(equal);
766
767 // build shifted value
768 bvt shifted_fraction=bv_utils.shift(fraction, bv_utilst::LEFT, i);
770
771 // build new exponent
772 bvt adjustment=bv_utils.build_constant(-i, exponent.size());
775 }
776
777 // Fraction all zero? It stays zero.
778 // The exponent is undefined in that case.
781 zero_fraction.resize(fraction.size(), const_literal(false));
783
784 fraction=new_fraction;
785 exponent=new_exponent;
786
787 #else
788
789 // n-log-n alignment shifter.
790 // The worst-case shift is the number of fraction
791 // bits minus one, in case the fraction is one exactly.
792 PRECONDITION(!fraction.empty());
793 std::size_t depth = address_bits(fraction.size() - 1);
794
795 if(exponent.size()<depth)
796 exponent=bv_utils.sign_extension(exponent, depth);
797
798 bvt exponent_delta=bv_utils.zeros(exponent.size());
799
800 for(int d=depth-1; d>=0; d--)
801 {
802 std::size_t distance=(1<<d);
803 INVARIANT(
804 fraction.size() > distance, "fraction must be larger than distance");
805
806 // check if first 'distance'-many bits are zeros
807 const bvt prefix=bv_utils.extract_msb(fraction, distance);
809
810 // If so, shift the zeros out left by 'distance'.
811 // Otherwise, leave as is.
812 const bvt shifted=
813 bv_utils.shift(fraction, bv_utilst::shiftt::SHIFT_LEFT, distance);
814
815 fraction=
817
818 // add corresponding weight to exponent
819 INVARIANT(
820 d < (signed)exponent_delta.size(),
821 "depth must be smaller than exponent size");
823 }
824
825 exponent=bv_utils.sub(exponent, exponent_delta);
826
827 #endif
828}
829
832{
833 PRECONDITION(exponent.size() >= spec.e);
834
836
837 // Is the exponent strictly less than -bias+1, i.e., exponent<-bias+1?
838 // This is transformed to distance=(-bias+1)-exponent
839 // i.e., distance>0
840 // Note that 1-bias is the exponent represented by 0...01,
841 // i.e. the exponent of the smallest normal number and thus the 'base'
842 // exponent for subnormal numbers.
843
844#if 1
845 // Need to sign extend to avoid overflow. Note that this is a
846 // relatively rare problem as the value needs to be close to the top
847 // of the exponent range and then range must not have been
848 // previously extended as add, multiply, etc. do. This is primarily
849 // to handle casting down from larger ranges.
850 exponent=bv_utils.sign_extension(exponent, exponent.size() + 1);
851#endif
852
853 bvt distance=bv_utils.sub(
854 bv_utils.build_constant(-bias+1, exponent.size()), exponent);
855
856 // use sign bit
858 !distance.back(),
859 !bv_utils.is_zero(distance));
860
861#if 1
862 // Care must be taken to not loose information required for the
863 // guard and sticky bits. +3 is for the hidden, guard and sticky bits.
864 if(fraction.size() < (spec.f + 3))
865 {
866 // Add zeros at the LSB end for the guard bit to shift into
867 fraction=
868 bv_utils.concatenate(bv_utils.zeros((spec.f + 3) - fraction.size()),
869 fraction);
870 }
871
872 bvt denormalisedFraction=fraction;
873
876 sticky_right_shift(fraction, distance, sticky_bit);
878
879 fraction=
881 denormal,
883 fraction);
884
885#else
886 fraction=
888 denormal,
889 bv_utils.shift(fraction, bv_utilst::LRIGHT, distance),
890 fraction);
891#endif
892
893 exponent=
895 bv_utils.build_constant(-bias, exponent.size()),
896 exponent);
897}
898
900{
901 // incoming: some fraction (with explicit 1),
902 // some exponent without bias
903 // outgoing: rounded, with right size, with hidden bit, bias
904
907
908 {
909 std::size_t exponent_bits = std::max(address_bits(spec.f), spec.e) + 1;
910
911 // before normalization, make sure exponent is large enough
913 {
914 // sign extend
917 }
918 }
919
920 // align it!
923
924 unbiased_floatt result;
927 result.sign=src.sign;
928 result.NaN=src.NaN;
929 result.infinity=src.infinity;
930
931 round_fraction(result);
932 round_exponent(result);
933
934 return pack(bias(result));
935}
936
939 const std::size_t dest_bits,
940 const literalt sign,
941 const bvt &fraction)
942{
943 PRECONDITION(dest_bits < fraction.size());
944
945 // we have too many fraction bits
946 std::size_t extra_bits=fraction.size()-dest_bits;
947
948 // more than two extra bits are superflus, and are
949 // turned into a sticky bit
950
952
953 if(extra_bits>=2)
954 {
955 // We keep most-significant bits, and thus the tail is made
956 // of least-significant bits.
957 bvt tail=bv_utils.extract(fraction, 0, extra_bits-2);
959 }
960
961 // the rounding bit is the last extra bit
962 INVARIANT(
963 extra_bits >= 1, "the extra bits include at least the rounding bit");
964 literalt rounding_bit=fraction[extra_bits-1];
965
966 // we get one bit of the fraction for some rounding decisions
968
969 // round-to-nearest (ties to even)
970 literalt round_to_even=
973
974 // round up
975 literalt round_to_plus_inf=
976 prop.land(!sign,
978
979 // round down
980 literalt round_to_minus_inf=
981 prop.land(sign,
983
984 // round to zero
985 literalt round_to_zero=
986 const_literal(false);
987
988 // now select appropriate one
989 return prop.lselect(rounding_mode_bits.round_to_even, round_to_even,
993 prop.new_variable())))); // otherwise non-det
994}
995
997{
998 std::size_t fraction_size=spec.f+1;
999
1000 // do we need to enlarge the fraction?
1001 if(result.fraction.size()<fraction_size)
1002 {
1003 // pad with zeros at bottom
1004 std::size_t padding=fraction_size-result.fraction.size();
1005
1008 result.fraction);
1009
1010 INVARIANT(
1011 result.fraction.size() == fraction_size,
1012 "sizes should be equal as result.fraction was zero-padded");
1013 }
1014 else if(result.fraction.size()==fraction_size) // it stays
1015 {
1016 // do nothing
1017 }
1018 else // fraction gets smaller -- rounding
1019 {
1020 std::size_t extra_bits=result.fraction.size()-fraction_size;
1021 INVARIANT(
1022 extra_bits >= 1,
1023 "the extra bits should at least include the rounding bit");
1024
1025 // this computes the rounding decision
1027 fraction_size, result.sign, result.fraction);
1028
1029 // chop off all the extra bits
1030 result.fraction=bv_utils.extract(
1031 result.fraction, extra_bits, result.fraction.size()-1);
1032
1033 INVARIANT(
1034 result.fraction.size() == fraction_size,
1035 "sizes should be equal as extra bits were chopped off from "
1036 "result.fraction");
1037
1038#if 0
1039 // *** does not catch when the overflow goes subnormal -> normal ***
1040 // incrementing the fraction might result in an overflow
1041 result.fraction=
1042 bv_utils.zero_extension(result.fraction, result.fraction.size()+1);
1043
1044 result.fraction=bv_utils.incrementer(result.fraction, increment);
1045
1046 literalt overflow=result.fraction.back();
1047
1048 // In case of an overflow, the exponent has to be incremented.
1049 // "Post normalization" is then required.
1050 result.exponent=
1052
1053 // post normalization of the fraction
1054 literalt integer_part1=result.fraction.back();
1055 literalt integer_part0=result.fraction[result.fraction.size()-2];
1057
1058 result.fraction.resize(result.fraction.size()-1);
1059 result.fraction.back()=new_integer_part;
1060
1061#else
1062 // When incrementing due to rounding there are two edge
1063 // cases we need to be aware of:
1064 // 1. If the number is normal, the increment can overflow.
1065 // In this case we need to increment the exponent and
1066 // set the MSB of the fraction to 1.
1067 // 2. If the number is the largest subnormal, the increment
1068 // can change the MSB making it normal. Thus the exponent
1069 // must be incremented but the fraction will be OK.
1070 literalt oldMSB=result.fraction.back();
1071
1072 result.fraction=bv_utils.incrementer(result.fraction, increment);
1073
1074 // Normal overflow when old MSB == 1 and new MSB == 0
1075 literalt overflow=prop.land(oldMSB, neg(result.fraction.back()));
1076
1077 // Subnormal to normal transition when old MSB == 0 and new MSB == 1
1079 prop.land(neg(oldMSB), result.fraction.back());
1080
1081 // In case of an overflow or subnormal to normal conversion,
1082 // the exponent has to be incremented.
1083 result.exponent=
1086
1087 // post normalization of the fraction
1088 // In the case of overflow, set the MSB to 1
1089 // The subnormal case will have (only) the MSB set to 1
1090 result.fraction.back()=prop.lor(result.fraction.back(), overflow);
1091#endif
1092 }
1093}
1094
1096{
1097 PRECONDITION(result.exponent.size() >= spec.e);
1098
1099 // do we need to enlarge the exponent?
1100 if(result.exponent.size() == spec.e) // it stays
1101 {
1102 // do nothing
1103 }
1104 else // exponent gets smaller -- chop off top bits
1105 {
1106 bvt old_exponent=result.exponent;
1107 result.exponent.resize(spec.e);
1108
1109 // max_exponent is the maximum representable
1110 // i.e. 1 higher than the maximum possible for a normal number
1111 bvt max_exponent=
1113 spec.max_exponent()-spec.bias(), old_exponent.size());
1114
1115 // the exponent is garbage if the fractional is zero
1116
1118 prop.land(
1119 !bv_utils.signed_less_than(old_exponent, max_exponent),
1120 !bv_utils.is_zero(result.fraction));
1121
1122#if 1
1123 // Directed rounding modes round overflow to the maximum normal
1124 // depending on the particular mode and the sign
1128 !result.sign),
1130 result.sign)));
1131
1134
1135
1138 spec.max_exponent()-(spec.bias() + 1), result.exponent.size());
1139
1140 result.exponent=
1142
1143 result.fraction=
1145 bv_utils.inverted(bv_utils.zeros(result.fraction.size())),
1146 result.fraction);
1147
1148 result.infinity=prop.lor(result.infinity,
1151#else
1153#endif
1154 }
1155}
1156
1159{
1160 PRECONDITION(src.fraction.size() == spec.f + 1);
1161
1162 biased_floatt result;
1163
1164 result.sign=src.sign;
1165 result.NaN=src.NaN;
1166 result.infinity=src.infinity;
1167
1168 // we need to bias the new exponent
1169 result.exponent=add_bias(src.exponent);
1170
1171 // strip off hidden bit
1172
1173 literalt hidden_bit=src.fraction[src.fraction.size()-1];
1175
1176 result.fraction=src.fraction;
1177 result.fraction.resize(spec.f);
1178
1179 // make exponent zero if its denormal
1180 // (includes zero)
1181 for(std::size_t i=0; i<result.exponent.size(); i++)
1182 result.exponent[i]=
1183 prop.land(result.exponent[i], !denormal);
1184
1185 return result;
1186}
1187
1189{
1190 PRECONDITION(src.size() == spec.e);
1191
1192 return bv_utils.add(
1193 src,
1195}
1196
1198{
1199 PRECONDITION(src.size() == spec.e);
1200
1201 return bv_utils.sub(
1202 src,
1204}
1205
1207{
1208 PRECONDITION(src.size() == spec.width());
1209
1210 unbiased_floatt result;
1211
1212 result.sign=sign_bit(src);
1213
1214 result.fraction=get_fraction(src);
1215 result.fraction.push_back(is_normal(src)); // add hidden bit
1216
1217 result.exponent=get_exponent(src);
1218 CHECK_RETURN(result.exponent.size() == spec.e);
1219
1220 // unbias the exponent
1222
1223 result.exponent=
1226 sub_bias(result.exponent));
1227
1228 result.infinity=is_infinity(src);
1229 result.zero=is_zero(src);
1230 result.NaN=is_NaN(src);
1231
1232 return result;
1233}
1234
1236{
1237 PRECONDITION(src.fraction.size() == spec.f);
1238 PRECONDITION(src.exponent.size() == spec.e);
1239
1240 bvt result;
1241 result.resize(spec.width());
1242
1243 // do sign
1244 // we make this 'false' for NaN
1245 result[result.size()-1]=
1246 prop.lselect(src.NaN, const_literal(false), src.sign);
1247
1249 prop.lor(src.NaN, src.infinity);
1250
1251 // just copy fraction
1252 for(std::size_t i=0; i<spec.f; i++)
1253 result[i]=prop.land(src.fraction[i], !infinity_or_NaN);
1254
1255 result[0]=prop.lor(result[0], src.NaN);
1256
1257 // do exponent
1258 for(std::size_t i=0; i<spec.e; i++)
1259 result[i+spec.f]=prop.lor(
1260 src.exponent[i],
1262
1263 return result;
1264}
1265
1267{
1269
1270 for(std::size_t i=0; i<src.size(); i++)
1271 int_value+=power(2, i)*prop.l_get(src[i]).is_true();
1272
1273 ieee_floatt result;
1274 result.spec=spec;
1275 result.unpack(int_value);
1276
1277 return result;
1278}
1279
1281 const bvt &op,
1282 const bvt &dist,
1284{
1285 std::size_t d=1;
1286 bvt result=op;
1287 sticky=const_literal(false);
1288
1289 for(std::size_t stage=0; stage<dist.size(); stage++)
1290 {
1291 if(dist[stage]!=const_literal(false))
1292 {
1294
1295 bvt lost_bits;
1296
1297 if(d<=result.size())
1298 lost_bits=bv_utils.extract(result, 0, d-1);
1299 else
1300 lost_bits=result;
1301
1302 sticky=prop.lor(
1304 sticky);
1305
1306 result=bv_utils.select(dist[stage], tmp, result);
1307 }
1308
1309 d=d<<1;
1310 }
1311
1312 return result;
1313}
1314
1316 const bvt &src1,
1317 const bvt &)
1318{
1319 return src1;
1320}
1321
1323 const bvt &op0,
1324 const bvt &)
1325{
1326 return op0;
1327}
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
static bvt inverted(const bvt &op)
Definition bv_utils.cpp:577
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
literalt is_all_ones(const bvt &op)
Definition bv_utils.h:153
literalt is_not_zero(const bvt &op)
Definition bv_utils.h:141
static bvt extract_msb(const bvt &a, std::size_t n)
Definition bv_utils.cpp:54
bvt add(const bvt &op0, const bvt &op1)
Definition bv_utils.h:61
bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:182
bvt absolute_value(const bvt &op)
Definition bv_utils.cpp:771
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:92
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition bv_utils.cpp:11
literalt is_zero(const bvt &op)
Definition bv_utils.h:138
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
bvt sign_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:177
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
bvt incrementer(const bvt &op, literalt carry_in)
Definition bv_utils.cpp:569
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition bv_utils.cpp:335
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition bv_utils.cpp:477
static bvt concatenate(const bvt &a, const bvt &b)
Definition bv_utils.cpp:76
bvt sub(const bvt &op0, const bvt &op1)
Definition bv_utils.h:62
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
Definition bv_utils.cpp:38
bvt inc(const bvt &op)
Definition bv_utils.h:33
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
Definition bv_utils.cpp:631
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
Definition bv_utils.cpp:889
bvt cond_negate(const bvt &bv, const literalt cond)
Definition bv_utils.cpp:758
bvt zeros(std::size_t new_size) const
Definition bv_utils.h:187
bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed)
literalt is_NaN(const bvt &)
virtual void normalization_shift(bvt &fraction, bvt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
bvt build_constant(const ieee_floatt &)
bv_utilst bv_utils
bvt debug2(const bvt &op0, const bvt &op1)
virtual bvt rem(const bvt &src1, const bvt &src2)
literalt is_plus_inf(const bvt &)
literalt is_infinity(const bvt &)
void set_rounding_mode(const bvt &)
void round_exponent(unbiased_floatt &result)
void round_fraction(unbiased_floatt &result)
bvt sticky_right_shift(const bvt &op, const bvt &dist, literalt &sticky)
virtual bvt rounder(const unbiased_floatt &)
unbiased_floatt unpack(const bvt &)
bvt from_unsigned_integer(const bvt &)
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt debug1(const bvt &op0, const bvt &op1)
bvt add_bias(const bvt &exponent)
bvt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
bvt get_fraction(const bvt &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
literalt is_minus_inf(const bvt &)
literalt fraction_rounding_decision(const std::size_t dest_bits, const literalt sign, const bvt &fraction)
rounding decision for fraction using sticky bit
bvt get_exponent(const bvt &)
Gets the unbiased exponent in a floating-point bit-vector.
void denormalization_shift(bvt &fraction, bvt &exponent)
make sure exponent is not too small; the exponent is unbiased
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
virtual bvt div(const bvt &src1, const bvt &src2)
bvt negate(const bvt &)
ieee_floatt get(const bvt &) const
literalt exponent_all_zeros(const bvt &)
literalt fraction_all_zeros(const bvt &)
bvt from_signed_integer(const bvt &)
literalt is_zero(const bvt &)
bvt sub(const bvt &src1, const bvt &src2)
bvt sub_bias(const bvt &exponent)
bvt limit_distance(const bvt &dist, mp_integer limit)
Limits the shift distance.
bvt conversion(const bvt &src, const ieee_float_spect &dest_spec)
bvt pack(const biased_floatt &)
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
bvt abs(const bvt &)
static literalt sign_bit(const bvt &src)
Definition float_utils.h:92
ieee_float_spect spec
Definition float_utils.h:88
literalt exponent_all_ones(const bvt &)
bvt to_signed_integer(const bvt &src, std::size_t int_width)
literalt is_normal(const bvt &)
literalt relation(const bvt &src1, relt rel, const bvt &src2)
rounding_mode_bitst rounding_mode_bits
Definition float_utils.h:67
biased_floatt bias(const unbiased_floatt &)
takes an unbiased float, and applies the bias
mp_integer bias() const
mp_integer max_exponent() const
std::size_t f
Definition ieee_float.h:27
std::size_t width() const
Definition ieee_float.h:51
std::size_t e
Definition ieee_float.h:27
const mp_integer & get_exponent() const
Definition ieee_float.h:253
const mp_integer & get_fraction() const
Definition ieee_float.h:254
void unpack(const mp_integer &i)
ieee_float_spect spec
Definition ieee_float.h:135
bool is_NaN() const
Definition ieee_float.h:249
bool get_sign() const
Definition ieee_float.h:248
bool is_infinity() const
Definition ieee_float.h:250
bool is_true() const
Definition literal.h:156
virtual literalt land(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lxor(literalt a, literalt b)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition prop.cpp:20
virtual literalt new_variable()=0
virtual literalt lor(literalt a, literalt b)=0
virtual tvt l_get(literalt a) const =0
literalt neg(literalt a)
Definition literal.h:193
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45