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