[llvm] [ConstraintElim] Link values to decompositions during queries if needed. (PR #224623)

Florian Hahn via llvm-commits llvm-commits at lists.llvm.org
Tue Sep 22 03:16:54 PDT 2026


https://github.com/fhahn updated https://github.com/llvm/llvm-project/pull/224623

>From a3772cf4ec76aa470d8970a7dc15c96725d091a2 Mon Sep 17 00:00:00 2001
From: Florian Hahn <flo at fhahn.com>
Date: Thu, 17 Sep 2026 19:18:07 +0100
Subject: [PATCH 1/3] Add test

---
 .../ConstraintElimination/decompose-at-use.ll | 125 ++++++++++++++++++
 1 file changed, 125 insertions(+)
 create mode 100644 llvm/test/Transforms/ConstraintElimination/decompose-at-use.ll

diff --git a/llvm/test/Transforms/ConstraintElimination/decompose-at-use.ll b/llvm/test/Transforms/ConstraintElimination/decompose-at-use.ll
new file mode 100644
index 0000000000000..6253d001acabe
--- /dev/null
+++ b/llvm/test/Transforms/ConstraintElimination/decompose-at-use.ll
@@ -0,0 +1,125 @@
+; NOTE: Assertions have been autogenerated by utils/update_test_checks.py UTC_ARGS: --version 6
+; RUN: opt -passes=constraint-elimination -S %s | FileCheck %s
+
+; %add is opaque when %a > %add is added as fact and decomposable to %b + 1 by the
+; time it is queried.
+define i1 @eq_after_signed_add_becomes_decomposable_and_known(i16 %a, i16 %b) {
+; CHECK-LABEL: define i1 @eq_after_signed_add_becomes_decomposable_and_known(
+; CHECK-SAME: i16 [[A:%.*]], i16 [[B:%.*]]) {
+; CHECK-NEXT:  [[ENTRY:.*:]]
+; CHECK-NEXT:    [[ADD:%.*]] = add i16 [[B]], 1
+; CHECK-NEXT:    [[C:%.*]] = icmp sgt i16 [[A]], [[ADD]]
+; CHECK-NEXT:    br i1 [[C]], label %[[THEN:.*]], label %[[EXIT:.*]]
+; CHECK:       [[THEN]]:
+; CHECK-NEXT:    [[PRE:%.*]] = icmp slt i16 [[B]], 100
+; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE]])
+; CHECK-NEXT:    ret i1 false
+; CHECK:       [[EXIT]]:
+; CHECK-NEXT:    ret i1 false
+;
+entry:
+  %add = add i16 %b, 1
+  %c = icmp sgt i16 %a, %add
+  br i1 %c, label %then, label %exit
+
+then:
+  %pre = icmp slt i16 %b, 100
+  call void @llvm.assume(i1 %pre)
+  %eq = icmp eq i16 %a, %add
+  ret i1 %eq
+
+exit:
+  ret i1 false
+}
+
+; Same as above, but the condition cannot be simplified.
+define i1 @eq_after_signed_add_becomes_decomposable_and_not_known(i16 %a, i16 %b) {
+; CHECK-LABEL: define i1 @eq_after_signed_add_becomes_decomposable_and_not_known(
+; CHECK-SAME: i16 [[A:%.*]], i16 [[B:%.*]]) {
+; CHECK-NEXT:  [[ENTRY:.*:]]
+; CHECK-NEXT:    [[ADD:%.*]] = add i16 [[B]], 1
+; CHECK-NEXT:    [[C:%.*]] = icmp sgt i16 [[A]], [[ADD]]
+; CHECK-NEXT:    br i1 [[C]], label %[[THEN:.*]], label %[[EXIT:.*]]
+; CHECK:       [[THEN]]:
+; CHECK-NEXT:    [[PRE:%.*]] = icmp slt i16 [[B]], 100
+; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE]])
+; CHECK-NEXT:    [[EQ:%.*]] = icmp eq i16 [[A]], 10
+; CHECK-NEXT:    ret i1 [[EQ]]
+; CHECK:       [[EXIT]]:
+; CHECK-NEXT:    ret i1 false
+;
+entry:
+  %add = add i16 %b, 1
+  %c = icmp sgt i16 %a, %add
+  br i1 %c, label %then, label %exit
+
+then:
+  %pre = icmp slt i16 %b, 100
+  call void @llvm.assume(i1 %pre)
+  %eq = icmp eq i16 %a, 10
+  ret i1 %eq
+
+exit:
+  ret i1 false
+}
+
+; Same shape, but the query also mentions %opaque for which there is no fact.
+define i1 @eq_with_new_variable_in_signed_system(i16 %a, i16 %b, i16 %opaque) {
+; CHECK-LABEL: define i1 @eq_with_new_variable_in_signed_system(
+; CHECK-SAME: i16 [[A:%.*]], i16 [[B:%.*]], i16 [[OPAQUE:%.*]]) {
+; CHECK-NEXT:  [[ENTRY:.*:]]
+; CHECK-NEXT:    [[ADD:%.*]] = add i16 [[A]], 1
+; CHECK-NEXT:    [[C:%.*]] = icmp sgt i16 [[ADD]], 10
+; CHECK-NEXT:    br i1 [[C]], label %[[THEN:.*]], label %[[EXIT:.*]]
+; CHECK:       [[THEN]]:
+; CHECK-NEXT:    [[PRECOND:%.*]] = icmp slt i16 [[A]], 100
+; CHECK-NEXT:    call void @llvm.assume(i1 [[PRECOND]])
+; CHECK-NEXT:    [[EQ:%.*]] = icmp eq i16 [[ADD]], [[OPAQUE]]
+; CHECK-NEXT:    ret i1 [[EQ]]
+; CHECK:       [[EXIT]]:
+; CHECK-NEXT:    ret i1 false
+;
+entry:
+  %add = add i16 %a, 1
+  %c = icmp sgt i16 %add, 10
+  br i1 %c, label %then, label %exit
+
+then:
+  %pre = icmp slt i16 %a, 100
+  call void @llvm.assume(i1 %pre)
+  %eq = icmp eq i16 %add, %opaque
+  ret i1 %eq
+
+exit:
+  ret i1 false
+}
+
+define i1 @eq_after_unsigned_sub_becomes_decomposable(i16 %a, i16 %y, i16 %z) {
+; CHECK-LABEL: define i1 @eq_after_unsigned_sub_becomes_decomposable(
+; CHECK-SAME: i16 [[A:%.*]], i16 [[Y:%.*]], i16 [[Z:%.*]]) {
+; CHECK-NEXT:  [[ENTRY:.*:]]
+; CHECK-NEXT:    [[S:%.*]] = sub i16 [[Y]], [[Z]]
+; CHECK-NEXT:    [[C:%.*]] = icmp ugt i16 [[A]], [[S]]
+; CHECK-NEXT:    br i1 [[C]], label %[[THEN:.*]], label %[[EXIT:.*]]
+; CHECK:       [[THEN]]:
+; CHECK-NEXT:    [[PRECOND:%.*]] = icmp uge i16 [[Y]], [[Z]]
+; CHECK-NEXT:    call void @llvm.assume(i1 [[PRECOND]])
+; CHECK-NEXT:    [[EQ:%.*]] = icmp eq i16 [[A]], [[S]]
+; CHECK-NEXT:    ret i1 [[EQ]]
+; CHECK:       [[EXIT]]:
+; CHECK-NEXT:    ret i1 false
+;
+entry:
+  %s = sub i16 %y, %z
+  %c = icmp ugt i16 %a, %s
+  br i1 %c, label %then, label %exit
+
+then:
+  %pre = icmp uge i16 %y, %z
+  call void @llvm.assume(i1 %pre)
+  %eq = icmp eq i16 %a, %s
+  ret i1 %eq
+
+exit:
+  ret i1 false
+}

>From 96c62cfebd6b2fc23628240af3249732e0e6b153 Mon Sep 17 00:00:00 2001
From: Florian Hahn <flo at fhahn.com>
Date: Thu, 17 Sep 2026 20:14:15 +0000
Subject: [PATCH 2/3] [ConstraintElim] Link values to decompositions during
 queries if needed.

Decomposition is context sensitive and uses information at the query
point to determine if operations have the required wrap flags.

This can lead to situation where at the time facts are added, we fail to
decompose an operation (like %y = add %x, 1), and only add it as
variable %y.

If at query time, we can decompose %y, the query will contains %x and 1
as variable/constant, with no connection to the fact added earlier.

This can pessimize results in some cases. To avoid this, add additional
rows connecting the variable and the decomposition (e.g. %y == decompose
(add %x, 1)) and re-try the query.

For now, only check top-level operands. This helps with a few cases in
practice (I initially noticed the issue when adding a new rule for
no-wrap inference). But is not complete, as this issue could happen at
each step of the decompose recursion. We can investigate this as
follow-up.

2 additional folds in
https://github.com/dtcxzyw/llvm-opt-benchmark-nightly/pull/1351, a fold
in ClamAV and fixes a regression with
https://github.com/llvm/llvm-project/pull/224621.

Compile-time impact is in the noise
https://llvm-compile-time-tracker.com/compare.php?from=c5c167c7436f035152289cb9489548ccf5328bb3&to=e4be2920133168a85d0cfbf9390b1bc752abcc0f&stat=instructions:u
---
 llvm/lib/Analysis/ConstraintSystem.cpp        |  2 +
 .../Scalar/ConstraintElimination.cpp          | 56 ++++++++++++++++++-
 .../ConstraintElimination/decompose-at-use.ll |  3 +-
 3 files changed, 58 insertions(+), 3 deletions(-)

diff --git a/llvm/lib/Analysis/ConstraintSystem.cpp b/llvm/lib/Analysis/ConstraintSystem.cpp
index 56cb646093f83..85ac780b5f720 100644
--- a/llvm/lib/Analysis/ConstraintSystem.cpp
+++ b/llvm/lib/Analysis/ConstraintSystem.cpp
@@ -219,6 +219,8 @@ bool ConstraintSystem::mayHaveSolution() {
 
 std::pair<ConstraintSystem, ConstraintSystem::RowTy>
 ConstraintSystem::getSubSystem(ArrayRef<Entry> R) const {
+  assert((R.empty() || R.back().Id <= NumVariables) &&
+         "query must only use variables of the system");
   // Only constraints that share a variable (transitively) with a query R can
   // affect whether system + !R has a solution.
   //
diff --git a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
index 46b39ff77accc..e630e241c7bd1 100644
--- a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
+++ b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
@@ -1801,6 +1801,27 @@ static void generateReproducer(Instruction *Cond, bool IsSigned, Module *M,
   assert(!verifyFunction(*F, &dbgs()));
 }
 
+/// If \p V is a variable in the system and constraint \p C does not contain \p
+/// V, it is likely we managed to decompose \p V at this point, but not earlier
+/// when the fact involving \p V was added. In that case, return a new row for V
+/// == decompose(V) to link the variable with the decomposition result.
+static RowTy getDecompositionLinkRow(Value *V, const ConstraintTy &C,
+                                     const ConstraintInfo &Info,
+                                     const DataLayout &DL) {
+  const auto &Value2Index = Info.getValue2Index(C.IsSigned);
+  auto It = Value2Index.find(V);
+  if (It == Value2Index.end() ||
+      any_of(C.Coefficients,
+             [Id = It->second](const Entry &E) { return E.Id == Id; }))
+    return {};
+
+  SmallVector<Value *> NewVariables;
+  RowTy Row =
+      getRowForLessEqual(Decomposition(V), decompose(V, Info, C.IsSigned, DL),
+                         Value2Index, NewVariables);
+  return NewVariables.empty() ? Row : RowTy();
+}
+
 static std::optional<bool> checkCondition(CmpInst::Predicate Pred, Value *A,
                                           Value *B, Instruction *CheckInst,
                                           ConstraintInfo &Info) {
@@ -1830,9 +1851,39 @@ static std::optional<bool> checkCondition(CmpInst::Predicate Pred, Value *A,
     return std::nullopt;
   };
 
+  // Retry the query after adding additional facts for A == decompose(A) and B
+  // == decompose(B), if needed.
+  auto TryWithLinkedDecomposition =
+      [&](const ConstraintTy &C) -> std::optional<bool> {
+    if (C.empty())
+      return std::nullopt;
+
+    auto &CS = Info.getCS(C.IsSigned);
+    unsigned NumVars = Info.getValue2Index(C.IsSigned).size();
+    unsigned NumPushed = 0;
+    for (Value *V : {A, B}) {
+      RowTy Row =
+          getDecompositionLinkRow(V, C, Info, CheckInst->getDataLayout());
+      RowTy Negated = ConstraintSystem::negateOrEqual(Row);
+      if (Row.empty() || Negated.empty())
+        continue;
+      NumPushed += CS.addRow(Row, NumVars);
+      NumPushed += CS.addRow(Negated, NumVars);
+    }
+    if (NumPushed == 0)
+      return std::nullopt;
+
+    std::optional<bool> Res = TryWithConstraint(C);
+    while (NumPushed--)
+      CS.popLastConstraint();
+    return Res;
+  };
+
   auto R = Info.getConstraintForSolving(Pred, A, B);
   if (auto ImpliedCondition = TryWithConstraint(R))
     return ImpliedCondition;
+  if (auto ImpliedCondition = TryWithLinkedDecomposition(R))
+    return ImpliedCondition;
 
   // For non-negative operands unsigned queries can also be checked against the
   // signed system.
@@ -1856,9 +1907,12 @@ static std::optional<bool> checkCondition(CmpInst::Predicate Pred, Value *A,
     SmallVector<Value *> NewVariables;
     auto SR = Info.getConstraint(Pred, A, B, NewVariables,
                                  /*ForceSignedSystem=*/true);
-    if (NewVariables.empty())
+    if (NewVariables.empty()) {
       if (auto ImpliedCondition = TryWithConstraint(SR))
         return ImpliedCondition;
+      if (auto ImpliedCondition = TryWithLinkedDecomposition(SR))
+        return ImpliedCondition;
+    }
   }
   return std::nullopt;
 }
diff --git a/llvm/test/Transforms/ConstraintElimination/decompose-at-use.ll b/llvm/test/Transforms/ConstraintElimination/decompose-at-use.ll
index 6253d001acabe..b295ca415d90e 100644
--- a/llvm/test/Transforms/ConstraintElimination/decompose-at-use.ll
+++ b/llvm/test/Transforms/ConstraintElimination/decompose-at-use.ll
@@ -104,8 +104,7 @@ define i1 @eq_after_unsigned_sub_becomes_decomposable(i16 %a, i16 %y, i16 %z) {
 ; CHECK:       [[THEN]]:
 ; CHECK-NEXT:    [[PRECOND:%.*]] = icmp uge i16 [[Y]], [[Z]]
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[PRECOND]])
-; CHECK-NEXT:    [[EQ:%.*]] = icmp eq i16 [[A]], [[S]]
-; CHECK-NEXT:    ret i1 [[EQ]]
+; CHECK-NEXT:    ret i1 false
 ; CHECK:       [[EXIT]]:
 ; CHECK-NEXT:    ret i1 false
 ;

>From 06443e5708ad708b8e12866da55f419062562d65 Mon Sep 17 00:00:00 2001
From: Florian Hahn <flo at fhahn.com>
Date: Tue, 22 Sep 2026 11:15:09 +0100
Subject: [PATCH 3/3] !fixup move likely in comment

---
 llvm/lib/Transforms/Scalar/ConstraintElimination.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
index e630e241c7bd1..13511bbbc8da8 100644
--- a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
+++ b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
@@ -1802,9 +1802,9 @@ static void generateReproducer(Instruction *Cond, bool IsSigned, Module *M,
 }
 
 /// If \p V is a variable in the system and constraint \p C does not contain \p
-/// V, it is likely we managed to decompose \p V at this point, but not earlier
-/// when the fact involving \p V was added. In that case, return a new row for V
-/// == decompose(V) to link the variable with the decomposition result.
+/// V, we managed to decompose \p V at this point, but likely not earlier when
+/// the fact involving \p V was added. In that case, return a new row for
+/// V <= decompose(V) to link the variable with the decomposition result.
 static RowTy getDecompositionLinkRow(Value *V, const ConstraintTy &C,
                                      const ConstraintInfo &Info,
                                      const DataLayout &DL) {



More information about the llvm-commits mailing list