CBMC
Loading...
Searching...
No Matches
float_bv.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_SOLVERS_FLOATBV_FLOAT_BV_H
11#define CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H
12
13#include <util/ieee_float.h>
14#include <util/std_expr.h>
15
17{
18public:
19 exprt operator()(const exprt &src) const
20 {
21 return convert(src);
22 }
23
24 exprt convert(const exprt &) const;
25
26 static exprt negation(const exprt &, const ieee_float_spect &);
27 static exprt abs(const exprt &, const ieee_float_spect &);
28 static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &);
29 static exprt is_zero(const exprt &);
30 static exprt isnan(const exprt &, const ieee_float_spect &);
31 static exprt isinf(const exprt &, const ieee_float_spect &);
32 static exprt isnormal(const exprt &, const ieee_float_spect &);
33 static exprt isfinite(const exprt &, const ieee_float_spect &);
34
35 // add/sub
37 bool subtract,
38 const exprt &,
39 const exprt &,
40 const exprt &rm,
41 const ieee_float_spect &) const;
42
43 // mul/div
44 exprt
45 mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
46 const;
47 exprt
48 div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
49 const;
50
51 // conversion
53 const exprt &,
54 const exprt &rm,
55 const ieee_float_spect &) const;
57 const exprt &,
58 const exprt &rm,
59 const ieee_float_spect &) const;
61 const exprt &src,
62 std::size_t dest_width,
63 const exprt &rm,
64 const ieee_float_spect &);
66 const exprt &src,
67 std::size_t dest_width,
68 const exprt &rm,
69 const ieee_float_spect &);
70 static exprt to_integer(
71 const exprt &src,
72 std::size_t dest_width,
73 bool is_signed,
74 const exprt &rm,
75 const ieee_float_spect &);
77 const exprt &src,
78 const exprt &rm,
80 const ieee_float_spect &dest_spec) const;
81
82 // relations
83 enum class relt { LT, LE, EQ, GT, GE };
84 static exprt
85 relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &);
86
87private:
88 // helpers
89 static ieee_float_spect get_spec(const exprt &);
90 // still biased
91 static exprt get_exponent(const exprt &, const ieee_float_spect &);
92 // without hidden bit
93 static exprt get_fraction(const exprt &, const ieee_float_spect &);
94 static exprt sign_bit(const exprt &);
95
96 static exprt exponent_all_ones(const exprt &, const ieee_float_spect &);
97 static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &);
98 static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &);
99
101 {
102 // these are mutually exclusive, obviously
108
109 void get(const exprt &rm);
110 explicit rounding_mode_bitst(const exprt &rm) { get(rm); }
111 };
112
113 // unpacked
114 static void normalization_shift(exprt &fraction, exprt &exponent);
115 static void denormalization_shift(
116 exprt &fraction,
117 exprt &exponent,
118 const ieee_float_spect &);
119
120 static exprt add_bias(const exprt &exponent, const ieee_float_spect &);
121 static exprt sub_bias(const exprt &exponent, const ieee_float_spect &);
122
124
138
139 // This has a biased exponent (unsigned)
140 // and an _implicit_ hidden bit.
142 {
143 };
144
145 // The hidden bit is explicit,
146 // and the exponent is not biased (signed)
148 {
149 };
150
151 static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &);
152
153 // this takes unpacked format, and returns packed
155 const unbiased_floatt &,
156 const exprt &rm,
157 const ieee_float_spect &) const;
158 static exprt pack(const biased_floatt &, const ieee_float_spect &);
159 static unbiased_floatt unpack(const exprt &, const ieee_float_spect &);
160
161 static void round_fraction(
162 unbiased_floatt &result,
163 const rounding_mode_bitst &,
164 const ieee_float_spect &);
165 static void round_exponent(
166 unbiased_floatt &result,
167 const rounding_mode_bitst &,
168 const ieee_float_spect &);
169
170 // rounding decision for fraction
172 const std::size_t dest_bits,
173 const exprt sign,
174 const exprt &fraction,
175 const rounding_mode_bitst &);
176
177 // helpers for adder
178
179 // computes src1.exponent-src2.exponent with extension
180 static exprt
182
183 // computes the "sticky-bit"
184 static exprt
185 sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky);
186};
187
188inline exprt float_bv(const exprt &src)
189{
190 return float_bvt()(src);
191}
192
193#endif // CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
The Boolean constant false.
Definition std_expr.h:3200
static unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
static void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
Definition float_bv.cpp:950
static exprt get_fraction(const exprt &, const ieee_float_spect &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition float_bv.cpp:934
static exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
static exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:249
static exprt to_integer(const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:366
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:326
static exprt isfinite(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:918
static exprt isnormal(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:488
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:302
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:517
static exprt is_zero(const exprt &)
Definition float_bv.cpp:233
exprt operator()(const exprt &src) const
Definition float_bv.h:19
static exprt abs(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:191
static void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
static exprt fraction_rounding_decision(const std::size_t dest_bits, const exprt sign, const exprt &fraction, const rounding_mode_bitst &)
rounding decision for fraction using sticky bit
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec) const
Definition float_bv.cpp:414
static exprt isnan(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:941
static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
static exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
Definition float_bv.cpp:926
static void denormalization_shift(exprt &fraction, exprt &exponent, const ieee_float_spect &)
make sure exponent is not too small; the exponent is unbiased
static exprt add_bias(const exprt &exponent, const ieee_float_spect &)
static exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const
static exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
Definition float_bv.cpp:498
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:737
exprt convert(const exprt &) const
Definition float_bv.cpp:19
static ieee_float_spect get_spec(const exprt &)
Definition float_bv.cpp:185
static exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:357
static exprt negation(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:201
static exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:826
static exprt isinf(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:909
static exprt sign_bit(const exprt &)
Definition float_bv.cpp:295
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition float_bv.cpp:686
static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:267
static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:258
static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
Definition float_bv.cpp:211
static exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition float_bv.cpp:348
static exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition float_bv.cpp:663
static exprt pack(const biased_floatt &, const ieee_float_spect &)
static void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
exprt float_bv(const exprt &src)
Definition float_bv.h:188
BigInt mp_integer
Definition smt_terms.h:17
API to expression classes.
rounding_mode_bitst(const exprt &rm)
Definition float_bv.h:110
void get(const exprt &rm)
Definition float_bv.cpp:277
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45