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