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