clarify NaN propagation in fptrunc

[RalfJung]

Follow-up to #66579: while implementing those semantics in Miri I realized there's a special case to be considered in truncating float casts.

Cc @nunoplopes @nikic @jyknight @jcranmer-intel

[llvmbot]

@llvm/pr-subscribers-llvm-ir

Changes

Follow-up to #66579: while implementing those semantics in Miri I realized there's a special case to be considered in truncating float casts.

Cc @nunoplopes @nikic @jyknight @jcranmer-intel

---

Full diff: https://github.com/llvm/llvm-project/pull/68554.diff

1 Files Affected:

• (modified) llvm/docs/LangRef.rst (+4-1)

diff --git a/llvm/docs/LangRef.rst b/llvm/docs/LangRef.rst
index 1883e9f6290b151..e27d4e0ed695319 100644
--- a/llvm/docs/LangRef.rst
+++ b/llvm/docs/LangRef.rst
@@ -11311,7 +11311,10 @@ environment <floatenv>`.
 NaN values follow the usual :ref:`NaN behaviors <floatnan>`, except that _if_ a
 NaN payload is propagated from the input ("Quieting NaN propagation" or
 "Unchanged NaN propagation" cases), then the low order bits of the NaN payload
-which cannot fit in the resulting type are discarded.
+which cannot fit in the resulting type are discarded. Note that if discarding
+the low order bits leads to an all-0 payload, this cannot be represented as a
+signaling NaN (it would represent an infinity instead), so in that case
+"Unchanged NaN propagation" is not possible.
 
 Example:
 """"""""

[nunoplopes]

So, discarding all 1-bits in the payload would give an Inf rather than a NaN then.

FWIW, I tried x86, and it returns the canonical quiet NaN: https://gcc.godbolt.org/z/o1K6rrov9
Same for an ARM server I've access to.

[RalfJung]

They should always return a quiet NaN, so if all 1s in the payload get truncated away it will naturally be the preferred NaN, without any special case. But LLVM might optimize away cast roundtrips and then a signaling NaN might be returned and then we have to exclude the special case where the sNaN has all-0 payloads.

[nunoplopes]

But LLVM might optimize away cast roundtrips and then a signaling NaN might be returned and then we have to exclude the special case where the sNaN has all-0 payloads.

Doesn't seem like: https://gcc.godbolt.org/z/z1sqhjnE8

[RalfJung]

Yeah removing the double-float-double roundtrip would be wrong to optimize away since the precision gets reduced (even ignoring NaNs, this cast changes the value and hence cannot be optimized away). But float-double-float should be legal, and LLVM does it. So in terms of the semantics, but fpext and fptruc can, under some conditions, return an sNaN -- but fptrunc can only return an sNaN if the input NaN is an sNaN and its payload has a 1 that is preserved by truncation.

[nunoplopes]

FWIW, I tried the suggested semantics on LLVM's test suite with Alive2 and it works fine. But without the fix also worked, so maybe there isn't sufficient coverage for these corner cases.

[RalfJung]

Without the fix, this Rust function would be allowed to return false

pub fn test() -> bool {
    let snan = f64::from_bits(0x7FF0_0000_0000_0001u64);
    assert!(snan.is_nan());
    let nan = snan as f32;
    nan.is_nan()
}

That's roughly the following IR

define noundef zeroext i1 @example::test() unnamed_addr #0 !dbg !7 {
start:
  %0 = alloca double, align 8
  call void @llvm.lifetime.start.p0(i64 8, ptr nonnull %0), !dbg !12
  store double 0x7FF0000000000001, ptr %0, align 8, !dbg !12
  %_2 = load double, ptr %0, align 8, !dbg !12
  call void @llvm.lifetime.end.p0(i64 8, ptr nonnull %0), !dbg !12
  %nan = fptrunc double %_2 to float, !dbg !18
  %_0 = fcmp uno float %nan, 0.000000e+00, !dbg !21
  ret i1 %_0, !dbg !29
}

[jyknight]

This seems the only reasonable answer, and I can't think of any valid optimization we might be doing now that could break it.