NaN vars are also non-deterministic values
so they must be taken into account when making the undef-ness refinement formula
MODIFY
ir/type.cpp
ir/type.cpp
@@ -490,7 +490,7 @@ bool FloatType::isNaNInt(const expr &e) const {
bool ok = sign.isExtract(nan, h, l) && fraction.isExtract(nan2, h, l) &&
nan.eq(nan2);
auto nan_name = nan.fn_name();
- ok &= string_view(nan_name).substr(0, 4) == "NaN!";
+ ok &= nan_name.starts_with("NaN!");
return ok && exponent.isAllOnes();
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -367,6 +367,8 @@ static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
// forall I .
// (forall N . src_nonpoison(I, N) /\ retval_src(I, N) == retval_src(I, 0))
// -> (forall N . retval_tgt(I, N) == retval_tgt(I, 0)
+ // FIXME? this is an approximation. Instead of 0, it should be N' because
+ // 0 may fail a precondition.
if (dynamic_cast<const VoidType *>(&type))
return false;
@@ -379,6 +381,10 @@ static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
for (auto &v : val.undef_vars) {
repls.emplace_back(v, expr::some(v));
}
+ for (auto &v : val.val.value.vars()) {
+ if (v.fn_name().starts_with("NaN!"))
+ repls.emplace_back(v, expr::some(v));
+ }
return val.val.value.subst(repls);
};

NaN vars are also non-deterministic values
so they must be taken into account when making the undef-ness refinement formula