; 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[x] = 0;
define void @single_loop_invariant(ptr %a, i64 %x, i64 %n) {
; CHECK-LABEL: 'single_loop_invariant'
; CHECK-NEXT:  Monotonicity check:
; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:      Expr: %x
; CHECK-NEXT:      Monotonicity: Invariant
; CHECK-EMPTY:
; CHECK-NEXT:  Src: store i8 0, ptr %idx, align 1 --> Dst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:    da analyze - consistent output [S]!
;
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 %x
  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
}

; for (int i = 0; i < n; i++)
;   a[(i % 2 == 0 ? x : y)] = 0;
define void @single_loop_variant(ptr %a, i64 %x, i64 %y, i64 %n) {
; CHECK-LABEL: 'single_loop_variant'
; CHECK-NEXT:  Monotonicity check:
; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:      Expr: %offset
; CHECK-NEXT:      Monotonicity: Unknown
; CHECK-NEXT:      Reason: %offset
; 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 sgt i64 %n, 0
  br i1 %guard, label %loop, label %exit

loop:
  %i = phi i64 [ 0, %entry ], [ %i.inc, %loop ]
  %offset = phi i64 [ %x, %entry ], [ %offset.next, %loop ]
  %offset.next = phi i64 [ %y, %entry ], [ %offset, %loop ]
  %idx = getelementptr inbounds i8, ptr %a, i64 %offset
  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
}

; for (int i = 0; i < n; i++)
;   for (int j = 0; j < m; j++)
;     a[x + i] = 0;
define void @invariant_plus_monotonic0(ptr %a, i64 %x, i64 %n, i64 %m) {
; CHECK-LABEL: 'invariant_plus_monotonic0'
; CHECK-NEXT:  Monotonicity check:
; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:      Expr: {%x,+,1}<nsw><%loop.i.header>
; 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 - consistent output [0 S]!
;
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 ]
  %offset = phi i64 [ %x, %entry ], [ %offset.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 ]
  %idx = getelementptr inbounds i8, ptr %a, i64 %offset
  store i8 0, ptr %idx
  %j.inc = add nuw 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
  %offset.inc = add nsw i64 %offset, 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 = 0; i < n; i++)
;   for (int j = 0; j < m; j++)
;     a[x + j] = 0;
define void @invariant_plus_monotonic1(ptr %a, i64 %x, i64 %n, i64 %m) {
; CHECK-LABEL: 'invariant_plus_monotonic1'
; CHECK-NEXT:  Monotonicity check:
; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:      Expr: {%x,+,1}<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 - consistent output [S 0]!
;
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 = phi i64 [ %x, %loop.j.preheader ], [ %offset.inc, %loop.j ]
  %idx = getelementptr inbounds i8, ptr %a, i64 %offset
  store i8 0, ptr %idx
  %j.inc = add nuw nsw i64 %j, 1
  %offset.inc = add nsw i64 %offset, 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
}