Test Failure: Transforms/LoopUnroll/runtime-loop-multiexit-dom-verify.ll

Test source: git

Log:

Source: <stdin>

----------------------------------------
define i64 @test1() {
%entry:
  br label %preheader

%preheader:
  %trip = zext i32 undef to i64
  br label %header

%header:
  %iv = phi i64 [ 2, %preheader ], [ %add.iv, %latch ]
  %add.iv = add nsw nuw i64 %iv, 2
  %cmp1 = icmp ult i64 %add.iv, %trip
  br i1 %cmp1, label %latch, label %headerexit

%latch:
  %shft = ashr i64 %add.iv, 1
  %cmp2 = icmp ult i64 %shft, %trip
  br i1 %cmp2, label %header, label %latchexit

%latchexit:
  %shftphi = phi i64 [ %shft, %latch ]
  br label %mergedexit

%headerexit:
  %addphi = phi i64 [ %add.iv, %header ]
  br label %mergedexit

%mergedexit:
  %retval = phi i64 [ %addphi, %headerexit ], [ %shftphi, %latchexit ]
  ret i64 %retval
}
=>
define i64 @test1() {
%entry:
  br label %preheader

%preheader:
  %trip = zext i32 undef to i64
  br label %header

%header:
  %iv = phi i64 [ 2, %preheader ], [ %add.iv.3, %latch.3 ]
  %add.iv = add nsw nuw i64 %iv, 2
  %cmp1 = icmp ult i64 %add.iv, %trip
  br i1 %cmp1, label %latch, label %headerexit

%latch:
  %shft = ashr i64 %add.iv, 1
  %cmp2 = icmp ult i64 %shft, %trip
  br i1 %cmp2, label %header.1, label %latchexit

%header.1:
  %add.iv.1 = add nsw nuw i64 %add.iv, 2
  %cmp1.1 = icmp ult i64 %add.iv.1, %trip
  br i1 %cmp1.1, label %latch.1, label %headerexit

%latch.1:
  %shft.1 = ashr i64 %add.iv.1, 1
  %cmp2.1 = icmp ult i64 %shft.1, %trip
  br i1 %cmp2.1, label %header.2, label %latchexit

%header.2:
  %add.iv.2 = add nsw nuw i64 %add.iv.1, 2
  %cmp1.2 = icmp ult i64 %add.iv.2, %trip
  br i1 %cmp1.2, label %latch.2, label %headerexit

%latch.2:
  %shft.2 = ashr i64 %add.iv.2, 1
  %cmp2.2 = icmp ult i64 %shft.2, %trip
  br i1 %cmp2.2, label %header.3, label %latchexit

%header.3:
  %add.iv.3 = add nsw nuw i64 %add.iv.2, 2
  %cmp1.3 = icmp ult i64 %add.iv.3, %trip
  br i1 %cmp1.3, label %latch.3, label %headerexit

%latch.3:
  %shft.3 = ashr i64 %add.iv.3, 1
  %cmp2.3 = icmp ult i64 %shft.3, %trip
  br i1 %cmp2.3, label %header, label %latchexit

%latchexit:
  %shftphi = phi i64 [ %shft, %latch ], [ %shft.1, %latch.1 ], [ %shft.2, %latch.2 ], [ %shft.3, %latch.3 ]
  br label %mergedexit

%headerexit:
  %addphi = phi i64 [ %add.iv, %header ], [ %add.iv.1, %header.1 ], [ %add.iv.2, %header.2 ], [ %add.iv.3, %header.3 ]
  br label %mergedexit

%mergedexit:
  %retval = phi i64 [ %addphi, %headerexit ], [ %shftphi, %latchexit ]
  ret i64 %retval
}
Transformation seems to be correct!


----------------------------------------
define void @test2(i1 %cond, i32 %n) {
%entry:
  br i1 %cond, label %preheader, label %mergedexit

%preheader:
  %trip = zext i32 %n to i64
  br label %header

%header:
  %iv = phi i64 [ 2, %preheader ], [ %add.iv, %latch ]
  %add.iv = add nsw nuw i64 %iv, 2
  %cmp1 = icmp ult i64 %add.iv, %trip
  br i1 %cmp1, label %latch, label %headerexit

%latch:
  %shft = ashr i64 %add.iv, 1
  %cmp2 = icmp ult i64 %shft, %trip
  br i1 %cmp2, label %header, label %latchexit

%latchexit:
  br label %mergedexit

%headerexit:
  br label %mergedexit

%mergedexit:
  ret void
}
=>
define void @test2(i1 %cond, i32 %n) {
%entry:
  br i1 %cond, label %preheader, label %mergedexit

%preheader:
  %trip = zext i32 %n to i64
  br label %header

%header:
  %iv = phi i64 [ 2, %preheader ], [ %add.iv.3, %latch.3 ]
  %add.iv = add nsw nuw i64 %iv, 2
  %cmp1 = icmp ult i64 %add.iv, %trip
  br i1 %cmp1, label %latch, label %headerexit

%latch:
  %shft = ashr i64 %add.iv, 1
  %cmp2 = icmp ult i64 %shft, %trip
  br i1 %cmp2, label %header.1, label %latchexit

%header.1:
  %add.iv.1 = add nsw nuw i64 %add.iv, 2
  %cmp1.1 = icmp ult i64 %add.iv.1, %trip
  br i1 %cmp1.1, label %latch.1, label %headerexit

%latch.1:
  %shft.1 = ashr i64 %add.iv.1, 1
  %cmp2.1 = icmp ult i64 %shft.1, %trip
  br i1 %cmp2.1, label %header.2, label %latchexit

%header.2:
  %add.iv.2 = add nsw nuw i64 %add.iv.1, 2
  %cmp1.2 = icmp ult i64 %add.iv.2, %trip
  br i1 %cmp1.2, label %latch.2, label %headerexit

%latch.2:
  %shft.2 = ashr i64 %add.iv.2, 1
  %cmp2.2 = icmp ult i64 %shft.2, %trip
  br i1 %cmp2.2, label %header.3, label %latchexit

%header.3:
  %add.iv.3 = add nsw nuw i64 %add.iv.2, 2
  %cmp1.3 = icmp ult i64 %add.iv.3, %trip
  br i1 %cmp1.3, label %latch.3, label %headerexit

%latch.3:
  %shft.3 = ashr i64 %add.iv.3, 1
  %cmp2.3 = icmp ult i64 %shft.3, %trip
  br i1 %cmp2.3, label %header, label %latchexit

%latchexit:
  br label %mergedexit

%headerexit:
  br label %mergedexit

%mergedexit:
  ret void
}
Transformation seems to be correct!


----------------------------------------
define i64 @test3(i32 %n) {
%entry:
  br label %preheader

%preheader:
  %trip = zext i32 %n to i64
  br label %header

%header:
  %iv = phi i64 [ 2, %preheader ], [ %add.iv, %latch ]
  %add.iv = add nsw nuw i64 %iv, 2
  %cmp1 = icmp ult i64 %add.iv, %trip
  br i1 %cmp1, label %latch, label %headerexit

%latch:
  %shft = ashr i64 %add.iv, 1
  %cmp2 = icmp ult i64 %shft, %trip
  br i1 %cmp2, label %header, label %latchexit

%latchexit:
  %shftphi = phi i64 [ %shft, %latch ]
  ret i64 %shftphi

%headerexit:
  br label %exitsucc

%exitsucc:
  ret i64 96
}
=>
define i64 @test3(i32 %n) {
%entry:
  br label %preheader

%preheader:
  %trip = zext i32 %n to i64
  br label %header

%header:
  %iv = phi i64 [ 2, %preheader ], [ %add.iv.3, %latch.3 ]
  %add.iv = add nsw nuw i64 %iv, 2
  %cmp1 = icmp ult i64 %add.iv, %trip
  br i1 %cmp1, label %latch, label %headerexit

%latch:
  %shft = ashr i64 %add.iv, 1
  %cmp2 = icmp ult i64 %shft, %trip
  br i1 %cmp2, label %header.1, label %latchexit

%header.1:
  %add.iv.1 = add nsw nuw i64 %add.iv, 2
  %cmp1.1 = icmp ult i64 %add.iv.1, %trip
  br i1 %cmp1.1, label %latch.1, label %headerexit

%latch.1:
  %shft.1 = ashr i64 %add.iv.1, 1
  %cmp2.1 = icmp ult i64 %shft.1, %trip
  br i1 %cmp2.1, label %header.2, label %latchexit

%header.2:
  %add.iv.2 = add nsw nuw i64 %add.iv.1, 2
  %cmp1.2 = icmp ult i64 %add.iv.2, %trip
  br i1 %cmp1.2, label %latch.2, label %headerexit

%latch.2:
  %shft.2 = ashr i64 %add.iv.2, 1
  %cmp2.2 = icmp ult i64 %shft.2, %trip
  br i1 %cmp2.2, label %header.3, label %latchexit

%header.3:
  %add.iv.3 = add nsw nuw i64 %add.iv.2, 2
  %cmp1.3 = icmp ult i64 %add.iv.3, %trip
  br i1 %cmp1.3, label %latch.3, label %headerexit

%latch.3:
  %shft.3 = ashr i64 %add.iv.3, 1
  %cmp2.3 = icmp ult i64 %shft.3, %trip
  br i1 %cmp2.3, label %header, label %latchexit

%latchexit:
  %shftphi = phi i64 [ %shft, %latch ], [ %shft.1, %latch.1 ], [ %shft.2, %latch.2 ], [ %shft.3, %latch.3 ]
  ret i64 %shftphi

%headerexit:
  br label %exitsucc

%exitsucc:
  ret i64 96
}
Transformation seems to be correct!


----------------------------------------
define void @test4(i16 %c3) {
%preheader:
  %c1 = zext i32 undef to i64
  br label %header

%header:
  %indvars.iv = phi i64 [ 0, %preheader ], [ %indvars.iv.next, %latch ]
  br label %exiting

%exiting:
  switch i16 %c3, label %default [
    i16 45, label %otherexit
    i16 95, label %latch
  ]

%otherexit:
  br label %default

%default:
  ret void

%latch:
  %indvars.iv.next = add nsw nuw i64 %indvars.iv, 1
  %c2 = icmp ult i64 %indvars.iv.next, %c1
  br i1 %c2, label %header, label %latchexit

%latchexit:
  ret void
}
=>
define void @test4(i16 %c3) {
%preheader:
  %c1 = zext i32 undef to i64
  %umax = umax i64 %c1, 1
  %0 = add nsw i64 %umax, -1
  %xtraiter = and i64 %umax, 3
  %lcmp.mod = icmp ne i64 %xtraiter, 0
  br i1 %lcmp.mod, label %header.prol.preheader, label %header.prol.loopexit

%header.prol.preheader:
  br label %header.prol

%header.prol:
  %indvars.iv.prol = phi i64 [ 0, %header.prol.preheader ], [ %indvars.iv.next.prol, %latch.prol ]
  %prol.iter = phi i64 [ 0, %header.prol.preheader ], [ %prol.iter.next, %latch.prol ]
  br label %exiting.prol

%exiting.prol:
  switch i16 %c3, label %default.loopexit.loopexit1 [
    i16 45, label %otherexit.loopexit2
    i16 95, label %latch.prol
  ]

%default.loopexit.loopexit1:
  br label %default.loopexit

%otherexit.loopexit2:
  br label %otherexit

%latch.prol:
  %indvars.iv.next.prol = add nsw nuw i64 %indvars.iv.prol, 1
  %c2.prol = icmp ult i64 %indvars.iv.next.prol, %c1
  %prol.iter.next = add i64 %prol.iter, 1
  %prol.iter.cmp = icmp ne i64 %prol.iter.next, %xtraiter
  br i1 %prol.iter.cmp, label %header.prol, label %header.prol.loopexit.unr-lcssa

%header.prol.loopexit.unr-lcssa:
  %indvars.iv.unr.ph = phi i64 [ %indvars.iv.next.prol, %latch.prol ]
  br label %header.prol.loopexit

%header.prol.loopexit:
  %indvars.iv.unr = phi i64 [ 0, %preheader ], [ %indvars.iv.unr.ph, %header.prol.loopexit.unr-lcssa ]
  %1 = icmp ult i64 %0, 3
  br i1 %1, label %latchexit, label %preheader.new

%preheader.new:
  br label %header

%header:
  %indvars.iv = phi i64 [ %indvars.iv.unr, %preheader.new ], [ %indvars.iv.next.3, %latch.3 ]
  br label %exiting

%exiting:
  switch i16 %c3, label %default.loopexit.loopexit [
    i16 45, label %otherexit.loopexit
    i16 95, label %latch
  ]

%latch:
  %indvars.iv.next = add nsw nuw i64 %indvars.iv, 1
  br label %exiting.1

%exiting.1:
  switch i16 %c3, label %default.loopexit.loopexit [
    i16 45, label %otherexit.loopexit
    i16 95, label %latch.1
  ]

%latch.1:
  %indvars.iv.next.1 = add nsw nuw i64 %indvars.iv.next, 1
  br label %exiting.2

%exiting.2:
  switch i16 %c3, label %default.loopexit.loopexit [
    i16 45, label %otherexit.loopexit
    i16 95, label %latch.2
  ]

%latch.2:
  %indvars.iv.next.2 = add nsw nuw i64 %indvars.iv.next.1, 1
  br label %exiting.3

%exiting.3:
  switch i16 %c3, label %default.loopexit.loopexit [
    i16 45, label %otherexit.loopexit
    i16 95, label %latch.3
  ]

%default.loopexit.loopexit:
  br label %default.loopexit

%default.loopexit:
  br label %default

%otherexit.loopexit:
  br label %otherexit

%otherexit:
  br label %default

%default:
  ret void

%latch.3:
  %indvars.iv.next.3 = add nsw nuw i64 %indvars.iv.next.2, 1
  %c2.3 = icmp ult i64 %indvars.iv.next.3, %c1
  br i1 %c2.3, label %header, label %latchexit.unr-lcssa

%latchexit.unr-lcssa:
  br label %latchexit

%latchexit:
  ret void
}
Transformation doesn't verify!
ERROR: Source is more defined than target

Example:
i16 %c3 = #x0000 (0)

Source:
i64 %c1 = #x0000000000000000 (0)	[based on undef value]
  >> Jump to %header
i64 %indvars.iv = #x0000000000000000 (0)
  >> Jump to %exiting
  >> Jump to %default

Target:
i64 %c1 = #x0000000001000000 (16777216)
i64 %umax = #x0000000001000000 (16777216)
i64 %0 = #x0000000000ffffff (16777215)
i64 %xtraiter = #x0000000000000001 (1)
i1 %lcmp.mod = #x1 (1)
UB triggered on br



------------------- SMT STATS -------------------
Num queries: 21
Num invalid: 0
Num skips:   0
Num trivial: 19 (47.5%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     14 (66.7%)
Num UNSAT:   7 (33.3%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 2'
+ /home/nuno/llvm/build/bin/FileCheck /home/nuno/llvm/llvm/test/Transforms/LoopUnroll/runtime-loop-multiexit-dom-verify.ll
+ /home/nuno/alive2/build/opt-alive.sh -loop-unroll -unroll-runtime=true -unroll-runtime-epilog=false -unroll-runtime-multi-exit=true -unroll-count=4 -verify-dom-info -S

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /home/nuno/llvm/build/bin/FileCheck /home/nuno/llvm/llvm/test/Transforms/LoopUnroll/runtime-loop-multiexit-dom-verify.ll

<-- Back