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 doesn't verify! (not unsound)
ERROR: The target program doesn't reach a return instruction.
Consider increasing the unroll factor if it has loops
-- 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 doesn't verify! (not unsound)
ERROR: The target program doesn't reach a return instruction.
Consider increasing the unroll factor if it has loops
-- 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 = #xfffe (65534, -2)
ptr %in = pointer(non-local, block_id=1, offset=11)

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

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 2	alloc type: 0	address: 0
Block 1 >	size: 10	align: 1	alloc type: 0	address: 1

Target:
i32 %0 = #x0000fffe (65534)
i16 %const = #xffff (65535, -1)
  >> Jump to %for.body
i32 %idx = #x0000fffe (65534)
i16 %1 = #xfffe (65534, -2)
i1 %cmp.i = #x0 (0)
  >> Jump to %if.then
ptr %idx.next = pointer(non-local, block_id=1, offset=131079)
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_76II6UPq_ZFK3.bc"


------------------- SMT STATS -------------------
Num queries: 44
Num invalid: 0
Num skips:   0
Num trivial: 36 (45.0%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     30 (68.2%)
Num UNSAT:   14 (31.8%)
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

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