@@ -457,3 +457,63 @@ loop.i.latch:
457457exit:
458458 ret void
459459}
460+
461+ ; In the following case, the computation `offset = offset_i + j` will not wrap,
462+ ; but `offset_i += 1024` will wrap both in a signed sense and an unsigned
463+ ; sense. We cannot prove the monotonicity in this case.
464+ ;
465+ ; offset_i = (1ULL << 63) - 256;
466+ ; for (i = 0; i < (1ULL << 62); i++, offset_i += 1024)
467+ ; for (j = 0; j < 32; j++) {
468+ ; offset = offset_i + j;
469+ ;
470+ ; // The value of `offset` is positive in a signed sense.
471+ ; if (offset < (1ULL << 63))
472+ ; a[offset] = 0;
473+ ; }
474+ ;
475+ define void @outer_loop_may_wrap (ptr %a ) {
476+ ; CHECK-LABEL: 'outer_loop_may_wrap'
477+ ; CHECK-NEXT: Monotonicity check:
478+ ; CHECK-NEXT: Inst: store i8 0, ptr %gep, align 1
479+ ; CHECK-NEXT: Expr: {{\{\{}}9223372036854775552,+,1024}<%loop.i.header>,+,1}<nuw><nsw><%loop.j.header>
480+ ; CHECK-NEXT: Monotonicity: Unknown
481+ ; CHECK-NEXT: Reason: {9223372036854775552,+,1024}<%loop.i.header>
482+ ; CHECK-EMPTY:
483+ ; CHECK-NEXT: Src: store i8 0, ptr %gep, align 1 --> Dst: store i8 0, ptr %gep, align 1
484+ ; CHECK-NEXT: da analyze - confused!
485+ ;
486+ entry:
487+ br label %loop.i.header
488+
489+ loop.i.header:
490+ %i = phi i64 [ 0 , %entry ], [ %i.inc , %loop.i.latch ]
491+ %subscript.i = phi i64 [ 9223372036854775552 , %entry ], [ %subscript.i.next , %loop.i.latch ] ; The initial value is 2^63 - 256
492+ br label %loop.j.header
493+
494+ loop.j.header:
495+ %j = phi i64 [ 0 , %loop.i.header ], [ %j.inc , %loop.j.latch ]
496+ %subscript = phi i64 [ %subscript.i , %loop.i.header ], [ %subscript.next , %loop.j.latch ]
497+ %cond = icmp sge i64 %subscript , 0
498+ br i1 %cond , label %if.then , label %loop.j.latch
499+
500+ if.then:
501+ %gep = getelementptr inbounds i8 , ptr %a , i64 %subscript
502+ store i8 0 , ptr %gep
503+ br label %loop.j.latch
504+
505+ loop.j.latch:
506+ %j.inc = add nuw nsw i64 %j , 1
507+ %subscript.next = add nuw nsw i64 %subscript , 1
508+ %ec.j = icmp eq i64 %j.inc , 32
509+ br i1 %ec.j , label %loop.i.latch , label %loop.j.header
510+
511+ loop.i.latch:
512+ %i.inc = add nuw nsw i64 %i , 1
513+ %subscript.i.next = add i64 %subscript.i , 1024
514+ %ec.i = icmp eq i64 %i.inc , 4611686018427387904 ; 2^62
515+ br i1 %ec.i , label %exit , label %loop.i.header
516+
517+ exit:
518+ ret void
519+ }
0 commit comments