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: assert(false);
61  }
62  }
63  };
64 
66 
67  explicit float_utilst(propt &_prop):
68  prop(_prop),
69  bv_utils(_prop)
70  {
71  }
72 
73  float_utilst(propt &_prop, const floatbv_typet &type):
74  spec(ieee_float_spect(type)),
75  prop(_prop),
76  bv_utils(_prop)
77  {
78  }
79 
80  void set_rounding_mode(const bvt &);
81 
82  virtual ~float_utilst()
83  {
84  }
85 
87 
89 
90  static inline literalt sign_bit(const bvt &src)
91  {
92  // this is the top bit
93  return src[src.size()-1];
94  }
95 
96  // extraction
97  bvt get_exponent(const bvt &); // still biased
98  bvt get_fraction(const bvt &); // without hidden bit
99  literalt is_normal(const bvt &);
100  literalt is_zero(const bvt &); // this returns true on both 0 and -0
101  literalt is_infinity(const bvt &);
102  literalt is_plus_inf(const bvt &);
103  literalt is_minus_inf(const bvt &);
104  literalt is_NaN(const bvt &);
105 
106  // add/sub
107  virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract);
108 
109  bvt add(const bvt &src1, const bvt &src2)
110  {
111  return add_sub(src1, src2, false);
112  }
113 
114  bvt sub(const bvt &src1, const bvt &src2)
115  {
116  return add_sub(src1, src2, true);
117  }
118 
119  // mul/div/rem
120  virtual bvt mul(const bvt &src1, const bvt &src2);
121  virtual bvt div(const bvt &src1, const bvt &src2);
122  virtual bvt rem(const bvt &src1, const bvt &src2);
123 
124  bvt abs(const bvt &);
125  bvt negate(const bvt &);
126 
127  // conversion
128  bvt from_unsigned_integer(const bvt &);
129  bvt from_signed_integer(const bvt &);
130  bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed);
131  bvt to_signed_integer(const bvt &src, std::size_t int_width);
132  bvt to_unsigned_integer(const bvt &src, std::size_t int_width);
133  bvt conversion(const bvt &src, const ieee_float_spect &dest_spec);
134 
135  // relations
136  enum class relt { LT, LE, EQ, GT, GE };
137  literalt relation(const bvt &src1, relt rel, const bvt &src2);
138 
139  // constants
140  ieee_floatt get(const bvt &) const;
141 
142  // helpers
143  literalt exponent_all_ones(const bvt &);
146 
147  // debugging hooks
148  bvt debug1(const bvt &op0, const bvt &op1);
149  bvt debug2(const bvt &op0, const bvt &op1);
150 
151 protected:
154 
155  // unpacked
156  virtual void normalization_shift(bvt &fraction, bvt &exponent);
157  void denormalization_shift(bvt &fraction, bvt &exponent);
158 
159  bvt add_bias(const bvt &exponent);
160  bvt sub_bias(const bvt &exponent);
161 
162  bvt limit_distance(const bvt &dist, mp_integer limit);
163 
165  {
168 
170  sign(const_literal(false)),
171  infinity(const_literal(false)),
172  zero(const_literal(false)),
173  NaN(const_literal(false))
174  {
175  }
176  };
177 
178  // this has a biased exponent
179  // and an _implicit_ hidden bit
181  {
182  };
183 
184  // the hidden bit is explicit,
185  // and the exponent is not biased
187  {
188  };
189 
191 
192  // this takes unpacked format, and returns packed
193  virtual bvt rounder(const unbiased_floatt &);
194  bvt pack(const biased_floatt &);
195  unbiased_floatt unpack(const bvt &);
196 
197  void round_fraction(unbiased_floatt &result);
198  void round_exponent(unbiased_floatt &result);
199 
200  // rounding decision for fraction
202  const std::size_t dest_bits,
203  const literalt sign,
204  const bvt &fraction);
205 
206  // helpers for adder
207 
208  // computes src1.exponent-src2.exponent with extension
210  const unbiased_floatt &src1,
211  const unbiased_floatt &src2);
212 
213  // computes the "sticky-bit"
215  const bvt &op,
216  const bvt &dist,
217  literalt &sticky);
218 };
219 
220 #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:1342
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:68
virtual ~float_utilst()
Definition: float_utils.h:82
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:75
bvt add_bias(const bvt &exponent)
bvt negate(const bvt &)
propt & prop
Definition: float_utils.h:152
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:90
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:16
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:86
bvt from_unsigned_integer(const bvt &)
Definition: float_utils.cpp:51
bvt add(const bvt &src1, const bvt &src2)
Definition: float_utils.h:109
rounding_mode_bitst rounding_mode_bits
Definition: float_utils.h:65
bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed)
Definition: float_utils.cpp:82
bvt abs(const bvt &)
bv_utilst bv_utils
Definition: float_utils.h:153
biased_floatt bias(const unbiased_floatt &)
takes an unbiased float, and applies the bias
float_utilst(propt &_prop)
Definition: float_utils.h:67
bvt limit_distance(const bvt &dist, mp_integer limit)
Limits the shift distance.
bvt from_signed_integer(const bvt &)
Definition: float_utils.cpp:33
bvt sub(const bvt &src1, const bvt &src2)
Definition: float_utils.h:114
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:73
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)