cprover
ieee_float.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_IEEE_FLOAT_H
11 #define CPROVER_UTIL_IEEE_FLOAT_H
12 
13 #include <iosfwd>
14 
15 #include "mp_arith.h"
16 #include "format_spec.h"
17 #include "irep.h"
18 #include "cprover_prefix.h"
19 
20 class constant_exprt;
21 class floatbv_typet;
22 
23 const char ID_cprover_rounding_mode_str[] = CPROVER_PREFIX "rounding_mode";
24 
26 {
27 public:
28  // Number of bits for fraction (excluding hidden bit)
29  // and exponent, respectively
30  std::size_t f, e;
31 
32  // x86 has an extended precision format with an explicit
33  // integer bit.
35 
36  mp_integer bias() const;
37 
38  explicit ieee_float_spect(const floatbv_typet &type)
39  {
40  from_type(type);
41  }
42 
43  void from_type(const floatbv_typet &type);
44 
45  ieee_float_spect():f(0), e(0), x86_extended(false)
46  {
47  }
48 
49  ieee_float_spect(std::size_t _f, std::size_t _e):
50  f(_f), e(_e), x86_extended(false)
51  {
52  }
53 
54  std::size_t width() const
55  {
56  // Add one for the sign bit.
57  // Add one if x86 explicit integer bit is used.
58  return f+e+1+(x86_extended?1:0);
59  }
60 
61  mp_integer max_exponent() const;
62  mp_integer max_fraction() const;
63 
64  class floatbv_typet to_type() const;
65 
66  // this is binary16 in IEEE 754-2008
68  {
69  // 16 bits in total
70  return ieee_float_spect(10, 5);
71  }
72 
73  // the well-know standard formats
75  {
76  // 32 bits in total
77  return ieee_float_spect(23, 8);
78  }
79 
81  {
82  // 64 bits in total
83  return ieee_float_spect(52, 11);
84  }
85 
87  {
88  // IEEE 754 binary128
89  return ieee_float_spect(112, 15);
90  }
91 
93  {
94  // Intel, not IEEE
95  ieee_float_spect result(63, 15);
96  result.x86_extended=true;
97  return result;
98  }
99 
101  {
102  // Intel, not IEEE
103  ieee_float_spect result(63, 15);
104  result.x86_extended=true;
105  return result;
106  }
107 
108  bool operator==(const ieee_float_spect &other) const
109  {
110  return f==other.f && e==other.e && x86_extended==other.x86_extended;
111  }
112 
113  bool operator!=(const ieee_float_spect &other) const
114  {
115  return !(*this==other);
116  }
117 };
118 
120 {
121 public:
122  // ROUND_TO_EVEN is also known as "round to nearest, ties to even", and
123  // is the IEEE default.
124  // The numbering below is what x86 uses in the control word.
126  {
130  };
131 
133 
135 
136  explicit ieee_floatt(const ieee_float_spect &_spec):
138  spec(_spec), sign_flag(false), exponent(0), fraction(0),
139  NaN_flag(false), infinity_flag(false)
140  {
141  }
142 
143  explicit ieee_floatt(const floatbv_typet &type):
145  spec(ieee_float_spect(type)),
146  sign_flag(false),
147  exponent(0),
148  fraction(0),
149  NaN_flag(false),
150  infinity_flag(false)
151  {
152  }
153 
156  sign_flag(false), exponent(0), fraction(0),
157  NaN_flag(false), infinity_flag(false)
158  {
159  }
160 
161  explicit ieee_floatt(const constant_exprt &expr):
163  {
164  from_expr(expr);
165  }
166 
167  void negate()
168  {
170  }
171 
172  void set_sign(bool _sign)
173  { sign_flag = _sign; }
174 
175  void make_zero()
176  {
177  sign_flag=false;
178  exponent=0;
179  fraction=0;
180  NaN_flag=false;
181  infinity_flag=false;
182  }
183 
184  static ieee_floatt zero(const floatbv_typet &type)
185  {
186  ieee_floatt result(type);
187  result.make_zero();
188  return result;
189  }
190 
191  void make_NaN();
192  void make_plus_infinity();
193  void make_minus_infinity();
194  void make_fltmax(); // maximum representable finite floating-point number
195  void make_fltmin(); // minimum normalized positive floating-point number
196 
197  static ieee_floatt NaN(const ieee_float_spect &_spec)
198  { ieee_floatt c(_spec); c.make_NaN(); return c; }
199 
201  { ieee_floatt c(_spec); c.make_plus_infinity(); return c; }
202 
204  { ieee_floatt c(_spec); c.make_minus_infinity(); return c; }
205 
206  // maximum representable finite floating-point number
207  static ieee_floatt fltmax(const ieee_float_spect &_spec)
208  { ieee_floatt c(_spec); c.make_fltmax(); return c; }
209 
210  // minimum normalized positive floating-point number
211  static ieee_floatt fltmin(const ieee_float_spect &_spec)
212  { ieee_floatt c(_spec); c.make_fltmin(); return c; }
213 
214  // set to next representable number towards plus infinity
215  void increment(bool distinguish_zero=false)
216  {
217  if(is_zero() && get_sign() && distinguish_zero)
218  negate();
219  else
220  next_representable(true);
221  }
222 
223  // set to previous representable number towards minus infinity
224  void decrement(bool distinguish_zero=false)
225  {
226  if(is_zero() && !get_sign() && distinguish_zero)
227  negate();
228  else
229  next_representable(false);
230  }
231 
232  bool is_zero() const
233  {
234  return !NaN_flag && !infinity_flag && fraction==0 && exponent==0;
235  }
236  bool get_sign() const { return sign_flag; }
237  bool is_NaN() const { return NaN_flag; }
238  bool is_infinity() const { return !NaN_flag && infinity_flag; }
239  bool is_normal() const;
240 
241  const mp_integer &get_exponent() const { return exponent; }
242  const mp_integer &get_fraction() const { return fraction; }
243 
244  // performs conversion to IEEE floating point format
245  void from_integer(const mp_integer &i);
246  void from_base10(const mp_integer &exp, const mp_integer &frac);
247  void build(const mp_integer &exp, const mp_integer &frac);
248  void unpack(const mp_integer &i);
249  void from_double(const double d);
250  void from_float(const float f);
251 
252  // performs conversions from IEEE float-point format
253  // to something else
254  double to_double() const;
255  float to_float() const;
256  bool is_double() const;
257  bool is_float() const;
258  mp_integer pack() const;
259  void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const;
260  void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const;
261  mp_integer to_integer() const; // this always rounds to zero
262 
263  // conversions
264  void change_spec(const ieee_float_spect &dest_spec);
265 
266  // output
267  void print(std::ostream &out) const;
268 
269  std::string to_ansi_c_string() const
270  {
271  return format(format_spect());
272  }
273 
274  std::string to_string_decimal(std::size_t precision) const;
275  std::string to_string_scientific(std::size_t precision) const;
276  std::string format(const format_spect &format_spec) const;
277 
278  // expressions
279  constant_exprt to_expr() const;
280  void from_expr(const constant_exprt &expr);
281 
282  // the usual operators
283  ieee_floatt &operator/=(const ieee_floatt &other);
284  ieee_floatt &operator*=(const ieee_floatt &other);
285  ieee_floatt &operator+=(const ieee_floatt &other);
286  ieee_floatt &operator-=(const ieee_floatt &other);
287 
288  bool operator<(const ieee_floatt &other) const;
289  bool operator<=(const ieee_floatt &other) const;
290  bool operator>(const ieee_floatt &other) const;
291  bool operator>=(const ieee_floatt &other) const;
292 
293  // warning: these do packed equality, not IEEE equality
294  // e.g., NAN==NAN
295  bool operator==(const ieee_floatt &other) const;
296  bool operator!=(const ieee_floatt &other) const;
297  bool operator==(int i) const;
298 
299  // these do IEEE equality, i.e., NAN!=NAN
300  bool ieee_equal(const ieee_floatt &other) const;
301  bool ieee_not_equal(const ieee_floatt &other) const;
302 
303 protected:
304  void divide_and_round(mp_integer &dividend, const mp_integer &divisor);
305  void align();
306  void next_representable(bool greater);
307 
308  // we store the number unpacked
309  bool sign_flag;
310  mp_integer exponent; // this is unbiased
311  mp_integer fraction; // this _does_ include the hidden bit
313 
314  // number of digits of an integer >=1 in base 10
315  static mp_integer base10_digits(const mp_integer &src);
316 };
317 
318 inline std::ostream &operator<<(
319  std::ostream &out,
320  const ieee_floatt &f)
321 {
322  return out << f.to_ansi_c_string();
323 }
324 
325 #endif // CPROVER_UTIL_IEEE_FLOAT_H
ieee_floatt::is_double
bool is_double() const
Definition: ieee_float.cpp:1174
ieee_floatt
Definition: ieee_float.h:120
ID_cprover_rounding_mode_str
const char ID_cprover_rounding_mode_str[]
Definition: ieee_float.h:23
ieee_floatt::operator==
bool operator==(const ieee_floatt &other) const
Definition: ieee_float.cpp:990
mp_arith.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
ieee_floatt::ieee_floatt
ieee_floatt()
Definition: ieee_float.h:154
ieee_floatt::decrement
void decrement(bool distinguish_zero=false)
Definition: ieee_float.h:224
ieee_floatt::extract_base2
void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const
Definition: ieee_float.cpp:408
ieee_floatt::ieee_floatt
ieee_floatt(const floatbv_typet &type)
Definition: ieee_float.h:143
ieee_floatt::to_ansi_c_string
std::string to_ansi_c_string() const
Definition: ieee_float.h:269
ieee_floatt::get_fraction
const mp_integer & get_fraction() const
Definition: ieee_float.h:242
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
ieee_floatt::is_normal
bool is_normal() const
Definition: ieee_float.cpp:365
ieee_floatt::get_exponent
const mp_integer & get_exponent() const
Definition: ieee_float.h:241
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::ieee_floatt
ieee_floatt(const ieee_float_spect &_spec)
Definition: ieee_float.h:136
ieee_floatt::change_spec
void change_spec(const ieee_float_spect &dest_spec)
Definition: ieee_float.cpp:1044
operator<<
std::ostream & operator<<(std::ostream &out, const ieee_floatt &f)
Definition: ieee_float.h:318
ieee_float_spect::quadruple_precision
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:86
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_float_spect::operator==
bool operator==(const ieee_float_spect &other) const
Definition: ieee_float.h:108
ieee_floatt::operator!=
bool operator!=(const ieee_floatt &other) const
Definition: ieee_float.cpp:1029
ieee_float_spect::half_precision
static ieee_float_spect half_precision()
Definition: ieee_float.h:67
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::x86_80
static ieee_float_spect x86_80()
Definition: ieee_float.h:92
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
ieee_floatt::infinity_flag
bool infinity_flag
Definition: ieee_float.h:312
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
ieee_float_spect::ieee_float_spect
ieee_float_spect()
Definition: ieee_float.h:45
ieee_floatt::is_zero
bool is_zero() const
Definition: ieee_float.h:232
ieee_floatt::fltmax
static ieee_floatt fltmax(const ieee_float_spect &_spec)
Definition: ieee_float.h:207
ieee_float_spect::width
std::size_t width() const
Definition: ieee_float.h:54
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
ieee_floatt::ieee_equal
bool ieee_equal(const ieee_floatt &other) const
Definition: ieee_float.cpp:1012
ieee_floatt::increment
void increment(bool distinguish_zero=false)
Definition: ieee_float.h:215
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
ieee_floatt::rounding_modet
rounding_modet
Definition: ieee_float.h:126
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
cprover_prefix.h
ieee_floatt::divide_and_round
void divide_and_round(mp_integer &dividend, const mp_integer &divisor)
Definition: ieee_float.cpp:647
ieee_floatt::is_infinity
bool is_infinity() const
Definition: ieee_float.h:238
ieee_floatt::negate
void negate()
Definition: ieee_float.h:167
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
format_spec.h
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::plus_infinity
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:200
ieee_floatt::spec
ieee_float_spect spec
Definition: ieee_float.h:134
ieee_float_spect::ieee_float_spect
ieee_float_spect(const floatbv_typet &type)
Definition: ieee_float.h:38
ieee_floatt::UNKNOWN
@ UNKNOWN
Definition: ieee_float.h:129
ieee_float_spect::operator!=
bool operator!=(const ieee_float_spect &other) const
Definition: ieee_float.h:113
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
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
ieee_floatt::ieee_floatt
ieee_floatt(const constant_exprt &expr)
Definition: ieee_float.h:161
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
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
ieee_floatt::sign_flag
bool sign_flag
Definition: ieee_float.h:309
ieee_floatt::zero
static ieee_floatt zero(const floatbv_typet &type)
Definition: ieee_float.h:184
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
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
ieee_floatt::NaN
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition: ieee_float.h:197
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
ieee_float_spect::single_precision
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
ieee_float_spect::x86_96
static ieee_float_spect x86_96()
Definition: ieee_float.h:100
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_float_spect::ieee_float_spect
ieee_float_spect(std::size_t _f, std::size_t _e)
Definition: ieee_float.h:49
ieee_floatt::make_fltmax
void make_fltmax()
Definition: ieee_float.cpp:1147
ieee_floatt::minus_infinity
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:203
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
ieee_floatt::fltmin
static ieee_floatt fltmin(const ieee_float_spect &_spec)
Definition: ieee_float.h:211
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
irep.h
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
ieee_floatt::from_double
void from_double(const double d)
Definition: ieee_float.cpp:1090