Clarify documentation on propagating signalling NaNs through (non-strict) fp-operations

[quaternic]

As documented in the reference, LLVM is allowed to perform optimizations such as

• x * -1.0 -> -x
• x + (-0.0) -> x
• pow(1.0, x) -> 1.0

These are seen as sufficiently useful to knowingly diverge from the rules required by IEEE-754. (Specifically, that they should return QNaN for any SNaN-input.) For more details you can see the discussion in #43070 . That led to documenting the current rule, which has been further revised in at least #66579 .

However, the rule as written also allows many other transformations such as:

• x * y -> y (when y is statically known to be some NaN)
• x * y -> is_signalling_nan(y) ? y : x * y

(Neither is much of an optimization compared to doing the correct thing, and LLVM does not perform them, but they are considered allowed by Alive2: https://alive2.llvm.org/ce/z/PenjbC)

These seem much more surprising to me, and more likely to break non-strictfp code that handles potentially signalling values, which it might obtain from, and pass to, a library using strictfp.

Are there cases where LLVM may currently propagate an SNaN untouched through an operation that would change a numeric value (other than just the sign)?

Preferably, it could be guaranteed in some form, that the "Unchanged NaN propagation" only applies transforming operations that pass the magnitude untouched, such as x * -1.0 -> -x, and that those cases treat the sign as the substitution would, so that x * -1.0 may never return an SNaN with the same sign as x (but can of course return an arbitrary QNaN).

If on the other hand, the intention is to allow all such transformations, and treat SNaN as a QNaN that just can't be created "from thin air", the documentation should point it out more directly, by reproducing such examples.

This came up in rust-lang/rfcs#3514, on specifying Rust floating point behavior.

[RalfJung]

Preferably, it could be guaranteed in some form, that the "Unchanged NaN propagation" only applies transforming operations that pass the magnitude untouched, such as x * -1.0 -> -x

The goal here is to have an operational spec: given two float inputs, what are the allowed float outputs. It sounds like you are saying the "Unchanged NaN propagation" rule should only apply on binary operators where one operand is the neutral element for that operator, or something like that? That doesn't cover the pow case though, that's using an absorbing element. And then maybe there are more cases that need to be covered, it seems hard to be sure.

This proposal also lacks an explanation for why restricting "Unchanged NaN propagation" is useful enough to justify a more complicated spec. I can see why removing "Unchanged NaN propagation" entirely is useful, but that's not on the table, and just restricting it like this does very little to actually make code that works with signalling values work better. Your code would work correctly for most values until you accidentally multiply by 1 somewhere and then suddenly quieting is not guaranteed any more.

IMO, if signalling values are relevant, you should use strictfp operations; it's not worth trying to shoehorn this into the non-strictfp spec.