[Support][ValueTraking] Improve KnownFPClass for fadd. Handle infinity signs (#190559)

Improve KnownFPClass reasoning for fadd:

- Refine NaN handling for infinities by checking opposite-sign cases:
   - `-inf` + `+inf` --> `nan`
  - `+inf` + `-inf` --> `nan`
  - `+inf` + `+inf` --> `+inf`
  - `-inf` + `-inf` --> `-inf`
- Introduce `cannotBeOrderedLessEqZero` as pair to
`cannotBeOrderedGreaterEqZero`.
This commit is contained in:
Max Graey 2026-04-06 17:23:20 +03:00 committed by GitHub
parent 59e899e16b
commit c4281fd5af
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
5 changed files with 62 additions and 9 deletions

View File

@ -127,6 +127,17 @@ struct KnownFPClass {
return isKnownNever(OrderedGreaterThanZeroMask);
}
/// Return true if it's known this can never be a positive value or a logical
/// 0.
///
/// NaN --> true
/// x <= +0 --> false
/// psub --> true if mode is ieee, false otherwise.
/// x > +0 --> true
bool cannotBeOrderedLessEqZero(DenormalMode Mode) const {
return isKnownNever(fcNegative) && isKnownNeverLogicalPosZero(Mode);
}
/// Return true if it's know this can never be a negative value or a logical
/// 0.
///

View File

@ -292,10 +292,11 @@ static KnownFPClass fadd_impl(const KnownFPClass &KnownLHS,
const KnownFPClass &KnownRHS, DenormalMode Mode) {
KnownFPClass Known;
// Adding positive and negative infinity produces NaN.
// TODO: Check sign of infinities.
// Adding positive and negative infinity produces NaN, but only if both
// opposite-sign infinity combinations are possible.
if (KnownLHS.isKnownNeverNaN() && KnownRHS.isKnownNeverNaN() &&
(KnownLHS.isKnownNeverInfinity() || KnownRHS.isKnownNeverInfinity()))
(KnownLHS.isKnownNever(fcPosInf) || KnownRHS.isKnownNever(fcNegInf)) &&
(KnownLHS.isKnownNever(fcNegInf) || KnownRHS.isKnownNever(fcPosInf)))
Known.knownNot(fcNan);
if (KnownLHS.cannotBeOrderedLessThanZero() &&

View File

@ -2297,6 +2297,50 @@ define float @fadd_known_positive_daz(float nofpclass(ninf nsub nnorm) %arg0, fl
ret float %add
}
define float @test_fadd_no_nan_from_no_ninf(float nofpclass(nan ninf) %arg0, float nofpclass(nan ninf) %arg1) {
; CHECK: Function Attrs: mustprogress nofree norecurse nosync nounwind willreturn memory(none)
; CHECK-LABEL: define nofpclass(nan) float @test_fadd_no_nan_from_no_ninf
; CHECK-SAME: (float nofpclass(nan ninf) [[ARG0:%.*]], float nofpclass(nan ninf) [[ARG1:%.*]]) #[[ATTR:[0-9]+]] {
; CHECK-NEXT: [[ADD:%.*]] = fadd float [[ARG0]], [[ARG1]]
; CHECK-NEXT: ret float [[ADD]]
;
%add = fadd float %arg0, %arg1
ret float %add
}
define float @test_fadd_no_nan_from_no_pinf(float nofpclass(nan pinf) %arg0, float nofpclass(nan pinf) %arg1) {
; CHECK: Function Attrs: mustprogress nofree norecurse nosync nounwind willreturn memory(none)
; CHECK-LABEL: define nofpclass(nan) float @test_fadd_no_nan_from_no_pinf
; CHECK-SAME: (float nofpclass(nan pinf) [[ARG0:%.*]], float nofpclass(nan pinf) [[ARG1:%.*]]) #[[ATTR:[0-9]+]] {
; CHECK-NEXT: [[ADD:%.*]] = fadd float [[ARG0]], [[ARG1]]
; CHECK-NEXT: ret float [[ADD]]
;
%add = fadd float %arg0, %arg1
ret float %add
}
define float @test_fadd_may_nan_from_no_pinf_no_ninf(float nofpclass(nan pinf) %arg0, float nofpclass(nan ninf) %arg1) {
; CHECK: Function Attrs: mustprogress nofree norecurse nosync nounwind willreturn memory(none)
; CHECK-LABEL: define float @test_fadd_may_nan_from_no_pinf_no_ninf
; CHECK-SAME: (float nofpclass(nan pinf) [[ARG0:%.*]], float nofpclass(nan ninf) [[ARG1:%.*]]) #[[ATTR:[0-9]+]] {
; CHECK-NEXT: [[ADD:%.*]] = fadd float [[ARG0]], [[ARG1]]
; CHECK-NEXT: ret float [[ADD]]
;
%add = fadd float %arg0, %arg1
ret float %add
}
define float @test_fadd_may_nan_from_no_ninf_no_pinf(float nofpclass(nan ninf) %arg0, float nofpclass(nan pinf) %arg1) {
; CHECK: Function Attrs: mustprogress nofree norecurse nosync nounwind willreturn memory(none)
; CHECK-LABEL: define float @test_fadd_may_nan_from_no_ninf_no_pinf
; CHECK-SAME: (float nofpclass(nan ninf) [[ARG0:%.*]], float nofpclass(nan pinf) [[ARG1:%.*]]) #[[ATTR:[0-9]+]] {
; CHECK-NEXT: [[ADD:%.*]] = fadd float [[ARG0]], [[ARG1]]
; CHECK-NEXT: ret float [[ADD]]
;
%add = fadd float %arg0, %arg1
ret float %add
}
define float @fadd_known_positive_nzero_lhs(float nofpclass(ninf nsub nnorm nzero) %arg0, float nofpclass(ninf nsub nnorm) %arg1) {
; CHECK: Function Attrs: mustprogress nofree norecurse nosync nounwind willreturn memory(none)
; CHECK-LABEL: define nofpclass(ninf nzero nsub nnorm) float @fadd_known_positive_nzero_lhs

View File

@ -490,7 +490,7 @@ define nofpclass(nzero) half @inferred_nan_output__fadd__no_pinf_no_nan__no_nan(
define nofpclass(nzero) half @inferred_nan_output__fadd__no_pinf_no_nan__no_pinf_no_nan(half nofpclass(nan pinf) %x, half nofpclass(nan pinf) %y) {
; CHECK-LABEL: define nofpclass(nzero) half @inferred_nan_output__fadd__no_pinf_no_nan__no_pinf_no_nan(
; CHECK-SAME: half nofpclass(nan pinf) [[X:%.*]], half nofpclass(nan pinf) [[Y:%.*]]) {
; CHECK-NEXT: [[ADD:%.*]] = fadd half [[X]], [[Y]]
; CHECK-NEXT: [[ADD:%.*]] = fadd nnan half [[X]], [[Y]]
; CHECK-NEXT: ret half [[ADD]]
;
%add = fadd half %x, %y
@ -500,7 +500,7 @@ define nofpclass(nzero) half @inferred_nan_output__fadd__no_pinf_no_nan__no_pinf
define nofpclass(nzero) half @inferred_nan_output__fadd__no_ninf_no_nan__no_ninf_no_nan(half nofpclass(nan ninf) %x, half nofpclass(nan ninf) %y) {
; CHECK-LABEL: define nofpclass(nzero) half @inferred_nan_output__fadd__no_ninf_no_nan__no_ninf_no_nan(
; CHECK-SAME: half nofpclass(nan ninf) [[X:%.*]], half nofpclass(nan ninf) [[Y:%.*]]) {
; CHECK-NEXT: [[ADD:%.*]] = fadd half [[X]], [[Y]]
; CHECK-NEXT: [[ADD:%.*]] = fadd nnan half [[X]], [[Y]]
; CHECK-NEXT: ret half [[ADD]]
;
%add = fadd half %x, %y

View File

@ -340,10 +340,7 @@ define i1 @uitofp_add(i32 %arg0) {
define i1 @uitofp_add_big(i1024 %arg0) {
; CHECK-LABEL: @uitofp_add_big(
; CHECK-NEXT: [[OP:%.*]] = uitofp i1024 [[ARG0:%.*]] to double
; CHECK-NEXT: [[ADD:%.*]] = fadd double [[OP]], [[OP]]
; CHECK-NEXT: [[TMP:%.*]] = fcmp ord double [[ADD]], [[ADD]]
; CHECK-NEXT: ret i1 [[TMP]]
; CHECK-NEXT: ret i1 true
;
%op = uitofp i1024 %arg0 to double
%add = fadd double %op, %op