[llvm] [ScalarEvolution] Avoid recursive proof blowup for recurrence starts (PR #225000)
Justin Leong via llvm-commits
llvm-commits at lists.llvm.org
Thu Oct 1 16:52:04 PDT 2026
https://github.com/justinleong22 updated https://github.com/llvm/llvm-project/pull/225000
>From aea70f24e1fe93b40505e1f92146b550f2b2e98f Mon Sep 17 00:00:00 2001
From: Justin Leong <117539348+justinleong22 at users.noreply.github.com>
Date: Sun, 20 Sep 2026 22:41:50 -0700
Subject: [PATCH 1/2] [ScalarEvolution] Avoid recursive proof blowup for
recurrence starts
Assisted-by: OpenAI Codex
---
llvm/lib/Analysis/ScalarEvolution.cpp | 15 +-
.../addrec-start-compile-time.ll | 208 ++++++++++++++++++
2 files changed, 218 insertions(+), 5 deletions(-)
create mode 100644 llvm/test/Transforms/LoopStrengthReduce/addrec-start-compile-time.ll
diff --git a/llvm/lib/Analysis/ScalarEvolution.cpp b/llvm/lib/Analysis/ScalarEvolution.cpp
index 50e0170b55089..0067f0fe2999b 100644
--- a/llvm/lib/Analysis/ScalarEvolution.cpp
+++ b/llvm/lib/Analysis/ScalarEvolution.cpp
@@ -12885,9 +12885,9 @@ static bool IsMinMaxConsistingOf(const SCEV *MaybeMinMaxExpr,
return is_contained(MinMaxExpr->operands(), Candidate);
}
-static bool IsKnownPredicateViaAddRecStart(ScalarEvolution &SE,
- CmpPredicate Pred, const SCEV *LHS,
- const SCEV *RHS) {
+static bool IsKnownPredicateViaAddRecStart(
+ CmpPredicate Pred, const SCEV *LHS, const SCEV *RHS,
+ function_ref<bool(const SCEV *, const SCEV *)> IsKnown) {
// If both sides are affine addrecs for the same loop, with equal
// steps, and we know the recurrences don't wrap, then we only
// need to check the predicate on the starting values.
@@ -12909,7 +12909,7 @@ static bool IsKnownPredicateViaAddRecStart(ScalarEvolution &SE,
if (!LAR->getNoWrapFlags(NW) || !RAR->getNoWrapFlags(NW))
return false;
- return SE.isKnownPredicate(Pred, LStart, RStart);
+ return IsKnown(LStart, RStart);
}
/// Is LHS `Pred` RHS true because one of them is an AddRec that is known not to
@@ -13196,7 +13196,12 @@ bool ScalarEvolution::isKnownViaNonRecursiveReasoning(CmpPredicate Pred,
return isKnownPredicateExtendIdiom(Pred, LHS, RHS) ||
isKnownPredicateViaConstantRanges(Pred, LHS, RHS) ||
IsKnownPredicateViaMinOrMax(*this, Pred, LHS, RHS) ||
- IsKnownPredicateViaAddRecStart(*this, Pred, LHS, RHS) ||
+ IsKnownPredicateViaAddRecStart(
+ Pred, LHS, RHS, [&](const SCEV *LStart, const SCEV *RStart) {
+ // Reentering the full predicate prover here can recursively
+ // branch into induction proofs for a chain of recurrences.
+ return isKnownViaNonRecursiveReasoning(Pred, LStart, RStart);
+ }) ||
IsKnownPredicateViaAddRecMonotonicity(*this, Pred, LHS, RHS) ||
isKnownPredicateViaNoOverflow(Pred, LHS, RHS);
}
diff --git a/llvm/test/Transforms/LoopStrengthReduce/addrec-start-compile-time.ll b/llvm/test/Transforms/LoopStrengthReduce/addrec-start-compile-time.ll
new file mode 100644
index 0000000000000..d93d9dccc7403
--- /dev/null
+++ b/llvm/test/Transforms/LoopStrengthReduce/addrec-start-compile-time.ll
@@ -0,0 +1,208 @@
+; RUN: opt -passes=loop-reduce -S < %s | FileCheck %s
+; REQUIRES: x86-registered-target
+;
+; A sequence of loops whose recurrence starts depend on earlier loops.
+; Proving comparisons of the starts must not recursively branch into full
+; induction proofs from the nonrecursive predicate prover (issue #221391).
+; Calls are to a declared function. No poison pointers, null calls,
+; unchecked memory accesses, or wrapping arithmetic are involved.
+target triple = "x86_64-unknown-linux-gnu"
+declare i1 @keep_going(i64)
+define i64 @chain() {
+; CHECK-LABEL: define i64 @chain()
+; CHECK: loop0:
+; CHECK: call i1 @keep_going
+; CHECK: loop16:
+; CHECK: call i1 @keep_going
+; CHECK: ret i64
+entry:
+ br label %loop0
+loop0:
+ %iv0 = phi i64 [0, %entry], [%next0, %cont0]
+ %next0 = add nuw nsw i64 %iv0, 1
+ %go0 = call i1 @keep_going(i64 %iv0)
+ br i1 %go0, label %cont0, label %after0
+cont0:
+ %guard0 = icmp ult i64 %iv0, 65533
+ br i1 %guard0, label %loop0, label %exit
+after0:
+ %start1 = add nuw nsw i64 %iv0, 2
+ br label %loop1
+loop1:
+ %iv1 = phi i64 [%start1, %after0], [%next1, %cont1]
+ %next1 = add nuw nsw i64 %iv1, 1
+ %go1 = call i1 @keep_going(i64 %iv1)
+ br i1 %go1, label %cont1, label %after1
+cont1:
+ %guard1 = icmp ult i64 %iv1, 65533
+ br i1 %guard1, label %loop1, label %exit
+after1:
+ %start2 = add nuw nsw i64 %iv1, 2
+ br label %loop2
+loop2:
+ %iv2 = phi i64 [%start2, %after1], [%next2, %cont2]
+ %next2 = add nuw nsw i64 %iv2, 1
+ %go2 = call i1 @keep_going(i64 %iv2)
+ br i1 %go2, label %cont2, label %after2
+cont2:
+ %guard2 = icmp ult i64 %iv2, 65533
+ br i1 %guard2, label %loop2, label %exit
+after2:
+ %start3 = add nuw nsw i64 %iv2, 2
+ br label %loop3
+loop3:
+ %iv3 = phi i64 [%start3, %after2], [%next3, %cont3]
+ %next3 = add nuw nsw i64 %iv3, 1
+ %go3 = call i1 @keep_going(i64 %iv3)
+ br i1 %go3, label %cont3, label %after3
+cont3:
+ %guard3 = icmp ult i64 %iv3, 65533
+ br i1 %guard3, label %loop3, label %exit
+after3:
+ %start4 = add nuw nsw i64 %iv3, 2
+ br label %loop4
+loop4:
+ %iv4 = phi i64 [%start4, %after3], [%next4, %cont4]
+ %next4 = add nuw nsw i64 %iv4, 1
+ %go4 = call i1 @keep_going(i64 %iv4)
+ br i1 %go4, label %cont4, label %after4
+cont4:
+ %guard4 = icmp ult i64 %iv4, 65533
+ br i1 %guard4, label %loop4, label %exit
+after4:
+ %start5 = add nuw nsw i64 %iv4, 2
+ br label %loop5
+loop5:
+ %iv5 = phi i64 [%start5, %after4], [%next5, %cont5]
+ %next5 = add nuw nsw i64 %iv5, 1
+ %go5 = call i1 @keep_going(i64 %iv5)
+ br i1 %go5, label %cont5, label %after5
+cont5:
+ %guard5 = icmp ult i64 %iv5, 65533
+ br i1 %guard5, label %loop5, label %exit
+after5:
+ %start6 = add nuw nsw i64 %iv5, 2
+ br label %loop6
+loop6:
+ %iv6 = phi i64 [%start6, %after5], [%next6, %cont6]
+ %next6 = add nuw nsw i64 %iv6, 1
+ %go6 = call i1 @keep_going(i64 %iv6)
+ br i1 %go6, label %cont6, label %after6
+cont6:
+ %guard6 = icmp ult i64 %iv6, 65533
+ br i1 %guard6, label %loop6, label %exit
+after6:
+ %start7 = add nuw nsw i64 %iv6, 2
+ br label %loop7
+loop7:
+ %iv7 = phi i64 [%start7, %after6], [%next7, %cont7]
+ %next7 = add nuw nsw i64 %iv7, 1
+ %go7 = call i1 @keep_going(i64 %iv7)
+ br i1 %go7, label %cont7, label %after7
+cont7:
+ %guard7 = icmp ult i64 %iv7, 65533
+ br i1 %guard7, label %loop7, label %exit
+after7:
+ %start8 = add nuw nsw i64 %iv7, 2
+ br label %loop8
+loop8:
+ %iv8 = phi i64 [%start8, %after7], [%next8, %cont8]
+ %next8 = add nuw nsw i64 %iv8, 1
+ %go8 = call i1 @keep_going(i64 %iv8)
+ br i1 %go8, label %cont8, label %after8
+cont8:
+ %guard8 = icmp ult i64 %iv8, 65533
+ br i1 %guard8, label %loop8, label %exit
+after8:
+ %start9 = add nuw nsw i64 %iv8, 2
+ br label %loop9
+loop9:
+ %iv9 = phi i64 [%start9, %after8], [%next9, %cont9]
+ %next9 = add nuw nsw i64 %iv9, 1
+ %go9 = call i1 @keep_going(i64 %iv9)
+ br i1 %go9, label %cont9, label %after9
+cont9:
+ %guard9 = icmp ult i64 %iv9, 65533
+ br i1 %guard9, label %loop9, label %exit
+after9:
+ %start10 = add nuw nsw i64 %iv9, 2
+ br label %loop10
+loop10:
+ %iv10 = phi i64 [%start10, %after9], [%next10, %cont10]
+ %next10 = add nuw nsw i64 %iv10, 1
+ %go10 = call i1 @keep_going(i64 %iv10)
+ br i1 %go10, label %cont10, label %after10
+cont10:
+ %guard10 = icmp ult i64 %iv10, 65533
+ br i1 %guard10, label %loop10, label %exit
+after10:
+ %start11 = add nuw nsw i64 %iv10, 2
+ br label %loop11
+loop11:
+ %iv11 = phi i64 [%start11, %after10], [%next11, %cont11]
+ %next11 = add nuw nsw i64 %iv11, 1
+ %go11 = call i1 @keep_going(i64 %iv11)
+ br i1 %go11, label %cont11, label %after11
+cont11:
+ %guard11 = icmp ult i64 %iv11, 65533
+ br i1 %guard11, label %loop11, label %exit
+after11:
+ %start12 = add nuw nsw i64 %iv11, 2
+ br label %loop12
+loop12:
+ %iv12 = phi i64 [%start12, %after11], [%next12, %cont12]
+ %next12 = add nuw nsw i64 %iv12, 1
+ %go12 = call i1 @keep_going(i64 %iv12)
+ br i1 %go12, label %cont12, label %after12
+cont12:
+ %guard12 = icmp ult i64 %iv12, 65533
+ br i1 %guard12, label %loop12, label %exit
+after12:
+ %start13 = add nuw nsw i64 %iv12, 2
+ br label %loop13
+loop13:
+ %iv13 = phi i64 [%start13, %after12], [%next13, %cont13]
+ %next13 = add nuw nsw i64 %iv13, 1
+ %go13 = call i1 @keep_going(i64 %iv13)
+ br i1 %go13, label %cont13, label %after13
+cont13:
+ %guard13 = icmp ult i64 %iv13, 65533
+ br i1 %guard13, label %loop13, label %exit
+after13:
+ %start14 = add nuw nsw i64 %iv13, 2
+ br label %loop14
+loop14:
+ %iv14 = phi i64 [%start14, %after13], [%next14, %cont14]
+ %next14 = add nuw nsw i64 %iv14, 1
+ %go14 = call i1 @keep_going(i64 %iv14)
+ br i1 %go14, label %cont14, label %after14
+cont14:
+ %guard14 = icmp ult i64 %iv14, 65533
+ br i1 %guard14, label %loop14, label %exit
+after14:
+ %start15 = add nuw nsw i64 %iv14, 2
+ br label %loop15
+loop15:
+ %iv15 = phi i64 [%start15, %after14], [%next15, %cont15]
+ %next15 = add nuw nsw i64 %iv15, 1
+ %go15 = call i1 @keep_going(i64 %iv15)
+ br i1 %go15, label %cont15, label %after15
+cont15:
+ %guard15 = icmp ult i64 %iv15, 65533
+ br i1 %guard15, label %loop15, label %exit
+after15:
+ %start16 = add nuw nsw i64 %iv15, 2
+ br label %loop16
+loop16:
+ %iv16 = phi i64 [%start16, %after15], [%next16, %cont16]
+ %next16 = add nuw nsw i64 %iv16, 1
+ %go16 = call i1 @keep_going(i64 %iv16)
+ br i1 %go16, label %cont16, label %after16
+cont16:
+ %guard16 = icmp ult i64 %iv16, 65533
+ br i1 %guard16, label %loop16, label %exit
+after16:
+ ret i64 %iv16
+exit:
+ ret i64 65534
+}
>From e02afc474e62fa12e3feb9991fcf76c40ecca033 Mon Sep 17 00:00:00 2001
From: Justin Leong <117539348+justinleong22 at users.noreply.github.com>
Date: Thu, 1 Oct 2026 16:51:38 -0700
Subject: [PATCH 2/2] [ScalarEvolution] Address review feedback on
recurrence-start proofs
Make the recurrence-start predicate helper a private member and call the nonrecursive prover directly. Move the x86-dependent regression into the X86 test directory, which already supplies the target requirement.
Assisted-by: OpenAI Codex
---
llvm/include/llvm/Analysis/ScalarEvolution.h | 5 +++++
llvm/lib/Analysis/ScalarEvolution.cpp | 17 +++++++----------
.../{ => X86}/addrec-start-compile-time.ll | 1 -
3 files changed, 12 insertions(+), 11 deletions(-)
rename llvm/test/Transforms/LoopStrengthReduce/{ => X86}/addrec-start-compile-time.ll (99%)
diff --git a/llvm/include/llvm/Analysis/ScalarEvolution.h b/llvm/include/llvm/Analysis/ScalarEvolution.h
index 7fddd4ca4119f..13fb39f0bbb5a 100644
--- a/llvm/include/llvm/Analysis/ScalarEvolution.h
+++ b/llvm/include/llvm/Analysis/ScalarEvolution.h
@@ -2380,6 +2380,11 @@ class ScalarEvolution {
bool isKnownPredicateViaConstantRanges(CmpPredicate Pred, SCEVUse LHS,
SCEVUse RHS);
+ /// Test whether "LHS Pred RHS" is true by comparing the starts of two
+ /// non-wrapping affine add recurrences with the same loop and step.
+ bool isKnownPredicateViaAddRecStart(CmpPredicate Pred, const SCEV *LHS,
+ const SCEV *RHS);
+
/// Try to prove the condition described by "LHS Pred RHS" by ruling out
/// integer overflow.
///
diff --git a/llvm/lib/Analysis/ScalarEvolution.cpp b/llvm/lib/Analysis/ScalarEvolution.cpp
index 0067f0fe2999b..7079182776404 100644
--- a/llvm/lib/Analysis/ScalarEvolution.cpp
+++ b/llvm/lib/Analysis/ScalarEvolution.cpp
@@ -12885,9 +12885,9 @@ static bool IsMinMaxConsistingOf(const SCEV *MaybeMinMaxExpr,
return is_contained(MinMaxExpr->operands(), Candidate);
}
-static bool IsKnownPredicateViaAddRecStart(
- CmpPredicate Pred, const SCEV *LHS, const SCEV *RHS,
- function_ref<bool(const SCEV *, const SCEV *)> IsKnown) {
+bool ScalarEvolution::isKnownPredicateViaAddRecStart(CmpPredicate Pred,
+ const SCEV *LHS,
+ const SCEV *RHS) {
// If both sides are affine addrecs for the same loop, with equal
// steps, and we know the recurrences don't wrap, then we only
// need to check the predicate on the starting values.
@@ -12909,7 +12909,9 @@ static bool IsKnownPredicateViaAddRecStart(
if (!LAR->getNoWrapFlags(NW) || !RAR->getNoWrapFlags(NW))
return false;
- return IsKnown(LStart, RStart);
+ // Reentering the full predicate prover here can recursively
+ // branch into induction proofs for a chain of recurrences.
+ return isKnownViaNonRecursiveReasoning(Pred, LStart, RStart);
}
/// Is LHS `Pred` RHS true because one of them is an AddRec that is known not to
@@ -13196,12 +13198,7 @@ bool ScalarEvolution::isKnownViaNonRecursiveReasoning(CmpPredicate Pred,
return isKnownPredicateExtendIdiom(Pred, LHS, RHS) ||
isKnownPredicateViaConstantRanges(Pred, LHS, RHS) ||
IsKnownPredicateViaMinOrMax(*this, Pred, LHS, RHS) ||
- IsKnownPredicateViaAddRecStart(
- Pred, LHS, RHS, [&](const SCEV *LStart, const SCEV *RStart) {
- // Reentering the full predicate prover here can recursively
- // branch into induction proofs for a chain of recurrences.
- return isKnownViaNonRecursiveReasoning(Pred, LStart, RStart);
- }) ||
+ isKnownPredicateViaAddRecStart(Pred, LHS, RHS) ||
IsKnownPredicateViaAddRecMonotonicity(*this, Pred, LHS, RHS) ||
isKnownPredicateViaNoOverflow(Pred, LHS, RHS);
}
diff --git a/llvm/test/Transforms/LoopStrengthReduce/addrec-start-compile-time.ll b/llvm/test/Transforms/LoopStrengthReduce/X86/addrec-start-compile-time.ll
similarity index 99%
rename from llvm/test/Transforms/LoopStrengthReduce/addrec-start-compile-time.ll
rename to llvm/test/Transforms/LoopStrengthReduce/X86/addrec-start-compile-time.ll
index d93d9dccc7403..d3871939ea655 100644
--- a/llvm/test/Transforms/LoopStrengthReduce/addrec-start-compile-time.ll
+++ b/llvm/test/Transforms/LoopStrengthReduce/X86/addrec-start-compile-time.ll
@@ -1,5 +1,4 @@
; RUN: opt -passes=loop-reduce -S < %s | FileCheck %s
-; REQUIRES: x86-registered-target
;
; A sequence of loops whose recurrence starts depend on earlier loops.
; Proving comparisons of the starts must not recursively branch into full
More information about the llvm-commits
mailing list