| ; 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: 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: |
| %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: 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 - 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: 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 - 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: 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 - 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: 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 - 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). It is theoretically multivariate monotonic by definition, |
| ; but we cannot handle non-affine addrec for now. |
| ; |
| ; 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: Unknown |
| ; CHECK-NEXT: Reason: %offset.i |
| ; 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 value of step reccurence is not invariant with respect to the outer most |
| ; loop (the i-loop). Actually, `offset_i` is not monotonic. |
| ; |
| ; 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) ? -1 : 3; |
| ; } |
| ; |
| define void @step_is_variant2(ptr %a) { |
| ; CHECK-LABEL: 'step_is_variant2' |
| ; CHECK-NEXT: Monotonicity check: |
| ; CHECK-NEXT: Inst: store i8 0, ptr %idx, align 1 |
| ; CHECK-NEXT: Expr: {%offset.i,+,1}<nsw><%loop.j> |
| ; CHECK-NEXT: Monotonicity: Unknown |
| ; CHECK-NEXT: Reason: %offset.i |
| ; 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 [ -1, %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) { |
| ; CHECK-LABEL: 'conditional_store0' |
| ; 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}<nw><%loop.j.header> |
| ; CHECK-NEXT: Monotonicity: Unknown |
| ; CHECK-NEXT: Reason: {{\{\{}}0,+,1}<nuw><nsw><%loop.i.header>,+,1}<nw><%loop.j.header> |
| ; 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 = 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.header, label %loop.i.latch |
| |
| loop.j.header: |
| %j = phi i64 [ 0, %loop.j.preheader ], [ %j.inc, %loop.j.latch ] |
| %offset = add nsw i64 %i, %j |
| %cond = freeze i1 poison |
| br i1 %cond, label %if.then, label %loop.j.latch |
| |
| if.then: |
| %idx = getelementptr inbounds i8, ptr %a, i64 %offset |
| store i8 0, ptr %idx |
| br label %loop.j.latch |
| |
| loop.j.latch: |
| %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.header |
| |
| 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 |
| } |
| |
| ; Similar to the @conditional_store0, but the definition of the `%offset` is |
| ; different from it and we can infer `nsw` in this case. |
| ; |
| ; for (int i = 0; i < n; i++) |
| ; for (int j = 0; j < m; j++) |
| ; if (cond) |
| ; a[i + j] = 0; |
| ; |
| define void @conditional_store1(ptr %a, i64 %n, i64 %m) { |
| ; CHECK-LABEL: 'conditional_store1' |
| ; 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.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 - 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.header, label %loop.i.latch |
| |
| loop.j.header: |
| %j = phi i64 [ 0, %loop.j.preheader ], [ %j.inc, %loop.j.latch ] |
| %offset = phi i64 [ %i, %loop.j.preheader ], [ %offset.next, %loop.j.latch ] |
| %cond = freeze i1 poison |
| br i1 %cond, label %if.then, label %loop.j.latch |
| |
| if.then: |
| %idx = getelementptr inbounds i8, ptr %a, i64 %offset |
| store i8 0, ptr %idx |
| br label %loop.j.latch |
| |
| loop.j.latch: |
| %j.inc = add nsw i64 %j, 1 |
| %offset.next = add nsw i64 %offset, 1 |
| %exitcond.j = icmp eq i64 %j.inc, %m |
| br i1 %exitcond.j, label %loop.i.latch, label %loop.j.header |
| |
| 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 |
| } |
| |
| ; In the following case, the computation `offset = offset_i + j` will not wrap, |
| ; but `offset_i += 1024` will wrap both in a signed sense and an unsigned |
| ; sense. We cannot prove the monotonicity in this case. |
| ; |
| ; offset_i = (1ULL << 63) - 256; |
| ; for (i = 0; i < (1ULL << 62); i++, offset_i += 1024) |
| ; for (j = 0; j < 32; j++) { |
| ; offset = offset_i + j; |
| ; |
| ; // The value of `offset` is positive in a signed sense. |
| ; if (offset < (1ULL << 63)) |
| ; a[offset] = 0; |
| ; } |
| ; |
| define void @outer_loop_may_wrap(ptr %a) { |
| ; CHECK-LABEL: 'outer_loop_may_wrap' |
| ; CHECK-NEXT: Monotonicity check: |
| ; CHECK-NEXT: Inst: store i8 0, ptr %gep, align 1 |
| ; CHECK-NEXT: Expr: {{\{\{}}9223372036854775552,+,1024}<%loop.i.header>,+,1}<nuw><nsw><%loop.j.header> |
| ; CHECK-NEXT: Monotonicity: Unknown |
| ; CHECK-NEXT: Reason: {9223372036854775552,+,1024}<%loop.i.header> |
| ; CHECK-EMPTY: |
| ; CHECK-NEXT: Src: store i8 0, ptr %gep, align 1 --> Dst: store i8 0, ptr %gep, 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 ] |
| %subscript.i = phi i64 [ 9223372036854775552, %entry ], [ %subscript.i.next, %loop.i.latch ] ; The initial value is 2^63 - 256 |
| br label %loop.j.header |
| |
| loop.j.header: |
| %j = phi i64 [ 0, %loop.i.header ], [ %j.inc, %loop.j.latch ] |
| %subscript = phi i64 [ %subscript.i, %loop.i.header ], [ %subscript.next, %loop.j.latch ] |
| %cond = icmp sge i64 %subscript, 0 |
| br i1 %cond, label %if.then, label %loop.j.latch |
| |
| if.then: |
| %gep = getelementptr inbounds i8, ptr %a, i64 %subscript |
| store i8 0, ptr %gep |
| br label %loop.j.latch |
| |
| loop.j.latch: |
| %j.inc = add nuw nsw i64 %j, 1 |
| %subscript.next = add nuw nsw i64 %subscript, 1 |
| %ec.j = icmp eq i64 %j.inc, 32 |
| br i1 %ec.j, label %loop.i.latch, label %loop.j.header |
| |
| loop.i.latch: |
| %i.inc = add nuw nsw i64 %i, 1 |
| %subscript.i.next = add i64 %subscript.i, 1024 |
| %ec.i = icmp eq i64 %i.inc, 4611686018427387904 ; 2^62 |
| br i1 %ec.i, label %exit, label %loop.i.header |
| |
| exit: |
| ret void |
| } |