[RFC] Clarify the behavior of FP operations on bit strings with nsz flag (original) (raw)

TLDR

This RFC suggests forbidding the use of nsz flags on FP operations on bit strings such as fabs/copysign/fneg.

Motivation

My mutation-based fuzzer found many disagreements between Alive2 and LLVM InstCombine: Compiler Explorer

----------------------------------------
define half @src1(half noundef %a) {
#0:
  %abs1 = fabs nsz half noundef %a
  %abs2 = fabs half %abs1
  ret half %abs2
}
=>
define half @src1(half noundef %a) nofree noundef willreturn memory(none) {
#0:
  %abs1 = fabs nsz half noundef %a
  ret half %abs1
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
half noundef %a = #x0000 (+0.0)

Source:
half %abs1 = #x0000 (+0.0)
half %abs2 = #x0000 (+0.0)

Target:
half %abs1 = #x8000 (-0.0)
Source value: #x0000 (+0.0)
Target value: #x8000 (-0.0)


----------------------------------------
define i1 @src2(half %x) {
#0:
  %fabs = fabs nnan nsz half %x
  %y = bitcast half %fabs to i16
  %sign = icmp sgt i16 %y, 1
  ret i1 %sign
}
=>
define i1 @src2(half %x) nofree willreturn memory(none) {
#0:
  %fabs = fabs nnan nsz half %x
  %y = bitcast half %fabs to i16
  %sign = icmp samesign ugt i16 %y, 1
  ret i1 %sign
}
Transformation doesn't verify!

ERROR: Target is more poisonous than source

Example:
half %x = #x0000 (+0.0)

Source:
half %fabs = #x0000 (+0.0)
i16 %y = #x0000 (0)
i1 %sign = #x0 (0)

Target:
half %fabs = #x8000 (-0.0)
i16 %y = #x8000 (32768, -32768)
i1 %sign = poison
Source value: #x0 (0)
Target value: poison


----------------------------------------
define float @src3(float noundef %x, i1 %cond) {
#0:
  %i32 = bitcast float noundef %x to i32
  %cmp = icmp slt i32 %i32, 0
  br i1 %cmp, label %if.then1, label %if.else

if.else:
  br i1 %cond, label %if.then2, label %if.end

if.then2:
  br label %if.end

if.then1:
  %fneg = fneg float noundef %x
  br label %if.end

if.end:
  %value = phi nsz float [ %fneg, %if.then1 ], [ noundef %x, %if.then2 ], [ noundef %x, %if.else ]
  %ret = fabs float %value
  ret float %ret
}
=>
define float @src3(float noundef %x, i1 %cond) nofree noundef willreturn memory(none) {
if.end:
  %value = fabs nsz float noundef %x
  ret float %value
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
float noundef %x = #x00000000 (+0.0)
i1 %cond = #x0 (0)

Source:
i32 %i32 = #x00000000 (0)
i1 %cmp = #x0 (0)
  >> Jump to %if.else
  >> Jump to %if.end
float %value = #x00000000 (+0.0)
float %ret = #x00000000 (+0.0)

Target:
float %value = #x80000000 (-0.0)
Source value: #x00000000 (+0.0)
Target value: #x80000000 (-0.0)


----------------------------------------
define i1 @src4(half noundef %x) {
#0:
  %fabs = fabs nnan nsz half noundef %x
  %is.finite = fcmp ueq half 0x7c00, %fabs
  %ord = fcmp ord half noundef %x, noundef %x
  %#1 = select i1 %ord, i1 %is.finite, i1 0
  ret i1 %#1
}
=>
define i1 @src4(half noundef %x) nofree willreturn memory(none) {
#0:
  %fabs = fabs nnan nsz half noundef %x
  %#1 = fcmp oeq half %fabs, 0x7c00
  ret i1 %#1
}
Transformation doesn't verify!

ERROR: Target is more poisonous than source

Example:
half noundef %x = #x7d00 (SNaN)

Source:
half %fabs = poison
i1 %is.finite = poison
i1 %ord = #x0 (0)
i1 %#1 = #x0 (0)

Target:
half %fabs = poison
i1 %#1 = poison
Source value: #x0 (0)
Target value: poison


----------------------------------------
define float @src5(float %a) {
#0:
  %b = fcmp nsz ult float %a, 0.000000
  %c = select i1 %b, float %a, float 0.000000
  ret float %c
}
=>
define float @src5(float %a) nofree willreturn memory(none) {
#0:
  %b.inv = fcmp nsz oge float %a, 0.000000
  %c = select nsz i1 %b.inv, float 0.000000, float %a
  ret float %c
}
Transformation doesn't verify!

ERROR: Target's return value is more undefined

Example:
float %a = #x00000000 (+0.0)

Source:
i1 %b = #x0 (0)
float %c = #x00000000 (+0.0)

Target:
i1 %b.inv = #x1 (1)
float %c = #x80000000 (-0.0)
Source value: #x00000000 (+0.0)
Target value: #x80000000 (-0.0)


----------------------------------------
define float @src6(float noundef %x) {
#0:
  %cmp1 = fcmp nsz ule float noundef %x, 1.000000
  %sel1 = select nnan i1 %cmp1, float noundef %x, float 1.000000
  %neg = fneg float %sel1
  ret float %neg
}
=>
define float @src6(float noundef %x) nofree noundef willreturn memory(none) {
#0:
  %cmp1.inv = fcmp nsz ogt float noundef %x, 1.000000
  %x.neg = fneg float noundef %x
  %neg = select nsz i1 %cmp1.inv, float -1.000000, float %x.neg
  ret float %neg
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
float noundef %x = #x00000000 (+0.0)

Source:
i1 %cmp1 = #x1 (1)
float %sel1 = #x00000000 (+0.0)
float %neg = #x80000000 (-0.0)

Target:
i1 %cmp1.inv = #x0 (0)
float %x.neg = #x80000000 (-0.0)
float %neg = #x00000000 (+0.0)
Source value: #x80000000 (-0.0)
Target value: #x00000000 (+0.0)


----------------------------------------
define half @src7(half %x) {
#0:
  %gtzero = fcmp nsz une half %x, 0x0000
  %negx = fsub half 0x0000, %x
  %fabs = select i1 %gtzero, half %x, half %negx
  ret half %fabs
}
=>
define half @src7(half returned %x) nofree willreturn memory(none) {
#0:
  ret half returned %x
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
half %x = #x8000 (-0.0)

Source:
i1 %gtzero = #x0 (0)
half %negx = #x0000 (+0.0)
half %fabs = #x0000 (+0.0)

Target:
Source value: #x0000 (+0.0)
Target value: #x8000 (-0.0)

Summary:
  0 correct transformations
  7 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

For cases @src1-@src4, Alive2 changes the sign bit of the zero result, even if the instruction just operates on the bit strings. For cases @src5-@src7, the root cause of these miscompilations seems a wrong nsz flag propagation from fcmp to select. It is strange to me that a select instruction can change the sign bit of a value…

In the first case, we assume that a fabs always returns a value with the sign bit cleared, even if the nsz flag is set. Then let’s add the following code into InstSimplify:

Value *simplifyIntrinsic(IntrinsicInst *II, const SimplifyQuery &SQ) {
  switch(II->getIntrinsicID()) {
    case Intrinsic::fabs: {
      if (computeKnownFPSignBit(II->getArgOperand(0), SQ) == false)
        return II->getArgOperand(0);
      break;
    }
    ...
  }
}

Both the ValueTracking and InstSimplify part are correct. But the funny thing is that this simplification is invalid This is because the simplification code does not know that the analysis code performs a refinement fabs_nsz -> fabs. We can safely preserve other poison-generating flags like nnan/ninf since poison will be propagated. But for nsz, it is not the case.

As per the IEEE 754-2008 standard, fabs/fneg/copysign only operate on the sign bit of inputs.
So I think the nsz flag is meaningless for these instructions. It will significantly reduce the number of nsz-related miscompilations.

Proposed Change to LangRef Wording

The LangRef should explicitly state that the nsz flag on fabs/fneg/copysign/select/phi/ssa.copy is not allowed. For a smooth migration, all the FMF setters will mask out the nsz flag on these instructions.

I have checked the current LLVM optimizations that check the nsz flag. For fabs/copysign, the nsz flag is ignored. I believe that we can check the nsz flag on other fp operations instead, to avoid dangerous flag propagation (See also [InstCombine] try to forward-propagate some FMF to select · llvm/llvm-project@0ee6bad · GitHub). For example, we can check the nsz flag on fsub for the transformation -(X -nsz Y) -> (Y -nsz X). It also allows us to remove the nsz flag propagation on select/phi instructions, which seems a long-standing issue for Mem2Reg/SROA (if I remember correctly).

TBH I think this workaround is still a bit hacky. The ideal solution is to make nsz have nice properties like poison-generating flags.

Alternative Solution

Another solution is to follow Alive2’s behavior and fix all the miscompilations in LLVM. That is impractical since we have to handle nsz carefully in all the places (e.g, ValueTracking), though the spec allows us to ignore it.

cc @nikic @arsenm @andykaylor @jyknight @jcranmer @efriedma-quic @davemgreen @spavloff @nlopes @regehr