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 
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  // the well-know standard formats
64  {
65  // 32 bits in total
66  return ieee_float_spect(23, 8);
67  }
68 
70  {
71  // 64 bits in total
72  return ieee_float_spect(52, 11);
73  }
74 
76  {
77  // IEEE 754 binary128
78  return ieee_float_spect(112, 15);
79  }
80 
82  {
83  // Intel, not IEEE
84  ieee_float_spect result(63, 15);
85  result.x86_extended=true;
86  return result;
87  }
88 
90  {
91  // Intel, not IEEE
92  ieee_float_spect result(63, 15);
93  result.x86_extended=true;
94  return result;
95  }
96 
97  bool operator==(const ieee_float_spect &other) const
98  {
99  return f==other.f && e==other.e && x86_extended==other.x86_extended;
100  }
101 
102  bool operator!=(const ieee_float_spect &other) const
103  {
104  return !(*this==other);
105  }
106 };
107 
109 {
110 public:
111  // ROUND_TO_EVEN is also known as "round to nearest, ties to even", and
112  // is the IEEE default.
113  // The numbering below is what x86 uses in the control word.
115  {
116  ROUND_TO_EVEN=0, ROUND_TO_MINUS_INF=1,
117  ROUND_TO_PLUS_INF=2, ROUND_TO_ZERO=3,
118  UNKNOWN, NONDETERMINISTIC
119  };
120 
122 
124 
125  explicit ieee_floatt(const ieee_float_spect &_spec):
126  rounding_mode(ROUND_TO_EVEN),
127  spec(_spec), sign_flag(false), exponent(0), fraction(0),
128  NaN_flag(false), infinity_flag(false)
129  {
130  }
131 
132  explicit ieee_floatt(const floatbv_typet &type):
133  rounding_mode(ROUND_TO_EVEN),
134  spec(ieee_float_spect(type)),
135  sign_flag(false),
136  exponent(0),
137  fraction(0),
138  NaN_flag(false),
139  infinity_flag(false)
140  {
141  }
142 
144  rounding_mode(ROUND_TO_EVEN),
145  sign_flag(false), exponent(0), fraction(0),
146  NaN_flag(false), infinity_flag(false)
147  {
148  }
149 
150  explicit ieee_floatt(const constant_exprt &expr):
151  rounding_mode(ROUND_TO_EVEN)
152  {
153  from_expr(expr);
154  }
155 
156  void negate()
157  {
158  sign_flag=!sign_flag;
159  }
160 
161  void set_sign(bool _sign)
162  { sign_flag = _sign; }
163 
164  void make_zero()
165  {
166  sign_flag=false;
167  exponent=0;
168  fraction=0;
169  NaN_flag=false;
170  infinity_flag=false;
171  }
172 
173  static ieee_floatt zero(const floatbv_typet &type)
174  {
175  ieee_floatt result(type);
176  result.make_zero();
177  return result;
178  }
179 
180  void make_NaN();
181  void make_plus_infinity();
182  void make_minus_infinity();
183  void make_fltmax(); // maximum representable finite floating-point number
184  void make_fltmin(); // minimum normalized positive floating-point number
185 
186  static ieee_floatt NaN(const ieee_float_spect &_spec)
187  { ieee_floatt c(_spec); c.make_NaN(); return c; }
188 
190  { ieee_floatt c(_spec); c.make_plus_infinity(); return c; }
191 
193  { ieee_floatt c(_spec); c.make_minus_infinity(); return c; }
194 
195  // maximum representable finite floating-point number
196  static ieee_floatt fltmax(const ieee_float_spect &_spec)
197  { ieee_floatt c(_spec); c.make_fltmax(); return c; }
198 
199  // minimum normalized positive floating-point number
200  static ieee_floatt fltmin(const ieee_float_spect &_spec)
201  { ieee_floatt c(_spec); c.make_fltmin(); return c; }
202 
203  // set to next representable number towards plus infinity
204  void increment(bool distinguish_zero=false)
205  {
206  if(is_zero() && get_sign() && distinguish_zero)
207  negate();
208  else
209  next_representable(true);
210  }
211 
212  // set to previous representable number towards minus infinity
213  void decrement(bool distinguish_zero=false)
214  {
215  if(is_zero() && !get_sign() && distinguish_zero)
216  negate();
217  else
218  next_representable(false);
219  }
220 
221  bool is_zero() const
222  {
223  return !NaN_flag && !infinity_flag && fraction==0 && exponent==0;
224  }
225  bool get_sign() const { return sign_flag; }
226  bool is_NaN() const { return NaN_flag; }
227  bool is_infinity() const { return !NaN_flag && infinity_flag; }
228  bool is_normal() const;
229 
230  const mp_integer &get_exponent() const { return exponent; }
231  const mp_integer &get_fraction() const { return fraction; }
232 
233  // performs conversion to IEEE floating point format
234  void from_integer(const mp_integer &i);
235  void from_base10(const mp_integer &exp, const mp_integer &frac);
236  void build(const mp_integer &exp, const mp_integer &frac);
237  void unpack(const mp_integer &i);
238  void from_double(const double d);
239  void from_float(const float f);
240 
241  // performs conversions from IEEE float-point format
242  // to something else
243  double to_double() const;
244  float to_float() const;
245  bool is_double() const;
246  bool is_float() const;
247  mp_integer pack() const;
248  void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const;
249  void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const;
250  mp_integer to_integer() const; // this always rounds to zero
251 
252  // conversions
253  void change_spec(const ieee_float_spect &dest_spec);
254 
255  // output
256  void print(std::ostream &out) const;
257 
258  std::string to_ansi_c_string() const
259  {
260  return format(format_spect());
261  }
262 
263  std::string to_string_decimal(std::size_t precision) const;
264  std::string to_string_scientific(std::size_t precision) const;
265  std::string format(const format_spect &format_spec) const;
266 
267  // expressions
268  constant_exprt to_expr() const;
269  void from_expr(const constant_exprt &expr);
270 
271  // the usual operators
272  ieee_floatt &operator/=(const ieee_floatt &other);
273  ieee_floatt &operator*=(const ieee_floatt &other);
274  ieee_floatt &operator+=(const ieee_floatt &other);
275  ieee_floatt &operator-=(const ieee_floatt &other);
276 
277  bool operator<(const ieee_floatt &other) const;
278  bool operator<=(const ieee_floatt &other) const;
279  bool operator>(const ieee_floatt &other) const;
280  bool operator>=(const ieee_floatt &other) const;
281 
282  // warning: these do packed equality, not IEEE equality
283  // e.g., NAN==NAN
284  bool operator==(const ieee_floatt &other) const;
285  bool operator!=(const ieee_floatt &other) const;
286  bool operator==(int i) const;
287 
288  // these do IEEE equality, i.e., NAN!=NAN
289  bool ieee_equal(const ieee_floatt &other) const;
290  bool ieee_not_equal(const ieee_floatt &other) const;
291 
292 protected:
293  void divide_and_round(mp_integer &fraction, const mp_integer &factor);
294  void align();
295  void next_representable(bool greater);
296 
297  // we store the number unpacked
298  bool sign_flag;
299  mp_integer exponent; // this is unbiased
300  mp_integer fraction; // this _does_ include the hidden bit
301  bool NaN_flag, infinity_flag;
302 
303  // number of digits of an integer >=1 in base 10
304  static mp_integer base10_digits(const mp_integer &src);
305 };
306 
307 inline std::ostream &operator<<(
308  std::ostream &out,
309  const ieee_floatt &f)
310 {
311  return out << f.to_ansi_c_string();
312 }
313 
314 #endif // CPROVER_UTIL_IEEE_FLOAT_H
bool get_sign() const
Definition: ieee_float.h:225
void decrement(bool distinguish_zero=false)
Definition: ieee_float.h:213
BigInt mp_integer
Definition: mp_arith.h:19
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
std::ostream & operator<<(std::ostream &out, const ieee_floatt &f)
Definition: ieee_float.h:307
guardt & operator-=(guardt &g1, const guardt &g2)
Definition: guard.cpp:93
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition: ieee_float.h:186
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1255
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:192
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void from_type(const floatbv_typet &type)
Definition: ieee_float.cpp:46
void make_NaN()
void set_sign(bool _sign)
Definition: ieee_float.h:161
mp_integer max_exponent() const
Definition: ieee_float.cpp:36
bool is_NaN() const
Definition: ieee_float.h:226
A constant literal expression.
Definition: std_expr.h:3685
const mp_integer & get_exponent() const
Definition: ieee_float.h:230
bool is_zero() const
Definition: ieee_float.h:221
tvt operator>(const interval_templatet< T > &a, const interval_templatet< T > &b)
mp_integer max_fraction() const
Definition: ieee_float.cpp:41
ieee_floatt(const ieee_float_spect &_spec)
Definition: ieee_float.h:125
static ieee_float_spect double_precision()
Definition: ieee_float.h:69
bool is_infinity() const
Definition: ieee_float.h:227
static ieee_float_spect x86_96()
Definition: ieee_float.h:89
tvt operator<=(const interval_templatet< T > &a, const interval_templatet< T > &b)
ieee_floatt(const floatbv_typet &type)
Definition: ieee_float.h:132
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:75
static ieee_float_spect single_precision()
Definition: ieee_float.h:63
void make_fltmin()
mp_integer fraction
Definition: ieee_float.h:300
bool sign_flag
Definition: ieee_float.h:298
bool operator!=(const ieee_float_spect &other) const
Definition: ieee_float.h:102
ieee_float_spect spec
Definition: ieee_float.h:123
ieee_floatt(const constant_exprt &expr)
Definition: ieee_float.h:150
mp_integer exponent
Definition: ieee_float.h:299
mp_integer bias() const
Definition: ieee_float.cpp:21
static ieee_floatt fltmax(const ieee_float_spect &_spec)
Definition: ieee_float.h:196
void make_minus_infinity()
bool operator==(const ieee_float_spect &other) const
Definition: ieee_float.h:97
void make_plus_infinity()
static ieee_float_spect x86_80()
Definition: ieee_float.h:81
bool NaN_flag
Definition: ieee_float.h:301
void increment(bool distinguish_zero=false)
Definition: ieee_float.h:204
void negate()
Definition: ieee_float.h:156
ieee_float_spect(const floatbv_typet &type)
Definition: ieee_float.h:34
void make_fltmax()
static ieee_floatt fltmin(const ieee_float_spect &_spec)
Definition: ieee_float.h:200
tvt operator>=(const interval_templatet< T > &a, const interval_templatet< T > &b)
rounding_modet rounding_mode
Definition: ieee_float.h:121
ieee_float_spect(std::size_t _f, std::size_t _e)
Definition: ieee_float.h:45
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:189
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
std::size_t width() const
Definition: ieee_float.h:50
std::size_t f
Definition: ieee_float.h:26
void make_zero()
Definition: ieee_float.h:164
tvt operator<(const interval_templatet< T > &a, const interval_templatet< T > &b)
std::string to_ansi_c_string() const
Definition: ieee_float.h:258
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::size_t e
Definition: ieee_float.h:26
const mp_integer & get_fraction() const
Definition: ieee_float.h:231
static ieee_floatt zero(const floatbv_typet &type)
Definition: ieee_float.h:173