semantics of fabs/fneg: make sign bit non-deterministic for NaN
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1103,7 +1103,7 @@ void FpUnaryOp::print(ostream &os) const {
}
StateValue FpUnaryOp::toSMT(State &s) const {
- expr (*fn)(const expr&, FpRoundingMode) = nullptr;
+ function<expr(const expr&, const Type&, FpRoundingMode)> fn;
bool bitwise = false;
bool normalize = true;
@@ -1111,45 +1111,77 @@ StateValue FpUnaryOp::toSMT(State &s) const {
case FAbs:
bitwise = true;
normalize = false;
- fn = [](const expr &v, FpRoundingMode rm) { return v.fabs(); };
+ fn = [&](const expr &v, const Type &ty, FpRoundingMode rm) {
+ auto isnan = ty.getAsFloatType()->getFloat(v).isNaN();
+ auto abs = v.fabs();
+ if (isnan.isFalse())
+ return abs;
+
+ expr flip = expr::mkFreshVar("#flipsign", false);
+ s.addNondetVar(flip);
+ return expr::mkIf(isnan, expr::mkIf(flip, v, v.fneg()), abs);
+ };
break;
case FNeg:
bitwise = true;
normalize = false;
- fn = [](const expr &v, FpRoundingMode rm) { return v.fneg(); };
+ fn = [&](const expr &v, const Type &ty, FpRoundingMode rm) {
+ auto isnan = ty.getAsFloatType()->getFloat(v).isNaN();
+ auto neg = v.fneg();
+ if (isnan.isFalse())
+ return neg;
+
+ expr flip = expr::mkFreshVar("#flipsign", false);
+ s.addNondetVar(flip);
+ return expr::mkIf(isnan && flip, v, neg);
+ };
break;
case Canonicalize:
- fn = [](const expr &v, FpRoundingMode rm) { return v; };
+ fn = [](const expr &v, const Type &ty, FpRoundingMode rm) { return v; };
break;
case Ceil:
- fn = [](const expr &v, FpRoundingMode rm) { return v.ceil(); };
+ fn = [](const expr &v, const Type &ty, FpRoundingMode rm) {
+ return v.ceil();
+ };
break;
case Floor:
- fn = [](const expr &v, FpRoundingMode rm) { return v.floor(); };
+ fn = [](const expr &v, const Type &ty, FpRoundingMode rm) {
+ return v.floor();
+ };
break;
case RInt:
case NearbyInt:
// TODO: they differ in exception behavior
- fn = [](const expr &v, FpRoundingMode rm) { return v.round(rm.toSMT()); };
+ fn = [](const expr &v, const Type &ty, FpRoundingMode rm) {
+ return v.round(rm.toSMT());
+ };
break;
case Round:
- fn = [](const expr &v, FpRoundingMode rm) { return v.round(expr::rna()); };
+ fn = [](const expr &v, const Type &ty, FpRoundingMode rm) {
+ return v.round(expr::rna());
+ };
break;
case RoundEven:
- fn = [](const expr &v, FpRoundingMode rm) { return v.round(expr::rne()); };
+ fn = [](const expr &v, const Type &ty, FpRoundingMode rm) {
+ return v.round(expr::rne());
+ };
break;
case Trunc:
- fn = [](const expr &v, FpRoundingMode rm) { return v.round(expr::rtz()); };
+ fn = [](const expr &v, const Type &ty, FpRoundingMode rm) {
+ return v.round(expr::rtz());
+ };
break;
case Sqrt:
- fn = [](const expr &v, FpRoundingMode rm) { return v.sqrt(rm.toSMT()); };
+ fn = [](const expr &v, const Type &ty, FpRoundingMode rm) {
+ return v.sqrt(rm.toSMT());
+ };
break;
}
auto scalar = [&](const StateValue &v, const Type &ty) {
return fm_poison(s, v.value, v.non_poison,
- [fn](auto &v, auto rm){ return fn(v, rm); }, ty, fmath, rm,
- bitwise, false, normalize);
+ [&](auto &v, auto rm){ return fn(v, ty, rm); }, ty, fmath,
+ rm, bitwise, false, normalize);
};
auto &v = s[*val];

MODIFY
tests/alive-tv/fp/fabs.srctgt.ll
tests/alive-tv/fp/fabs.srctgt.ll
@@ -26,9 +26,8 @@ define void @tgt() {
%zero = fdiv float 0.0, 1.0
%inf = fdiv float 1.0, 0.0
%nan = fdiv float 0.0, 0.0
- %posnan = call float @llvm.fabs.f32(float %nan)
- call void @f(float %one, float %one, float %zero, float %zero, float %inf, float %inf, float %posnan, float %posnan)
+ call void @f(float %one, float %one, float %zero, float %zero, float %inf, float %inf, float %nan, float %nan)
ret void
}

MODIFY
tests/unit/fabs/fabs.opt
tests/unit/fabs/fabs.opt
@@ -8,6 +8,12 @@ Name: constant2
=>
%r = 2.0
+Name: nnan
+%negnan = fdiv float 0.0, -0.0
+%r = fabs float %negnan
+ =>
+%r = %negnan
+
Name: fabs-twice
%k = fabs float %x
%r = fabs float %k

semantics of fabs/fneg: make sign bit non-deterministic for NaN