floating point value mismatches from the middle-end

[regehr]

I'm seeing a fair number of value mismatches from FP optimizations in the middle end, such as the one below, and also ones where it's turning an SNaN output into a QNaN, and also ones where it's making things more poisonous. Are these real bugs that I should report? Or are some of these Alive being overly sensitive?

To be clear, these are coming up in the context of the ARM lifter, which relies on the middle end, but the issues I'm seeing are in the middle end, not the backend.

regehr@john-home:~/test/errors/2435$ cat test-022757115.ll
; ModuleID = '<stdin>'
source_filename = "<stdin>"

define double @select_fcmp_ole_zero(double %0) {
  %2 = fcmp ole double %0, 0.000000e+00
  %3 = fsub double 0.000000e+00, %0
  %4 = select i1 %2, double %3, double %0
  ret double %4
}
regehr@john-home:~/test/errors/2435$ ~/alive2-regehr/build/alive-tv test-022757115.ll

----------------------------------------
define double @select_fcmp_ole_zero(double %#0) {
#1:
  %#2 = fcmp ole double %#0, 0.000000
  %#3 = fsub double 0.000000, %#0
  %#4 = select i1 %#2, double %#3, double %#0
  ret double %#4
}
=>
define double @select_fcmp_ole_zero(double %#0) nofree willreturn memory(none) {
#1:
  %#2 = fabs double %#0
  ret double %#2
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
double %#0 = #xfff0000000008000 (SNaN)

Source:
i1 %#2 = #x0 (0)
double %#3 = #x7ff8000000000000 (QNaN)
double %#4 = #xfff0000000008000 (SNaN)

Target:
double %#2 = #x7ff0000000008000 (SNaN)
Source value: #xfff0000000008000 (SNaN)
Target value: #x7ff0000000008000 (SNaN)

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
regehr@john-home:~/test/errors/2435$ 

[arsenm]

This is a canonicalization dropping transform, which is supposed to be allowed

[nunoplopes]

I think it's a bug in LLVM. This is only correct if the select has the 'nnan' flag or when the comparison is reversed (to ogt). 'fcmp ole' returns false for NaNs. and thus the select will always return the input as-is. But fabs sets the sign bit to 0, so it may change the sign of NaNs. Thus either LangRef needs further patching or LLVM is wrong here.

[nunoplopes]

There's an open LLVM bug report to track these select folds: https://github.com/llvm/llvm-project/issues/49625