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) const
22  {
23  return convert(src);
24  }
25 
26  exprt convert(const exprt &) const;
27 
28  static exprt negation(const exprt &, const ieee_float_spect &);
29  static exprt abs(const exprt &, const ieee_float_spect &);
30  static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &);
31  static exprt is_zero(const exprt &);
32  static exprt isnan(const exprt &, const ieee_float_spect &);
33  static exprt isinf(const exprt &, const ieee_float_spect &);
34  static exprt isnormal(const exprt &, const ieee_float_spect &);
35  static 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 &) const;
44 
45  // mul/div
46  exprt
47  mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
48  const;
49  exprt
50  div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
51  const;
52 
53  // conversion
55  const exprt &,
56  const exprt &rm,
57  const ieee_float_spect &) const;
59  const exprt &,
60  const exprt &rm,
61  const ieee_float_spect &) const;
62  static exprt to_signed_integer(
63  const exprt &src,
64  std::size_t dest_width,
65  const exprt &rm,
66  const ieee_float_spect &);
68  const exprt &src,
69  std::size_t dest_width,
70  const exprt &rm,
71  const ieee_float_spect &);
72  static exprt to_integer(
73  const exprt &src,
74  std::size_t dest_width,
75  bool is_signed,
76  const exprt &rm,
77  const ieee_float_spect &);
79  const exprt &src,
80  const exprt &rm,
81  const ieee_float_spect &src_spec,
82  const ieee_float_spect &dest_spec) const;
83 
84  // relations
85  enum class relt { LT, LE, EQ, GT, GE };
86  static exprt
87  relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &);
88 
89 private:
90  // helpers
91  static ieee_float_spect get_spec(const exprt &);
92  // still biased
93  static exprt get_exponent(const exprt &, const ieee_float_spect &);
94  // without hidden bit
95  static exprt get_fraction(const exprt &, const ieee_float_spect &);
96  static exprt sign_bit(const exprt &);
97 
98  static exprt exponent_all_ones(const exprt &, const ieee_float_spect &);
99  static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &);
100  static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &);
101 
103  {
104  // these are mutually exclusive, obviously
109 
110  void get(const exprt &rm);
111  explicit rounding_mode_bitst(const exprt &rm) { get(rm); }
112  };
113 
114  // unpacked
115  static void normalization_shift(exprt &fraction, exprt &exponent);
116  static void denormalization_shift(
117  exprt &fraction,
118  exprt &exponent,
119  const ieee_float_spect &);
120 
121  static exprt add_bias(const exprt &exponent, const ieee_float_spect &);
122  static exprt sub_bias(const exprt &exponent, const ieee_float_spect &);
123 
124  static exprt limit_distance(const exprt &dist, mp_integer limit);
125 
127  {
130 
132  sign(false_exprt()),
134  zero(false_exprt()),
135  NaN(false_exprt())
136  {
137  }
138  };
139 
140  // This has a biased exponent (unsigned)
141  // and an _implicit_ hidden bit.
143  {
144  };
145 
146  // The hidden bit is explicit,
147  // and the exponent is not biased (signed)
149  {
150  };
151 
152  static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &);
153 
154  // this takes unpacked format, and returns packed
155  exprt rounder(
156  const unbiased_floatt &,
157  const exprt &rm,
158  const ieee_float_spect &) const;
159  static exprt pack(const biased_floatt &, const ieee_float_spect &);
160  static unbiased_floatt unpack(const exprt &, const ieee_float_spect &);
161 
162  static void round_fraction(
163  unbiased_floatt &result,
164  const rounding_mode_bitst &,
165  const ieee_float_spect &);
166  static void round_exponent(
167  unbiased_floatt &result,
168  const rounding_mode_bitst &,
169  const ieee_float_spect &);
170 
171  // rounding decision for fraction
173  const std::size_t dest_bits,
174  const exprt sign,
175  const exprt &fraction,
176  const rounding_mode_bitst &);
177 
178  // helpers for adder
179 
180  // computes src1.exponent-src2.exponent with extension
181  static exprt
182  subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2);
183 
184  // computes the "sticky-bit"
185  static exprt
186  sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky);
187 };
188 
189 inline exprt float_bv(const exprt &src)
190 {
191  return float_bvt()(src);
192 }
193 
194 #endif // CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H
static void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Definition: float_bv.cpp:1199
static exprt isinf(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:816
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:211
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
static exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:727
static ieee_float_spect get_spec(const exprt &)
Definition: float_bv.cpp:97
BigInt mp_integer
Definition: mp_arith.h:22
static exprt add_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1299
static exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
Definition: float_bv.cpp:400
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:275
static exprt is_zero(const exprt &)
Definition: float_bv.cpp:145
static exprt pack(const biased_floatt &, const ieee_float_spect &)
Definition: float_bv.cpp:1352
static exprt sign_bit(const exprt &)
Definition: float_bv.cpp:204
static exprt negation(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:113
static void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Definition: float_bv.cpp:1092
static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
Definition: float_bv.cpp:1265
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:323
exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:991
static exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:266
static exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:161
exprt convert(const exprt &) const
Definition: float_bv.cpp:16
static exprt isnormal(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:390
API to expression classes.
static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:123
static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:170
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:235
static exprt abs(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:103
The Boolean constant false.
Definition: std_expr.h:4452
exprt float_bv(const exprt &src)
Definition: float_bv.h:189
static exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
Definition: float_bv.cpp:833
static exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1309
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
Definition: float_bv.cpp:1034
static exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
Definition: float_bv.cpp:1384
Base class for all expressions.
Definition: expr.h:54
static exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition: float_bv.cpp:565
static unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:1319
static void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns &#39;zero&#39; if fraction is zero
Definition: float_bv.cpp:861
static exprt isfinite(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:825
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:843
static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:179
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:589
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:419
rounding_mode_bitst(const exprt &rm)
Definition: float_bv.h:111
exprt operator()(const exprt &src) const
Definition: float_bv.h:21
static exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:257
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:638
static 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:913
static exprt isnan(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:852