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#include "cprover_prefix.h"
18
19class constant_exprt;
20class floatbv_typet;
21
23{
24public:
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
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
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{
118public:
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
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
220 { ieee_floatt c(_spec); c.make_fltmax(); return c; }
221
222 // minimum normalized positive floating-point number
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
315protected:
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
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
330inline 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:40
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: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:97
void from_type(const floatbv_typet &type)
Definition: ieee_float.cpp:45
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:782
void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const
Definition: ieee_float.cpp:437
void make_minus_infinity()
void make_fltmax()
const mp_integer & get_exponent() const
Definition: ieee_float.h:253
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.
const mp_integer & get_fraction() const
Definition: ieee_float.h:254
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:320
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: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: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: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:209
std::string to_string_decimal(std::size_t precision) const
Definition: ieee_float.cpp:139
void negate()
Definition: ieee_float.h:179
void make_NaN()
bool sign_flag
Definition: ieee_float.h:321
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: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: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:250
void make_fltmin()
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:516
rounding_modet rounding_mode
Definition: ieee_float.h:133
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:223
mp_integer pack() const
Definition: ieee_float.cpp:375
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:473
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: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:155
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
STL namespace.
BigInt mp_integer
Definition: smt_terms.h:12