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
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:229
void decrement(bool distinguish_zero=false)
Definition: ieee_float.h:224
BigInt mp_integer
Definition: mp_arith.h:22
ieee_floatt & operator-=(const ieee_floatt &other)
Definition: ieee_float.cpp:904
std::ostream & operator<<(std::ostream &out, const ieee_floatt &f)
Definition: ieee_float.h:318
bool operator>=(const ieee_floatt &other) const
Definition: ieee_float.cpp:985
bool operator!=(const ieee_floatt &other) const
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition: ieee_float.h:197
#define CPROVER_PREFIX
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1398
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:203
ieee_floatt & operator+=(const ieee_floatt &other)
Definition: ieee_float.cpp:813
void from_expr(const constant_exprt &expr)
void build(const mp_integer &exp, const mp_integer &frac)
Definition: ieee_float.cpp:469
bool operator==(const ieee_floatt &other) const
Definition: ieee_float.cpp:990
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...
void make_NaN()
void set_sign(bool _sign)
Definition: ieee_float.h:172
void print(std::ostream &out) const
Definition: ieee_float.cpp:61
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:4384
const mp_integer & get_exponent() const
Definition: ieee_float.h:241
bool is_zero() const
Definition: ieee_float.h:232
mp_integer max_fraction() const
Definition: ieee_float.cpp:41
ieee_floatt(const ieee_float_spect &_spec)
Definition: ieee_float.h:136
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
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:409
bool is_infinity() const
Definition: ieee_float.h:238
static ieee_float_spect x86_96()
Definition: ieee_float.h:100
mp_integer to_integer() const
bool ieee_equal(const ieee_floatt &other) const
ieee_floatt(const floatbv_typet &type)
Definition: ieee_float.h:143
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:316
bool is_normal() const
Definition: ieee_float.cpp:366
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:86
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
void make_fltmin()
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
Definition: ieee_float.cpp:483
static ieee_float_spect half_precision()
Definition: ieee_float.h:67
bool operator<=(const ieee_floatt &other) const
Definition: ieee_float.cpp:957
void from_float(const float f)
mp_integer fraction
Definition: ieee_float.h:311
bool sign_flag
Definition: ieee_float.h:309
bool operator!=(const ieee_float_spect &other) const
Definition: ieee_float.h:113
bool infinity_flag
Definition: ieee_float.h:312
ieee_float_spect spec
Definition: ieee_float.h:134
ieee_floatt(const constant_exprt &expr)
Definition: ieee_float.h:161
mp_integer exponent
Definition: ieee_float.h:310
mp_integer bias() const
Definition: ieee_float.cpp:21
static ieee_floatt fltmax(const ieee_float_spect &_spec)
Definition: ieee_float.h:207
std::string format(const format_spect &format_spec) const
Definition: ieee_float.cpp:66
void make_minus_infinity()
void align()
Definition: ieee_float.cpp:520
bool operator==(const ieee_float_spect &other) const
Definition: ieee_float.h:108
static mp_integer base10_digits(const mp_integer &src)
Definition: ieee_float.cpp:126
void make_plus_infinity()
static ieee_float_spect x86_80()
Definition: ieee_float.h:92
const char ID_cprover_rounding_mode_str[]
Definition: ieee_float.h:23
bool NaN_flag
Definition: ieee_float.h:312
void from_double(const double d)
mp_integer pack() const
Definition: ieee_float.cpp:371
void increment(bool distinguish_zero=false)
Definition: ieee_float.h:215
void negate()
Definition: ieee_float.h:167
bool is_float() const
bool operator>(const ieee_floatt &other) const
Definition: ieee_float.cpp:980
ieee_float_spect(const floatbv_typet &type)
Definition: ieee_float.h:38
void make_fltmax()
ieee_floatt & operator/=(const ieee_floatt &other)
Definition: ieee_float.cpp:703
std::string to_string_decimal(std::size_t precision) const
Definition: ieee_float.cpp:135
bool is_double() const
static ieee_floatt fltmin(const ieee_float_spect &_spec)
Definition: ieee_float.h:211
void divide_and_round(mp_integer &dividend, const mp_integer &divisor)
Definition: ieee_float.cpp:648
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:512
void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const
Definition: ieee_float.cpp:433
bool ieee_not_equal(const ieee_floatt &other) const
rounding_modet rounding_mode
Definition: ieee_float.h:132
ieee_float_spect(std::size_t _f, std::size_t _e)
Definition: ieee_float.h:49
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:200
std::size_t width() const
Definition: ieee_float.h:54
ieee_floatt & operator*=(const ieee_floatt &other)
Definition: ieee_float.cpp:777
std::size_t f
Definition: ieee_float.h:30
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
const mp_integer & get_fraction() const
Definition: ieee_float.h:242
bool operator<(const ieee_floatt &other) const
Definition: ieee_float.cpp:911
static ieee_floatt zero(const floatbv_typet &type)
Definition: ieee_float.h:184