Wrong signs on division producing NaN

[dtolnay]

Noticed this while playing with #54235.

fn f(x: f64) -> f64 {
    0f64 / x
}

fn main() {
    println!("{:?}", (0f64 / 0f64).is_sign_negative());
    println!("{:?}", f(0f64).is_sign_negative());
}

As of rustc 1.31.0-nightly (46880f4 2018-10-15) on x86_64-unknown-linux-gnu, in debug mode this program prints false true and in release mode prints false false. Two of my expectations are violated:

• The output should be consistent between debug mode and release mode.
• The first and second println should print the same value.

(Happy to reconsider if these expectations are unfounded.)

[dtolnay]

Compilers 1.19 and older consistently print false false which aligns with my expectations; 1.20 and newer behave as above.

[hanna-kruppe]

Evidently LLVM does not guarantee the sign of NaNs, just as it does not guarantee the signaling bit or payload. I can't say I would have known that, but it doesn't surprise me either.

Two observations that explain these discrepancies:

• (0f64 / 0f64) is constant folded even in debug mode (by IRBuilder), while f(0f64) obviously is only constant folded when inlined, i.e., in release mode.
• When constant folding a floating point computation that results in a NaN, LLVM prefers 0x7FF8000000000000 (which has positive sign). Apparently your CPU differs and produces a negative NaN for the runtime division.

[RalfJung]

In other words, the semantics of floating point operations would be something like "if the result is a NaN, non-deterministically pick any legal NaN representation". This non-determinism explains why debug and release builds differ in behavior.

I wonder if we should make Miri pick a random NaN payload and sign and signalling bit, just to drive home this point...

[RalfJung]

@hanna-kruppe notes that "NaNs are unstable under copying" seems rather excessive and in fact people might rely on NaN payloads being preserved on copy.

A less drastic alternative is to say that every single FP operation (arithmetic and intrinsics and whatnot, but not copying), when it returns a NaN, non-deterministically picks any NaN representation.

[hanna-kruppe]

I believe it was @Lokathor who made this point, though I don't disagree.

However, I have doubts whether either option is enough to explain away the behavior LLVM can produce today. Don't have time to summarize but here's a link to the Zulip discussion for future reference: https://rust-lang.zulipchat.com/#narrow/stream/213817-t-lang/topic/floating.20point.20semantics

[RalfJung]

However, I have doubts whether either option is enough to explain away the behavior LLVM can produce today.

I did not see anything in that discussion that makes it sound like either option wouldn't work -- by current impression is that both correctly describe LLVM behavior. What did I miss? (Not urgent, just respond when you got time again.)

[hanna-kruppe]

Specifically https://rust-lang.zulipchat.com/#narrow/stream/213817-t-lang/topic/floating.20point.20semantics/near/194786318 and the whole earlier discussion about how combinations of other optimizations can result in different uses of the same value (in Rust / the initial LLVM IR) observing different results. We talked about how maybe floats should be "frozen" when moving into the integer domain but this does not currently happen and as I said in https://rust-lang.zulipchat.com/#narrow/stream/213817-t-lang/topic/floating.20point.20semantics/near/194786318 LLVM can currently eliminate the float<->int bitcasts/transmutes/etc. that we do have (even if one might argue that it shouldn't).

[RalfJung]

Hm okay if LLVM will duplicate casts then that would indeed contradict a "typed copy messes up NaN" semantics.

For the "FP operations pick arbitrary NaN" semantics, I suppose LLVM will also happily duplicate floating point operations since it considers them deterministic?

But together with "NaNs are not preserved", that actually leads to a contradiction, and if we can make LLVM do the right optimizations in the right order we can likely show a miscompilation from this.

[hanna-kruppe]

Right, I believe there's potential miscompilations lurking there, but they're probably very difficult to tease out -- maybe even impossible today, if the stars don't align.