Implement support for quiet NaNs
This switch changes semantics of NaNs overall such that there's no canonicalization of the bit pattern
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -78,10 +78,11 @@ expr FloatConst::getTypeConstraints() const {
StateValue FloatConst::toSMT(State &s) const {
if (auto n = get_if<string>(&val)) {
if (!bit_value)
- return { expr::mkNumber(n->c_str(), getType().getDummyValue(true).value),
+ return { expr::mkNumber(n->c_str(),
+ getType().getAsFloatType()->getDummyFloat())
+ .float2BV(),
true };
- return { expr::mkNumber(n->c_str(), expr::mkUInt(0, getType().bits()))
- .BV2float(getType().getDummyValue(true).value),
+ return { expr::mkNumber(n->c_str(), expr::mkUInt(0, getType().bits())),
true };
}
@@ -95,7 +96,7 @@ StateValue FloatConst::toSMT(State &s) const {
case FloatType::Quad:
case FloatType::Unknown: UNREACHABLE();
}
- return { std::move(e), true };
+ return { e.float2BV(), true };
}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -647,14 +647,31 @@ static expr handle_subnormal(FPDenormalAttrs::Type attr, expr &&v) {
return std::move(v);
}
-static StateValue fm_poison(State &s, const expr &a, const expr &ap,
- const expr &b, const expr &bp, const expr &c,
+static StateValue fm_poison(State &s, const expr &a0, const expr &ap,
+ const expr &b0, const expr &bp, const expr &c0,
const expr &cp,
- function<expr(expr&,expr&,expr&)> fn,
+ function<expr(const expr&, const expr&,
+ const expr&)> fn,
const Type &ty, FastMathFlags fmath,
bool only_input = false,
bool flush_denormal = true,
+ bool convert_output_bv = true,
int nary = 3) {
+ AndExpr non_poison;
+ non_poison.add(ap);
+ if (nary >= 2)
+ non_poison.add(bp);
+ if (nary >= 3)
+ non_poison.add(cp);
+
+ auto fpty = ty.getAsFloatType();
+ if (!fpty)
+ return { fn(a0, b0, c0), non_poison() };
+
+ expr a = fpty->getFloat(a0);
+ expr b = fpty->getFloat(b0);
+ expr c = fpty->getFloat(c0);
+
expr new_a, new_b, new_c;
if (fmath.flags & FastMathFlags::NSZ) {
new_a = any_fp_zero(s, a);
@@ -679,12 +696,6 @@ static StateValue fm_poison(State &s, const expr &a, const expr &ap,
}
expr val = fn(new_a, new_b, new_c);
- AndExpr non_poison;
- non_poison.add(ap);
- if (nary >= 2)
- non_poison.add(bp);
- if (nary >= 3)
- non_poison.add(cp);
if (fmath.flags & FastMathFlags::NNaN) {
non_poison.add(!a.isNaN());
@@ -725,27 +736,32 @@ static StateValue fm_poison(State &s, const expr &a, const expr &ap,
if (fmath.flags & FastMathFlags::NSZ && !only_input)
val = any_fp_zero(s, std::move(val));
- return { std::move(val), non_poison() };
+ return { convert_output_bv && val.isFloat() ? fpty->fromFloat(s, val)
+ : std::move(val),
+ non_poison() };
}
static StateValue fm_poison(State &s, const expr &a, const expr &ap,
const expr &b, const expr &bp,
- function<expr(expr&,expr&)> fn,
+ function<expr(const expr&, const expr&)> fn,
const Type &ty, FastMathFlags fmath,
bool only_input = false,
- bool flush_denormal = true) {
+ bool flush_denormal = true,
+ bool convert_output_bv = true) {
return fm_poison(s, a, ap, std::move(b), bp, expr(), expr(),
- [&](expr &a, expr &b, expr &c) { return fn(a, b); },
- ty, fmath, only_input, flush_denormal, 2);
+ [&](auto &a, auto &b, auto &c) { return fn(a, b); },
+ ty, fmath, only_input, flush_denormal, convert_output_bv, 2);
}
static StateValue fm_poison(State &s, const expr &a, const expr &ap,
- function<expr(expr&)> fn, const Type &ty,
+ function<expr(const expr&)> fn, const Type &ty,
FastMathFlags fmath, bool only_input = false,
- bool flush_denormal = true) {
+ bool flush_denormal = true,
+ bool convert_output_bv = true) {
return fm_poison(s, a, ap, expr(), expr(), expr(), expr(),
- [&](expr &a, expr &b, expr &c) { return fn(a); },
- ty, fmath, only_input, flush_denormal, 1);
+ [&](auto &a, auto &b, auto &c) { return fn(a); },
+ ty, fmath, only_input, flush_denormal,
+ convert_output_bv, 1);
}
static StateValue round_value_(const function<StateValue(FpRoundingMode)> &fn,
@@ -767,13 +783,14 @@ static StateValue round_value_(const function<StateValue(FpRoundingMode)> &fn,
}
static StateValue round_value(const function<StateValue(FpRoundingMode)> &fn,
- const State &s, const Type &ty,
- FpRoundingMode rm,
+ State &s, const Type &ty, FpRoundingMode rm,
bool enable_subnormal_flush = true) {
auto [v, np] = round_value_(fn, s, rm);
if (enable_subnormal_flush)
v = handle_subnormal(s.getFn().getFnAttrs().getFPDenormal(ty).output,
std::move(v));
+ if (auto *fpty = ty.getAsFloatType())
+ v = fpty->fromFloat(s, v);
return { std::move(v), std::move(np) };
}
@@ -857,8 +874,8 @@ StateValue FpBinOp::toSMT(State &s) const {
auto scalar = [&](const auto &a, const auto &b, const Type &ty) {
return round_value([&](auto rm) {
return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison,
- [&](expr &a, expr &b){ return fn(a, b, rm); }, ty,
- fmath, !flush_denormal, flush_denormal);
+ [&](auto &a, auto &b){ return fn(a, b, rm); }, ty,
+ fmath, !flush_denormal, flush_denormal, false);
}, s, ty, rm, flush_denormal);
};
@@ -1097,8 +1114,8 @@ StateValue FpUnaryOp::toSMT(State &s) const {
return
round_value([&](auto rm) {
return fm_poison(s, v.value, v.non_poison,
- [&](expr &v){ return fn(v, rm); }, ty, fmath,
- !flush_denormal, flush_denormal);
+ [&](auto &v){ return fn(v, rm); }, ty, fmath,
+ !flush_denormal, flush_denormal, false);
}, s, ty, rm, flush_denormal);
};
@@ -1363,8 +1380,8 @@ StateValue FpTernaryOp::toSMT(State &s) const {
return round_value([&](auto rm) {
return fm_poison(s, a.value, a.non_poison, b.value, b.non_poison,
c.value, c.non_poison,
- [&](expr &a, expr &b, expr &c){ return fn(a, b, c, rm);},
- ty, fmath);
+ [&](auto &a, auto &b, auto &c) {return fn(a, b, c, rm);},
+ ty, fmath, false, true, false);
}, s, ty, rm);
};
@@ -1424,22 +1441,23 @@ void TestOp::print(ostream &os) const {
StateValue TestOp::toSMT(State &s) const {
auto &a = s[*lhs];
auto &b = s[*rhs];
- function<expr(const expr&)> fn;
+ function<expr(const expr&, const Type&)> fn;
switch (op) {
case Is_FPClass:
- fn = [&](const expr &a) -> expr {
+ fn = [&](const expr &v, const Type &ty) -> expr {
uint64_t n;
if (!b.value.isUInt(n) || !b.non_poison.isTrue()) {
s.addUB(expr(false));
return {};
}
+ auto *fpty = ty.getAsFloatType();
+ auto a = fpty->getFloat(v);
OrExpr result;
- // TODO: distinguish between quiet and signaling NaNs
if (n & (1 << 0))
- result.add(a.isNaN());
+ result.add(fpty->isNaN(v, true));
if (n & (1 << 1))
- result.add(a.isNaN());
+ result.add(fpty->isNaN(v, false));
if (n & (1 << 2))
result.add(a.isFPNegative() && a.isInf());
if (n & (1 << 3))
@@ -1461,8 +1479,8 @@ StateValue TestOp::toSMT(State &s) const {
break;
}
- auto scalar = [&](const StateValue &v) -> StateValue {
- return { fn(v.value), expr(v.non_poison) };
+ auto scalar = [&](const StateValue &v, const Type &ty) -> StateValue {
+ return { fn(v.value, ty), expr(v.non_poison) };
};
if (getType().isVectorType()) {
@@ -1470,11 +1488,11 @@ StateValue TestOp::toSMT(State &s) const {
auto ty = lhs->getType().getAsAggregateType();
for (unsigned i = 0, e = ty->numElementsConst(); i != e; ++i) {
- vals.emplace_back(scalar(ty->extract(a, i)));
+ vals.emplace_back(scalar(ty->extract(a, i), ty->getChild(i)));
}
return getType().getAsAggregateType()->aggregateVals(vals);
}
- return scalar(a);
+ return scalar(a, lhs->getType());
}
expr TestOp::getTypeConstraints(const Function &f) const {
@@ -1669,14 +1687,14 @@ StateValue FpConversionOp::toSMT(State &s) const {
switch (op) {
case SIntToFP:
fn = [](auto &val, auto &to_type, auto rm) -> StateValue {
- return
- { val.sint2fp(to_type.getDummyValue(false).value, rm.toSMT()), true };
+ return { val.sint2fp(to_type.getAsFloatType()->getDummyFloat(),
+ rm.toSMT()), true };
};
break;
case UIntToFP:
fn = [](auto &val, auto &to_type, auto rm) -> StateValue {
- return
- { val.uint2fp(to_type.getDummyValue(false).value, rm.toSMT()), true };
+ return { val.uint2fp(to_type.getAsFloatType()->getDummyFloat(),
+ rm.toSMT()), true };
};
break;
case FPToSInt:
@@ -1716,15 +1734,19 @@ StateValue FpConversionOp::toSMT(State &s) const {
case FPExt:
case FPTrunc:
fn = [](auto &val, auto &to_type, auto rm) -> StateValue {
- return { val.float2Float(to_type.getDummyValue(false).value, rm.toSMT()),
- true };
+ return { val.float2Float(to_type.getAsFloatType()->getDummyFloat(),
+ rm.toSMT()), true };
};
break;
}
- auto scalar = [&](const StateValue &sv, const Type &to_type) -> StateValue {
+ auto scalar = [&](const StateValue &sv, const Type &from_type,
+ const Type &to_type) -> StateValue {
+ auto val = sv.value;
+ if (auto *ty = from_type.getAsFloatType())
+ val = ty->getFloat(val);
auto [v, np]
- = round_value([&](auto rm) { return fn(sv.value, to_type, rm); }, s,
+ = round_value([&](auto rm) { return fn(val, to_type, rm); }, s,
to_type, rm);
return { std::move(v), sv.non_poison && np };
};
@@ -1735,11 +1757,12 @@ StateValue FpConversionOp::toSMT(State &s) const {
auto retty = getType().getAsAggregateType();
for (unsigned i = 0, e = ty->numElementsConst(); i != e; ++i) {
- vals.emplace_back(scalar(ty->extract(v, i), retty->getChild(i)));
+ vals.emplace_back(scalar(ty->extract(v, i), ty->getChild(i),
+ retty->getChild(i)));
}
return retty->aggregateVals(vals);
}
- return scalar(v, getType());
+ return scalar(v, val->getType(), getType());
}
expr FpConversionOp::getTypeConstraints(const Function &f) const {
@@ -2552,7 +2575,7 @@ StateValue FCmp::toSMT(State &s) const {
auto &a_eval = s[*a];
auto &b_eval = s[*b];
- auto fn = [&](const auto &a, const auto &b) -> StateValue {
+ auto fn = [&](const auto &a, const auto &b, const Type &ty) -> StateValue {
auto cmp = [&](const expr &a, const expr &b) {
switch (cond) {
case OEQ: return a.foeq(b);
@@ -2574,18 +2597,19 @@ StateValue FCmp::toSMT(State &s) const {
}
};
auto [val, np] = fm_poison(s, a.value, a.non_poison, b.value, b.non_poison,
- cmp, getType(), fmath, true, true);
+ cmp, ty, fmath, true, true, false);
return { val.toBVBool(), std::move(np) };
};
if (auto agg = a->getType().getAsAggregateType()) {
vector<StateValue> vals;
for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
- vals.emplace_back(fn(agg->extract(a_eval, i), agg->extract(b_eval, i)));
+ vals.emplace_back(fn(agg->extract(a_eval, i), agg->extract(b_eval, i),
+ agg->getChild(i)));
}
return getType().getAsAggregateType()->aggregateVals(vals);
}
- return fn(a_eval, b_eval);
+ return fn(a_eval, b_eval, a->getType());
}
expr FCmp::getTypeConstraints(const Function &f) const {

MODIFY
ir/type.cpp
ir/type.cpp
@@ -393,32 +393,38 @@ static array<pair<unsigned, unsigned>, 5> float_sizes = {
/* BFloat */ make_pair(16, 8),
};
-unsigned FloatType::bits() const {
- assert(fpType != Unknown);
- return float_sizes[fpType].first;
+expr FloatType::getDummyFloat() const {
+ expr ty;
+ switch (fpType) {
+ case Half: ty = expr::mkHalf(0); break;
+ case Float: ty = expr::mkFloat(0); break;
+ case Double: ty = expr::mkDouble(0); break;
+ case Quad: ty = expr::mkQuad(0); break;
+ case BFloat: ty = expr::mkBFloat(0); break;
+ case Unknown: UNREACHABLE();
}
-
-const FloatType* FloatType::getAsFloatType() const {
- return this;
+ return ty;
}
-expr FloatType::toBV(expr e) const {
- return e.float2BV();
-}
+expr FloatType::getFloat(const expr &v) const {
+ expr ty = getDummyFloat();
-StateValue FloatType::toBV(StateValue v) const {
- return Type::toBV(std::move(v));
-}
+ if (isNaNInt(v))
+ return expr::mkNaN(ty);
-expr FloatType::fromBV(expr e) const {
- return e.BV2float(getDummyValue(true).value);
-}
+ expr cond, then, els, n, n2;
+ // match (ite (isNaN x) int_nan (fp.to_ieee_bv x))
+ if (v.isIf(cond, then, els) &&
+ cond.isNaNCheck(n) &&
+ isNaNInt(then) &&
+ els.isfloat2BV(n2) &&
+ n.eq(n2))
+ return n;
-StateValue FloatType::fromBV(StateValue v) const {
- return Type::fromBV(std::move(v));
+ return v.BV2float(ty);
}
-expr FloatType::toInt(State &s, expr fp) const {
+expr FloatType::fromFloat(State &s, const expr &fp) const {
expr isnan = fp.isNaN();
expr val = fp.float2BV();
@@ -429,6 +435,7 @@ expr FloatType::toInt(State &s, expr fp) const {
unsigned fraction_bits = bits() - exp_bits - 1;
unsigned var_bits = fraction_bits + 1;
+ // NaN has a non-deterministic non-zero fraction bit pattern
expr var = expr::mkFreshVar("NaN", expr::mkUInt(0, var_bits));
expr fraction = var.extract(fraction_bits - 1, 0);
@@ -442,8 +449,25 @@ expr FloatType::toInt(State &s, expr fp) const {
return expr::mkIf(isnan, nan, val);
}
-StateValue FloatType::toInt(State &s, StateValue v) const {
- return Type::toInt(s, std::move(v));
+expr FloatType::isNaN(const expr &v, bool signalling) const {
+ unsigned exp_bits = float_sizes[fpType].second;
+ unsigned fraction_bits = bits() - exp_bits - 1;
+
+ expr exponent = v.extract(fraction_bits + exp_bits - 1, fraction_bits);
+ expr fraction = v.extract(fraction_bits - 1, 0);
+ expr isqnan = expr::mkUF("isQNaN", { fraction }, false);
+ if (signalling)
+ isqnan = !isqnan;
+ return exponent == -1u && fraction != 0 && isqnan;
+}
+
+unsigned FloatType::bits() const {
+ assert(fpType != Unknown);
+ return float_sizes[fpType].first;
+}
+
+const FloatType* FloatType::getAsFloatType() const {
+ return this;
}
bool FloatType::isNaNInt(const expr &e) const {
@@ -469,41 +493,12 @@ bool FloatType::isNaNInt(const expr &e) const {
return ok && exponent.isAllOnes();
}
-expr FloatType::fromInt(expr e) const {
- if (isNaNInt(e))
- return expr::mkNaN(getDummyValue(true).value);
-
- expr cond, then, els, n, n2;
- // match (ite (isNaN x) int_nan (fp.to_ieee_bv x))
- if (e.isIf(cond, then, els) &&
- cond.isNaNCheck(n) &&
- isNaNInt(then) &&
- els.isfloat2BV(n2) &&
- n.eq(n2))
- return n;
-
- return fromBV(std::move(e));
-}
-
-StateValue FloatType::fromInt(StateValue v) const {
- return Type::fromInt(std::move(v));
-}
-
expr FloatType::sizeVar() const {
return defined ? expr::mkUInt(bits(), var_bw_bits) : Type::sizeVar();
}
StateValue FloatType::getDummyValue(bool non_poison) const {
- expr e;
- switch (fpType) {
- case Half: e = expr::mkHalf(0); break;
- case Float: e = expr::mkFloat(0); break;
- case Double: e = expr::mkDouble(0); break;
- case Quad: e = expr::mkQuad(0); break;
- case BFloat: e = expr::mkBFloat(0); break;
- case Unknown: UNREACHABLE();
- }
- return { std::move(e), non_poison };
+ return { expr::mkUInt(0, bits()), non_poison };
}
expr FloatType::getTypeConstraints() const {
@@ -553,30 +548,27 @@ FloatType::refines(State &src_s, State &tgt_s, const StateValue &src,
expr FloatType::mkInput(State &s, const char *name,
const ParamAttrs &attrs) const {
- switch (fpType) {
- case Half: return expr::mkHalfVar(name);
- case Float: return expr::mkFloatVar(name);
- case Double: return expr::mkDoubleVar(name);
- case Quad: return expr::mkQuadVar(name);
- case BFloat: return expr::mkBFloatVar(name);
- case Unknown: UNREACHABLE();
- }
- UNREACHABLE();
+ return expr::mkVar(name, bits());
}
void FloatType::printVal(ostream &os, const State &s, const expr &e) const {
- if (e.isNaN().isTrue()) {
- os << "NaN";
+ if (isNaN(e, true).isTrue()) {
+ os << "SNaN";
return;
}
- e.float2BV().printHexadecimal(os);
+ if (isNaN(e, false).isTrue()) {
+ os << "QNaN";
+ return;
+ }
+ e.printHexadecimal(os);
os << " (";
- if (e.isFPZero().isTrue()) {
- os << (e.isFPNegative().isTrue() ? "-0.0" : "+0.0");
- } else if (e.isInf().isTrue()) {
- os << (e.isFPNegative().isTrue() ? "-oo" : "+oo");
+ auto f = getFloat(e);
+ if (f.isFPZero().isTrue()) {
+ os << (f.isFPNegative().isTrue() ? "-0.0" : "+0.0");
+ } else if (f.isInf().isTrue()) {
+ os << (f.isFPNegative().isTrue() ? "-oo" : "+oo");
} else {
- os << e.float2Real().numeral_string();
+ os << f.float2Real().numeral_string();
}
os << ')';
}

MODIFY
ir/type.h
ir/type.h
@@ -194,6 +194,11 @@ public:
unsigned bits() const override;
FpType getFpType() const { return fpType; };
+ smt::expr getDummyFloat() const;
+ smt::expr getFloat(const smt::expr &v) const;
+ smt::expr fromFloat(State &s, const smt::expr &fp) const;
+ smt::expr isNaN(const smt::expr &v, bool signalling) const;
+
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
@@ -202,14 +207,6 @@ public:
bool isFloatType() const override;
smt::expr enforceFloatType() const override;
const FloatType* getAsFloatType() const override;
- smt::expr toBV(smt::expr e) const override;
- IR::StateValue toBV(IR::StateValue v) const override;
- smt::expr fromBV(smt::expr e) const override;
- IR::StateValue fromBV(IR::StateValue v) const override;
- smt::expr toInt(State &s, smt::expr v) const override;
- IR::StateValue toInt(State &s, IR::StateValue v) const override;
- smt::expr fromInt(smt::expr v) const override;
- IR::StateValue fromInt(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -382,6 +382,11 @@ bool expr::isBool() const {
return Z3_get_sort_kind(ctx(), sort()) == Z3_BOOL_SORT;
}
+bool expr::isFloat() const {
+ C();
+ return Z3_get_sort_kind(ctx(), sort()) == Z3_FLOATING_POINT_SORT;
+}
+
bool expr::isTrue() const {
C();
return Z3_get_bool_value(ctx(), ast()) == Z3_L_TRUE;

MODIFY
smt/expr.h
smt/expr.h
@@ -113,6 +113,7 @@ public:
bool isVar() const;
bool isBV() const;
bool isBool() const;
+ bool isFloat() const;
bool isTrue() const;
bool isFalse() const;
bool isZero() const;

Implement support for quiet NaNs
This switch changes semantics of NaNs overall such that there's no canonicalization of the bit pattern