cprover
ieee_float.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "ieee_float.h"
10
11#include <limits>
12
13#include "arith_tools.h"
14#include "bitvector_types.h"
15#include "floatbv_expr.h"
16#include "invariant.h"
17#include "std_expr.h"
18
20{
21 return power(2, e-1)-1;
22}
23
25{
26 floatbv_typet result;
27 result.set_f(f);
28 result.set_width(width());
29 if(x86_extended)
30 result.set(ID_x86_extended, true);
31 return result;
32}
33
35{
36 return power(2, e)-1;
37}
38
40{
41 return power(2, f)-1;
42}
43
45{
46 std::size_t width=type.get_width();
47 f=type.get_f();
48 DATA_INVARIANT(f != 0, "mantissa must be at least 1 bit");
50 f < width,
51 "mantissa bits must be less than "
52 "originating type width");
53 e=width-f-1;
54 x86_extended=type.get_bool(ID_x86_extended);
55 if(x86_extended)
56 e=e-1; // no hidden bit
57}
58
60{
61 return floatbv_rounding_mode(static_cast<unsigned>(rm));
62}
63
64void ieee_floatt::print(std::ostream &out) const
65{
66 out << to_ansi_c_string();
67}
68
69std::string ieee_floatt::format(const format_spect &format_spec) const
70{
71 std::string result;
72
73 switch(format_spec.style)
74 {
76 result+=to_string_decimal(format_spec.precision);
77 break;
78
80 result+=to_string_scientific(format_spec.precision);
81 break;
82
84 {
85 // On Linux, the man page says:
86 // "Style e is used if the exponent from its conversion
87 // is less than -4 or greater than or equal to the precision."
88 //
89 // On BSD, it's
90 // "The argument is printed in style f (F) or in style e (E)
91 // whichever gives full precision in minimum space."
92
93 mp_integer _exponent, _fraction;
94 extract_base10(_fraction, _exponent);
95
96 mp_integer adjusted_exponent=base10_digits(_fraction)+_exponent;
97
98 if(adjusted_exponent>=format_spec.precision ||
99 adjusted_exponent<-4)
100 {
101 result+=to_string_scientific(format_spec.precision);
102 }
103 else
104 {
105 result+=to_string_decimal(format_spec.precision);
106
107 // Implementations tested also appear to suppress trailing zeros
108 // and trailing dots.
109
110 {
111 std::size_t trunc_pos=result.find_last_not_of('0');
112 if(trunc_pos!=std::string::npos)
113 result.resize(trunc_pos+1);
114 }
115
116 if(!result.empty() && result.back()=='.')
117 result.resize(result.size()-1);
118 }
119 }
120 break;
121 }
122
123 while(result.size()<format_spec.min_width)
124 result=" "+result;
125
126 return result;
127}
128
130{
131 PRECONDITION(src >= 0);
132 mp_integer tmp=src;
133 mp_integer result=0;
134 while(tmp!=0) { ++result; tmp/=10; }
135 return result;
136}
137
138std::string ieee_floatt::to_string_decimal(std::size_t precision) const
139{
140 std::string result;
141
142 if(sign_flag)
143 result+='-';
144
145 if((NaN_flag || infinity_flag) && !sign_flag)
146 result+='+';
147
148 // special cases
149 if(NaN_flag)
150 result+="NaN";
151 else if(infinity_flag)
152 result+="inf";
153 else if(is_zero())
154 {
155 result+='0';
156
157 // add zeros, if needed
158 if(precision>0)
159 {
160 result+='.';
161 for(std::size_t i=0; i<precision; i++)
162 result+='0';
163 }
164 }
165 else
166 {
167 mp_integer _exponent, _fraction;
168 extract_base2(_fraction, _exponent);
169
170 // convert to base 10
171 if(_exponent>=0)
172 {
173 result+=integer2string(_fraction*power(2, _exponent));
174
175 // add dot and zeros, if needed
176 if(precision>0)
177 {
178 result+='.';
179 for(std::size_t i=0; i<precision; i++)
180 result+='0';
181 }
182 }
183 else
184 {
185 #if 1
186 mp_integer position=-_exponent;
187
188 // 10/2=5 -- this makes it base 10
189 _fraction*=power(5, position);
190
191 // apply rounding
192 if(position>precision)
193 {
194 mp_integer r=power(10, position-precision);
195 mp_integer remainder=_fraction%r;
196 _fraction/=r;
197 // not sure if this is the right kind of rounding here
198 if(remainder>=r/2)
199 ++_fraction;
200 position=precision;
201 }
202
203 std::string tmp=integer2string(_fraction);
204
205 // pad with zeros from the front, if needed
206 while(mp_integer(tmp.size())<=position) tmp="0"+tmp;
207
208 const std::size_t dot =
209 tmp.size() - numeric_cast_v<std::size_t>(position);
210 result+=std::string(tmp, 0, dot)+'.';
211 result+=std::string(tmp, dot, std::string::npos);
212
213 // append zeros if needed
214 for(mp_integer i=position; i<precision; ++i)
215 result+='0';
216 #else
217
218 result+=integer2string(_fraction);
219
220 if(_exponent!=0)
221 result+="*2^"+integer2string(_exponent);
222
223 #endif
224 }
225 }
226
227 return result;
228}
229
232std::string ieee_floatt::to_string_scientific(std::size_t precision) const
233{
234 std::string result;
235
236 if(sign_flag)
237 result+='-';
238
239 if((NaN_flag || infinity_flag) && !sign_flag)
240 result+='+';
241
242 // special cases
243 if(NaN_flag)
244 result+="NaN";
245 else if(infinity_flag)
246 result+="inf";
247 else if(is_zero())
248 {
249 result+='0';
250
251 // add zeros, if needed
252 if(precision>0)
253 {
254 result+='.';
255 for(std::size_t i=0; i<precision; i++)
256 result+='0';
257 }
258
259 result+="e0";
260 }
261 else
262 {
263 mp_integer _exponent, _fraction;
264 extract_base10(_fraction, _exponent);
265
266 // C99 appears to say that conversion to decimal should
267 // use the currently selected IEEE rounding mode.
268 if(base10_digits(_fraction)>precision+1)
269 {
270 // re-align
271 mp_integer distance=base10_digits(_fraction)-(precision+1);
272 mp_integer p=power(10, distance);
273 mp_integer remainder=_fraction%p;
274 _fraction/=p;
275 _exponent+=distance;
276
277 if(remainder==p/2)
278 {
279 // need to do rounding mode here
280 ++_fraction;
281 }
282 else if(remainder>p/2)
283 ++_fraction;
284 }
285
286 std::string decimals=integer2string(_fraction);
287
288 CHECK_RETURN(!decimals.empty());
289
290 // First add top digit to result.
291 result+=decimals[0];
292
293 // Now add dot and further zeros, if needed.
294 if(precision>0)
295 {
296 result+='.';
297
298 while(decimals.size()<precision+1)
299 decimals+='0';
300
301 result+=decimals.substr(1, precision);
302 }
303
304 // add exponent
305 result+='e';
306
307 std::string exponent_str=
308 integer2string(base10_digits(_fraction)+_exponent-1);
309
310 if(!exponent_str.empty() && exponent_str[0]!='-')
311 result+='+';
312
313 result+=exponent_str;
314 }
315
316 return result;
317}
318
320{
321 PRECONDITION(spec.f != 0);
322 PRECONDITION(spec.e != 0);
323
324 {
325 mp_integer tmp=i;
326
327 // split this apart
328 mp_integer pf=power(2, spec.f);
329 fraction=tmp%pf;
330 tmp/=pf;
331
332 mp_integer pe=power(2, spec.e);
333 exponent=tmp%pe;
334 tmp/=pe;
335
336 sign_flag=(tmp!=0);
337 }
338
339 // NaN?
341 {
342 make_NaN();
343 }
344 else if(exponent==spec.max_exponent() && fraction==0) // Infinity
345 {
346 NaN_flag=false;
347 infinity_flag=true;
348 }
349 else if(exponent==0 && fraction==0) // zero
350 {
351 NaN_flag=false;
352 infinity_flag=false;
353 }
354 else if(exponent==0) // denormal?
355 {
356 NaN_flag=false;
357 infinity_flag=false;
358 exponent=-spec.bias()+1; // NOT -spec.bias()!
359 }
360 else // normal
361 {
362 NaN_flag=false;
363 infinity_flag=false;
364 fraction+=power(2, spec.f); // hidden bit!
365 exponent-=spec.bias(); // un-bias
366 }
367}
368
370{
371 return fraction>=power(2, spec.f);
372}
373
375{
376 mp_integer result=0;
377
378 // sign bit
379 if(sign_flag)
380 result+=power(2, spec.e+spec.f);
381
382 if(NaN_flag)
383 {
384 result+=power(2, spec.f)*spec.max_exponent();
385 result+=1;
386 }
387 else if(infinity_flag)
388 {
389 result+=power(2, spec.f)*spec.max_exponent();
390 }
391 else if(fraction==0 && exponent==0)
392 {
393 // zero
394 }
395 else if(is_normal()) // normal?
396 {
397 // fraction -- need to hide hidden bit
398 result+=fraction-power(2, spec.f); // hidden bit
399
400 // exponent -- bias!
401 result+=power(2, spec.f)*(exponent+spec.bias());
402 }
403 else // denormal
404 {
405 result+=fraction; // denormal -- no hidden bit
406 // the exponent is zero
407 }
408
409 return result;
410}
411
413 mp_integer &_fraction,
414 mp_integer &_exponent) const
415{
416 if(is_zero() || is_NaN() || is_infinity())
417 {
418 _fraction=_exponent=0;
419 return;
420 }
421
422 _exponent=exponent;
423 _fraction=fraction;
424
425 // adjust exponent
426 _exponent-=spec.f;
427
428 // try to integer-ize
429 while((_fraction%2)==0)
430 {
431 _fraction/=2;
432 ++_exponent;
433 }
434}
435
437 mp_integer &_fraction,
438 mp_integer &_exponent) const
439{
440 if(is_zero() || is_NaN() || is_infinity())
441 {
442 _fraction=_exponent=0;
443 return;
444 }
445
446 _exponent=exponent;
447 _fraction=fraction;
448
449 // adjust exponent
450 _exponent-=spec.f;
451
452 // now make it base 10
453 if(_exponent>=0)
454 {
455 _fraction*=power(2, _exponent);
456 _exponent=0;
457 }
458 else // _exponent<0
459 {
460 // 10/2=5 -- this makes it base 10
461 _fraction*=power(5, -_exponent);
462 }
463
464 // try to re-normalize
465 while((_fraction%10)==0)
466 {
467 _fraction/=10;
468 ++_exponent;
469 }
470}
471
473 const mp_integer &_fraction,
474 const mp_integer &_exponent)
475{
476 sign_flag=_fraction<0;
477 fraction=_fraction;
478 if(sign_flag)
480 exponent=_exponent;
481 exponent+=spec.f;
482 align();
483}
484
487 const mp_integer &_fraction,
488 const mp_integer &_exponent)
489{
491 sign_flag=_fraction<0;
492 fraction=_fraction;
493 if(sign_flag)
496 exponent+=_exponent;
497
498 if(_exponent<0)
499 {
500 // bring to max. precision
501 mp_integer e_power=power(2, spec.e);
502 fraction*=power(2, e_power);
503 exponent-=e_power;
504 fraction/=power(5, -_exponent);
505 }
506 else if(_exponent>0)
507 {
508 // fix base
509 fraction*=power(5, _exponent);
510 }
511
512 align();
513}
514
516{
519 fraction=i;
520 align();
521}
522
524{
525 // NaN?
526 if(NaN_flag)
527 {
528 fraction=0;
529 exponent=0;
530 sign_flag=false;
531 return;
532 }
533
534 // do sign
535 if(fraction<0)
536 {
539 }
540
541 // zero?
542 if(fraction==0)
543 {
544 exponent=0;
545 return;
546 }
547
548 // 'usual case'
549 mp_integer f_power=power(2, spec.f);
550 mp_integer f_power_next=power(2, spec.f+1);
551
552 std::size_t lowPower2=fraction.floorPow2();
553 mp_integer exponent_offset=0;
554
555 if(lowPower2<spec.f) // too small
556 {
557 exponent_offset-=(spec.f-lowPower2);
558
559 INVARIANT(
560 fraction * power(2, (spec.f - lowPower2)) >= f_power,
561 "normalisation result must be >= lower bound");
562 INVARIANT(
563 fraction * power(2, (spec.f - lowPower2)) < f_power_next,
564 "normalisation result must be < upper bound");
565 }
566 else if(lowPower2>spec.f) // too large
567 {
568 exponent_offset+=(lowPower2-spec.f);
569
570 INVARIANT(
571 fraction / power(2, (lowPower2 - spec.f)) >= f_power,
572 "normalisation result must be >= lower bound");
573 INVARIANT(
574 fraction / power(2, (lowPower2 - spec.f)) < f_power_next,
575 "normalisation result must be < upper bound");
576 }
577
578 mp_integer biased_exponent=exponent+exponent_offset+spec.bias();
579
580 // exponent too large (infinity)?
581 if(biased_exponent>=spec.max_exponent())
582 {
583 // we need to consider the rounding mode here
584 switch(rounding_mode)
585 {
586 case UNKNOWN:
587 case NONDETERMINISTIC:
588 case ROUND_TO_EVEN:
589 infinity_flag=true;
590 break;
591
593 // the result of the rounding is never larger than the argument
594 if(sign_flag)
595 infinity_flag=true;
596 else
597 make_fltmax();
598 break;
599
601 // the result of the rounding is never smaller than the argument
602 if(sign_flag)
603 {
604 make_fltmax();
605 sign_flag=true; // restore sign
606 }
607 else
608 infinity_flag=true;
609 break;
610
611 case ROUND_TO_ZERO:
612 if(sign_flag)
613 {
614 make_fltmax();
615 sign_flag=true; // restore sign
616 }
617 else
618 make_fltmax(); // positive
619 break;
620 }
621
622 return; // done
623 }
624 else if(biased_exponent<=0) // exponent too small?
625 {
626 // produce a denormal (or zero)
627 mp_integer new_exponent=mp_integer(1)-spec.bias();
628 exponent_offset=new_exponent-exponent;
629 }
630
631 exponent+=exponent_offset;
632
633 if(exponent_offset>0)
634 {
635 divide_and_round(fraction, power(2, exponent_offset));
636
637 // rounding might make the fraction too big!
638 if(fraction==f_power_next)
639 {
640 fraction=f_power;
641 ++exponent;
642 }
643 }
644 else if(exponent_offset<0)
645 fraction*=power(2, -exponent_offset);
646
647 if(fraction==0)
648 exponent=0;
649}
650
652 mp_integer &dividend,
653 const mp_integer &divisor)
654{
655 const mp_integer remainder = dividend % divisor;
656 dividend /= divisor;
657
658 if(remainder!=0)
659 {
660 switch(rounding_mode)
661 {
662 case ROUND_TO_EVEN:
663 {
664 mp_integer divisor_middle = divisor / 2;
665 if(remainder < divisor_middle)
666 {
667 // crop
668 }
669 else if(remainder > divisor_middle)
670 {
671 ++dividend;
672 }
673 else // exactly in the middle -- go to even
674 {
675 if((dividend % 2) != 0)
676 ++dividend;
677 }
678 }
679 break;
680
681 case ROUND_TO_ZERO:
682 // this means just crop
683 break;
684
686 if(sign_flag)
687 ++dividend;
688 break;
689
691 if(!sign_flag)
692 ++dividend;
693 break;
694
695 case NONDETERMINISTIC:
696 case UNKNOWN:
698 }
699 }
700}
701
703{
705}
706
708{
709 PRECONDITION(other.spec.f == spec.f);
710
711 // NaN/x = NaN
712 if(NaN_flag)
713 return *this;
714
715 // x/NaN = NaN
716 if(other.NaN_flag)
717 {
718 make_NaN();
719 return *this;
720 }
721
722 // 0/0 = NaN
723 if(is_zero() && other.is_zero())
724 {
725 make_NaN();
726 return *this;
727 }
728
729 // x/0 = +-inf
730 if(other.is_zero())
731 {
732 infinity_flag=true;
733 if(other.sign_flag)
734 negate();
735 return *this;
736 }
737
738 // x/inf = NaN
739 if(other.infinity_flag)
740 {
741 if(infinity_flag)
742 {
743 make_NaN();
744 return *this;
745 }
746
747 bool old_sign=sign_flag;
748 make_zero();
749 sign_flag=old_sign;
750
751 if(other.sign_flag)
752 negate();
753
754 return *this;
755 } // inf/x = inf
756 else if(infinity_flag)
757 {
758 if(other.sign_flag)
759 negate();
760
761 return *this;
762 }
763
764 exponent-=other.exponent;
765 fraction*=power(2, spec.f);
766
767 // to account for error
768 fraction*=power(2, spec.f);
769 exponent-=spec.f;
770
771 fraction/=other.fraction;
772
773 if(other.sign_flag)
774 negate();
775
776 align();
777
778 return *this;
779}
780
782{
783 PRECONDITION(other.spec.f == spec.f);
784
785 if(other.NaN_flag)
786 make_NaN();
787 if(NaN_flag)
788 return *this;
789
790 if(infinity_flag || other.infinity_flag)
791 {
792 if(is_zero() || other.is_zero())
793 {
794 // special case Inf * 0 is NaN
795 make_NaN();
796 return *this;
797 }
798
799 if(other.sign_flag)
800 negate();
801 infinity_flag=true;
802 return *this;
803 }
804
805 exponent+=other.exponent;
806 exponent-=spec.f;
807 fraction*=other.fraction;
808
809 if(other.sign_flag)
810 negate();
811
812 align();
813
814 return *this;
815}
816
818{
819 PRECONDITION(other.spec == spec);
820 ieee_floatt _other=other;
821
822 if(other.NaN_flag)
823 make_NaN();
824 if(NaN_flag)
825 return *this;
826
827 if(infinity_flag && other.infinity_flag)
828 {
829 if(sign_flag==other.sign_flag)
830 return *this;
831 make_NaN();
832 return *this;
833 }
834 else if(infinity_flag)
835 return *this;
836 else if(other.infinity_flag)
837 {
838 infinity_flag=true;
839 sign_flag=other.sign_flag;
840 return *this;
841 }
842
843 // 0 + 0 needs special treatment for the signs
844 if(is_zero() && other.is_zero())
845 {
846 if(get_sign()==other.get_sign())
847 return *this;
848 else
849 {
851 {
852 set_sign(true);
853 return *this;
854 }
855 else
856 {
857 set_sign(false);
858 return *this;
859 }
860 }
861 }
862
863 // get smaller exponent
864 if(_other.exponent<exponent)
865 {
866 fraction*=power(2, exponent-_other.exponent);
867 exponent=_other.exponent;
868 }
869 else if(exponent<_other.exponent)
870 {
871 _other.fraction*=power(2, _other.exponent-exponent);
872 _other.exponent=exponent;
873 }
874
875 INVARIANT(
876 exponent == _other.exponent,
877 "prior block equalises the exponents by setting both to the "
878 "minimum of their previous values while adjusting the mantissa");
879
880 if(sign_flag)
881 fraction.negate();
882 if(_other.sign_flag)
883 _other.fraction.negate();
884
885 fraction+=_other.fraction;
886
887 // if the result is zero,
888 // there is some set of rules to get the sign
889 if(fraction==0)
890 {
892 sign_flag=true;
893 else
894 sign_flag=false;
895 }
896 else // fraction!=0
897 {
899 if(sign_flag)
900 fraction.negate();
901 }
902
903 align();
904
905 return *this;
906}
907
909{
910 ieee_floatt _other=other;
911 _other.sign_flag=!_other.sign_flag;
912 return (*this)+=_other;
913}
914
915bool ieee_floatt::operator<(const ieee_floatt &other) const
916{
917 if(NaN_flag || other.NaN_flag)
918 return false;
919
920 // check both zero?
921 if(is_zero() && other.is_zero())
922 return false;
923
924 // one of them zero?
925 if(is_zero())
926 return !other.sign_flag;
927 else if(other.is_zero())
928 return sign_flag;
929
930 // check sign
931 if(sign_flag!=other.sign_flag)
932 return sign_flag;
933
934 // handle infinity
935 if(infinity_flag)
936 {
937 if(other.infinity_flag)
938 return false;
939 else
940 return sign_flag;
941 }
942 else if(other.infinity_flag)
943 return !sign_flag;
944
945 // check exponent
946 if(exponent!=other.exponent)
947 {
948 if(sign_flag) // both negative
949 return exponent>other.exponent;
950 else
951 return exponent<other.exponent;
952 }
953
954 // check significand
955 if(sign_flag) // both negative
956 return fraction>other.fraction;
957 else
958 return fraction<other.fraction;
959}
960
961bool ieee_floatt::operator<=(const ieee_floatt &other) const
962{
963 if(NaN_flag || other.NaN_flag)
964 return false;
965
966 // check zero
967 if(is_zero() && other.is_zero())
968 return true;
969
970 // handle infinity
971 if(infinity_flag && other.infinity_flag &&
972 sign_flag==other.sign_flag)
973 return true;
974
975 if(!infinity_flag && !other.infinity_flag &&
976 sign_flag==other.sign_flag &&
977 exponent==other.exponent &&
978 fraction==other.fraction)
979 return true;
980
981 return *this<other;
982}
983
984bool ieee_floatt::operator>(const ieee_floatt &other) const
985{
986 return other<*this;
987}
988
989bool ieee_floatt::operator>=(const ieee_floatt &other) const
990{
991 return other<=*this;
992}
993
994bool ieee_floatt::operator==(const ieee_floatt &other) const
995{
996 // packed equality!
997 if(NaN_flag && other.NaN_flag)
998 return true;
999 else if(NaN_flag || other.NaN_flag)
1000 return false;
1001
1002 if(infinity_flag && other.infinity_flag &&
1003 sign_flag==other.sign_flag)
1004 return true;
1005 else if(infinity_flag || other.infinity_flag)
1006 return false;
1007
1008 // if(a.is_zero() && b.is_zero()) return true;
1009
1010 return
1011 exponent==other.exponent &&
1012 fraction==other.fraction &&
1013 sign_flag==other.sign_flag;
1014}
1015
1016bool ieee_floatt::ieee_equal(const ieee_floatt &other) const
1017{
1018 if(NaN_flag || other.NaN_flag)
1019 return false;
1020 if(is_zero() && other.is_zero())
1021 return true;
1022 PRECONDITION(spec == other.spec);
1023 return *this==other;
1024}
1025
1027{
1028 ieee_floatt other(spec);
1029 other.from_integer(i);
1030 return *this==other;
1031}
1032
1033bool ieee_floatt::operator!=(const ieee_floatt &other) const
1034{
1035 return !(*this==other);
1036}
1037
1039{
1040 if(NaN_flag || other.NaN_flag)
1041 return true; // !!!
1042 if(is_zero() && other.is_zero())
1043 return false;
1044 PRECONDITION(spec == other.spec);
1045 return *this!=other;
1046}
1047
1049{
1050 mp_integer _exponent=exponent-spec.f;
1051 mp_integer _fraction=fraction;
1052
1053 if(sign_flag)
1054 _fraction.negate();
1055
1056 spec=dest_spec;
1057
1058 if(_fraction==0)
1059 {
1060 // We have a zero. It stays a zero.
1061 // Don't call build to preserve sign.
1062 }
1063 else
1064 build(_fraction, _exponent);
1065}
1066
1068{
1070 unpack(bvrep2integer(expr.get_value(), spec.width(), false));
1071}
1072
1074{
1075 if(NaN_flag || infinity_flag || is_zero())
1076 return 0;
1077
1078 mp_integer result=fraction;
1079
1080 mp_integer new_exponent=exponent-spec.f;
1081
1082 // if the exponent is negative, divide
1083 if(new_exponent<0)
1084 result/=power(2, -new_exponent);
1085 else
1086 result*=power(2, new_exponent); // otherwise, multiply
1087
1088 if(sign_flag)
1089 result.negate();
1090
1091 return result;
1092}
1093
1094void ieee_floatt::from_double(const double d)
1095{
1096 spec.f=52;
1097 spec.e=11;
1098 DATA_INVARIANT(spec.width() == 64, "width must be 64 bits");
1099
1100 static_assert(
1101 std::numeric_limits<double>::is_iec559,
1102 "this requires the double layout is according to the ieee754 "
1103 "standard");
1104 static_assert(
1105 sizeof(double) == sizeof(std::uint64_t), "ensure double has 64 bit width");
1106
1107 union
1108 {
1109 double d;
1110 std::uint64_t i;
1111 } u;
1112
1113 u.d=d;
1114
1115 unpack(u.i);
1116}
1117
1118void ieee_floatt::from_float(const float f)
1119{
1120 spec.f=23;
1121 spec.e=8;
1122 DATA_INVARIANT(spec.width() == 32, "width must be 32 bits");
1123
1124 static_assert(
1125 std::numeric_limits<float>::is_iec559,
1126 "this requires the float layout is according to the ieee754 "
1127 "standard");
1128 static_assert(
1129 sizeof(float) == sizeof(std::uint32_t), "ensure float has 32 bit width");
1130
1131 union
1132 {
1133 float f;
1134 std::uint32_t i;
1135 } u;
1136
1137 u.f=f;
1138
1139 unpack(u.i);
1140}
1141
1143{
1144 NaN_flag=true;
1145 // sign=false;
1146 exponent=0;
1147 fraction=0;
1148 infinity_flag=false;
1149}
1150
1152{
1153 mp_integer bit_pattern=
1154 power(2, spec.e+spec.f)-1-power(2, spec.f);
1155 unpack(bit_pattern);
1156}
1157
1159{
1160 unpack(power(2, spec.f));
1161}
1162
1164{
1165 NaN_flag=false;
1166 sign_flag=false;
1167 exponent=0;
1168 fraction=0;
1169 infinity_flag=true;
1170}
1171
1173{
1175 sign_flag=true;
1176}
1177
1179{
1180 return spec.f==52 && spec.e==11;
1181}
1182
1184{
1185 return spec.f==23 && spec.e==8;
1186}
1187
1191{
1193 union { double f; uint64_t i; } a;
1194
1195 if(infinity_flag)
1196 {
1197 if(sign_flag)
1198 return -std::numeric_limits<double>::infinity();
1199 else
1200 return std::numeric_limits<double>::infinity();
1201 }
1202
1203 if(NaN_flag)
1204 {
1205 if(sign_flag)
1206 return -std::numeric_limits<double>::quiet_NaN();
1207 else
1208 return std::numeric_limits<double>::quiet_NaN();
1209 }
1210
1211 mp_integer i=pack();
1212 CHECK_RETURN(i.is_ulong());
1213 CHECK_RETURN(i <= std::numeric_limits<std::uint64_t>::max());
1214
1215 a.i=i.to_ulong();
1216 return a.f;
1217}
1218
1222{
1223 // if false - ieee_floatt::to_float not supported on this architecture
1224 static_assert(
1225 std::numeric_limits<float>::is_iec559,
1226 "this requires the float layout is according to the IEC 559/IEEE 754 "
1227 "standard");
1228 static_assert(
1229 sizeof(float) == sizeof(uint32_t), "a 32 bit float type is required");
1230
1231 union { float f; uint32_t i; } a;
1232
1233 if(infinity_flag)
1234 {
1235 if(sign_flag)
1236 return -std::numeric_limits<float>::infinity();
1237 else
1238 return std::numeric_limits<float>::infinity();
1239 }
1240
1241 if(NaN_flag)
1242 {
1243 if(sign_flag)
1244 return -std::numeric_limits<float>::quiet_NaN();
1245 else
1246 return std::numeric_limits<float>::quiet_NaN();
1247 }
1248
1249 a.i = numeric_cast_v<uint32_t>(pack());
1250 return a.f;
1251}
1252
1256{
1257 if(is_NaN())
1258 return;
1259
1260 bool old_sign=get_sign();
1261
1262 if(is_zero())
1263 {
1264 unpack(1);
1265 set_sign(!greater);
1266
1267 return;
1268 }
1269
1270 if(is_infinity())
1271 {
1272 if(get_sign()==greater)
1273 {
1274 make_fltmax();
1275 set_sign(old_sign);
1276 }
1277 return;
1278 }
1279
1280 bool dir;
1281 if(greater)
1282 dir=!get_sign();
1283 else
1284 dir=get_sign();
1285
1286 set_sign(false);
1287
1288 mp_integer old=pack();
1289 if(dir)
1290 ++old;
1291 else
1292 --old;
1293
1294 unpack(old);
1295
1296 // sign change impossible (zero case caught earlier)
1297 set_sign(old_sign);
1298}
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
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.
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
void set_width(std::size_t width)
Definition: std_types.h:869
std::size_t get_width() const
Definition: std_types.h:864
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
typet & type()
Return the type of the expression.
Definition: expr.h:82
Fixed-width bit-vector with IEEE floating-point interpretation.
void set_f(std::size_t b)
std::size_t get_f() const
stylet style
Definition: format_spec.h:28
unsigned precision
Definition: format_spec.h:19
unsigned min_width
Definition: format_spec.h:18
mp_integer max_fraction() const
Definition: ieee_float.cpp:39
class floatbv_typet to_type() const
Definition: ieee_float.cpp:24
mp_integer bias() const
Definition: ieee_float.cpp:19
mp_integer max_exponent() const
Definition: ieee_float.cpp:34
void from_type(const floatbv_typet &type)
Definition: ieee_float.cpp:44
static ieee_float_spect double_precision()
Definition: ieee_float.h:77
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
bool is_double() const
ieee_floatt & operator*=(const ieee_floatt &other)
Definition: ieee_float.cpp:781
void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const
Definition: ieee_float.cpp:436
void make_minus_infinity()
void make_fltmax()
void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const
Definition: ieee_float.cpp:412
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:319
ieee_float_spect spec
Definition: ieee_float.h:135
mp_integer exponent
Definition: ieee_float.h:322
mp_integer to_integer() const
std::string to_ansi_c_string() const
Definition: ieee_float.h:281
bool is_NaN() const
Definition: ieee_float.h:249
void make_plus_infinity()
bool operator!=(const ieee_floatt &other) const
bool ieee_equal(const ieee_floatt &other) const
ieee_floatt & operator+=(const ieee_floatt &other)
Definition: ieee_float.cpp:817
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
void divide_and_round(mp_integer &dividend, const mp_integer &divisor)
Definition: ieee_float.cpp:651
bool is_float() const
bool get_sign() const
Definition: ieee_float.h:248
void make_zero()
Definition: ieee_float.h:187
void set_sign(bool _sign)
Definition: ieee_float.h:184
void from_float(const float f)
bool NaN_flag
Definition: ieee_float.h:324
void from_expr(const constant_exprt &expr)
bool operator==(const ieee_floatt &other) const
Definition: ieee_float.cpp:994
static constant_exprt rounding_mode_expr(rounding_modet)
Definition: ieee_float.cpp:59
bool operator<=(const ieee_floatt &other) const
Definition: ieee_float.cpp:961
std::string to_string_scientific(std::size_t precision) const
format as [-]d.ddde+-d Note that printf always produces at least two digits for the exponent.
Definition: ieee_float.cpp:232
std::string to_string_decimal(std::size_t precision) const
Definition: ieee_float.cpp:138
void negate()
Definition: ieee_float.h:179
void make_NaN()
bool sign_flag
Definition: ieee_float.h:321
ieee_floatt & operator-=(const ieee_floatt &other)
Definition: ieee_float.cpp:908
bool operator>(const ieee_floatt &other) const
Definition: ieee_float.cpp:984
void next_representable(bool greater)
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinit...
bool ieee_not_equal(const ieee_floatt &other) const
bool infinity_flag
Definition: ieee_float.h:324
bool is_zero() const
Definition: ieee_float.h:244
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
ieee_floatt & operator/=(const ieee_floatt &other)
Definition: ieee_float.cpp:707
bool operator>=(const ieee_floatt &other) const
Definition: ieee_float.cpp:989
std::string format(const format_spect &format_spec) const
Definition: ieee_float.cpp:69
bool is_infinity() const
Definition: ieee_float.h:250
void make_fltmin()
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:515
rounding_modet rounding_mode
Definition: ieee_float.h:133
static mp_integer base10_digits(const mp_integer &src)
Definition: ieee_float.cpp:129
bool is_normal() const
Definition: ieee_float.cpp:369
mp_integer pack() const
Definition: ieee_float.cpp:374
mp_integer fraction
Definition: ieee_float.h:323
@ NONDETERMINISTIC
Definition: ieee_float.h:127
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:126
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:125
void build(const mp_integer &exp, const mp_integer &frac)
Definition: ieee_float.cpp:472
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
Definition: ieee_float.cpp:486
void from_double(const double d)
bool operator<(const ieee_floatt &other) const
Definition: ieee_float.cpp:915
void change_spec(const ieee_float_spect &dest_spec)
void align()
Definition: ieee_float.cpp:523
void print(std::ostream &out) const
Definition: ieee_float.cpp:64
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:353
constant_exprt floatbv_rounding_mode(unsigned rm)
returns the a rounding mode expression for a given IEEE rounding mode, encoded using the recommendati...
API to expression classes for floating-point arithmetic.
static int8_t r
Definition: irep_hash.h:60
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.