[llvm] [DA] Add initial support for monotonicity check (PR #162280)
via llvm-commits
llvm-commits at lists.llvm.org
Thu Oct 9 11:57:28 PDT 2025
================
@@ -0,0 +1,459 @@
+; 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 (int i = 0; i < n; i++)
+; a[i] = 0;
+;
+define void @single_loop_nsw(ptr %a, i64 %n) {
+; CHECK-LABEL: 'single_loop_nsw'
+; CHECK-NEXT: Monotonicity check:
+; CHECK-NEXT: Inst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: Expr: {0,+,1}<nuw><nsw><%loop>
+; CHECK-NEXT: Monotonicity: MultiSignedMonotonic
+; 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!
+;
+entry:
+ %guard = icmp sgt i64 %n, 0
+ br i1 %guard, label %loop, label %exit
+
+loop:
+ %i = phi i64 [ 0, %entry ], [ %i.inc, %loop ]
+ %idx = getelementptr inbounds i8, ptr %a, i64 %i
+ store i8 0, ptr %idx
+ %i.inc = add nsw i64 %i, 1
+ %exitcond = icmp eq i64 %i.inc, %n
+ br i1 %exitcond, label %exit, label %loop
+
+exit:
+ ret void
+}
+
+; The purpose of the variable `begin` is to avoid violating the size limitation
+; of the allocated object in LLVM IR, which would cause UB.
+;
+; for (unsigned long long i = begin; i < end; i++)
+; a[i] = 0;
+;
+define void @single_loop_nuw(ptr %a, i64 %begin, i64 %end) {
+; CHECK-LABEL: 'single_loop_nuw'
+; CHECK-NEXT: Monotonicity check:
+; CHECK-NEXT: Inst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: Expr: {%begin,+,1}<nuw><%loop>
+; CHECK-NEXT: Monotonicity: Unknown
+; CHECK-NEXT: Reason: {%begin,+,1}<nuw><%loop>
+; CHECK-EMPTY:
+; CHECK-NEXT: Src: store i8 0, ptr %idx, align 1 --> Dst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: da analyze - confused!
+;
+entry:
+ %guard = icmp ult i64 %begin, %end
+ br i1 %guard, label %loop, label %exit
+
+loop:
+ %i = phi i64 [ %begin, %entry ], [ %i.inc, %loop ]
+ %idx = getelementptr i8, ptr %a, i64 %i
+ store i8 0, ptr %idx
+ %i.inc = add nuw i64 %i, 1
+ %exitcond = icmp eq i64 %i.inc, %end
+ br i1 %exitcond, label %exit, label %loop
+
+exit:
+ ret void
+}
+
+; for (int i = 0; i < n; i++)
+; for (int j = 0; j < m; j++)
+; a[i + j] = 0;
+;
+define void @nested_loop_nsw0(ptr %a, i64 %n, i64 %m) {
+; CHECK-LABEL: 'nested_loop_nsw0'
+; 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: MultiSignedMonotonic
+; CHECK-EMPTY:
+; CHECK-NEXT: Src: store i8 0, ptr %idx, align 1 --> Dst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: da analyze - output [* *]!
+;
+entry:
+ %guard.i = icmp sgt i64 %n, 0
+ br i1 %guard.i, label %loop.i.header, label %exit
+
+loop.i.header:
+ %i = phi i64 [ 0, %entry ], [ %i.inc, %loop.i.latch ]
+ br label %loop.j.preheader
+
+loop.j.preheader:
+ %gurard.j = icmp sgt i64 %m, 0
+ br i1 %gurard.j, label %loop.j, label %loop.i.latch
+
+loop.j:
+ %j = phi i64 [ 0, %loop.j.preheader ], [ %j.inc, %loop.j ]
+ %offset = add nsw i64 %i, %j
+ %idx = getelementptr inbounds i8, ptr %a, i64 %offset
+ store i8 0, ptr %idx
+ %j.inc = add nsw i64 %j, 1
+ %exitcond.j = icmp eq i64 %j.inc, %m
+ br i1 %exitcond.j, label %loop.i.latch, label %loop.j
+
+loop.i.latch:
+ %i.inc = add nsw i64 %i, 1
+ %exitcond.i = icmp eq i64 %i.inc, %n
+ br i1 %exitcond.i, label %exit, label %loop.i.header
+
+exit:
+ ret void
+}
+
+; for (int i = n - 1; i >= 0; i--)
+; for (int j = 0; j < m; j++)
+; a[i + j] = 0;
+;
+define void @nested_loop_nsw1(ptr %a, i64 %n, i64 %m) {
+; CHECK-LABEL: 'nested_loop_nsw1'
+; CHECK-NEXT: Monotonicity check:
+; CHECK-NEXT: Inst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: Expr: {{\{\{}}(-1 + %n),+,-1}<nsw><%loop.i.header>,+,1}<nsw><%loop.j>
+; CHECK-NEXT: Monotonicity: MultiSignedMonotonic
+; CHECK-EMPTY:
+; CHECK-NEXT: Src: store i8 0, ptr %idx, align 1 --> Dst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: da analyze - output [* *]!
+;
+entry:
+ %guard.i = icmp sgt i64 %n, 0
+ br i1 %guard.i, label %loop.i.header, label %exit
+
+loop.i.header:
+ %i = phi i64 [ %n, %entry ], [ %i.dec, %loop.i.latch ]
+ %i.dec = add nsw i64 %i, -1
+ br label %loop.j.preheader
+
+loop.j.preheader:
+ %gurard.j = icmp sgt i64 %m, 0
+ br i1 %gurard.j, label %loop.j, label %loop.i.latch
+
+loop.j:
+ %j = phi i64 [ 0, %loop.j.preheader ], [ %j.inc, %loop.j ]
+ %offset = add nsw i64 %i.dec, %j
+ %idx = getelementptr inbounds i8, ptr %a, i64 %offset
+ store i8 0, ptr %idx
+ %j.inc = add nsw i64 %j, 1
+ %exitcond.j = icmp eq i64 %j.inc, %m
+ br i1 %exitcond.j, label %loop.i.latch, label %loop.j
+
+loop.i.latch:
+ %exitcond.i = icmp eq i64 %i.dec, 0
+ br i1 %exitcond.i, label %exit, label %loop.i.header
+
+exit:
+ ret void
+}
+
+; for (int i = 0; i < n; i--)
+; for (int j = 0; j < m; j++)
+; a[i - j] = 0;
+;
+define void @nested_loop_nsw2(ptr %a, i64 %n, i64 %m) {
+; CHECK-LABEL: 'nested_loop_nsw2'
+; 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}<nsw><%loop.j>
+; CHECK-NEXT: Monotonicity: MultiSignedMonotonic
+; CHECK-EMPTY:
+; CHECK-NEXT: Src: store i8 0, ptr %idx, align 1 --> Dst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: da analyze - output [* *]!
+;
+entry:
+ %guard.i = icmp sgt i64 %n, 0
+ br i1 %guard.i, label %loop.i.header, label %exit
+
+loop.i.header:
+ %i = phi i64 [ 0, %entry ], [ %i.inc, %loop.i.latch ]
+ br label %loop.j.preheader
+
+loop.j.preheader:
+ %gurard.j = icmp sgt i64 %m, 0
+ br i1 %gurard.j, label %loop.j, label %loop.i.latch
+
+loop.j:
+ %j = phi i64 [ 0, %loop.j.preheader ], [ %j.inc, %loop.j ]
+ %offset = sub nsw i64 %i, %j
+ %idx = getelementptr inbounds i8, ptr %a, i64 %offset
+ store i8 0, ptr %idx
+ %j.inc = add nsw i64 %j, 1
+ %exitcond.j = icmp eq i64 %j.inc, %m
+ br i1 %exitcond.j, label %loop.i.latch, label %loop.j
+
+loop.i.latch:
+ %i.inc = add nsw i64 %i, 1
+ %exitcond.i = icmp eq i64 %i.inc, %n
+ br i1 %exitcond.i, label %exit, label %loop.i.header
+
+exit:
+ ret void
+}
+
+; for (int i = begin0; i < end0; i++)
+; for (int j = begin1; j < end1; j++) {
+; unsigned long long offset = (unsigned long long)i + (unsigned long long)j;
+; a[offset] = 0;
+; }
+;
+define void @nested_loop_nuw(ptr %a, i64 %begin0, i64 %end0, i64 %begin1, i64 %end1) {
+; CHECK-LABEL: 'nested_loop_nuw'
+; CHECK-NEXT: Monotonicity check:
+; CHECK-NEXT: Inst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: Expr: {{\{\{}}(%begin0 + %begin1),+,1}<nw><%loop.i.header>,+,1}<nw><%loop.j>
+; CHECK-NEXT: Monotonicity: Unknown
+; CHECK-NEXT: Reason: {{\{\{}}(%begin0 + %begin1),+,1}<nw><%loop.i.header>,+,1}<nw><%loop.j>
+; CHECK-EMPTY:
+; CHECK-NEXT: Src: store i8 0, ptr %idx, align 1 --> Dst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: da analyze - confused!
+;
+entry:
+ %guard.i.0 = icmp slt i64 0, %begin0
+ %guard.i.1 = icmp slt i64 %begin0, %end0
+ %guard.i.2 = icmp slt i64 0, %end0
+ %and.i.0 = and i1 %guard.i.0, %guard.i.1
+ %and.i.1 = and i1 %and.i.0, %guard.i.2
+ br i1 %and.i.1, label %loop.i.header, label %exit
+
+loop.i.header:
+ %i = phi i64 [ %begin0, %entry ], [ %i.inc, %loop.i.latch ]
+ br label %loop.j.preheader
+
+loop.j.preheader:
+ %guard.j.0 = icmp slt i64 0, %begin1
+ %guard.j.1 = icmp slt i64 %begin1, %end1
+ %guard.j.2 = icmp slt i64 0, %end1
+ %and.j.0 = and i1 %guard.j.0, %guard.j.1
+ %and.j.1 = and i1 %and.j.0, %guard.j.2
+ br i1 %and.j.1, label %loop.j, label %loop.i.latch
+
+loop.j:
+ %j = phi i64 [ %begin1, %loop.j.preheader ], [ %j.inc, %loop.j ]
+ %offset = add nuw i64 %i, %j
+ %idx = getelementptr i8, ptr %a, i64 %offset
+ store i8 0, ptr %idx
+ %j.inc = add nsw i64 %j, 1
+ %exitcond.j = icmp eq i64 %j.inc, %end1
+ br i1 %exitcond.j, label %loop.i.latch, label %loop.j
+
+loop.i.latch:
+ %i.inc = add nsw i64 %i, 1
+ %exitcond.i = icmp eq i64 %i.inc, %end0
+ br i1 %exitcond.i, label %exit, label %loop.i.header
+
+exit:
+ ret void
+}
+
+; for (int i = 0; i < n; i++)
+; for (int j = 0; j < m; j++)
+; a[i + step*j] = 0;
+;
+define void @nested_loop_step(ptr %a, i64 %n, i64 %m, i64 %step) {
+; CHECK-LABEL: 'nested_loop_step'
+; CHECK-NEXT: Monotonicity check:
+; CHECK-NEXT: Inst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: Expr: {{\{\{}}0,+,1}<nuw><nsw><%loop.i.header>,+,%step}<nsw><%loop.j>
+; CHECK-NEXT: Monotonicity: MultiSignedMonotonic
+; CHECK-EMPTY:
+; CHECK-NEXT: Src: store i8 0, ptr %idx, align 1 --> Dst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: da analyze - output [* *]!
+;
+entry:
+ %guard.i = icmp sgt i64 %n, 0
+ br i1 %guard.i, label %loop.i.header, label %exit
+
+loop.i.header:
+ %i = phi i64 [ 0, %entry ], [ %i.inc, %loop.i.latch ]
+ br label %loop.j.preheader
+
+loop.j.preheader:
+ %gurard.j = icmp sgt i64 %m, 0
+ br i1 %gurard.j, label %loop.j, label %loop.i.latch
+
+loop.j:
+ %j = phi i64 [ 0, %loop.j.preheader ], [ %j.inc, %loop.j ]
+ %offset.j = phi i64 [ 0, %loop.j.preheader ], [ %offset.j.next, %loop.j ]
+ %offset = add nsw i64 %i, %offset.j
+ %idx = getelementptr inbounds i8, ptr %a, i64 %offset
+ store i8 0, ptr %idx
+ %j.inc = add nsw i64 %j, 1
+ %offset.j.next = add nsw i64 %offset.j, %step
+ %exitcond.j = icmp eq i64 %j.inc, %m
+ br i1 %exitcond.j, label %loop.i.latch, label %loop.j
+
+loop.i.latch:
+ %i.inc = add nsw i64 %i, 1
+ %exitcond.i = icmp eq i64 %i.inc, %n
+ br i1 %exitcond.i, label %exit, label %loop.i.header
+
+exit:
+ ret void
+}
+
+; The value of step reccurence is not invariant with respect to the outer most
+; loop (the i-loop).
+;
+; offset_i = 0;
+; for (int i = 0; i < 100; i++) {
+; for (int j = 0; j < 100; j++)
+; a[offset_i + j] = 0;
+; offset_i += (i % 2 == 0) ? 0 : 3;
+; }
+;
+define void @step_is_variant(ptr %a) {
+; CHECK-LABEL: 'step_is_variant'
+; CHECK-NEXT: Monotonicity check:
+; CHECK-NEXT: Inst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: Expr: {%offset.i,+,1}<nuw><nsw><%loop.j>
+; CHECK-NEXT: Monotonicity: MultiSignedMonotonic
+; CHECK-EMPTY:
+; CHECK-NEXT: Src: store i8 0, ptr %idx, align 1 --> Dst: store i8 0, ptr %idx, align 1
+; CHECK-NEXT: da analyze - confused!
+;
+entry:
+ br label %loop.i.header
+
+loop.i.header:
+ %i = phi i64 [ 0, %entry ], [ %i.inc, %loop.i.latch ]
+ %offset.i = phi i64 [ 0, %entry ], [ %offset.i.next, %loop.i.latch ]
+ %step.i.0 = phi i64 [ 0, %entry ], [ %step.i.1, %loop.i.latch ]
+ %step.i.1 = phi i64 [ 3, %entry ], [ %step.i.0, %loop.i.latch ]
+ br label %loop.j
+
+loop.j:
+ %j = phi i64 [ 0, %loop.i.header ], [ %j.inc, %loop.j ]
+ %offset = add nsw i64 %offset.i, %j
+ %idx = getelementptr inbounds i8, ptr %a, i64 %offset
+ store i8 0, ptr %idx
+ %j.inc = add nsw i64 %j, 1
+ %exitcond.j = icmp eq i64 %j.inc, 100
+ br i1 %exitcond.j, label %loop.i.latch, label %loop.j
+
+loop.i.latch:
+ %i.inc = add nsw i64 %i, 1
+ %offset.i.next = add nsw i64 %offset.i, %step.i.0
+ %exitcond.i = icmp eq i64 %i.inc, 100
+ br i1 %exitcond.i, label %exit, label %loop.i.header
+
+exit:
+ ret void
+}
+
+; The AddRec doesn't have nsw flag for the j-loop, since the store may not be
+; executed.
+;
+; for (int i = 0; i < n; i++)
+; for (int j = 0; j < m; j++)
+; if (cond)
+; a[i + j] = 0;
+;
+define void @conditional_store0(ptr %a, i64 %n, i64 %m) {
----------------
amehsan wrote:
just looking at the pseudo C and your comment above: Something like this might be a test case for SCEV, but not for DA. In DA I believe you should just close your eyes and assume any nsw/nuw flag given to you is correct.
https://github.com/llvm/llvm-project/pull/162280
More information about the llvm-commits
mailing list