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
float_bvt::rounding_mode_bitst::get
void get(const exprt &rm)
Definition: float_bv.cpp:258
float_bvt::isnormal
static exprt isnormal(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:459
float_bvt::exponent_all_zeros
static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:239
float_bvt::get_exponent
static exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
Definition: float_bv.cpp:896
float_bv
exprt float_bv(const exprt &src)
Definition: float_bv.h:189
float_bvt::abs
static exprt abs(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:172
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
is_signed
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
float_bvt::unpacked_floatt::infinity
exprt infinity
Definition: float_bv.h:128
float_bvt::biased_floatt
Definition: float_bv.h:143
float_bvt::unpacked_floatt::unpacked_floatt
unpacked_floatt()
Definition: float_bv.h:131
float_bvt::unpack
static unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:1384
float_bvt::sub_bias
static exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1374
float_bvt::normalization_shift
static void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
Definition: float_bv.cpp:924
float_bvt
Definition: float_bv.h:19
bv_utils.h
exprt
Base class for all expressions.
Definition: expr.h:53
float_bvt::fraction_rounding_decision
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:1099
float_bvt::sticky_right_shift
static exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
Definition: float_bv.cpp:1448
float_bvt::rounding_mode_bitst::round_to_even
exprt round_to_even
Definition: float_bv.h:105
float_bvt::rounding_mode_bitst::round_to_zero
exprt round_to_zero
Definition: float_bv.h:106
float_bvt::limit_distance
static exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition: float_bv.cpp:634
float_bvt::unpacked_floatt::zero
exprt zero
Definition: float_bv.h:128
float_bvt::get_fraction
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:906
float_bvt::add_sub
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:488
float_bvt::relt::LE
@ LE
ieee_float_spect
Definition: ieee_float.h:26
float_bvt::isfinite
static exprt isfinite(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:888
float_bvt::operator()
exprt operator()(const exprt &src) const
Definition: float_bv.h:21
float_bvt::to_signed_integer
static exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:326
float_bvt::unpacked_floatt
Definition: float_bv.h:127
float_bvt::fraction_all_zeros
static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:248
float_bvt::mul
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:658
float_bvt::rounding_mode_bitst::round_to_plus_inf
exprt round_to_plus_inf
Definition: float_bv.h:107
float_bvt::round_exponent
static void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Definition: float_bv.cpp:1264
float_bvt::unpacked_floatt::fraction
exprt fraction
Definition: float_bv.h:129
float_bvt::isinf
static exprt isinf(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:879
float_bvt::relation
static exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:796
float_bvt::get_spec
static ieee_float_spect get_spec(const exprt &)
Definition: float_bv.cpp:166
float_bvt::div
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:707
float_bvt::add_bias
static exprt add_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1364
float_bvt::denormalization_shift
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:978
float_bvt::rounding_mode_bitst::round_to_minus_inf
exprt round_to_minus_inf
Definition: float_bv.h:108
float_bvt::isnan
static exprt isnan(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:915
float_bvt::relt::EQ
@ EQ
float_bvt::relt::GE
@ GE
float_bvt::from_signed_integer
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:280
float_bvt::is_zero
static exprt is_zero(const exprt &)
Definition: float_bv.cpp:214
float_bvt::unpacked_floatt::exponent
exprt exponent
Definition: float_bv.h:129
float_bvt::negation
static exprt negation(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:182
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
float_bvt::subtract_exponents
static exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
Definition: float_bv.cpp:469
float_bvt::to_integer
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:344
float_bvt::pack
static exprt pack(const biased_floatt &, const ieee_float_spect &)
Definition: float_bv.cpp:1417
float_bvt::sign_bit
static exprt sign_bit(const exprt &)
Definition: float_bv.cpp:273
float_bvt::conversion
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:392
float_bvt::round_fraction
static void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Definition: float_bv.cpp:1157
float_bvt::to_unsigned_integer
static exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:335
float_bvt::unpacked_floatt::NaN
exprt NaN
Definition: float_bv.h:128
ieee_float.h
float_bvt::bias
static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
Definition: float_bv.cpp:1330
float_bvt::unpacked_floatt::sign
exprt sign
Definition: float_bv.h:128
float_bvt::rounder
exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:1056
float_bvt::relt::LT
@ LT
float_bvt::rounding_mode_bitst
Definition: float_bv.h:103
float_bvt::unbiased_floatt
Definition: float_bv.h:149
float_bvt::exponent_all_ones
static exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:230
float_bvt::rounding_mode_bitst::rounding_mode_bitst
rounding_mode_bitst(const exprt &rm)
Definition: float_bv.h:111
float_bvt::convert
exprt convert(const exprt &) const
Definition: float_bv.cpp:16
std_expr.h
API to expression classes.
float_bvt::is_equal
static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:192
float_bvt::relt::GT
@ GT
float_bvt::relt
relt
Definition: float_bv.h:85
float_bvt::from_unsigned_integer
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
Definition: float_bv.cpp:304