diff --git a/ir/instr.cpp b/ir/instr.cpp index 3d0e64f50..ef9ac5d7d 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -772,7 +772,7 @@ static StateValue fm_poison(State &s, expr a, const expr &ap, expr b, if (!bitwise && val.isFloat()) { val = handle_subnormal(s, s.getFn().getFnAttrs().getFPDenormal(ty).output, std::move(val)); - val = fpty->fromFloat(s, val, nary, a, b, c); + val = fpty->fromFloat(s, val, *fpty, nary, a, b, c); } return { std::move(val), non_poison() }; @@ -1767,7 +1767,8 @@ StateValue FpConversionOp::toSMT(State &s) const { return { to_type.isFloatType() ? to_type.getAsFloatType() - ->fromFloat(s, ret.value, from_type.isFloatType(), sv.value) + ->fromFloat(s, ret.value, from_type, from_type.isFloatType(), + sv.value) : std::move(ret.value), np()}; }; diff --git a/ir/type.cpp b/ir/type.cpp index dafb9f0c5..9417699c2 100644 --- a/ir/type.cpp +++ b/ir/type.cpp @@ -424,8 +424,8 @@ expr FloatType::getFloat(const expr &v) const { return v.BV2float(ty); } -expr FloatType::fromFloat(State &s, const expr &fp, unsigned nary, - const expr &a, const expr &b, +expr FloatType::fromFloat(State &s, const expr &fp, const Type &from_type0, + unsigned nary, const expr &a, const expr &b, const expr &c) const { expr isnan = fp.isNaN(); expr val = fp.float2BV(); @@ -433,8 +433,7 @@ expr FloatType::fromFloat(State &s, const expr &fp, unsigned nary, if (isnan.isFalse()) return val; - unsigned exp_bits = float_sizes[fpType].second; - unsigned fraction_bits = bits() - exp_bits - 1 /* sign */; + unsigned fraction_bits = fractionBits(); unsigned var_bits = fraction_bits-1 + 1 /* sign */; // sign bit, exponent (-1), qnan bit (1) or snan (0), rest of fraction @@ -447,16 +446,24 @@ expr FloatType::fromFloat(State &s, const expr &fp, unsigned nary, // 2) input NaN // 3) quieted input NaN + const FloatType &from_type = *from_type0.getAsFloatType(); + auto maybe_quiet = [&](const expr &e) { - expr qnan = e.extract(fraction_bits - 1, fraction_bits - 1); - return (qnan | var.extract(0, 0)).concat(e.extract(fraction_bits - 2, 0)); + // account for fpext/fptruc + expr fraction = e.trunc(min(from_type.fractionBits(), fraction_bits)); + if (fraction.bits() < fraction_bits) + fraction = fraction.concat_zeros(fraction_bits - fraction.bits()); + assert(!fraction.isValid() || fraction.bits() == fraction_bits); + + expr qnan = fraction.extract(fraction_bits - 1, fraction_bits - 1); + return (qnan | var.extract(0, 0)).concat(fraction.trunc(fraction_bits - 1)); }; if (nary >= 1) { - exprs.add(maybe_quiet(a), getFloat(a).isNaN()); + exprs.add(maybe_quiet(a), from_type.getFloat(a).isNaN()); if (nary >= 2) { - exprs.add(maybe_quiet(b), getFloat(b).isNaN()); + exprs.add(maybe_quiet(b), from_type.getFloat(b).isNaN()); if (nary >= 3) - exprs.add(maybe_quiet(c), getFloat(c).isNaN()); + exprs.add(maybe_quiet(c), from_type.getFloat(c).isNaN()); } } @@ -467,7 +474,7 @@ expr FloatType::fromFloat(State &s, const expr &fp, unsigned nary, auto [fraction, domain, choice_var, pre] = std::move(exprs)(); assert(!domain.isValid() || domain.isTrue()); - expr nan = var.sign().concat(expr::mkInt(-1, exp_bits)).concat(fraction); + expr nan = var.sign().concat(expr::mkInt(-1, expBits())).concat(fraction); assert(isNaNInt(nan)); s.addNonDetVar(std::move(choice_var)); @@ -477,10 +484,9 @@ expr FloatType::fromFloat(State &s, const expr &fp, unsigned nary, } expr FloatType::isNaN(const expr &v, bool signalling) const { - unsigned exp_bits = float_sizes[fpType].second; - unsigned fraction_bits = bits() - exp_bits - 1; + unsigned fraction_bits = fractionBits(); - expr bits = v.extract(fraction_bits + exp_bits - 1, fraction_bits - 1); + expr bits = v.extract(fraction_bits + expBits() - 1, fraction_bits - 1); if (signalling) { expr fraction = v.extract(fraction_bits - 2, 0); return bits == (UINT64_MAX << 1ull) && fraction != 0; @@ -494,6 +500,15 @@ unsigned FloatType::bits() const { return float_sizes[fpType].first; } +unsigned FloatType::expBits() const { + assert(fpType != Unknown); + return float_sizes[fpType].second; +} + +unsigned FloatType::fractionBits() const { + return bits() - expBits() - 1 /* sign bit */; +} + const FloatType* FloatType::getAsFloatType() const { return this; } @@ -505,18 +520,16 @@ bool FloatType::isNaNInt(const expr &e) const { // unsigned var_bits = fraction_bits-1 + 1 /* sign */; // expr var = s.getFreshNondetVar("#NaN", expr::mkUInt(0, var_bits)); // var.sign().concat(expr::mkInt(-1, exp_bits)).concat(fraction) - auto bw = e.bits(); - unsigned exp_bits = float_sizes[fpType].second; - unsigned fraction_bits = bw - exp_bits - 1 /* sign bit */; + auto bw = bits(); - expr exponent = e.extract(bw - 2, fraction_bits); - assert(exponent.bits() == exp_bits); + expr exponent = e.extract(bw - 2, fractionBits()); + assert(exponent.bits() == expBits()); expr nan; unsigned h, l; return exponent.isAllOnes() && e.sign().isExtract(nan, h, l) && - h == l && h == fraction_bits - 1 && + h == l && h == fractionBits() - 1 && nan.fn_name().starts_with("#NaN"); } diff --git a/ir/type.h b/ir/type.h index 7cf18a887..d56897130 100644 --- a/ir/type.h +++ b/ir/type.h @@ -185,6 +185,8 @@ class FloatType final : public Type { FpType fpType = Unknown; bool defined = false; + unsigned expBits() const; + unsigned fractionBits() const; bool isNaNInt(const smt::expr &e) const; public: @@ -196,9 +198,9 @@ class FloatType final : public Type { smt::expr getDummyFloat() const; smt::expr getFloat(const smt::expr &v) const; - smt::expr fromFloat(State &s, const smt::expr &fp, unsigned nary, - const smt::expr &a, const smt::expr &b = {}, - const smt::expr &c = {}) const; + smt::expr fromFloat(State &s, const smt::expr &fp, const Type &from_type, + unsigned nary, const smt::expr &a, + const smt::expr &b = {}, const smt::expr &c = {}) const; smt::expr isNaN(const smt::expr &v, bool signalling) const; IR::StateValue getDummyValue(bool non_poison) const override;