ValueTracking: Teach CannotBeOrderedLessThanZero about copysign

[foad]

Seems reasonable. Can we get alive2 proofs for floating point things like this yet @nlopes?

[arsenm]

Alive2 says this is ok and seems to understand copysign. For some of the other complex functions in other patches, it doesn’t complain but it also doesn’t complain when I try things that are obviously wrong

[nlopes]

In D139312#3970743, @foad wrote:

Seems reasonable. Can we get alive2 proofs for floating point things like this yet @nlopes?

Most FP stuff should be working now. Exceptions include: some fast-math flags (arcp/contract/reassoc/afn), exceptions, and some intrinsics. The rest should all be working; if not please file a bug report :)

In D139312#3970765, @arsenm wrote:

Alive2 says this is ok and seems to understand copysign. For some of the other complex functions in other patches, it doesn’t complain but it also doesn’t complain when I try things that are obviously wrong

As noted above, most FP should be working. If Alive2 misses a bug, please do file a bug report. Alive2 is not supposed to miss (almost no) bugs.

[spatel]

llvm/test/Transforms/InstSimplify/floating-point-arithmetic.ll

964

Something went wrong - this is a miscompile without 'nsz' on the sqrt (otherwise, it can return -0.0):
https://alive2.llvm.org/ce/z/yqXQmQ

[arsenm]

llvm/test/Transforms/InstSimplify/floating-point-arithmetic.ll

964

But this is being consumed by an fcmp - the sign of the zero shouldn't matter for the final result. Alive bug?

[spatel]

llvm/test/Transforms/InstSimplify/floating-point-arithmetic.ll

964

No - the negative sign of the -0.0 is applied to the magnitude parameter (%unknown).
So the sequence could be something like:
copysign(42.0, sqrt(-0.0)) >= 0.0
-42.0 >= 0.0 --> false

[arsenm]

The whole reason I used sqrt in the test was to test -0 and I still got it wrong

[spatel]

LGTM

[arsenm]

7f4429c0e48b9c7d31ff587604707cf10d3acdf0

llvm/lib/Analysis/ValueTracking.cpp

case Intrinsic::minimum:
       return cannotBeOrderedLessThanZeroImpl(I->getOperand(0), TLI, SignBitOnly,
                                              Depth + 1) &&
              cannotBeOrderedLessThanZeroImpl(I->getOperand(1), TLI, SignBitOnly,
                                              Depth + 1);
     case Intrinsic::exp:
     case Intrinsic::exp2:
     case Intrinsic::fabs:
       return true;
-
+    case Intrinsic::copysign:
+      // Only the sign operand matters.
+      return cannotBeOrderedLessThanZeroImpl(I->getOperand(1), TLI, true,
+                                             Depth + 1);
     case Intrinsic::sqrt:
       // sqrt(x) is always >= -0 or NaN.  Moreover, sqrt(x) == -0 iff x == -0.
       if (!SignBitOnly)
         return true;
       return CI->hasNoNaNs() && (CI->hasNoSignedZeros() ||
                                  CannotBeNegativeZero(CI->getOperand(0), TLI));
 
     case Intrinsic::powi:

llvm/test/Transforms/InstSimplify/floating-point-arithmetic.ll

;
   %6 = call float @sqrtf(float %5)
   %7 = fadd float %6, 0.0
   ret float %7
 }
 
 declare float @llvm.fabs.f32(float)
 declare float @llvm.canonicalize.f32(float)
 declare float @llvm.arithmetic.fence.f32(float)
+declare float @llvm.copysign.f32(float, float)
 declare <2 x float> @llvm.fabs.v2f32(<2 x float>)
 declare float @llvm.sqrt.f32(float)
 declare float @llvm.maxnum.f32(float, float)
 
 define float @fabs_select_positive_constants(i32 %c) {
 ; CHECK-LABEL: @fabs_select_positive_constants(
 ; CHECK-NEXT:    [[CMP:%.*]] = icmp eq i32 [[C:%.*]], 0
 ; CHECK-NEXT:    [[SELECT:%.*]] = select i1 [[CMP]], float 1.000000e+00, float 2.000000e+00

 ; CHECK-NEXT:    [[KNOWN_POSITIVE:%.*]] = call float @llvm.arithmetic.fence.f32(float [[UNKNOWN:%.*]])
 ; CHECK-NEXT:    [[CMP:%.*]] = fcmp nnan oge float [[KNOWN_POSITIVE]], 0.000000e+00
 ; CHECK-NEXT:    ret i1 [[CMP]]
 ;
   %known.positive = call float @llvm.arithmetic.fence.f32(float %unknown)
   %cmp = fcmp nnan oge float %known.positive, 0.0
   ret i1 %cmp
 }
+
+define i1 @copysign_known_positive_maybe_neg0(float %unknown, float %sign) {
+; CHECK-LABEL: @copysign_known_positive_maybe_neg0(
+; CHECK-NEXT:    [[SQRT:%.*]] = call nnan ninf float @llvm.sqrt.f32(float [[SIGN:%.*]])
+; CHECK-NEXT:    [[COPYSIGN:%.*]] = call float @llvm.copysign.f32(float [[UNKNOWN:%.*]], float [[SQRT]])
+; CHECK-NEXT:    [[CMP:%.*]] = fcmp nnan oge float [[COPYSIGN]], 0.000000e+00
+; CHECK-NEXT:    ret i1 [[CMP]]
+;
+  %sqrt = call ninf nnan float @llvm.sqrt.f32(float %sign)
+  %copysign = call float @llvm.copysign.f32(float %unknown, float %sqrt)
+  %cmp = fcmp nnan oge float %copysign, 0.0
+  ret i1 %cmp
+}
+
+define i1 @copysign_known_positive(float %unknown, float %sign) {
+; CHECK-LABEL: @copysign_known_positive(
+; CHECK-NEXT:    ret i1 true
+;
+  %sqrt = call ninf nnan nsz float @llvm.sqrt.f32(float %sign)
+  %copysign = call float @llvm.copysign.f32(float %unknown, float %sqrt)
+  %cmp = fcmp nnan oge float %copysign, 0.0
+  ret i1 %cmp
+}
+
+define i1 @copysign_unknown_positive(float %unknown, float %unknown.sign) {
+; CHECK-LABEL: @copysign_unknown_positive(
+; CHECK-NEXT:    [[COPYSIGN:%.*]] = call float @llvm.copysign.f32(float [[UNKNOWN:%.*]], float [[UNKNOWN_SIGN:%.*]])
+; CHECK-NEXT:    [[CMP:%.*]] = fcmp nnan oge float [[COPYSIGN]], 0.000000e+00
+; CHECK-NEXT:    ret i1 [[CMP]]
+;
+  %copysign = call float @llvm.copysign.f32(float %unknown, float %unknown.sign)
+  %cmp = fcmp nnan oge float %copysign, 0.0
+  ret i1 %cmp
+}