Test Failure: Transforms/TypePromotion/ARM/phis-ret.ll

Test source: git

Log:

Source: /bitbucket/nlopes/llvm/llvm/test/Transforms/TypePromotion/ARM/phis-ret.ll
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. TypePromotionPass

----------------------------------------
define void @phi_feeding_phi_args(i8 %a, i8 %b) {
entry:
  %#0 = icmp ugt i8 %a, %b
  br i1 %#0, label %preheader, label %empty

empty:
  br label %preheader

preheader:
  %#1 = phi i8 [ %a, %entry ], [ %b, %empty ]
  br label %loop

loop:
  %val = phi i8 [ %#1, %preheader ], [ %inc2, %if.end ]
  %cmp = icmp ult i8 %val, 254
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = sub nuw i8 %val, 2
  br label %if.end

if.else:
  %inc1 = shl nuw i8 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i8 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp eq i8 %inc2, 255
  br i1 %cmp1, label %exit, label %loop

exit:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 3. TypePromotionPass

----------------------------------------
define void @phi_feeding_phi_args(i8 %a, i8 %b) {
entry:
  %#0 = icmp ugt i8 %a, %b
  br i1 %#0, label %preheader, label %empty

empty:
  br label %preheader

preheader:
  %#1 = phi i8 [ %a, %entry ], [ %b, %empty ]
  br label %loop

loop:
  %val = phi i8 [ %#1, %preheader ], [ %inc2, %if.end ]
  %cmp = icmp ult i8 %val, 254
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = sub nuw i8 %val, 2
  br label %if.end

if.else:
  %inc1 = shl nuw i8 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i8 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp eq i8 %inc2, 255
  br i1 %cmp1, label %exit, label %loop

exit:
  ret void
}
=>
define void @phi_feeding_phi_args(i8 %a, i8 %b) {
entry:
  %#0 = zext i8 %a to i32
  %#1 = zext i8 %b to i32
  %#2 = icmp ugt i32 %#0, %#1
  br i1 %#2, label %preheader, label %empty

empty:
  br label %preheader

preheader:
  %#3 = phi i32 [ %#0, %entry ], [ %#1, %empty ]
  br label %loop

loop:
  %val = phi i32 [ %#3, %preheader ], [ %inc2, %if.end ]
  %cmp = icmp ult i32 %val, 254
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = sub nuw i32 %val, 2
  br label %if.end

if.else:
  %inc1 = shl nuw i32 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i32 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp eq i32 %inc2, 255
  br i1 %cmp1, label %exit, label %loop

exit:
  ret void
}
Transformation seems to be correct!

-- 4. VerifierPass : Skipping NOP
-- 5. VerifierPass : Skipping NOP
-- 6. PassManager<Function> : Skipping NOP
-- 7. PassManager<Function> : Skipping NOP
-- 8. TypePromotionPass

----------------------------------------
define void @phi_feeding_phi_zeroext_args(i8 zeroext %a, i8 zeroext %b) {
entry:
  %#0 = icmp ugt i8 zeroext %a, zeroext %b
  br i1 %#0, label %preheader, label %empty

empty:
  br label %preheader

preheader:
  %#1 = phi i8 [ zeroext %a, %entry ], [ zeroext %b, %empty ]
  br label %loop

loop:
  %val = phi i8 [ %#1, %preheader ], [ %inc2, %if.end ]
  %cmp = icmp ult i8 %val, 254
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = sub nuw i8 %val, 2
  br label %if.end

if.else:
  %inc1 = shl nuw i8 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i8 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp eq i8 %inc2, 255
  br i1 %cmp1, label %exit, label %loop

exit:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 9. TypePromotionPass

----------------------------------------
define void @phi_feeding_phi_zeroext_args(i8 zeroext %a, i8 zeroext %b) {
entry:
  %#0 = icmp ugt i8 zeroext %a, zeroext %b
  br i1 %#0, label %preheader, label %empty

empty:
  br label %preheader

preheader:
  %#1 = phi i8 [ zeroext %a, %entry ], [ zeroext %b, %empty ]
  br label %loop

loop:
  %val = phi i8 [ %#1, %preheader ], [ %inc2, %if.end ]
  %cmp = icmp ult i8 %val, 254
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = sub nuw i8 %val, 2
  br label %if.end

if.else:
  %inc1 = shl nuw i8 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i8 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp eq i8 %inc2, 255
  br i1 %cmp1, label %exit, label %loop

exit:
  ret void
}
=>
define void @phi_feeding_phi_zeroext_args(i8 zeroext %a, i8 zeroext %b) {
entry:
  %#0 = zext i8 zeroext %a to i32
  %#1 = zext i8 zeroext %b to i32
  %#2 = icmp ugt i32 %#0, %#1
  br i1 %#2, label %preheader, label %empty

empty:
  br label %preheader

preheader:
  %#3 = phi i32 [ %#0, %entry ], [ %#1, %empty ]
  br label %loop

loop:
  %val = phi i32 [ %#3, %preheader ], [ %inc2, %if.end ]
  %cmp = icmp ult i32 %val, 254
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = sub nuw i32 %val, 2
  br label %if.end

if.else:
  %inc1 = shl nuw i32 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i32 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp eq i32 %inc2, 255
  br i1 %cmp1, label %exit, label %loop

exit:
  ret void
}
Transformation seems to be correct!

-- 10. VerifierPass : Skipping NOP
-- 11. VerifierPass : Skipping NOP
-- 12. PassManager<Function> : Skipping NOP
-- 13. PassManager<Function> : Skipping NOP
-- 14. TypePromotionPass

----------------------------------------
define void @phi_i16() {
entry:
  br label %loop

loop:
  %val = phi i16 [ 0, %entry ], [ %inc2, %if.end ]
  %cmp = icmp ult i16 %val, 128
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = add nuw i16 %val, 2
  br label %if.end

if.else:
  %inc1 = add nuw i16 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i16 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp ult i16 %inc2, 253
  br i1 %cmp1, label %loop, label %exit

exit:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 15. TypePromotionPass

----------------------------------------
define void @phi_i16() {
entry:
  br label %loop

loop:
  %val = phi i16 [ 0, %entry ], [ %inc2, %if.end ]
  %cmp = icmp ult i16 %val, 128
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = add nuw i16 %val, 2
  br label %if.end

if.else:
  %inc1 = add nuw i16 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i16 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp ult i16 %inc2, 253
  br i1 %cmp1, label %loop, label %exit

exit:
  ret void
}
=>
define void @phi_i16() {
entry:
  br label %loop

loop:
  %val = phi i32 [ 0, %entry ], [ %inc2, %if.end ]
  %cmp = icmp ult i32 %val, 128
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = add nuw i32 %val, 2
  br label %if.end

if.else:
  %inc1 = add nuw i32 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i32 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp ult i32 %inc2, 253
  br i1 %cmp1, label %loop, label %exit

exit:
  ret void
}
Transformation seems to be correct!

-- 16. VerifierPass : Skipping NOP
-- 17. VerifierPass : Skipping NOP
-- 18. PassManager<Function> : Skipping NOP
-- 19. PassManager<Function> : Skipping NOP
-- 20. TypePromotionPass

----------------------------------------
define i8 @ret_i8() {
entry:
  br label %loop

loop:
  %val = phi i8 [ 0, %entry ], [ %inc2, %if.end ]
  %cmp = icmp ult i8 %val, 128
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = add nuw i8 %val, 2
  br label %if.end

if.else:
  %inc1 = add nuw i8 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i8 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp ult i8 %inc2, 253
  br i1 %cmp1, label %exit, label %loop

exit:
  ret i8 %inc2
}
Transformation seems to be correct! (syntactically equal)

-- 21. TypePromotionPass

----------------------------------------
define i8 @ret_i8() {
entry:
  br label %loop

loop:
  %val = phi i8 [ 0, %entry ], [ %inc2, %if.end ]
  %cmp = icmp ult i8 %val, 128
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = add nuw i8 %val, 2
  br label %if.end

if.else:
  %inc1 = add nuw i8 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i8 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp ult i8 %inc2, 253
  br i1 %cmp1, label %exit, label %loop

exit:
  ret i8 %inc2
}
=>
define i8 @ret_i8() {
entry:
  br label %loop

loop:
  %val = phi i32 [ 0, %entry ], [ %inc2, %if.end ]
  %cmp = icmp ult i32 %val, 128
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = add nuw i32 %val, 2
  br label %if.end

if.else:
  %inc1 = add nuw i32 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i32 [ %inc, %if.then ], [ %inc1, %if.else ]
  %cmp1 = icmp ult i32 %inc2, 253
  br i1 %cmp1, label %exit, label %loop

exit:
  %#0 = trunc i32 %inc2 to i8
  ret i8 %#0
}
Transformation seems to be correct!

-- 22. VerifierPass : Skipping NOP
-- 23. VerifierPass : Skipping NOP
-- 24. PassManager<Function> : Skipping NOP
-- 25. PassManager<Function> : Skipping NOP
-- 26. TypePromotionPass

----------------------------------------
define i16 @phi_multiple_undefs(i16 zeroext %arg) {
entry:
  br label %loop

loop:
  %val = phi i16 [ undef, %entry ], [ %inc2, %if.end ]
  %cmp = icmp ult i16 %val, 128
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = add nuw i16 %val, 2
  br label %if.end

if.else:
  %inc1 = add nuw i16 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i16 [ %inc, %if.then ], [ %inc1, %if.else ]
  %unrelated = phi i16 [ undef, %if.then ], [ zeroext %arg, %if.else ]
  %cmp1 = icmp ult i16 %inc2, 253
  br i1 %cmp1, label %loop, label %exit

exit:
  ret i16 %unrelated
}
Transformation seems to be correct! (syntactically equal)

-- 27. TypePromotionPass

----------------------------------------
define i16 @phi_multiple_undefs(i16 zeroext %arg) {
entry:
  br label %loop

loop:
  %val = phi i16 [ undef, %entry ], [ %inc2, %if.end ]
  %cmp = icmp ult i16 %val, 128
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = add nuw i16 %val, 2
  br label %if.end

if.else:
  %inc1 = add nuw i16 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i16 [ %inc, %if.then ], [ %inc1, %if.else ]
  %unrelated = phi i16 [ undef, %if.then ], [ zeroext %arg, %if.else ]
  %cmp1 = icmp ult i16 %inc2, 253
  br i1 %cmp1, label %loop, label %exit

exit:
  ret i16 %unrelated
}
=>
define i16 @phi_multiple_undefs(i16 zeroext %arg) {
entry:
  br label %loop

loop:
  %val = phi i32 [ 0, %entry ], [ %inc2, %if.end ]
  %cmp = icmp ult i32 %val, 128
  br i1 %cmp, label %if.then, label %if.else

if.then:
  %inc = add nuw i32 %val, 2
  br label %if.end

if.else:
  %inc1 = add nuw i32 %val, 1
  br label %if.end

if.end:
  %inc2 = phi i32 [ %inc, %if.then ], [ %inc1, %if.else ]
  %unrelated = phi i16 [ undef, %if.then ], [ zeroext %arg, %if.else ]
  %cmp1 = icmp ult i32 %inc2, 253
  br i1 %cmp1, label %loop, label %exit

exit:
  ret i16 %unrelated
}
Transformation seems to be correct!

-- 28. VerifierPass : Skipping NOP
-- 29. VerifierPass : Skipping NOP
-- 30. PassManager<Function> : Skipping NOP
-- 31. PassManager<Function> : Skipping NOP
-- 32. TypePromotionPass

----------------------------------------
define i16 @promote_arg_return(i16 zeroext %arg1, i16 zeroext %arg2, ptr %res) {
#0:
  %add = add nuw i16 zeroext %arg1, 15
  %mul = mul nsw nuw i16 %add, 3
  %cmp = icmp ult i16 %mul, zeroext %arg2
  %conv = zext i1 %cmp to i8
  store i8 %conv, ptr %res, align 1
  ret i16 zeroext %arg1
}
Transformation seems to be correct! (syntactically equal)

-- 33. TypePromotionPass

----------------------------------------
define i16 @promote_arg_return(i16 zeroext %arg1, i16 zeroext %arg2, ptr %res) {
#0:
  %add = add nuw i16 zeroext %arg1, 15
  %mul = mul nsw nuw i16 %add, 3
  %cmp = icmp ult i16 %mul, zeroext %arg2
  %conv = zext i1 %cmp to i8
  store i8 %conv, ptr %res, align 1
  ret i16 zeroext %arg1
}
=>
define i16 @promote_arg_return(i16 zeroext %arg1, i16 zeroext %arg2, ptr %res) {
#0:
  %#1 = zext i16 zeroext %arg1 to i32
  %#2 = zext i16 zeroext %arg2 to i32
  %add = add nuw i32 %#1, 15
  %mul = mul nsw nuw i32 %add, 3
  %cmp = icmp ult i32 %mul, %#2
  %conv = zext i1 %cmp to i8
  store i8 %conv, ptr %res, align 1
  %#3 = trunc i32 %#1 to i16
  ret i16 %#3
}
Transformation seems to be correct!

-- 34. VerifierPass : Skipping NOP
-- 35. VerifierPass : Skipping NOP
-- 36. PassManager<Function> : Skipping NOP
-- 37. PassManager<Function> : Skipping NOP
-- 38. TypePromotionPass

----------------------------------------
define i16 @signext_bitcast_phi_select(i16 signext %start, ptr %in) {
entry:
  %const = bitcast i16 65535 to i16
  br label %for.body

for.body:
  %idx = phi i16 [ %select, %if.else ], [ signext %start, %entry ]
  %cmp.i = icmp sgt i16 %idx, %const
  br i1 %cmp.i, label %exit, label %if.then

if.then:
  %idx.next = gep ptr %in, 2 x i16 %idx
  %ld = load i16, ptr %idx.next, align 2
  %cmp1.i = icmp eq i16 %ld, %idx
  br i1 %cmp1.i, label %exit, label %if.else

exit:
  %res = phi i16 [ %ld, %if.then ], [ 0, %for.body ]
  ret i16 %res

if.else:
  %lobit = lshr i16 %idx, 15
  %lobit.not = xor i16 %lobit, 1
  %select = add nuw i16 %lobit.not, %idx
  br label %for.body
}
Transformation seems to be correct! (syntactically equal)

-- 39. TypePromotionPass

----------------------------------------
define i16 @signext_bitcast_phi_select(i16 signext %start, ptr %in) {
entry:
  %const = bitcast i16 65535 to i16
  br label %for.body

for.body:
  %idx = phi i16 [ %select, %if.else ], [ signext %start, %entry ]
  %cmp.i = icmp sgt i16 %idx, %const
  br i1 %cmp.i, label %exit, label %if.then

if.then:
  %idx.next = gep ptr %in, 2 x i16 %idx
  %ld = load i16, ptr %idx.next, align 2
  %cmp1.i = icmp eq i16 %ld, %idx
  br i1 %cmp1.i, label %exit, label %if.else

exit:
  %res = phi i16 [ %ld, %if.then ], [ 0, %for.body ]
  ret i16 %res

if.else:
  %lobit = lshr i16 %idx, 15
  %lobit.not = xor i16 %lobit, 1
  %select = add nuw i16 %lobit.not, %idx
  br label %for.body
}
=>
define i16 @signext_bitcast_phi_select(i16 signext %start, ptr %in) {
entry:
  %#0 = zext i16 signext %start to i32
  %const = bitcast i16 65535 to i16
  br label %for.body

for.body:
  %idx = phi i32 [ %select, %if.else ], [ %#0, %entry ]
  %#1 = trunc i32 %idx to i16
  %cmp.i = icmp sgt i16 %#1, %const
  br i1 %cmp.i, label %exit, label %if.then

if.then:
  %idx.next = gep ptr %in, 2 x i32 %idx
  %ld = load i16, ptr %idx.next, align 2
  %#2 = zext i16 %ld to i32
  %cmp1.i = icmp eq i32 %#2, %idx
  br i1 %cmp1.i, label %exit, label %if.else

exit:
  %res = phi i32 [ %#2, %if.then ], [ 0, %for.body ]
  %#3 = trunc i32 %res to i16
  ret i16 %#3

if.else:
  %lobit = lshr i32 %idx, 15
  %lobit.not = xor i32 %lobit, 1
  %select = add nuw i32 %lobit.not, %idx
  br label %for.body
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
i16 signext %start = #xfff9 (65529, -7)
ptr %in = pointer(non-local, block_id=1, offset=15)

Source:
i16 %const = #xffff (65535, -1)
  >> Jump to %for.body
i16 %idx = #xfff9 (65529, -7)
i1 %cmp.i = #x0 (0)
  >> Jump to %if.then
ptr %idx.next = pointer(non-local, block_id=1, offset=1)
i16 %ld = #xfff9 (65529, -7)
i1 %cmp1.i = #x1 (1)
  >> Jump to %exit
i16 %res = #xfff9 (65529, -7)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 2	alloc type: 0	alive: false	address: 0
Block 1 >	size: 8	align: 1	alloc type: 0	alive: true	address: 1
Contents:
#b0000000000000010000000000000000: #x0000
#b0000000000000000000000000000000: #xfff9
else: poison


Target:
i32 %#0 = #x0000fff9 (65529)
i16 %const = #xffff (65535, -1)
  >> Jump to %for.body
i32 %idx = #x0000fff9 (65529)
i16 %#1 = #xfff9 (65529, -7)
i1 %cmp.i = #x0 (0)
  >> Jump to %if.then
ptr %idx.next = pointer(non-local, block_id=1, offset=131073)
i16 %ld = UB triggered!


Pass: TypePromotionPass
Command line: '/home/nlopes/llvm/build/bin/opt' '-load=/home/nlopes/alive2/build/tv/tv.so' '-load-pass-plugin=/home/nlopes/alive2/build/tv/tv.so' '-tv-exit-on-error' '-mtriple=arm' '-passes=typepromotion,verify' '-S' '/bitbucket/nlopes/llvm/llvm/test/Transforms/TypePromotion/ARM/phis-ret.ll' '-o' '-' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/phis-ret_QTs20QWY_fSCW.bc"


------------------- SMT STATS -------------------
Num queries: 46
Num invalid: 0
Num skips:   0
Num trivial: 46 (50.0%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     32 (69.6%)
Num UNSAT:   14 (30.4%)
Alive2: Transform doesn't verify; aborting!

stderr:

RUN: at line 2: /home/nlopes/alive2/build/opt-alive.sh -mtriple=arm -passes=typepromotion,verify  -S /bitbucket/nlopes/llvm/llvm/test/Transforms/TypePromotion/ARM/phis-ret.ll -o - | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/TypePromotion/ARM/phis-ret.ll
+ /home/nlopes/alive2/build/opt-alive.sh -mtriple=arm -passes=typepromotion,verify -S /bitbucket/nlopes/llvm/llvm/test/Transforms/TypePromotion/ARM/phis-ret.ll -o -
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/TypePromotion/ARM/phis-ret.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/TypePromotion/ARM/phis-ret.ll

<-- Back