cprover
Loading...
Searching...
No Matches
ieee_float.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
18class constant_exprt;
19class floatbv_typet;
20
22{
23public:
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
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
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{
117public:
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
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
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
219 { ieee_floatt c(_spec); c.make_fltmax(); return c; }
220
221 // minimum normalized positive floating-point number
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
314protected:
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
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
329inline 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:2995
Fixed-width bit-vector with IEEE floating-point interpretation.
mp_integer max_fraction() const
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
mp_integer bias() const
mp_integer max_exponent() const
static ieee_float_spect x86_96()
Definition ieee_float.h:96
void from_type(const floatbv_typet &type)
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)
void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const
void make_minus_infinity()
void make_fltmax()
const mp_integer & get_exponent() const
Definition ieee_float.h:252
void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
const mp_integer & get_fraction() const
Definition ieee_float.h:253
void unpack(const mp_integer &i)
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)
constant_exprt to_expr() const
void divide_and_round(mp_integer &dividend, const mp_integer &divisor)
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)
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
static constant_exprt rounding_mode_expr(rounding_modet)
bool operator<=(const ieee_floatt &other) const
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.
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition ieee_float.h:208
std::string to_string_decimal(std::size_t precision) const
void negate()
Definition ieee_float.h:178
ieee_floatt & operator-=(const ieee_floatt &other)
bool operator>(const ieee_floatt &other) const
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)
bool operator>=(const ieee_floatt &other) const
std::string format(const format_spect &format_spec) const
bool is_infinity() const
Definition ieee_float.h:249
void make_fltmin()
void from_integer(const mp_integer &i)
rounding_modet rounding_mode
Definition ieee_float.h:132
static mp_integer base10_digits(const mp_integer &src)
bool is_normal() const
static ieee_floatt fltmin(const ieee_float_spect &_spec)
Definition ieee_float.h:222
mp_integer pack() const
mp_integer fraction
Definition ieee_float.h:322
void decrement(bool distinguish_zero=false)
Definition ieee_float.h:235
void build(const mp_integer &exp, const mp_integer &frac)
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)
void from_double(const double d)
bool operator<(const ieee_floatt &other) const
void change_spec(const ieee_float_spect &dest_spec)
void print(std::ostream &out) const
ieee_floatt(const floatbv_typet &type)
Definition ieee_float.h:154
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
STL namespace.
BigInt mp_integer
Definition smt_terms.h:17