cprover
float_utils.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_UTILS_H
11 #define CPROVER_SOLVERS_FLOATBV_FLOAT_UTILS_H
12 
13 #include <util/ieee_float.h>
14 
16 
18 {
19 public:
21  {
22  public:
23  // these are mutually exclusive, obviously
28 
34  {
35  }
36 
37  void set(const ieee_floatt::rounding_modet mode)
38  {
40  const_literal(false);
41 
42  switch(mode)
43  {
46  break;
47 
50  break;
51 
54  break;
55 
58  break;
59 
60  default:
62  }
63  }
64  };
65 
67 
68  explicit float_utilst(propt &_prop):
69  prop(_prop),
70  bv_utils(_prop)
71  {
72  }
73 
74  float_utilst(propt &_prop, const floatbv_typet &type):
75  spec(ieee_float_spect(type)),
76  prop(_prop),
77  bv_utils(_prop)
78  {
79  }
80 
81  void set_rounding_mode(const bvt &);
82 
83  virtual ~float_utilst()
84  {
85  }
86 
88 
90 
91  static inline literalt sign_bit(const bvt &src)
92  {
93  // this is the top bit
94  return src[src.size()-1];
95  }
96 
97  // extraction
98  bvt get_exponent(const bvt &); // still biased
99  bvt get_fraction(const bvt &); // without hidden bit
100  literalt is_normal(const bvt &);
101  literalt is_zero(const bvt &); // this returns true on both 0 and -0
102  literalt is_infinity(const bvt &);
103  literalt is_plus_inf(const bvt &);
104  literalt is_minus_inf(const bvt &);
105  literalt is_NaN(const bvt &);
106 
107  // add/sub
108  virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract);
109 
110  bvt add(const bvt &src1, const bvt &src2)
111  {
112  return add_sub(src1, src2, false);
113  }
114 
115  bvt sub(const bvt &src1, const bvt &src2)
116  {
117  return add_sub(src1, src2, true);
118  }
119 
120  // mul/div/rem
121  virtual bvt mul(const bvt &src1, const bvt &src2);
122  virtual bvt div(const bvt &src1, const bvt &src2);
123  virtual bvt rem(const bvt &src1, const bvt &src2);
124 
125  bvt abs(const bvt &);
126  bvt negate(const bvt &);
127 
128  // conversion
129  bvt from_unsigned_integer(const bvt &);
130  bvt from_signed_integer(const bvt &);
131  bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed);
132  bvt to_signed_integer(const bvt &src, std::size_t int_width);
133  bvt to_unsigned_integer(const bvt &src, std::size_t int_width);
134  bvt conversion(const bvt &src, const ieee_float_spect &dest_spec);
135 
136  // relations
137  enum class relt { LT, LE, EQ, GT, GE };
138  literalt relation(const bvt &src1, relt rel, const bvt &src2);
139 
140  // constants
141  ieee_floatt get(const bvt &) const;
142 
143  // helpers
144  literalt exponent_all_ones(const bvt &);
147 
148  // debugging hooks
149  bvt debug1(const bvt &op0, const bvt &op1);
150  bvt debug2(const bvt &op0, const bvt &op1);
151 
152 protected:
155 
156  // unpacked
157  virtual void normalization_shift(bvt &fraction, bvt &exponent);
158  void denormalization_shift(bvt &fraction, bvt &exponent);
159 
160  bvt add_bias(const bvt &exponent);
161  bvt sub_bias(const bvt &exponent);
162 
163  bvt limit_distance(const bvt &dist, mp_integer limit);
164 
166  {
169 
171  sign(const_literal(false)),
172  infinity(const_literal(false)),
173  zero(const_literal(false)),
174  NaN(const_literal(false))
175  {
176  }
177  };
178 
179  // this has a biased exponent
180  // and an _implicit_ hidden bit
182  {
183  };
184 
185  // the hidden bit is explicit,
186  // and the exponent is not biased
188  {
189  };
190 
192 
193  // this takes unpacked format, and returns packed
194  virtual bvt rounder(const unbiased_floatt &);
195  bvt pack(const biased_floatt &);
196  unbiased_floatt unpack(const bvt &);
197 
198  void round_fraction(unbiased_floatt &result);
199  void round_exponent(unbiased_floatt &result);
200 
201  // rounding decision for fraction
203  const std::size_t dest_bits,
204  const literalt sign,
205  const bvt &fraction);
206 
207  // helpers for adder
208 
209  // computes src1.exponent-src2.exponent with extension
211  const unbiased_floatt &src1,
212  const unbiased_floatt &src2);
213 
214  // computes the "sticky-bit"
216  const bvt &op,
217  const bvt &dist,
218  literalt &sticky);
219 };
220 
221 #endif // CPROVER_SOLVERS_FLOATBV_FLOAT_UTILS_H
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
BigInt mp_integer
Definition: mp_arith.h:22
literalt is_minus_inf(const bvt &)
void round_exponent(unbiased_floatt &result)
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1398
bvt sub_bias(const bvt &exponent)
virtual void normalization_shift(bvt &fraction, bvt &exponent)
normalize fraction/exponent pair returns &#39;zero&#39; if fraction is zero
bvt to_signed_integer(const bvt &src, std::size_t int_width)
Definition: float_utils.cpp:67
virtual ~float_utilst()
Definition: float_utils.h:83
void denormalization_shift(bvt &fraction, bvt &exponent)
make sure exponent is not too small; the exponent is unbiased
virtual bvt rem(const bvt &src1, const bvt &src2)
literalt is_normal(const bvt &)
literalt exponent_all_ones(const bvt &)
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
Definition: float_utils.cpp:74
bvt add_bias(const bvt &exponent)
bvt negate(const bvt &)
propt & prop
Definition: float_utils.h:153
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt debug1(const bvt &op0, const bvt &op1)
bvt conversion(const bvt &src, const ieee_float_spect &dest_spec)
bvt get_exponent(const bvt &)
Gets the unbiased exponent in a floating-point bit-vector.
literalt is_zero(const bvt &)
static literalt sign_bit(const bvt &src)
Definition: float_utils.h:91
literalt is_plus_inf(const bvt &)
unbiased_floatt unpack(const bvt &)
virtual bvt div(const bvt &src1, const bvt &src2)
literalt fraction_rounding_decision(const std::size_t dest_bits, const literalt sign, const bvt &fraction)
rounding decision for fraction using sticky bit
TO_BE_DOCUMENTED.
Definition: prop.h:24
bvt get_fraction(const bvt &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
bvt debug2(const bvt &op0, const bvt &op1)
bvt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
literalt exponent_all_zeros(const bvt &)
void set_rounding_mode(const bvt &)
Definition: float_utils.cpp:15
literalt is_infinity(const bvt &)
literalt const_literal(bool value)
Definition: literal.h:187
literalt is_NaN(const bvt &)
ieee_float_spect spec
Definition: float_utils.h:87
bvt from_unsigned_integer(const bvt &)
Definition: float_utils.cpp:50
bvt add(const bvt &src1, const bvt &src2)
Definition: float_utils.h:110
rounding_mode_bitst rounding_mode_bits
Definition: float_utils.h:66
bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed)
Definition: float_utils.cpp:81
bvt abs(const bvt &)
bv_utilst bv_utils
Definition: float_utils.h:154
biased_floatt bias(const unbiased_floatt &)
takes an unbiased float, and applies the bias
float_utilst(propt &_prop)
Definition: float_utils.h:68
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
bvt limit_distance(const bvt &dist, mp_integer limit)
Limits the shift distance.
bvt from_signed_integer(const bvt &)
Definition: float_utils.cpp:32
bvt sub(const bvt &src1, const bvt &src2)
Definition: float_utils.h:115
bvt sticky_right_shift(const bvt &op, const bvt &dist, literalt &sticky)
std::vector< literalt > bvt
Definition: literal.h:200
float_utilst(propt &_prop, const floatbv_typet &type)
Definition: float_utils.h:74
virtual bvt rounder(const unbiased_floatt &)
bvt pack(const biased_floatt &)
void round_fraction(unbiased_floatt &result)
bvt build_constant(const ieee_floatt &)
literalt fraction_all_zeros(const bvt &)
literalt relation(const bvt &src1, relt rel, const bvt &src2)