[llvm] [DA] Add tests for nsw doesn't hold on entier iteration (PR #162281)

Ehsan Amiri via llvm-commits llvm-commits at lists.llvm.org
Wed Nov 19 06:38:30 PST 2025


================
@@ -0,0 +1,141 @@
+; NOTE: Assertions have been autogenerated by utils/update_analyze_test_checks.py UTC_ARGS: --version 6
+; RUN: opt < %s -disable-output -passes="print<da>" -da-dump-monotonicity-report \
+; RUN:     -da-enable-monotonicity-check 2>&1 | FileCheck %s
+
+; for (i = 0; i < INT64_MAX - 1; i++)
+;   if (i < 1000)
+;     for (j = 0; j < 2000; j++)
+;       a[i + j] = 0;
+;
+; FIXME: This is not monotonic. The nsw flag is valid under
+; the condition i < 1000, not for all i.
+define void @nsw_under_loop_guard0(ptr %a) {
+; CHECK-LABEL: 'nsw_under_loop_guard0'
+; CHECK-NEXT:  Monotonicity check:
+; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT:      Expr: {{\{\{}}0,+,1}<nuw><nsw><%loop.i.header>,+,1}<nuw><nsw><%loop.j>
+; CHECK-NEXT:      Monotonicity: MultivariateSignedMonotonic
+; CHECK-EMPTY:
+; CHECK-NEXT:  Src: store i8 0, ptr %idx, align 1 --> Dst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT:    da analyze - none!
----------------
amehsan wrote:

> each dependence test assumes monotonicity over the entire iteration space

This is not correct. I will start posting proofs of correctness without any assumption about "monotonicity over the entire iteration space" in an issue.

https://github.com/llvm/llvm-project/pull/162281


More information about the llvm-commits mailing list