fix bitcast float->int to yield all possible NaN values
fixes
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -758,14 +758,14 @@ StateValue ConversionOp::toSMT(State &s) const {
};
break;
case BitCast:
- fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [&s](auto &val, auto &from_type, auto &to_type) -> StateValue {
expr newval;
if ((to_type.isIntType() && from_type.isIntType()) ||
(to_type.isFloatType() && from_type.isFloatType()) ||
(to_type.isPtrType() && from_type.isPtrType()))
newval = val;
else if (to_type.isIntType() && from_type.isFloatType())
- newval = val.float2BV();
+ newval = from_type.getAsFloatType()->toInt(s, val);
else if (to_type.isFloatType() && from_type.isIntType())
newval = val.BV2float(to_type.getDummyValue(true).value);
else

MODIFY
ir/type.cpp
ir/type.cpp
@@ -341,15 +341,40 @@ void IntType::print(ostream &os) const {
}
-static array<unsigned, 3> float_sizes = {
- /* Half */ 16,
- /* Float */ 32,
- /* Double */ 64,
+// total bits, exponent bits
+static array<pair<unsigned, unsigned>, 3> float_sizes = {
+ /* Half */ make_pair(16, 5),
+ /* Float */ make_pair(32, 8),
+ /* Double */ make_pair(64, 11),
};
unsigned FloatType::bits() const {
assert(fpType != Unknown);
- return float_sizes[fpType];
+ return float_sizes[fpType].first;
+}
+
+expr FloatType::toInt(State &s, const expr &fp) const {
+ expr isnan = fp.isNaN();
+ expr val = fp.float2BV();
+
+ if (isnan.isFalse())
+ return val;
+
+ unsigned exp_bits = float_sizes[fpType].second;
+ unsigned fraction_bits = bits() - exp_bits - 1;
+ unsigned var_bits = fraction_bits + 1;
+
+ expr var = expr::mkFreshVar("NaN", expr::mkUInt(0, var_bits));
+ expr fraction = var.extract(fraction_bits - 1, 0);
+
+ // sign bit, exponent (-1), fraction (non-zero)
+ expr nan = var.extract(fraction_bits, fraction_bits)
+ .concat(expr::mkInt(-1, exp_bits))
+ .concat(fraction);
+ s.addPre(fraction != 0);
+ s.addQuantVar(var);
+
+ return expr::mkIf(isnan, nan, val);
}
const FloatType* FloatType::getAsFloatType() const {
@@ -393,7 +418,7 @@ expr FloatType::getTypeConstraints() const {
expr r(false);
for (auto sz : float_sizes) {
- r |= sizeVar() == sz;
+ r |= sizeVar() == sz.first;
}
return r;
}
@@ -408,7 +433,7 @@ void FloatType::fixup(const Model &m) {
unsigned m_sz = m.getUInt(sizeVar());
for (unsigned i = 0, e = float_sizes.size(); i != e; ++i) {
- if (m_sz == float_sizes[i]) {
+ if (m_sz == float_sizes[i].first) {
fpType = FpType(i);
return;
}

MODIFY
ir/type.h
ir/type.h
@@ -176,6 +176,8 @@ public:
: Type(std::move(name)), fpType(fpType), defined(true) {}
unsigned bits() const override;
FpType getFpType() const { return fpType; };
+ smt::expr toInt(State &s, const smt::expr &fp) const;
+
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;

MODIFY
tests/unit/fpbitcast.opt
tests/unit/fpbitcast.opt
+; TEST-ARGS: -disable-undef-input
+
Name: NaN
%v = fdiv half %a, 0.0
%r = bitcast %v to i16
@@ -5,4 +7,14 @@ Name: NaN
%v = fdiv half %a, 0.0
%r = bitcast %v to i16
-; XFAIL: Value mismatch
+Name: NaN 2
+%v = fdiv float 0.0, 0.0
+%r = bitcast %v to i32
+ =>
+%r = i32 0x7f800001
+
+Name: NaN 3
+%v = fdiv float 0.0, 0.0
+%r = bitcast %v to i32
+ =>
+%r = i32 0xff800002

MODIFY
tests/unit/fpbitcast2.opt
tests/unit/fpbitcast2.opt
+Name: NaN 2
%v = fdiv float 0.0, 0.0
%r = bitcast %v to i32
=>
-%r = i32 0x7f800001
+%r = i32 0x7f800000
-; XFAIL: Value mismatch
+; ERROR: Value mismatch

DELETE
tests/unit/fpbitcast3.opt
-%v = fdiv float 0.0, 0.0
-%r = bitcast %v to i32
- =>
-%r = i32 0x7f800002
-
-; TODO
-; XFAIL: Value mismatch

fix bitcast float->int to yield all possible NaN values
fixes #160