InstSimplify: Fold fdiv nnan nsz x, 0 -> inf

[kpn]

It looks like by 754 sec 7.3 a (-x)/(+0) == -Inf, but the nsz is documented as saying the sign of the result is "insignificant", so I think we're good here.

LGTM

[spatel]

In D136097#3862928, @kpn wrote:

It looks like by 754 sec 7.3 a (-x)/(+0) == -Inf, but the nsz is documented as saying the sign of the result is "insignificant", so I think we're good here.

LGTM

"nsz" means the sign of a zero result is insignificant, not any result. -42.0 / 0.0 should be -Inf, not +Inf?

[arsenm]

In D136097#3862946, @spatel wrote:

In D136097#3862928, @kpn wrote:

It looks like by 754 sec 7.3 a (-x)/(+0) == -Inf, but the nsz is documented as saying the sign of the result is "insignificant", so I think we're good here.

LGTM

"nsz" means the sign of a zero result is insignificant, not any result. -42.0 / 0.0 should be -Inf, not +Inf?

That's what I would expect. alive2 has been giving me some nsz results that puzzle me https://alive2.llvm.org/ce/z/v-9wqk

[kpn]

In D136097#3862946, @spatel wrote:

In D136097#3862928, @kpn wrote:

It looks like by 754 sec 7.3 a (-x)/(+0) == -Inf, but the nsz is documented as saying the sign of the result is "insignificant", so I think we're good here.

LGTM

"nsz" means the sign of a zero result is insignificant, not any result. -42.0 / 0.0 should be -Inf, not +Inf?

English is fun! Yes, I think you are correct. With D136098 is this patch needed, especially if that patch's TODO is completed?

[arsenm]

Filed https://github.com/AliveToolkit/alive2/issues/855

[nlopes]

In D136097#3862946, @spatel wrote:

In D136097#3862928, @kpn wrote:

It looks like by 754 sec 7.3 a (-x)/(+0) == -Inf, but the nsz is documented as saying the sign of the result is "insignificant", so I think we're good here.

LGTM

"nsz" means the sign of a zero result is insignificant, not any result. -42.0 / 0.0 should be -Inf, not +Inf?

It's documented as ignoring the sign of a zero argument or a zero result.
Thus, when nsw is involved, we should consider the result of -42.0 / 0.0 and -42.0 / -0.0. This case the 0.0 is a constant, but that doesn't matter.

Alive2 is correct here AFAICT.

[spatel]

In D136097#3863158, @nlopes wrote:

In D136097#3862946, @spatel wrote:

In D136097#3862928, @kpn wrote:

It looks like by 754 sec 7.3 a (-x)/(+0) == -Inf, but the nsz is documented as saying the sign of the result is "insignificant", so I think we're good here.

LGTM

"nsz" means the sign of a zero result is insignificant, not any result. -42.0 / 0.0 should be -Inf, not +Inf?

It's documented as ignoring the sign of a zero argument or a zero result.
Thus, when nsw is involved, we should consider the result of -42.0 / 0.0 and -42.0 / -0.0. This case the 0.0 is a constant, but that doesn't matter.

Alive2 is correct here AFAICT.

Ah, thanks for clearing that up. The "nsz" wording has always been a less solid than I'd like, but I'm not sure how to change it.
I suspect this transform would cause some fallout with users because it's a stretch to go from -0.0 isn't different than 0.0, therefore, -Inf isn't different than +Inf. There was a suggestion in a previous discussion that we really need entirely new FP types to use with fast-math-flags, so it's clear that -0.0, Inf, or NaN values simply do not exist when the corresponding compile flag is used, but I don't think anyone has looked seriously at implementing that. There's more discussion about the general problem here:
https://github.com/llvm/llvm-project/issues/51601

[nlopes]

In D136097#3863230, @spatel wrote:

In D136097#3863158, @nlopes wrote:

In D136097#3862946, @spatel wrote:

In D136097#3862928, @kpn wrote:

It looks like by 754 sec 7.3 a (-x)/(+0) == -Inf, but the nsz is documented as saying the sign of the result is "insignificant", so I think we're good here.

LGTM

"nsz" means the sign of a zero result is insignificant, not any result. -42.0 / 0.0 should be -Inf, not +Inf?

It's documented as ignoring the sign of a zero argument or a zero result.
Thus, when nsw is involved, we should consider the result of -42.0 / 0.0 and -42.0 / -0.0. This case the 0.0 is a constant, but that doesn't matter.

Alive2 is correct here AFAICT.

Ah, thanks for clearing that up. The "nsz" wording has always been a less solid than I'd like, but I'm not sure how to change it.
I suspect this transform would cause some fallout with users because it's a stretch to go from -0.0 isn't different than 0.0, therefore, -Inf isn't different than +Inf. There was a suggestion in a previous discussion that we really need entirely new FP types to use with fast-math-flags, so it's clear that -0.0, Inf, or NaN values simply do not exist when the corresponding compile flag is used, but I don't think anyone has looked seriously at implementing that. There's more discussion about the general problem here:
https://github.com/llvm/llvm-project/issues/51601

That bug report seems to be a bit orthogonal. The issue there is that the fmath flags are attached to some instructions, but not all. Since values can't have fmath flags themselves, things like function arguments, when flowing directly to instructions without fmath flags make clang lose information when generating IR. Hence the proposal to add fmath to loads (I don't think you need fmath in store).

Regarding the semantics of nsz, I don't have any opinion as I'm clueless about FP. I'm just reading the current semantics to the letter, but I'm happy to implement whatever semantics you want in Alive2.

[kpn]

In D136097#3863230, @spatel wrote:

Ah, thanks for clearing that up. The "nsz" wording has always been a less solid than I'd like, but I'm not sure how to change it.
I suspect this transform would cause some fallout with users because it's a stretch to go from -0.0 isn't different than 0.0, therefore, -Inf isn't different than +Inf. There was a suggestion in a previous discussion that we really need entirely new FP types to use with fast-math-flags, so it's clear that -0.0, Inf, or NaN values simply do not exist when the corresponding compile flag is used, but I don't think anyone has looked seriously at implementing that. There's more discussion about the general problem here:
https://github.com/llvm/llvm-project/issues/51601

I just pushed a change to the LangRef that will hopefully avoid misreadings like the one I made: 1b06307aa43c3d366843866985abcd95aedb78a2

[spatel]

In D136097#3865271, @kpn wrote:

I just pushed a change to the LangRef that will hopefully avoid misreadings like the one I made: 1b06307aa43c3d366843866985abcd95aedb78a2

Thanks!

In D136097#3864398, @nlopes wrote:

https://github.com/llvm/llvm-project/issues/51601

That bug report seems to be a bit orthogonal.

Oops, I pasted the wrong link.
https://github.com/llvm/llvm-project/issues/51117
...this bug report has a bunch of links back to the old dev-lists where there were threads about what to do about NaN/Inf constants referenced in source built with -ffinite-math-only. I don't think we reached a conclusion.

llvm/lib/Analysis/InstructionSimplify.cpp

if (FMF.noNaNs()) {
     // We can ignore signed zeros because +-0.0/+-0.0 is NaN and ignored.
     if (match(Op0, m_FNegNSZ(m_Specific(Op1))) ||
         match(Op1, m_FNegNSZ(m_Specific(Op0))))
       return ConstantFP::get(Op0->getType(), -1.0);
 
     // nnan ninf X / 0.0 -> poison
     if (FMF.noInfs() && match(Op1, m_AnyZeroFP()))
       return PoisonValue::get(Op1->getType());
+
+    // nnan nsz X / 0.0 -> inf
+    if (FMF.noSignedZeros() && match(Op1, m_AnyZeroFP()))
+      return ConstantFP::getInfinity(Op1->getType());
   }
 
   return nullptr;
 }
 
 Value *llvm::simplifyFDivInst(Value *Op0, Value *Op1, FastMathFlags FMF,
                               const SimplifyQuery &Q,
                               fp::ExceptionBehavior ExBehavior,

llvm/test/Transforms/InstSimplify/fdiv.ll

 ;
   %fdiv = fdiv nnan ninf <2 x float> %x, <float 0.0, float undef>
   ret <2 x float> %fdiv
 }
 
 ; https://alive2.llvm.org/ce/z/ryZBn6
 define float @fdiv_nnan_nsz_ninf_by_zero_f32(float %x) {
 ; CHECK-LABEL: @fdiv_nnan_nsz_ninf_by_zero_f32(
-; CHECK-NEXT:    [[FDIV:%.*]] = fdiv nnan nsz float [[X:%.*]], 0.000000e+00
-; CHECK-NEXT:    ret float [[FDIV]]
+; CHECK-NEXT:    ret float 0x7FF0000000000000
 ;
   %fdiv = fdiv nnan nsz float %x, 0.0
   ret float %fdiv
 }
 
 define float @fdiv_nnan_nsz_ninf_by_negzero_f32(float %x) {
 ; CHECK-LABEL: @fdiv_nnan_nsz_ninf_by_negzero_f32(
-; CHECK-NEXT:    [[FDIV:%.*]] = fdiv nnan nsz float [[X:%.*]], -0.000000e+00
-; CHECK-NEXT:    ret float [[FDIV]]
+; CHECK-NEXT:    ret float 0x7FF0000000000000
 ;
   %fdiv = fdiv nnan nsz float %x, -0.0
   ret float %fdiv
 }
 
 define <2 x float> @fdiv_nnan_nsz_ninf_by_zero_v2f32(<2 x float> %x) {
 ; CHECK-LABEL: @fdiv_nnan_nsz_ninf_by_zero_v2f32(
-; CHECK-NEXT:    [[FDIV:%.*]] = fdiv nnan nsz <2 x float> [[X:%.*]], zeroinitializer
-; CHECK-NEXT:    ret <2 x float> [[FDIV]]
+; CHECK-NEXT:    ret <2 x float> <float 0x7FF0000000000000, float 0x7FF0000000000000>
 ;
   %fdiv = fdiv nnan nsz <2 x float> %x, zeroinitializer
   ret <2 x float> %fdiv
 }
 
 define <2 x float> @fdiv_nnan_nsz_ninf_by_negzero_v2f32(<2 x float> %x) {
 ; CHECK-LABEL: @fdiv_nnan_nsz_ninf_by_negzero_v2f32(
-; CHECK-NEXT:    [[FDIV:%.*]] = fdiv nnan nsz <2 x float> [[X:%.*]], <float -0.000000e+00, float -0.000000e+00>
-; CHECK-NEXT:    ret <2 x float> [[FDIV]]
+; CHECK-NEXT:    ret <2 x float> <float 0x7FF0000000000000, float 0x7FF0000000000000>
 ;
   %fdiv = fdiv nnan nsz <2 x float> %x, <float -0.0, float -0.0>
   ret <2 x float> %fdiv
 }