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