[ConstraintElim] Drop invalid rows instead of failing the elimination

[dtcxzyw]

This patch tries to drop invalid rows when overflow occurs instead of failing the elimination immediately.
Fixes the regression in velox/buffer/Buffer.h, which was introduced by #76262.

See also dtcxzyw/llvm-opt-benchmark#35 (comment).

[llvmbot]

@llvm/pr-subscribers-llvm-transforms

@llvm/pr-subscribers-llvm-analysis

Author: Yingwei Zheng (dtcxzyw)

Changes

This patch tries to drop invalid rows when overflow occurs instead of failing the elimination immediately.
Fixes the regression in velox/buffer/Buffer.h, which was introduced by #76262.

See also dtcxzyw/llvm-opt-benchmark#35 (comment).

---

Full diff: https://github.com/llvm/llvm-project/pull/76299.diff

2 Files Affected:

• (modified) llvm/lib/Analysis/ConstraintSystem.cpp (+18-9)
• (added) llvm/test/Transforms/ConstraintElimination/constraint-overflow.ll (+42)

diff --git a/llvm/lib/Analysis/ConstraintSystem.cpp b/llvm/lib/Analysis/ConstraintSystem.cpp
index 8a802515b6f4fb..43bd5e5b0ccbdc 100644
--- a/llvm/lib/Analysis/ConstraintSystem.cpp
+++ b/llvm/lib/Analysis/ConstraintSystem.cpp
@@ -73,6 +73,8 @@ bool ConstraintSystem::eliminateUsingFM() {
       }
 
       SmallVector<Entry, 8> NR;
+      bool Valid = true;
+      uint32_t NextGCD = NewGCD;
       unsigned IdxUpper = 0;
       unsigned IdxLower = 0;
       auto &LowerRow = RemainingRows[LowerR];
@@ -96,27 +98,34 @@ bool ConstraintSystem::eliminateUsingFM() {
           IdxUpper++;
         }
 
-        if (MulOverflow(UpperV, ((-1) * LowerLast / GCD), M1))
-          return false;
+        if (MulOverflow(UpperV, ((-1) * LowerLast / GCD), M1)) {
+          Valid = false;
+          break;
+        }
         if (IdxLower < LowerRow.size() && LowerRow[IdxLower].Id == CurrentId) {
           LowerV = LowerRow[IdxLower].Coefficient;
           IdxLower++;
         }
 
-        if (MulOverflow(LowerV, (UpperLast / GCD), M2))
-          return false;
-        if (AddOverflow(M1, M2, N))
-          return false;
+        if (MulOverflow(LowerV, (UpperLast / GCD), M2)) {
+          Valid = false;
+          break;
+        }
+        if (AddOverflow(M1, M2, N)) {
+          Valid = false;
+          break;
+        }
         if (N == 0)
           continue;
         NR.emplace_back(N, CurrentId);
 
-        NewGCD =
-            APIntOps::GreatestCommonDivisor({32, (uint32_t)N}, {32, NewGCD})
+        NextGCD =
+            APIntOps::GreatestCommonDivisor({32, (uint32_t)N}, {32, NextGCD})
                 .getZExtValue();
       }
-      if (NR.empty())
+      if (!Valid || NR.empty())
         continue;
+      NewGCD = NextGCD;
       Constraints.push_back(std::move(NR));
       // Give up if the new system gets too big.
       if (Constraints.size() > 500)
diff --git a/llvm/test/Transforms/ConstraintElimination/constraint-overflow.ll b/llvm/test/Transforms/ConstraintElimination/constraint-overflow.ll
new file mode 100644
index 00000000000000..6200f3adf0088d
--- /dev/null
+++ b/llvm/test/Transforms/ConstraintElimination/constraint-overflow.ll
@@ -0,0 +1,42 @@
+; NOTE: Assertions have been autogenerated by utils/update_test_checks.py UTC_ARGS: --version 4
+; RUN: opt -passes=constraint-elimination -S %s | FileCheck %s
+
+define void @f(i64 %a3, i64 %numElements) {
+; CHECK-LABEL: define void @f(
+; CHECK-SAME: i64 [[A3:%.*]], i64 [[NUMELEMENTS:%.*]]) {
+; CHECK-NEXT:  entry:
+; CHECK-NEXT:    [[COND:%.*]] = icmp ule i64 [[NUMELEMENTS]], 1152921504606846975
+; CHECK-NEXT:    call void @llvm.assume(i1 [[COND]])
+; CHECK-NEXT:    [[A1:%.*]] = shl nuw i64 [[NUMELEMENTS]], 4
+; CHECK-NEXT:    br label [[IF_END:%.*]]
+; CHECK:       if.end:
+; CHECK-NEXT:    [[CMP:%.*]] = icmp ugt i64 [[A1]], [[A3]]
+; CHECK-NEXT:    br i1 [[CMP]], label [[IF_END_I:%.*]], label [[ABORT:%.*]]
+; CHECK:       if.end.i:
+; CHECK-NEXT:    br i1 false, label [[ABORT]], label [[EXIT:%.*]]
+; CHECK:       abort:
+; CHECK-NEXT:    tail call void @llvm.trap()
+; CHECK-NEXT:    unreachable
+; CHECK:       exit:
+; CHECK-NEXT:    ret void
+;
+entry:
+  %cond = icmp ule i64 %numElements, 1152921504606846975
+  call void @llvm.assume(i1 %cond)
+  %a1 = shl nuw i64 %numElements, 4
+  br label %if.end
+if.end:
+  %cmp = icmp ugt i64 %a1, %a3
+  br i1 %cmp, label %if.end.i, label %abort
+if.end.i:
+  %cmp2.not.i = icmp ult i64 %a1, %a3
+  br i1 %cmp2.not.i, label %abort, label %exit
+abort:
+  tail call void @llvm.trap()
+  unreachable
+exit:
+  ret void
+}
+
+declare void @llvm.trap()
+declare void @llvm.assume(i1)

[fhahn]

Interesting find!

See also dtcxzyw/llvm-opt-benchmark#35 (comment).

I am curious how you use this to spot regressions and if there's anything to automate?

The tests have been split out to a separate commit, but will get squashed on merge. Could you do a separate PR for the tests? Or commit them directly with the suggested adjustment?

[dtcxzyw]

I am curious how you use this to spot regressions

I find these regressions by reviewing the IR diffs of real-world applications, which are generated by different version of opt. TBH it is a time-consuming job :( But I think this new system is better than my old CI because the old system creates a bunch of false positive regression reports.

and if there's anything to automate?

The system will build the trunk version of LLVM and run the benchmark every hour.

BTW, this regression was also detected by the pre-commit test dtcxzyw/llvm-opt-benchmark#30 (comment).
If you would like to test your patch before merging it, feel free to ping me and I will create a pull request in llvm-opt-benchmark :)

[dtcxzyw]

The tests have been split out to a separate commit, but will get squashed on merge. Could you do a separate PR for the tests? Or commit them directly with the suggested adjustment?

Done. #76512

[dtcxzyw]

Another question: Does (-1) * LowerLast never overflow?

[dtcxzyw]

Ping.

[fhahn]

I think it might be possible to construct a case where it overflows. Ideally we would construct such a case, add a test and check for overflow.

[nikic]

Why is it valid to simply drop these rows? Doesn't this mean we lose constraints?

[dtcxzyw]

Why is it valid to simply drop these rows? Doesn't this mean we lose constraints?

sat means that the constraint system may have a solution. Returning sat for an inconsistent system is allowed. So it is safe to drop constraints.

[nikic]

Why is it valid to simply drop these rows? Doesn't this mean we lose constraints?

sat means that the constraint system may have a solution. Returning sat for an inconsistent system is allowed. So it is safe to drop constraints.

I see. I think this should be spelled out in the eliminateUsingFM() documentation. If I understand correctly, the current implementation does preserve satisfiability during elimination (in the sense of "iff") -- but it's a stronger property than we need, so we can relax it, as this patch does. Or is it already possible for the current eliminateUsingFM() implementation to turn an unsat system into a sat one?

[fhahn]

Intuitively this makes sense, as dropping information/rows should only ever turn an unsatisfiable system into a satisfiable system, but not the other way around.

I'd still like to manually check the steps, as we may drop rows we created to eliminate a variable.

[dtcxzyw]

Ping.

[dtcxzyw]

Ping.

[dtcxzyw]

Ping.