Ignore sign difference between two NaNs

[dtcxzyw]

As we discussed in #1037, we don't care about the sign of NaN values. This patch only checks the NaN payload when both values are NaNs.

Here is a false positive case: https://alive2.llvm.org/ce/z/iSh4-Z
Related PR: llvm/llvm-project#121580

[dtcxzyw]

I don't know how to fix the test failure in tests/alive-tv/bugs/pr45152.srctgt.ll :(

[nunoplopes]

There was no discussion about this change of the semantics AFAICT. Could you please open a discuss first at discourse so we can reach consensus before changing Alive2?
Thanks!

[dtcxzyw]

I decided to fix it in LLVM. This case is a little different from #1037 since there is no floating-point operation being performed. As per the IEEE 754-2008 standard, the sign bit of a NaN is only allowed to be refined in floating point operations except for copy, negate, abs, and copySign.

[dtcxzyw]

See also llvm/llvm-project#59279

[regehr]

sorry to add to a closed issue, but I just want to add that using arm-tv I run across quite a lot of issues relating to LLVM and Alive disagreeing about whether NaN and +0/-1 transformations are valid. @dtcxzyw I would be super happy to feed you examples if you're interested!

[dtcxzyw]

sorry to add to a closed issue, but I just want to add that using arm-tv I run across quite a lot of issues relating to LLVM and Alive disagreeing about whether NaN and +0/-1 transformations are valid. @dtcxzyw I would be super happy to feed you examples if you're interested!

Feel free to create a post on Discourse, and then we can discuss these cases in public :)
I also found some disagreements between Alive2 and InstCombine with mutation-based fuzzing. I am drafting two RFCs to clarify the LangRef wording.