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 
16 #include "../flattening/bv_utils.h"
17 
18 class float_bvt
19 {
20 public:
22  {
23  }
24 
26  {
27  }
28 
29  exprt operator()(const exprt &src)
30  {
31  return convert(src);
32  }
33 
34  exprt convert(const exprt &);
35 
36  exprt negation(const exprt &, const ieee_float_spect &);
37  exprt abs(const exprt &, const ieee_float_spect &);
38  exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &);
39  exprt is_zero(const exprt &, const ieee_float_spect &);
40  exprt isnan(const exprt &, const ieee_float_spect &);
41  exprt isinf(const exprt &, const ieee_float_spect &);
42  exprt isnormal(const exprt &, const ieee_float_spect &);
43  exprt isfinite(const exprt &, const ieee_float_spect &);
44 
45  // add/sub
46  exprt add_sub(
47  bool subtract,
48  const exprt &,
49  const exprt &,
50  const exprt &rm,
51  const ieee_float_spect &);
52 
53  // mul/div
54  exprt mul(
55  const exprt &,
56  const exprt &,
57  const exprt &rm,
58  const ieee_float_spect &);
59  exprt div(
60  const exprt &,
61  const exprt &,
62  const exprt &rm,
63  const ieee_float_spect &);
64 
65  // conversion
67  const exprt &,
68  const exprt &rm,
69  const ieee_float_spect &);
71  const exprt &,
72  const exprt &rm,
73  const ieee_float_spect &);
75  const exprt &src,
76  std::size_t dest_width,
77  const exprt &rm,
78  const ieee_float_spect &);
80  const exprt &src,
81  std::size_t dest_width,
82  const exprt &rm,
83  const ieee_float_spect &);
85  const exprt &src,
86  std::size_t dest_width,
87  bool is_signed,
88  const exprt &rm,
89  const ieee_float_spect &);
91  const exprt &src,
92  const exprt &rm,
93  const ieee_float_spect &src_spec,
94  const ieee_float_spect &dest_spec);
95 
96  // relations
97  enum class relt { LT, LE, EQ, GT, GE };
99  const exprt &,
100  relt rel,
101  const exprt &,
102  const ieee_float_spect &);
103 
104 protected:
105  // helpers
107  // still biased
108  exprt get_exponent(const exprt &, const ieee_float_spect &);
109  // without hidden bit
110  exprt get_fraction(const exprt &, const ieee_float_spect &);
111  exprt sign_bit(const exprt &);
112 
113  exprt exponent_all_ones(const exprt &, const ieee_float_spect &);
116 
118  {
119  public:
120  // these are mutually exclusive, obviously
125 
126  void get(const exprt &rm);
127  explicit rounding_mode_bitst(const exprt &rm) { get(rm); }
128  };
129 
130  // unpacked
131  void normalization_shift(exprt &fraction, exprt &exponent);
133  exprt &fraction,
134  exprt &exponent,
135  const ieee_float_spect &);
136 
137  exprt add_bias(const exprt &exponent, const ieee_float_spect &);
138  exprt sub_bias(const exprt &exponent, const ieee_float_spect &);
139 
140  exprt limit_distance(const exprt &dist, mp_integer limit);
141 
143  {
144  exprt sign, infinity, zero, NaN;
145  exprt fraction, exponent;
146 
148  sign(false_exprt()),
149  infinity(false_exprt()),
150  zero(false_exprt()),
151  NaN(false_exprt())
152  {
153  }
154  };
155 
156  // This has a biased exponent (unsigned)
157  // and an _implicit_ hidden bit.
159  {
160  };
161 
162  // The hidden bit is explicit,
163  // and the exponent is not biased (signed)
165  {
166  };
167 
169 
170  // this takes unpacked format, and returns packed
171  virtual exprt rounder(
172  const unbiased_floatt &,
173  const exprt &rm,
174  const ieee_float_spect &);
175  exprt pack(const biased_floatt &, const ieee_float_spect &);
176  unbiased_floatt unpack(const exprt &, const ieee_float_spect &);
177 
178  void round_fraction(
179  unbiased_floatt &result,
180  const rounding_mode_bitst &,
181  const ieee_float_spect &);
182  void round_exponent(
183  unbiased_floatt &result,
184  const rounding_mode_bitst &,
185  const ieee_float_spect &);
186 
187  // rounding decision for fraction
189  const std::size_t dest_bits,
190  const exprt sign,
191  const exprt &fraction,
192  const rounding_mode_bitst &);
193 
194  // helpers for adder
195 
196  // computes src1.exponent-src2.exponent with extension
198  const unbiased_floatt &src1,
199  const unbiased_floatt &src2);
200 
201  // computes the "sticky-bit"
203  const exprt &op,
204  const exprt &dist,
205  exprt &sticky);
206 };
207 
208 inline exprt float_bv(const exprt &src)
209 {
210  return float_bvt()(src);
211 }
212 
213 #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:1227
exprt isinf(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:836
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:598
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:745
ieee_float_spect get_spec(const exprt &)
Definition: float_bv.cpp:98
BigInt mp_integer
Definition: mp_arith.h:19
exprt add_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1335
exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
Definition: float_bv.cpp:404
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:281
exprt convert(const exprt &)
Definition: float_bv.cpp:17
exprt pack(const biased_floatt &, const ieee_float_spect &)
Definition: float_bv.cpp:1388
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:241
exprt sign_bit(const exprt &)
Definition: float_bv.cpp:210
exprt negation(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:115
float_bvt()
Definition: float_bv.h:21
void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Definition: float_bv.cpp:1117
biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
Definition: float_bv.cpp:1302
exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:272
exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:167
virtual exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:1009
exprt isnormal(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:394
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:176
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec)
Definition: float_bv.cpp:329
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:217
exprt abs(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:104
The boolean constant false.
Definition: std_expr.h:3753
exprt float_bv(const exprt &src)
Definition: float_bv.h:208
exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
Definition: float_bv.cpp:853
exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
Definition: float_bv.cpp:1345
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:1054
exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
Definition: float_bv.cpp:1423
exprt is_zero(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:148
Base class for all expressions.
Definition: expr.h:46
exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
Definition: float_bv.cpp:572
~float_bvt()
Definition: float_bv.h:25
unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:1355
void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns &#39;zero&#39; if fraction is zero
Definition: float_bv.cpp:881
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:424
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:653
exprt isfinite(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:845
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:863
exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:185
rounding_mode_bitst(const exprt &rm)
Definition: float_bv.h:127
exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Definition: float_bv.cpp:263
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:930
exprt operator()(const exprt &src)
Definition: float_bv.h:29
exprt isnan(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:872