cprover
float_bv.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_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 
18 class float_bvt
19 {
20 public:
21  exprt operator()(const exprt &src)
22  {
23  return convert(src);
24  }
25 
26  exprt convert(const exprt &);
27 
28  exprt negation(const exprt &, const ieee_float_spect &);
29  exprt abs(const exprt &, const ieee_float_spect &);
30  exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &);
31  exprt is_zero(const exprt &);
32  exprt isnan(const exprt &, const ieee_float_spect &);
33  exprt isinf(const exprt &, const ieee_float_spect &);
34  exprt isnormal(const exprt &, const ieee_float_spect &);
35  exprt isfinite(const exprt &, const ieee_float_spect &);
36 
37  // add/sub
38  exprt add_sub(
39  bool subtract,
40  const exprt &,
41  const exprt &,
42  const exprt &rm,
43  const ieee_float_spect &);
44 
45  // mul/div
46  exprt mul(
47  const exprt &,
48  const exprt &,
49  const exprt &rm,
50  const ieee_float_spect &);
51  exprt div(
52  const exprt &,
53  const exprt &,
54  const exprt &rm,
55  const ieee_float_spect &);
56 
57  // conversion
59  const exprt &,
60  const exprt &rm,
61  const ieee_float_spect &);
63  const exprt &,
64  const exprt &rm,
65  const ieee_float_spect &);
67  const exprt &src,
68  std::size_t dest_width,
69  const exprt &rm,
70  const ieee_float_spect &);
72  const exprt &src,
73  std::size_t dest_width,
74  const exprt &rm,
75  const ieee_float_spect &);
77  const exprt &src,
78  std::size_t dest_width,
79  bool is_signed,
80  const exprt &rm,
81  const ieee_float_spect &);
83  const exprt &src,
84  const exprt &rm,
85  const ieee_float_spect &src_spec,
86  const ieee_float_spect &dest_spec);
87 
88  // relations
89  enum class relt { LT, LE, EQ, GT, GE };
91  const exprt &,
92  relt rel,
93  const exprt &,
94  const ieee_float_spect &);
95 
96 private:
97  // helpers
99  // still biased
100  exprt get_exponent(const exprt &, const ieee_float_spect &);
101  // without hidden bit
102  exprt get_fraction(const exprt &, const ieee_float_spect &);
103  exprt sign_bit(const exprt &);
104 
105  exprt exponent_all_ones(const exprt &, const ieee_float_spect &);
108 
110  {
111  // these are mutually exclusive, obviously
116 
117  void get(const exprt &rm);
118  explicit rounding_mode_bitst(const exprt &rm) { get(rm); }
119  };
120 
121  // unpacked
122  void normalization_shift(exprt &fraction, exprt &exponent);
124  exprt &fraction,
125  exprt &exponent,
126  const ieee_float_spect &);
127 
128  exprt add_bias(const exprt &exponent, const ieee_float_spect &);
129  exprt sub_bias(const exprt &exponent, const ieee_float_spect &);
130 
131  exprt limit_distance(const exprt &dist, mp_integer limit);
132 
134  {
137 
139  sign(false_exprt()),
141  zero(false_exprt()),
142  NaN(false_exprt())
143  {
144  }
145  };
146 
147  // This has a biased exponent (unsigned)
148  // and an _implicit_ hidden bit.
150  {
151  };
152 
153  // The hidden bit is explicit,
154  // and the exponent is not biased (signed)
156  {
157  };
158 
160 
161  // this takes unpacked format, and returns packed
162  exprt rounder(
163  const unbiased_floatt &,
164  const exprt &rm,
165  const ieee_float_spect &);
166  exprt pack(const biased_floatt &, const ieee_float_spect &);
167  unbiased_floatt unpack(const exprt &, const ieee_float_spect &);
168 
169  void round_fraction(
170  unbiased_floatt &result,
171  const rounding_mode_bitst &,
172  const ieee_float_spect &);
173  void round_exponent(
174  unbiased_floatt &result,
175  const rounding_mode_bitst &,
176  const ieee_float_spect &);
177 
178  // rounding decision for fraction
180  const std::size_t dest_bits,
181  const exprt sign,
182  const exprt &fraction,
183  const rounding_mode_bitst &);
184 
185  // helpers for adder
186 
187  // computes src1.exponent-src2.exponent with extension
189  const unbiased_floatt &src1,
190  const unbiased_floatt &src2);
191 
192  // computes the "sticky-bit"
194  const exprt &op,
195  const exprt &dist,
196  exprt &sticky);
197 };
198 
199 inline exprt float_bv(const exprt &src)
200 {
201  return float_bvt()(src);
202 }
203 
204 #endif // CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H
void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Definition: float_bv.cpp:1198
exprt isinf(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:819
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:592
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:730
ieee_float_spect get_spec(const exprt &)
Definition: float_bv.cpp:98
BigInt mp_integer
Definition: mp_arith.h:22
exprt add_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1300
exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
Definition: float_bv.cpp:402
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:279
exprt convert(const exprt &)
Definition: float_bv.cpp:17
exprt is_zero(const exprt &)
Definition: float_bv.cpp:148
exprt pack(const biased_floatt &, const ieee_float_spect &)
Definition: float_bv.cpp:1353
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:239
exprt sign_bit(const exprt &)
Definition: float_bv.cpp:208
exprt negation(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:115
void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Definition: float_bv.cpp:1092
biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
Definition: float_bv.cpp:1267
exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:270
exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:165
exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:992
exprt isnormal(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:392
API to expression classes.
exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:126
exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:174
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec)
Definition: float_bv.cpp:327
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:215
exprt abs(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:104
The boolean constant false.
Definition: std_expr.h:4497
exprt float_bv(const exprt &src)
Definition: float_bv.h:199
exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
Definition: float_bv.cpp:836
exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1310
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
Definition: float_bv.cpp:1035
exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
Definition: float_bv.cpp:1385
Base class for all expressions.
Definition: expr.h:42
exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition: float_bv.cpp:568
unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:1320
void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns &#39;zero&#39; if fraction is zero
Definition: float_bv.cpp:864
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:422
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:641
exprt isfinite(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:828
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:846
exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:183
rounding_mode_bitst(const exprt &rm)
Definition: float_bv.h:118
exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:261
void denormalization_shift(exprt &fraction, exprt &exponent, const ieee_float_spect &)
make sure exponent is not too small; the exponent is unbiased
Definition: float_bv.cpp:914
exprt operator()(const exprt &src)
Definition: float_bv.h:21
exprt isnan(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:855