[llvm] b7877e0 - [ConstraintElim] Derive an unsigned IV bound from a signed relational latch. (#222762)
via llvm-commits
llvm-commits at lists.llvm.org
Sun Sep 13 11:09:42 PDT 2026
Author: Florian Hahn
Date: 2026-09-13T19:09:37+01:00
New Revision: b7877e01cb1087d81fd72eb320c3c7d3f8e03500
URL: https://github.com/llvm/llvm-project/commit/b7877e01cb1087d81fd72eb320c3c7d3f8e03500
DIFF: https://github.com/llvm/llvm-project/commit/b7877e01cb1087d81fd72eb320c3c7d3f8e03500.diff
LOG: [ConstraintElim] Derive an unsigned IV bound from a signed relational latch. (#222762)
For a known non-negative backedge (either via isKnownNonNegative or
because the increment is increasing), 0 <=s PN <= B holds and implies
that B is non-negative as well.
Use that to translate a signed condition to the equivalent unsigned one.
Note that the general signed->unsigned rewrite cannot catch this,
because the precondition also needs rewriting to unsigned.
No llvm-opt-benchmark-nightly impact, but it can help remove runtime
checks generated by sanitizers or Swift code. An end-to-end C example is
https://clang.godbolt.org/z/vbd91MjaM.
Alive2 Proof: https://alive2.llvm.org/ce/z/G3Mv7t
PR: https://github.com/llvm/llvm-project/pull/222762
Added:
Modified:
llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
llvm/test/Transforms/ConstraintElimination/induction-relational-predicate-latch.ll
Removed:
################################################################################
diff --git a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
index da2d61e1c6e27..f73f8c9180a44 100644
--- a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
+++ b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
@@ -1188,6 +1188,21 @@ void State::addInfoForInductions(BasicBlock &BB) {
WorkList.push_back(FactOrCheck::getConditionFact(
DTN, ContinuePred, PN, B, ConditionTy(ContinuePred, StartValue, B)));
+ // A signed bound can be translated to the unsigned system if PN is signed
+ // non-decreasing (StartValue s<= PN s< B) and StartValue u< B holds.
+ // Then StartValue, PN and B must all have the same sign.
+ if (ICmpInst::isSigned(ContinuePred)) {
+ assert((ContinuePred == CmpInst::ICMP_SLT ||
+ ContinuePred == CmpInst::ICMP_SLE) &&
+ "Expected a signed less-than continuation predicate");
+ MonotonicInfo Info = getMonotonicityInfo(*PN, Backedge);
+ if (Info.Signed && !Info.Decreasing) {
+ CmpInst::Predicate UPred = ICmpInst::getUnsignedPredicate(ContinuePred);
+ WorkList.push_back(FactOrCheck::getConditionFact(
+ DTN, UPred, PN, B, ConditionTy(UPred, StartValue, B)));
+ }
+ }
+
// A relational latch steps past B rather than landing on it, so none of the
// reasoning below applies.
return;
diff --git a/llvm/test/Transforms/ConstraintElimination/induction-relational-predicate-latch.ll b/llvm/test/Transforms/ConstraintElimination/induction-relational-predicate-latch.ll
index 803679831b988..bdc1f406fce90 100644
--- a/llvm/test/Transforms/ConstraintElimination/induction-relational-predicate-latch.ll
+++ b/llvm/test/Transforms/ConstraintElimination/induction-relational-predicate-latch.ll
@@ -712,3 +712,246 @@ loop.exit:
call void @use(i1 %c)
ret void
}
+
+; %iv is known non-negative, so the signed condition in the latch can also be
+; translated to an unsigned bound.
+define void @signed_latch_unsigned_fact(i64 %n, i1 %header.ec) {
+; CHECK-LABEL: define void @signed_latch_unsigned_fact(
+; CHECK-SAME: i64 [[N:%.*]], i1 [[HEADER_EC:%.*]]) {
+; CHECK-NEXT: [[ENTRY:.*]]:
+; CHECK-NEXT: [[PRE:%.*]] = icmp ne i64 [[N]], 0
+; CHECK-NEXT: call void @llvm.assume(i1 [[PRE]])
+; CHECK-NEXT: br label %[[LOOP_HEADER:.*]]
+; CHECK: [[LOOP_HEADER]]:
+; CHECK-NEXT: [[IV:%.*]] = phi i64 [ 0, %[[ENTRY]] ], [ [[IV_NEXT:%.*]], %[[LOOP_LATCH:.*]] ]
+; CHECK-NEXT: call void @use(i1 true)
+; CHECK-NEXT: br i1 [[HEADER_EC]], label %[[EXIT:.*]], label %[[LOOP_LATCH]]
+; CHECK: [[LOOP_LATCH]]:
+; CHECK-NEXT: [[IV_NEXT]] = add nsw i64 [[IV]], 2
+; CHECK-NEXT: [[EC:%.*]] = icmp slt i64 [[IV_NEXT]], [[N]]
+; CHECK-NEXT: br i1 [[EC]], label %[[LOOP_HEADER]], label %[[EXIT]]
+; CHECK: [[EXIT]]:
+; CHECK-NEXT: ret void
+;
+entry:
+ %pre = icmp ne i64 %n, 0
+ call void @llvm.assume(i1 %pre)
+ br label %loop.header
+
+loop.header:
+ %iv = phi i64 [ 0, %entry ], [ %iv.next, %loop.latch ]
+ %c = icmp ult i64 %iv, %n
+ call void @use(i1 %c)
+ br i1 %header.ec, label %exit, label %loop.latch
+
+loop.latch:
+ %iv.next = add nsw i64 %iv, 2
+ %ec = icmp slt i64 %iv.next, %n
+ br i1 %ec, label %loop.header, label %exit
+
+exit:
+ ret void
+}
+
+; Same, but the step may wrap.
+define void @neg_wrapping_step_no_unsigned_fact(i64 %n, i1 %header.ec) {
+; CHECK-LABEL: define void @neg_wrapping_step_no_unsigned_fact(
+; CHECK-SAME: i64 [[N:%.*]], i1 [[HEADER_EC:%.*]]) {
+; CHECK-NEXT: [[ENTRY:.*]]:
+; CHECK-NEXT: [[PRE:%.*]] = icmp ne i64 [[N]], 0
+; CHECK-NEXT: call void @llvm.assume(i1 [[PRE]])
+; CHECK-NEXT: br label %[[LOOP_HEADER:.*]]
+; CHECK: [[LOOP_HEADER]]:
+; CHECK-NEXT: [[IV:%.*]] = phi i64 [ 0, %[[ENTRY]] ], [ [[IV_NEXT:%.*]], %[[LOOP_LATCH:.*]] ]
+; CHECK-NEXT: [[C:%.*]] = icmp ult i64 [[IV]], [[N]]
+; CHECK-NEXT: call void @use(i1 [[C]])
+; CHECK-NEXT: br i1 [[HEADER_EC]], label %[[EXIT:.*]], label %[[LOOP_LATCH]]
+; CHECK: [[LOOP_LATCH]]:
+; CHECK-NEXT: [[IV_NEXT]] = add i64 [[IV]], 2
+; CHECK-NEXT: [[EC:%.*]] = icmp slt i64 [[IV_NEXT]], [[N]]
+; CHECK-NEXT: br i1 [[EC]], label %[[LOOP_HEADER]], label %[[EXIT]]
+; CHECK: [[EXIT]]:
+; CHECK-NEXT: ret void
+;
+entry:
+ %pre = icmp ne i64 %n, 0
+ call void @llvm.assume(i1 %pre)
+ br label %loop.header
+
+loop.header:
+ %iv = phi i64 [ 0, %entry ], [ %iv.next, %loop.latch ]
+ %c = icmp ult i64 %iv, %n
+ call void @use(i1 %c)
+ br i1 %header.ec, label %exit, label %loop.latch
+
+loop.latch:
+ %iv.next = add i64 %iv, 2
+ %ec = icmp slt i64 %iv.next, %n
+ br i1 %ec, label %loop.header, label %exit
+
+exit:
+ ret void
+}
+
+define void @signed_latch_unsigned_fact_variable_start(i64 %start, i64 %n, i1 %header.ec) {
+; CHECK-LABEL: define void @signed_latch_unsigned_fact_variable_start(
+; CHECK-SAME: i64 [[START:%.*]], i64 [[N:%.*]], i1 [[HEADER_EC:%.*]]) {
+; CHECK-NEXT: [[ENTRY:.*]]:
+; CHECK-NEXT: [[PRE:%.*]] = icmp ult i64 [[START]], [[N]]
+; CHECK-NEXT: call void @llvm.assume(i1 [[PRE]])
+; CHECK-NEXT: [[PRE_POS:%.*]] = icmp sge i64 [[START]], 0
+; CHECK-NEXT: call void @llvm.assume(i1 [[PRE_POS]])
+; CHECK-NEXT: br label %[[LOOP_HEADER:.*]]
+; CHECK: [[LOOP_HEADER]]:
+; CHECK-NEXT: [[IV:%.*]] = phi i64 [ [[START]], %[[ENTRY]] ], [ [[IV_NEXT:%.*]], %[[LOOP_LATCH:.*]] ]
+; CHECK-NEXT: call void @use(i1 true)
+; CHECK-NEXT: br i1 [[HEADER_EC]], label %[[EXIT:.*]], label %[[LOOP_LATCH]]
+; CHECK: [[LOOP_LATCH]]:
+; CHECK-NEXT: [[IV_NEXT]] = add nsw i64 [[IV]], 2
+; CHECK-NEXT: [[EC:%.*]] = icmp slt i64 [[IV_NEXT]], [[N]]
+; CHECK-NEXT: br i1 [[EC]], label %[[LOOP_HEADER]], label %[[EXIT]]
+; CHECK: [[EXIT]]:
+; CHECK-NEXT: ret void
+;
+entry:
+ %pre.1 = icmp ult i64 %start, %n
+ call void @llvm.assume(i1 %pre.1)
+ %start.pos = icmp sge i64 %start, 0
+ call void @llvm.assume(i1 %start.pos)
+ br label %loop.header
+
+loop.header:
+ %iv = phi i64 [ %start, %entry ], [ %iv.next, %loop.latch ]
+ %c = icmp ult i64 %iv, %n
+ call void @use(i1 %c)
+ br i1 %header.ec, label %exit, label %loop.latch
+
+loop.latch:
+ %iv.next = add nsw i64 %iv, 2
+ %ec = icmp slt i64 %iv.next, %n
+ br i1 %ec, label %loop.header, label %exit
+
+exit:
+ ret void
+}
+
+; Same as above, but with missing %start < %n precondition.
+define void @signed_latch_unsigned_fact_variable_start_missing_ult(i64 %start, i64 %n, i1 %header.ec) {
+; CHECK-LABEL: define void @signed_latch_unsigned_fact_variable_start_missing_ult(
+; CHECK-SAME: i64 [[START:%.*]], i64 [[N:%.*]], i1 [[HEADER_EC:%.*]]) {
+; CHECK-NEXT: [[ENTRY:.*]]:
+; CHECK-NEXT: [[PRE_POS:%.*]] = icmp sge i64 [[START]], 0
+; CHECK-NEXT: call void @llvm.assume(i1 [[PRE_POS]])
+; CHECK-NEXT: br label %[[LOOP_HEADER:.*]]
+; CHECK: [[LOOP_HEADER]]:
+; CHECK-NEXT: [[IV:%.*]] = phi i64 [ [[START]], %[[ENTRY]] ], [ [[IV_NEXT:%.*]], %[[LOOP_LATCH:.*]] ]
+; CHECK-NEXT: [[C:%.*]] = icmp ult i64 [[IV]], [[N]]
+; CHECK-NEXT: call void @use(i1 [[C]])
+; CHECK-NEXT: br i1 [[HEADER_EC]], label %[[EXIT:.*]], label %[[LOOP_LATCH]]
+; CHECK: [[LOOP_LATCH]]:
+; CHECK-NEXT: [[IV_NEXT]] = add nsw i64 [[IV]], 2
+; CHECK-NEXT: [[EC:%.*]] = icmp slt i64 [[IV_NEXT]], [[N]]
+; CHECK-NEXT: br i1 [[EC]], label %[[LOOP_HEADER]], label %[[EXIT]]
+; CHECK: [[EXIT]]:
+; CHECK-NEXT: ret void
+;
+entry:
+ %start.pos = icmp sge i64 %start, 0
+ call void @llvm.assume(i1 %start.pos)
+ br label %loop.header
+
+loop.header:
+ %iv = phi i64 [ %start, %entry ], [ %iv.next, %loop.latch ]
+ %c = icmp ult i64 %iv, %n
+ call void @use(i1 %c)
+ br i1 %header.ec, label %exit, label %loop.latch
+
+loop.latch:
+ %iv.next = add nsw i64 %iv, 2
+ %ec = icmp slt i64 %iv.next, %n
+ br i1 %ec, label %loop.header, label %exit
+
+exit:
+ ret void
+}
+
+; Continuing on sgt does not imply an unsigned lower bound. For n = -2,
+; incrementing iv from -1 to 0 makes the unsigned comparison false.
+define void @signed_gt_latch_no_unsigned_fact(i64 %n) {
+; CHECK-LABEL: define void @signed_gt_latch_no_unsigned_fact(
+; CHECK-SAME: i64 [[N:%.*]]) {
+; CHECK-NEXT: [[ENTRY:.*]]:
+; CHECK-NEXT: [[PRE:%.*]] = icmp ugt i64 -1, [[N]]
+; CHECK-NEXT: call void @llvm.assume(i1 [[PRE]])
+; CHECK-NEXT: br label %[[LOOP_HEADER:.*]]
+; CHECK: [[LOOP_HEADER]]:
+; CHECK-NEXT: [[IV:%.*]] = phi i64 [ -1, %[[ENTRY]] ], [ [[IV_NEXT:%.*]], %[[LOOP_LATCH:.*]] ]
+; CHECK-NEXT: [[C:%.*]] = icmp ugt i64 [[IV]], [[N]]
+; CHECK-NEXT: call void @use(i1 [[C]])
+; CHECK-NEXT: [[STOP:%.*]] = icmp eq i64 [[IV]], 1
+; CHECK-NEXT: br i1 [[STOP]], label %[[EXIT:.*]], label %[[LOOP_LATCH]]
+; CHECK: [[LOOP_LATCH]]:
+; CHECK-NEXT: [[IV_NEXT]] = add nsw i64 [[IV]], 1
+; CHECK-NEXT: [[EC:%.*]] = icmp sgt i64 [[IV_NEXT]], [[N]]
+; CHECK-NEXT: br i1 [[EC]], label %[[LOOP_HEADER]], label %[[EXIT]]
+; CHECK: [[EXIT]]:
+; CHECK-NEXT: ret void
+;
+entry:
+ %pre = icmp ugt i64 -1, %n
+ call void @llvm.assume(i1 %pre)
+ br label %loop.header
+
+loop.header:
+ %iv = phi i64 [ -1, %entry ], [ %iv.next, %loop.latch ]
+ %c = icmp ugt i64 %iv, %n
+ call void @use(i1 %c)
+ %stop = icmp eq i64 %iv, 1
+ br i1 %stop, label %exit, label %loop.latch
+
+loop.latch:
+ %iv.next = add nsw i64 %iv, 1
+ %ec = icmp sgt i64 %iv.next, %n
+ br i1 %ec, label %loop.header, label %exit
+
+exit:
+ ret void
+}
+
+; Exiting on sgt instead gives a signed <= continuation, which does imply an
+; unsigned upper bound for this non-negative induction.
+define void @signed_gt_exit_unsigned_fact(i64 %n) {
+; CHECK-LABEL: define void @signed_gt_exit_unsigned_fact(
+; CHECK-SAME: i64 [[N:%.*]]) {
+; CHECK-NEXT: [[ENTRY:.*]]:
+; CHECK-NEXT: br label %[[LOOP_HEADER:.*]]
+; CHECK: [[LOOP_HEADER]]:
+; CHECK-NEXT: [[IV:%.*]] = phi i64 [ 0, %[[ENTRY]] ], [ [[IV_NEXT:%.*]], %[[LOOP_LATCH:.*]] ]
+; CHECK-NEXT: call void @use(i1 true)
+; CHECK-NEXT: [[STOP:%.*]] = icmp eq i64 [[IV]], 4
+; CHECK-NEXT: br i1 [[STOP]], label %[[EXIT:.*]], label %[[LOOP_LATCH]]
+; CHECK: [[LOOP_LATCH]]:
+; CHECK-NEXT: [[IV_NEXT]] = add nuw nsw i64 [[IV]], 1
+; CHECK-NEXT: [[EC:%.*]] = icmp sgt i64 [[IV_NEXT]], [[N]]
+; CHECK-NEXT: br i1 [[EC]], label %[[EXIT]], label %[[LOOP_HEADER]]
+; CHECK: [[EXIT]]:
+; CHECK-NEXT: ret void
+;
+entry:
+ br label %loop.header
+
+loop.header:
+ %iv = phi i64 [ 0, %entry ], [ %iv.next, %loop.latch ]
+ %c = icmp ule i64 %iv, %n
+ call void @use(i1 %c)
+ %stop = icmp eq i64 %iv, 4
+ br i1 %stop, label %exit, label %loop.latch
+
+loop.latch:
+ %iv.next = add nsw i64 %iv, 1
+ %ec = icmp sgt i64 %iv.next, %n
+ br i1 %ec, label %exit, label %loop.header
+
+exit:
+ ret void
+}
More information about the llvm-commits
mailing list