InstCombine: incorrect fabs formation

[nunoplopes]

Test Transforms/InstCombine/fabs.ll shows the following transformation:

define double @select_fcmp_ole_zero(double %x) {
  %lezero = fcmp ole double %x, 0.000000
  %negx = fsub double 0.000000, %x, exceptions=ignore
  %fabs = select i1 %lezero, double %negx, double %x
  ret double %fabs
}
=>
define double @select_fcmp_ole_zero(double %x) {
  %1 = fabs double %x, exceptions=ignore
  ret double %1
}

This is not correct as fabs produces a non-deterministic NaN payload, while the original function preserved the NaN payload when x > 0.

cc @arsenm @jcranmer-intel @jyknight @rotateright

[nunoplopes]

Similar pattern in Transforms/InstCombine/fneg-fabs.ll:

define double @select_nsz_nfabs_ult(double %x) {
  %cmp = fcmp ult double %x, 0.000000
  %negX = fneg double %x
  %sel = select nsz i1 %cmp, double %x, double %negX
  ret double %sel
}
=>
define double @select_nsz_nfabs_ult(double %x) {
  %1 = fabs nsz double %x
  %sel = fneg nsz double %1
  ret double %sel
}

[rotateright]

We don't state it explicitly in the LangRef, but fabs is purely a signbit operation (as is fneg).

So the LLVM 'fabs' conforms to the libm 'fabs' which implements the IEEE-754 abs() that says (in section 5.5.1 of the 2008 version):
"Implementations shall provide the following homogeneous quiet-computational sign bit operations for all supported arithmetic formats; they only affect the sign bit. The operations treat floating-point numbers and NaNs alike, and signal no exception. These operations may propagate non-canonical encodings."

So if we're transforming to fabs, the payload isn't changed?

[jcranmer-intel]

Yes, fabs, fneg, copysign should all touch only the sign bit, preserving NaN payload.

[nunoplopes]

I had it like that, but several optimizations were failing. I'll collect a few so you can decide the semantics you want :)

[nunoplopes]

Ok, I can only see only real failure from InstCombine/fneg.ll:

define float @fnabs_2(float %a) {
  %fneg = fneg float %a
  %cmp = fcmp olt float %a, %fneg
  %sel = select nsz i1 %cmp, float %fneg, float %a
  %fneg1 = fneg float %sel
  ret float %fneg1
}
=>
define float @fnabs_2(float %a) {
  %1 = fabs nsz float %a
  %fneg1 = fneg float %1
  ret float %fneg1
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
float %a = #xff810000 (NaN)

Source:
float %fneg = #x7f810000 (NaN)
i1 %cmp = #x0 (0)
float %sel = #xff810000 (NaN)
float %fneg1 = #x7f810000 (NaN)

Target:
float %1 = #x7f810000 (NaN)
float %fneg1 = #xff810000 (NaN)
Source value: #x7f810000 (NaN)
Target value: #xff810000 (NaN)

Should we just restrict this to ops with nnan?

FWIW, there are two more cases, but they involve undef, so I think we can ignore them while we quietly work on removing undef from LLVM..

[arsenm]

Ok, I can only see only real failure from InstCombine/fneg.ll:

Source value: #x7f810000 (NaN)
Target value: #xff810000 (NaN)

The sign bit of a NaN is meaningless, so this isn't wrong

[nunoplopes]

Ok, I've changed fabs/fneg/copysign to return a non-deterministic sign when the input is NaN.
I'm seeing only 2 related failures now:

; InstCombine/fabs.ll
define double @select_fcmp_ole_zero(double %x) {
  %lezero = fcmp ole double %x, 0.000000
  %negx = fsub double 0.000000, %x
  %fabs = select i1 %lezero, double %negx, double %x
  ret double %fabs
}
=>
define double @select_fcmp_ole_zero(double %x) {
  %1 = fabs double %x
  ret double %1
}
Transformation doesn't verify! (unsound)
ERROR: Target's return value is more undefined

Example:
double %x = #xfff0004000000000 (NaN)
i1 %lezero = #x0 (0)

The issue is that the fcmp in source evaluates to false when the input is NaN. That makes the select return the original, unmodified %x.
However, the tgt program returns %x with a non-deterministic sign bit.
So either the transformation is changed to have some nnan attribute, for example. Or it needs to be removed. It's not correct under this semantics of a non-deterministic NaN sign bit (@RalfJung).

[nunoplopes]

The other failure:

; InstCombine/fneg-fabs.ll
define double @select_nsz_nfabs_ult(double %x) {
  %cmp = fcmp ult double %x, 0.000000
  %negX = fneg double %x
  %sel = select nsz i1 %cmp, double %x, double %negX
  ret double %sel
}
=>
define double @select_nsz_nfabs_ult(double %x) {
  %1 = fabs nsz double %x
  %sel = fneg nsz double %1
  ret double %sel
}

[jyknight]

The sign bit of a NaN is meaningless, so this isn't wrong

I've changed fabs/fneg/copysign to return a non-deterministic sign when the input is NaN.

No, that's wrong. Yes, the sign is "meaningless", and is effectively arbitrary when resulting from a floating-point operation. But, the sign-manipulation operations are considered bit-manipulation instructions, not as floating-point operations. They affect ONLY the sign bit of the values, and have deterministic outcome even for NaNs -- even for signaling NaN.

Therefore, the fnabs_2 example was indeed incorrect. All of the operations there -- except the compare -- only manipulate sign bits. And olt is fully defined for qNaNs. So, the outcome is entirely deterministic, no wiggle-room available. The transformed version similarly only has sign-manipulation, so no wiggle room there either.

[nunoplopes]

Ok, so the sign bit of fabs should always be 0 irrespective of the input?

I can flip the semantics again in Alive2; I just want you guys to converge first. And maybe to fix some of the optimizations above as they can't all be correct. We (you) have to choose which ones to keep and which ones to restrict to fast-math.

[jyknight]

Ok, so the sign bit of fabs should always be 0 irrespective of the input?

Yes. Or, well, at least...that is the behavior specified by IEEE754, (typically) implemented in FP hardware, and specified by WebAssembly.

It's not currently documented precisely in LangRef, but, I think those are the most sensible semantics for LLVM IR as well.

[RalfJung]

There's a short list of functions that are specified as behaving "bitwise" and they should probably be modeled as fully deterministic, not clobbering NaN payload and sign bits: copy, negate, abs, copySign. (Source 1, Source 2)