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