From d02121f9f5be5b50fd0def845740193c15aa2b2f Mon Sep 17 00:00:00 2001 From: John Regehr Date: Mon, 14 Sep 2026 12:37:49 -0600 Subject: [PATCH] fix --- ir/instr.cpp | 17 ++++++++++------- ...denormal-input-flush-preservesign.srctgt.ll | 12 ++++++++++++ .../alive-tv/fp/denormal-input-flush.srctgt.ll | 14 ++++++++++++++ ...enormal-output-flush-not-mandated.srctgt.ll | 17 +++++++++++++++++ .../fp/is_fpclass-denormal-dapz.srctgt.ll | 18 ++++++++++++++++++ 5 files changed, 71 insertions(+), 7 deletions(-) create mode 100644 tests/alive-tv/fp/denormal-input-flush-preservesign.srctgt.ll create mode 100644 tests/alive-tv/fp/denormal-input-flush.srctgt.ll create mode 100644 tests/alive-tv/fp/denormal-output-flush-not-mandated.srctgt.ll create mode 100644 tests/alive-tv/fp/is_fpclass-denormal-dapz.srctgt.ll diff --git a/ir/instr.cpp b/ir/instr.cpp index 20613c968..d6909adb5 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -714,18 +714,20 @@ static expr any_fp_zero(State &s, expr v) { return expr::mkIf(var && is_zero, v.fneg(), v); } -static expr handle_subnormal(State &s, FPDenormalAttrs::Type attr, expr &&v) { +static expr handle_subnormal(State &s, FPDenormalAttrs::Type attr, expr &&v, + bool mandatory) { auto nondet = [&]() { return s.getFreshNondetVar("subnormal", true); }; + auto flush = [&]() { return mandatory ? expr(true) : nondet(); }; expr subnormal = v.isFPSubNormal(); switch (attr) { case FPDenormalAttrs::IEEE: break; case FPDenormalAttrs::PositiveZero: - v = expr::mkIf(subnormal && nondet(), expr::mkNumber("0", v), v); + v = expr::mkIf(subnormal && flush(), expr::mkNumber("0", v), v); break; case FPDenormalAttrs::PreserveSign: - v = expr::mkIf(subnormal && nondet(), + v = expr::mkIf(subnormal && flush(), expr::mkIf(v.isFPNegative(), expr::mkNumber("-0", v), expr::mkNumber("0", v)), @@ -802,11 +804,11 @@ static StateValue fm_poison(State &s, expr a, const expr &ap, expr b, if (!bitwise) { auto fpdenormal = s.getFn().getFnAttrs().getFPDenormal(from_ty).input; - fp_a = handle_subnormal(s, fpdenormal, std::move(fp_a)); + fp_a = handle_subnormal(s, fpdenormal, std::move(fp_a), /*mandatory=*/true); if (nary >= 2) - fp_b = handle_subnormal(s, fpdenormal, std::move(fp_b)); + fp_b = handle_subnormal(s, fpdenormal, std::move(fp_b), /*mandatory=*/true); if (nary >= 3) - fp_c = handle_subnormal(s, fpdenormal, std::move(fp_c)); + fp_c = handle_subnormal(s, fpdenormal, std::move(fp_c), /*mandatory=*/true); } function fn_rm @@ -851,7 +853,8 @@ 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(from_ty).output, - std::move(val)); + std::move(val), + /*mandatory=*/false); const FloatType &ty = to_ty ? *to_ty->getAsFloatType() : fpty; val = ty.fromFloat(s, val, fpty, nary, a, b, c); } diff --git a/tests/alive-tv/fp/denormal-input-flush-preservesign.srctgt.ll b/tests/alive-tv/fp/denormal-input-flush-preservesign.srctgt.ll new file mode 100644 index 000000000..5cf9a49d2 --- /dev/null +++ b/tests/alive-tv/fp/denormal-input-flush-preservesign.srctgt.ll @@ -0,0 +1,12 @@ +; As denormal-input-flush.srctgt.ll, but preservesign keeps the sign of the +; flushed input, so the result is -inf rather than +inf. + +define float @src() denormal_fpenv(ieee|preservesign) { + ret float 0xFFF0000000000000 +} + +define float @tgt() denormal_fpenv(ieee|preservesign) { +; 0xB800000000000000 is -0x1p-127, a negative subnormal float + %v = fdiv float 1.000000e+00, 0xB800000000000000 + ret float %v +} diff --git a/tests/alive-tv/fp/denormal-input-flush.srctgt.ll b/tests/alive-tv/fp/denormal-input-flush.srctgt.ll new file mode 100644 index 000000000..00a5ea8ec --- /dev/null +++ b/tests/alive-tv/fp/denormal-input-flush.srctgt.ll @@ -0,0 +1,14 @@ +; LangRef, denormal_fpenv: "If the input mode is preservesign, or +; positivezero, a floating-point operation must treat any input denormal +; value as zero." Unlike output flushing, input flushing is mandatory, so +; the fdiv below definitely sees +0.0 and definitely returns +inf. + +define float @src() denormal_fpenv(ieee|positivezero) { + ret float 0x7FF0000000000000 +} + +define float @tgt() denormal_fpenv(ieee|positivezero) { +; 0xB800000000000000 is -0x1p-127, a negative subnormal float + %v = fdiv float 1.000000e+00, 0xB800000000000000 + ret float %v +} diff --git a/tests/alive-tv/fp/denormal-output-flush-not-mandated.srctgt.ll b/tests/alive-tv/fp/denormal-output-flush-not-mandated.srctgt.ll new file mode 100644 index 000000000..27879993c --- /dev/null +++ b/tests/alive-tv/fp/denormal-output-flush-not-mandated.srctgt.ll @@ -0,0 +1,17 @@ +; ERROR: Value mismatch + +; The mirror image of denormal-input-flush.srctgt.ll: LangRef says of the +; output mode that "It is not mandated that flushing to zero occurs", so a +; denormal result may or may not be flushed. The target may return a subnormal, +; so it is not a refinement of the source, which always returns zero. + +define float @src() denormal_fpenv(positivezero|ieee) { + ret float 0.000000e+00 +} + +define float @tgt() denormal_fpenv(positivezero|ieee) { +; 0x3810000000000000 is 0x1p-126, the smallest normal float; halving it +; produces a subnormal result + %v = fdiv float 0x3810000000000000, 2.000000e+00 + ret float %v +} diff --git a/tests/alive-tv/fp/is_fpclass-denormal-dapz.srctgt.ll b/tests/alive-tv/fp/is_fpclass-denormal-dapz.srctgt.ll new file mode 100644 index 000000000..f8dde7f11 --- /dev/null +++ b/tests/alive-tv/fp/is_fpclass-denormal-dapz.srctgt.ll @@ -0,0 +1,18 @@ +; llvm/test/Transforms/InstCombine/is_fpclass.ll, +; @test_class_is_p0_n0_psub_nsub_f32_dapz +; +; Under an input denormal mode of positivezero, a subnormal operand of the +; fcmp is treated as +0.0, so "x is zero or subnormal" is exactly "x == 0". +; llvm.is.fpclass itself classifies the unflushed value. + +define i1 @src(float %x) denormal_fpenv(ieee|positivezero) { + %val = call i1 @llvm.is.fpclass.f32(float %x, i32 240) + ret i1 %val +} + +define i1 @tgt(float %x) denormal_fpenv(ieee|positivezero) { + %val = fcmp oeq float %x, 0.000000e+00 + ret i1 %val +} + +declare i1 @llvm.is.fpclass.f32(float, i32 immarg)