; 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

; int8_t offset = start;
; for (int i = 0; i < 100; i++, offset += step)
;   a[sext(offset)] = 0;
;
define void @sext_nsw(ptr %a, i8 %start, i8 %step) {
; CHECK-LABEL: 'sext_nsw'
; CHECK-NEXT:  Monotonicity check:
; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:      Expr: {(sext i8 %start to i64),+,(sext i8 %step to i64)}<nsw><%loop>
; 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!
;
entry:
  br label %loop

loop:
  %i = phi i64 [ 0, %entry ], [ %i.inc, %loop ]
  %offset = phi i8 [ %start, %entry ], [ %offset.next, %loop ]
  %offset.sext = sext i8 %offset to i64
  %idx = getelementptr i8, ptr %a, i64 %offset.sext
  store i8 0, ptr %idx
  %i.inc = add nsw i64 %i, 1
  %offset.next = add nsw i8 %offset, %step
  %exitcond = icmp eq i64 %i.inc, 100
  br i1 %exitcond, label %exit, label %loop

exit:
  ret void
}

; The addition for `%offset.next` can wrap, so we cannot prove monotonicity.
;
; int8_t offset = start;
; for (int i = 0; i < 100; i++, offset += step)
;   a[sext(offset)] = 0;
;
define void @sext_may_wrap(ptr %a, i8 %start, i8 %step) {
; CHECK-LABEL: 'sext_may_wrap'
; CHECK-NEXT:  Monotonicity check:
; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:      Expr: (sext i8 {%start,+,%step}<%loop> to i64)
; CHECK-NEXT:      Monotonicity: Unknown
; CHECK-NEXT:      Reason: (sext i8 {%start,+,%step}<%loop> to i64)
; 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

loop:
  %i = phi i64 [ 0, %entry ], [ %i.inc, %loop ]
  %offset = phi i8 [ %start, %entry ], [ %offset.next, %loop ]
  %offset.sext = sext i8 %offset to i64
  %idx = getelementptr i8, ptr %a, i64 %offset.sext
  store i8 0, ptr %idx
  %i.inc = add nsw i64 %i, 1
  %offset.next = add i8 %offset, %step
  %exitcond = icmp eq i64 %i.inc, 100
  br i1 %exitcond, label %exit, label %loop

exit:
  ret void
}

; for (int8_t i = 0; i < 100; i++)
;   a[zext(offset)] = 0;
;
define void @zext_pos(ptr %a) {
; CHECK-LABEL: 'zext_pos'
; 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: 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!
;
entry:
  br label %loop

loop:
  %i = phi i8 [ 0, %entry ], [ %i.inc, %loop ]
  %offset.zext = zext nneg i8 %i to i64
  %idx = getelementptr i8, ptr %a, i64 %offset.zext
  store i8 0, ptr %idx
  %i.inc = add nsw i8 %i, 1
  %exitcond = icmp eq i8 %i.inc, 100
  br i1 %exitcond, label %exit, label %loop

exit:
  ret void
}

; The zero-extened value of `offset` is no longer monotonic. In fact, the
; values of `offset` in each iteration are:
;
;    iteration |   0 | 1 | 2 | ...
; -------------|-----|---|---|---------
;       offset |  -1 | 0 | 1 | ...
; zext(offset) | 255 | 0 | 1 | ...
;
;
; for (int8_t i = -1; i < 100; i++)
;   a[zext(offset)] = 0;
;
define void @zext_cross_zero(ptr %a) {
; CHECK-LABEL: 'zext_cross_zero'
; CHECK-NEXT:  Monotonicity check:
; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:      Expr: (zext i8 {-1,+,1}<nsw><%loop> to i64)
; CHECK-NEXT:      Monotonicity: Unknown
; CHECK-NEXT:      Reason: (zext i8 {-1,+,1}<nsw><%loop> to i64)
; 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

loop:
  %i = phi i8 [ -1, %entry ], [ %i.inc, %loop ]
  %offset.zext = zext nneg i8 %i to i64
  %idx = getelementptr i8, ptr %a, i64 %offset.zext
  store i8 0, ptr %idx
  %i.inc = add nsw i8 %i, 1
  %exitcond = icmp eq i8 %i.inc, 100
  br i1 %exitcond, label %exit, label %loop

exit:
  ret void
}

; In principle, we can prove that `zext(offset)` is monotonic since we know
; that `offset` is non-negative.
;
; int8_t offset = 0;
; for (int i = 0; i < 100; i++, offset += step)
;   a[zext(offset)] = 0;
;
define void @zext_nneg_nsw(ptr %a, i8 %step) {
; CHECK-LABEL: 'zext_nneg_nsw'
; CHECK-NEXT:  Monotonicity check:
; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:      Expr: (zext i8 {0,+,%step}<nsw><%loop> to i64)
; CHECK-NEXT:      Monotonicity: Unknown
; CHECK-NEXT:      Reason: (zext i8 {0,+,%step}<nsw><%loop> to i64)
; 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

loop:
  %i = phi i64 [ 0, %entry ], [ %i.inc, %loop ]
  %offset = phi i8 [ 0, %entry ], [ %offset.next, %loop ]
  %offset.zext = zext nneg i8 %offset to i64
  %idx = getelementptr i8, ptr %a, i64 %offset.zext
  store i8 0, ptr %idx
  %i.inc = add nsw i64 %i, 1
  %offset.next = add nsw i8 %offset, %step
  %exitcond = icmp eq i64 %i.inc, 100
  br i1 %exitcond, label %exit, label %loop

exit:
  ret void
}

; SCEV handles `i & 1` as an i1 addrec. Ensure that the monotonicity analysis
; properly analyzes it.
;
; for (i = 0; i < 100; i++)
;  a[i & 1] = 0;
;
define void @offset_truncated_to_i1(ptr %a) {
; CHECK-LABEL: 'offset_truncated_to_i1'
; CHECK-NEXT:  Monotonicity check:
; CHECK-NEXT:    Inst: store i8 0, ptr %idx, align 1
; CHECK-NEXT:      Expr: (zext i1 {false,+,true}<%loop> to i64)
; CHECK-NEXT:      Monotonicity: Unknown
; CHECK-NEXT:      Reason: (zext i1 {false,+,true}<%loop> to i64)
; 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

loop:
  %i = phi i64 [ 0, %entry ], [ %i.inc, %loop ]
  %and = and i64 %i, 1
  %idx = getelementptr inbounds i8, ptr %a, i64 %and
  store i8 0, ptr %idx
  %i.inc = add nsw i64 %i, 1
  %exitcond = icmp eq i64 %i.inc, 100
  br i1 %exitcond, label %exit, label %loop

exit:
  ret void
}