1/*******************************************************************\
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
19 bvt round_to_plus_inf=
21 bvt round_to_minus_inf=
39 // we need to convert negative integers
44 // build an exponent (unbiased) -- this is signed!
59 // build an exponent (unbiased) -- this is signed!
91 // The following is the usual case in ANSI-C, and we optimize for that.
94 // Keep in sync with float_bvt::to_integer — the body below is a
95 // line-for-line translation of that function between the
96 // literalt/bvt and exprt APIs.
110 // if the exponent is positive, shift right by (fraction.size() - 1) minus
111 // the exponent. The shift distance is built in a bit-vector wide enough to
112 // hold both `fraction.size() - 1` and the (sign-extended) exponent, so it
113 // does not wrap for wide destination types -- e.g. a narrow source such as
114 // _Float16 (spec.e = 5) converted to a 64-bit integer. Keep in sync with
115 // float_bvt::to_integer.
124 // if the exponent is negative, we have zero anyways
128 for(std::size_t i = 0; i < result.size(); i++)
131 // chop out the right number of bits from the result
139 "result bitvector width should equal the destination bitvector width");
141 // if signed, apply sign.
146 // It's unclear what the behaviour for negative floats
147 // to integer shall be.
170 // Zero? NaN? Infinity?
174 // add 2^f, where f is the number of fraction bits,
175 // by adding f to the exponent
181 // abs(x) >= magic_number? If so, then there is no fractional part.
190 // restore the original sign bit
191 tmp2.back() = src.back();
203 // Catch the special case in which we extend,
204 // e.g. single to double.
205 // In this case, rounding can be avoided,
206 // but a denormal number may be come normal.
207 // Be careful to exclude the difficult case
208 // when denormalised numbers in the old format
209 // can be converted to denormalised numbers in the
210 // new format. Note that this is rare and will only
211 // happen with very non-standard formats.
217 // Using the fact that f doesn't include the hidden bit
228 // the fraction gets zero-padded
233 // the exponent gets sign-extended
237 // if the number was denormal and is normal in the new format,
242 // normalization_shift unconditionally extends the exponent size to avoid
243 // arithmetic overflow, but this cannot have happened here as the exponent
244 // had already been extended to dest_spec's size
248 // the flags get copied
253 // no rounding needed!
257 else // NOLINT(readability/braces)
260 // we actually need to round
287 // compute shift distance (here is the subtraction)
303 // figure out which operand has the bigger exponent
310 // swap fractions as needed
320 // limit the distance: shifting more than f+3 bits is unnecessary
323 // pad fractions with 2 zeros from below
329 // shift new_fraction2
335 // sticky bit: or of the bits lost by the right-shift
339 // need to have two extra fraction bits for addition and rounding
358 // adjust the exponent for the fact that we added two bits to the fraction
377 // 1. The zero flag isn't used apart from in divide and
378 // is only set on unpack
379 // 2. Subnormals mean that addition or subtraction can't round to 0,
380 // thus we can perform this test now
381 // 3. The rules for sign are different for zero
420 // for(std::size_t i=0; i<result.fraction.size(); i++)
421 // result.fraction[i]=const_literal(true);
423 for(std::size_t i=0; i<result.
fraction.size(); i++)
449 // bitwise or with or_upper_bits
450 for(std::size_t i=0; i<result.size(); i++)
462 // zero-extend the fractions
468 // multiply fractions
472 // extend exponents to account for overflow
473 // add two bits, as we do extra arithmetic on it later
481 // adjust, we are thowing in an extra fraction bit
482 // it has been extended above
498 // infinity * 0 is NaN!
513 // Fused multiply-add: round(src1 * src2 + src3) with a single rounding.
514 // The product src1 * src2 is computed exactly (double-width fraction),
515 // then src3 is added, and the result is rounded once.
521 // --- Exact product a*b ---
527 // Product fraction has width 2*(f+1) bits (double-width fraction w.r.t.
529 // The value is prod_fraction * 2^(prod_exponent - (prod_fraction.size()-1)).
530 // Keep full width for exact intermediate result.
541 // --- Align c's fraction to the product's wider format ---
542 // Product fraction: prod_width bits, binary point after MSB.
543 // c fraction: (f+1) bits. Pad on the right to match width, then
544 // adjust exponent to compensate.
552 // --- Add product + c (same logic as add_sub) ---
591 // NaN: any input NaN, inf*0, or inf+(-inf) in the addition
631 // pad fraction1 with zeros
637 // zero-extend fraction2
646 // is there a remainder?
649 // we throw this into the result, as one additional bit,
650 // to get the right rounding decision
654 // We will subtract the exponents;
655 // to account for overflow, we add a bit.
656 // we add a second bit for the adjust by extra fraction bits
662 // subtract exponents
665 // adjust, as we have thown in extra fraction bits
673 // Infinity? This happens when
674 // 1) dividing a non-nan/non-zero by zero, or
675 // 2) first operand is inf and second is non-nan and non-zero
676 // In particular, inf/0=inf.
692 // Division by infinity produces zero, unless we have NaN
704 /* The semantics of floating-point remainder implemented as below
705 is the sensible one. Unfortunately this is not the one required
706 by IEEE-754 or fmod / remainder. Martin has discussed the
707 'correct' semantics with Christoph and Alberto at length as
708 well as talking to various hardware designers and we still
709 hasn't found a good way to implement them in a solver.
710 We have some approaches that are correct but they really
715 // stub: do (src2.infinity ? src1 : (src1/src2)*src2))
749 // special cases: -0 and 0 are equal
754 // NaN compares to nothing
763 // signs different? trivial! Unless Zero.
768 // as long as the signs match: compare like unsigned numbers
770 // this works due to the BIAS
773 // if both are negative (and not the same), need to turn around!
874 // removes the fractional part
875 exponent.erase(exponent.begin(), exponent.begin()+
spec.
f);
878 exponent.resize(
spec.
e);
887 // removes the fractional part
888 exponent.erase(exponent.begin(), exponent.begin()+
spec.
f);
891 exponent.resize(
spec.
e);
899 // does not include hidden bit
909 // this thing is quadratic!
914 // i is the shift distance
915 for(std::size_t i=0; i<fraction.size(); i++)
919 // the bits above need to be zero
920 for(std::size_t j=0; j<i; j++)
922 !fraction[fraction.size()-1-j]);
924 // this one needs to be one
925 equal.push_back(fraction[fraction.size()-1-i]);
927 // iff all of that holds, we shift here!
930 // build shifted value
934 // build new exponent
940 // Fraction all zero? It stays zero.
941 // The exponent is undefined in that case.
952 // n-log-n alignment shifter.
953 // The worst-case shift is the number of fraction
954 // bits minus one, in case the fraction is one exactly.
958 // sign-extend to ensure the arithmetic below cannot result in overflow/underflow
964 // Fraction smaller than the max distance? Pad up with zeros.
970 for(
int d=depth-1; d>=0; d--)
972 std::size_t distance=(1<<d);
975 fraction.size() >= distance,
"fraction must be larger or equal distance");
977 // check if first 'distance'-many bits are zeros
981 // If so, shift the zeros out left by 'distance'.
982 // Otherwise, leave as is.
989 // add corresponding weight to exponent
992 "depth must be smaller than exponent size");
1008 // Is the exponent strictly less than -bias+1, i.e., exponent<-bias+1?
1009 // This is transformed to distance=(-bias+1)-exponent
1011 // Note that 1-bias is the exponent represented by 0...01,
1012 // i.e. the exponent of the smallest normal number and thus the 'base'
1013 // exponent for subnormal numbers.
1016 // Need to sign extend to avoid overflow. Note that this is a
1017 // relatively rare problem as the value needs to be close to the top
1018 // of the exponent range and then range must not have been
1019 // previously extended as add, multiply, etc. do. This is primarily
1020 // to handle casting down from larger ranges.
1033 // Care must be taken to not loose information required for the
1034 // guard and sticky bits. +3 is for the hidden, guard and sticky bits.
1035 if(fraction.size() < (
spec.
f + 3))
1037 // Add zeros at the LSB end for the guard bit to shift into
1072 // incoming: some fraction (with explicit 1),
1073 // some exponent without bias
1074 // outgoing: rounded, with right size, but still unpacked
1082 // before normalization, make sure exponent is large enough
1117 const bvt &fraction)
1121 // we have too many fraction bits
1124 // more than two extra bits are superflus, and are
1125 // turned into a sticky bit
1131 // We keep most-significant bits, and thus the tail is made
1132 // of least-significant bits.
1137 // the rounding bit is the last extra bit
1139 extra_bits >= 1,
"the extra bits include at least the rounding bit");
1142 // we get one bit of the fraction for some rounding decisions
1145 // round-to-nearest (ties to even)
1164 // round-to-nearest (ties to away)
1167 // now select appropriate one
1182 // do we need to enlarge the fraction?
1185 // pad with zeros at bottom
1194 "sizes should be equal as result.fraction was zero-padded");
1200 else // fraction gets smaller -- rounding
1205 "the extra bits should at least include the rounding bit");
1207 // this computes the rounding decision
1211 // chop off all the extra bits
1217 "sizes should be equal as extra bits were chopped off from "
1221 // *** does not catch when the overflow goes subnormal -> normal ***
1222 // incrementing the fraction might result in an overflow
1230 // In case of an overflow, the exponent has to be incremented.
1231 // "Post normalization" is then required.
1235 // post normalization of the fraction
1244 // When incrementing due to rounding there are two edge
1245 // cases we need to be aware of:
1246 // 1. If the number is normal, the increment can overflow.
1247 // In this case we need to increment the exponent and
1248 // set the MSB of the fraction to 1.
1249 // 2. If the number is the largest subnormal, the increment
1250 // can change the MSB making it normal. Thus the exponent
1251 // must be incremented but the fraction will be OK.
1256 // Normal overflow when old MSB == 1 and new MSB == 0
1259 // Subnormal to normal transition when old MSB == 0 and new MSB == 1
1263 // In case of an overflow or subnormal to normal conversion,
1264 // the exponent has to be incremented.
1269 // post normalization of the fraction
1270 // In the case of overflow, set the MSB to 1
1271 // The subnormal case will have (only) the MSB set to 1
1281 // do we need to enlarge the exponent?
1286 else // exponent gets smaller -- chop off top bits
1291 // max_exponent is the maximum representable
1292 // i.e. 1 higher than the maximum possible for a normal number
1297 // the exponent is garbage if the fractional is zero
1305 // Directed rounding modes round overflow to the maximum normal
1306 // depending on the particular mode and the sign
1350 // we need to bias the new exponent
1353 // strip off hidden bit
1361 // make exponent zero if its denormal
1363 for(std::size_t i=0; i<result.
exponent.size(); i++)
1402 // unbias the exponent
1426 // we make this 'false' for NaN
1427 result[result.size()-1]=
1433 // just copy fraction
1434 for(std::size_t i=0; i<
spec.
f; i++)
1440 for(std::size_t i=0; i<
spec.
e; i++)
1452 for(std::size_t i=0; i<src.size(); i++)
1479 if(d<=result.size())
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
static bvt inverted(const bvt &op)
literalt signed_less_than(const bvt &bv0, const bvt &bv1)
literalt is_all_ones(const bvt &op)
literalt is_not_zero(const bvt &op)
static bvt extract_msb(const bvt &a, std::size_t n)
bvt add(const bvt &op0, const bvt &op1)
static bvt zero_extension(const bvt &bv, std::size_t new_size)
bvt absolute_value(const bvt &op)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
static bvt build_constant(const mp_integer &i, std::size_t width)
literalt is_zero(const bvt &op)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
literalt unsigned_less_than(const bvt &bv0, const bvt &bv1)
bvt incrementer(const bvt &op, literalt carry_in)
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
static bvt concatenate(const bvt &a, const bvt &b)
bvt sub(const bvt &op0, const bvt &op1)
static bvt extract(const bvt &a, std::size_t first, std::size_t last)
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
void unsigned_divider(const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
bvt cond_negate(const bvt &bv, const literalt cond)
static bvt zeros(std::size_t new_size)
static bvt sign_extension(const bvt &bv, std::size_t new_size)
unbiased_floatt rounder(const unbiased_floatt &)
bvt to_integer(const bvt &src, std::size_t int_width, bool is_signed)
literalt is_NaN(const bvt &)
virtual void normalization_shift(bvt &fraction, bvt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
bvt debug2(const bvt &op0, const bvt &op1)
virtual bvt rem(const bvt &src1, const bvt &src2)
bvt round_to_integral(const bvt &)
literalt is_plus_inf(const bvt &)
ieee_float_valuet get(const bvt &) const
literalt is_infinity(const bvt &)
void set_rounding_mode(const bvt &)
void round_exponent(unbiased_floatt &result)
void round_fraction(unbiased_floatt &result)
bvt sticky_right_shift(const bvt &op, const bvt &dist, literalt &sticky)
unbiased_floatt unpack(const bvt &)
bvt from_unsigned_integer(const bvt &)
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt debug1(const bvt &op0, const bvt &op1)
bvt add_bias(const bvt &exponent)
bvt round_and_pack(const unbiased_floatt &)
bvt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
bvt get_fraction(const bvt &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
literalt is_minus_inf(const bvt &)
literalt fraction_rounding_decision(const std::size_t dest_bits, const literalt sign, const bvt &fraction)
rounding decision for fraction using sticky bit
bvt get_exponent(const bvt &)
Gets the unbiased exponent in a floating-point bit-vector.
void denormalization_shift(bvt &fraction, bvt &exponent)
make sure exponent is not too small; the exponent is unbiased
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
bvt build_constant(const ieee_float_valuet &)
virtual bvt div(const bvt &src1, const bvt &src2)
literalt exponent_all_zeros(const bvt &)
literalt fraction_all_zeros(const bvt &)
bvt fma(const bvt &multiply_lhs, const bvt &multiply_rhs, const bvt &addend)
Fused multiply-add: round(multiply_lhs * multiply_rhs + addend) with a single rounding step.
bvt from_signed_integer(const bvt &)
literalt is_zero(const bvt &)
bvt sub(const bvt &src1, const bvt &src2)
bvt sub_bias(const bvt &exponent)
bvt limit_distance(const bvt &dist, mp_integer limit)
Limits the shift distance.
bvt conversion(const bvt &src, const ieee_float_spect &dest_spec)
bvt pack(const biased_floatt &)
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
static literalt sign_bit(const bvt &src)
literalt exponent_all_ones(const bvt &)
bvt to_signed_integer(const bvt &src, std::size_t int_width)
literalt is_normal(const bvt &)
literalt relation(const bvt &src1, relt rel, const bvt &src2)
rounding_mode_bitst rounding_mode_bits
biased_floatt bias(const unbiased_floatt &)
takes an unbiased float, and applies the bias
mp_integer max_exponent() const
std::size_t width() const
An IEEE 754 floating-point value, including specificiation.
const mp_integer & get_fraction() const
void unpack(const mp_integer &)
const mp_integer & get_exponent() const
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
virtual literalt land(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lxor(literalt a, literalt b)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
virtual literalt new_variable()=0
virtual literalt lor(literalt a, literalt b)=0
virtual tvt l_get(literalt a) const =0
std::vector< literalt > bvt
literalt const_literal(bool value)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
literalt round_to_minus_inf
literalt round_to_plus_inf
bool is_signed(const typet &t)
Convenience function – is the type signed?