CBMC: /home/runner/work/cbmc/cbmc/src/util/ieee_float.cpp Source File

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

AltStyle によって変換されたページ (->オリジナル) /