CBMC
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):
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
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
117{
118public:
120
122 : spec(_spec),
124 exponent(0),
125 fraction(0),
128 {
129 }
130
131 explicit ieee_float_valuet(const floatbv_typet &type)
132 : spec(ieee_float_spect(type)),
134 exponent(0),
135 fraction(0),
138 {
139 }
140
141 explicit ieee_float_valuet(const constant_exprt &expr)
142 {
143 from_expr(expr);
144 }
145
147 : sign_flag(false),
148 exponent(0),
149 fraction(0),
152 {
153 }
154
155 void negate()
156 {
158 }
159
160 void set_sign(bool _sign)
161 { sign_flag = _sign; }
162
164 {
165 sign_flag=false;
166 exponent=0;
167 fraction=0;
168 NaN_flag=false;
169 infinity_flag=false;
170 }
171
173 {
174 ieee_float_valuet result(type);
175 result.make_zero();
176 return result;
177 }
178
180 {
181 ieee_float_valuet result(spec);
182 result.make_zero();
183 return result;
184 }
185
186 static ieee_float_valuet one(const floatbv_typet &);
187 static ieee_float_valuet one(const ieee_float_spect &);
188
189 void make_NaN();
190 void make_plus_infinity();
191 void make_minus_infinity();
192 void make_fltmax(); // maximum representable finite floating-point number
193 void make_fltmin(); // minimum normalized positive floating-point number
194
196 {
198 c.make_NaN();
199 return c;
200 }
201
203 {
205 c.make_plus_infinity();
206 return c;
207 }
208
210 {
212 c.make_minus_infinity();
213 return c;
214 }
215
216 // maximum representable finite floating-point number
218 {
220 c.make_fltmax();
221 return c;
222 }
223
224 // minimum normalized positive floating-point number
226 {
228 c.make_fltmin();
229 return c;
230 }
231
232 // set to next representable number towards plus infinity
234 {
235 if(is_zero() && get_sign() && distinguish_zero)
236 negate();
237 else
238 next_representable(true);
239 }
240
241 // set to previous representable number towards minus infinity
243 {
244 if(is_zero() && !get_sign() && distinguish_zero)
245 negate();
246 else
247 next_representable(false);
248 }
249
250 bool is_zero() const
251 {
252 return !NaN_flag && !infinity_flag && fraction==0 && exponent==0;
253 }
254 bool get_sign() const { return sign_flag; }
255 bool is_NaN() const { return NaN_flag; }
256 bool is_infinity() const { return !NaN_flag && infinity_flag; }
257 bool is_normal() const;
258
259 const mp_integer &get_exponent() const { return exponent; }
260 const mp_integer &get_fraction() const { return fraction; }
261
262 // Construct IEEE floating point value
263 void unpack(const mp_integer &);
264 void from_double(double);
265 void from_float(float);
266
267 // performs conversions from IEEE float-point format
268 // to something else
269 double to_double() const;
270 float to_float() const;
271 bool is_double() const;
272 bool is_float() const;
273 mp_integer pack() const;
276 mp_integer to_integer() const; // this always rounds to zero
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 bool operator<(const ieee_float_valuet &) const;
295 bool operator<=(const ieee_float_valuet &) const;
296 bool operator>(const ieee_float_valuet &) const;
297 bool operator>=(const ieee_float_valuet &) const;
298
299 // warning: these do packed equality, not IEEE equality
300 // e.g., NAN==NAN
301 bool operator==(const ieee_float_valuet &) const;
302 bool operator!=(const ieee_float_valuet &) const;
303 bool operator==(int) const;
304
305 // these do IEEE equality, i.e., NAN!=NAN
306 bool ieee_equal(const ieee_float_valuet &) const;
307 bool ieee_not_equal(const ieee_float_valuet &) const;
308
309protected:
310 // we store the number unpacked
312 mp_integer exponent; // this is unbiased
313 mp_integer fraction; // this _does_ include the hidden bit
315
316 // number of digits of an integer >=1 in base 10
317 static mp_integer base10_digits(const mp_integer &src);
318
319 void next_representable(bool greater);
320};
321
322inline std::ostream &operator<<(std::ostream &out, const ieee_float_valuet &f)
323{
324 return out << f.to_ansi_c_string();
325}
326
330{
331public:
332 // ROUND_TO_EVEN is also known as "round to nearest, ties to even", and
333 // is the IEEE default.
334 // ROUND_TO_AWAY is also known as "round to infinity".
335 // The numbering below is what x86 uses in the control word and
336 // what is recommended in C11 5.2.4.2.2.
337 // The numbering of ROUND_TO_AWAY is not specified in C11 5.2.4.2.2.
348
350 {
351 return _rounding_mode;
352 }
353
354 // A helper to turn a rounding mode into a constant bitvector expression
356
361
366
371
376
377 // performs conversion to IEEE floating point format,
378 // with rounding.
379 void from_integer(const mp_integer &i);
380 void from_base10(const mp_integer &exp, const mp_integer &frac);
381 void build(const mp_integer &exp, const mp_integer &frac);
382
383 // performs conversions from IEEE float-point format
384 // to something else
385 double to_double() const;
386 float to_float() const;
387 mp_integer to_integer() const; // this always rounds to zero
388
389 // conversions
391
392 // the usual operators
393 ieee_floatt &operator/=(const ieee_floatt &other);
394 ieee_floatt &operator*=(const ieee_floatt &other);
395 ieee_floatt &operator+=(const ieee_floatt &other);
396 ieee_floatt &operator-=(const ieee_floatt &other);
397
398protected:
400
401 void divide_and_round(mp_integer &dividend, const mp_integer &divisor);
402 void align();
403};
404
405#endif // CPROVER_UTIL_IEEE_FLOAT_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A constant literal expression.
Definition std_expr.h:3117
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
An IEEE 754 floating-point value, including specificiation.
Definition ieee_float.h:117
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
ieee_float_valuet(const ieee_float_spect &_spec)
Definition ieee_float.h:121
void set_sign(bool _sign)
Definition ieee_float.h:160
static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:209
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
bool ieee_equal(const ieee_float_valuet &) const
bool is_NaN() const
Definition ieee_float.h:255
bool operator>=(const ieee_float_valuet &) const
bool operator<(const ieee_float_valuet &) const
static ieee_float_valuet one(const floatbv_typet &)
mp_integer exponent
Definition ieee_float.h:312
bool operator!=(const ieee_float_valuet &) const
void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const
ieee_float_spect spec
Definition ieee_float.h:119
void from_expr(const constant_exprt &expr)
bool is_float() const
bool ieee_not_equal(const ieee_float_valuet &) const
ieee_float_valuet(const constant_exprt &expr)
Definition ieee_float.h:141
mp_integer fraction
Definition ieee_float.h:313
constant_exprt to_expr() const
mp_integer pack() const
static ieee_float_valuet fltmin(const ieee_float_spect &_spec)
Definition ieee_float.h:225
bool operator==(const ieee_float_valuet &) const
bool get_sign() const
Definition ieee_float.h:254
static ieee_float_valuet fltmax(const ieee_float_spect &_spec)
Definition ieee_float.h:217
std::string to_ansi_c_string() const
Definition ieee_float.h:281
std::string to_string_decimal(std::size_t precision) const
const mp_integer & get_fraction() const
Definition ieee_float.h:260
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.
void print(std::ostream &out) const
void next_representable(bool greater)
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinit...
bool is_zero() const
Definition ieee_float.h:250
static ieee_float_valuet zero(const floatbv_typet &type)
Definition ieee_float.h:172
void from_float(float)
static mp_integer base10_digits(const mp_integer &src)
static ieee_float_valuet NaN(const ieee_float_spect &_spec)
Definition ieee_float.h:195
bool is_double() const
bool operator<=(const ieee_float_valuet &) const
mp_integer to_integer() const
void decrement(bool distinguish_zero=false)
Definition ieee_float.h:242
std::string format(const format_spect &format_spec) const
static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:202
void unpack(const mp_integer &)
void increment(bool distinguish_zero=false)
Definition ieee_float.h:233
bool is_normal() const
void from_double(double)
ieee_float_valuet(const floatbv_typet &type)
Definition ieee_float.h:131
void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const
bool operator>(const ieee_float_valuet &) const
bool is_infinity() const
Definition ieee_float.h:256
static ieee_float_valuet zero(const ieee_float_spect &spec)
Definition ieee_float.h:179
const mp_integer & get_exponent() const
Definition ieee_float.h:259
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
Definition ieee_float.h:330
ieee_floatt & operator*=(const ieee_floatt &other)
ieee_floatt(ieee_float_valuet __value, rounding_modet __rounding_mode)
Definition ieee_float.h:372
float to_float() const
mp_integer to_integer() const
ieee_floatt & operator+=(const ieee_floatt &other)
void divide_and_round(mp_integer &dividend, const mp_integer &divisor)
static constant_exprt rounding_mode_expr(rounding_modet)
ieee_floatt(const floatbv_typet &type, rounding_modet __rounding_mode)
Definition ieee_float.h:362
ieee_floatt & operator-=(const ieee_floatt &other)
double to_double() const
ieee_floatt & operator/=(const ieee_floatt &other)
ieee_floatt(const constant_exprt &expr, rounding_modet __rounding_mode)
Definition ieee_float.h:367
rounding_modet _rounding_mode
Definition ieee_float.h:399
void from_integer(const mp_integer &i)
rounding_modet rounding_mode() const
Definition ieee_float.h:349
void build(const mp_integer &exp, const mp_integer &frac)
ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
Definition ieee_float.h:357
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
void change_spec(const ieee_float_spect &dest_spec)
std::ostream & operator<<(std::ostream &out, const ieee_float_valuet &f)
Definition ieee_float.h:322
double exp(double x)
Definition math.c:2546
BigInt mp_integer
Definition smt_terms.h:17