Test Failure: Transforms/DFAJumpThreading/dfa-jump-threading-transform.ll

Test source: git

Log:

Source: /bitbucket/nlopes/llvm/llvm/test/Transforms/DFAJumpThreading/dfa-jump-threading-transform.ll
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. DFAJumpThreadingPass

----------------------------------------
define i32 @test1(i32 %num) {
entry:
  br label %for.body

for.body:
  %count = phi i32 [ 0, %entry ], [ %inc, %for.inc ]
  %state = phi i32 [ 1, %entry ], [ %state.next, %for.inc ]
  switch i32 %state, label %for.inc [
    i32 1, label %case1
    i32 2, label %case2
  ]

case1:
  br label %for.inc

case2:
  %cmp = icmp eq i32 %count, 50
  %sel = select i1 %cmp, i32 1, i32 2
  br label %for.inc

for.inc:
  %state.next = phi i32 [ %sel, %case2 ], [ 1, %for.body ], [ 2, %case1 ]
  %inc = add nsw i32 %count, 1
  %cmp.exit = icmp slt i32 %inc, %num
  br i1 %cmp.exit, label %for.body, label %for.end

for.end:
  ret i32 0
}
Transformation seems to be correct! (syntactically equal)

-- 3. DFAJumpThreadingPass

----------------------------------------
define i32 @test1(i32 %num) {
entry:
  br label %for.body

for.body:
  %count = phi i32 [ 0, %entry ], [ %inc, %for.inc ]
  %state = phi i32 [ 1, %entry ], [ %state.next, %for.inc ]
  switch i32 %state, label %for.inc [
    i32 1, label %case1
    i32 2, label %case2
  ]

case1:
  br label %for.inc

case2:
  %cmp = icmp eq i32 %count, 50
  %sel = select i1 %cmp, i32 1, i32 2
  br label %for.inc

for.inc:
  %state.next = phi i32 [ %sel, %case2 ], [ 1, %for.body ], [ 2, %case1 ]
  %inc = add nsw i32 %count, 1
  %cmp.exit = icmp slt i32 %inc, %num
  br i1 %cmp.exit, label %for.body, label %for.end

for.end:
  ret i32 0
}
=>
define i32 @test1(i32 %num) {
entry:
  br label %for.body

for.body:
  %count = phi i32 [ 0, %entry ]
  %state = phi i32 [ 1, %entry ]
  switch i32 %state, label %for.inc.jt1 [
    i32 1, label %case1
    i32 2, label %case2
  ]

case2:
  %count1 = phi i32 [ %count.jt2, %for.body.jt2 ], [ %count, %for.body ]
  %cmp = icmp eq i32 %count1, 50
  br i1 %cmp, label %for.inc.jt1, label %sel.si.unfold.false.jt2

for.inc.jt1:
  %count3 = phi i32 [ %count, %for.body ], [ %count1, %case2 ]
  %inc.jt1 = add nsw i32 %count3, 1
  %cmp.exit.jt1 = icmp slt i32 %inc.jt1, %num
  br i1 %cmp.exit.jt1, label %for.body.jt1, label %for.end

for.body.jt1:
  %count.jt1 = phi i32 [ %inc.jt1, %for.inc.jt1 ]
  br label %case1

case1:
  %count2 = phi i32 [ %count.jt1, %for.body.jt1 ], [ %count, %for.body ]
  br label %for.inc.jt2

sel.si.unfold.false.jt2:
  br label %for.inc.jt2

for.inc.jt2:
  %count4 = phi i32 [ %count1, %sel.si.unfold.false.jt2 ], [ %count2, %case1 ]
  %inc.jt2 = add nsw i32 %count4, 1
  %cmp.exit.jt2 = icmp slt i32 %inc.jt2, %num
  br i1 %cmp.exit.jt2, label %for.body.jt2, label %for.end

for.body.jt2:
  %count.jt2 = phi i32 [ %inc.jt2, %for.inc.jt2 ]
  br label %case2

for.end:
  ret i32 0
}
Transformation seems to be correct!

-- 4. PassManager<Function> : Skipping NOP
-- 5. PassManager<Function> : Skipping NOP
-- 6. DFAJumpThreadingPass

----------------------------------------
define i32 @test2(i32 %init) {
entry:
  %cmp = icmp eq i32 %init, 0
  %sel = select i1 %cmp, i32 0, i32 2
  br label %loop.1

loop.1:
  %state.1 = phi i32 [ %sel, %entry ], [ %state.1.be2, %loop.1.backedge ]
  br label %loop.2

loop.2:
  %state.2 = phi i32 [ %state.1, %loop.1 ], [ %state.2.be, %loop.2.backedge ]
  br label %loop.3

loop.3:
  %state = phi i32 [ %state.2, %loop.2 ], [ 3, %case2 ]
  switch i32 %state, label %infloop.i [
    i32 2, label %case2
    i32 3, label %case3
    i32 4, label %case4
    i32 0, label %case0
    i32 1, label %case1
  ]

infloop.i:
  br label %infloop.i

case2:
  br i1 %cmp, label %loop.3, label %loop.1.backedge

case3:
  br i1 %cmp, label %loop.2.backedge, label %case4

case4:
  br i1 %cmp, label %loop.2.backedge, label %loop.1.backedge

loop.2.backedge:
  %state.2.be = phi i32 [ 3, %case4 ], [ 0, %case3 ]
  br label %loop.2

loop.1.backedge:
  %state.1.be = phi i32 [ 2, %case4 ], [ 4, %case2 ]
  %state.1.be2 = select i1 %cmp, i32 1, i32 %state.1.be
  br label %loop.1

case0:
  br label %exit

case1:
  br label %exit

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

-- 7. DFAJumpThreadingPass

----------------------------------------
define i32 @test2(i32 %init) {
entry:
  %cmp = icmp eq i32 %init, 0
  %sel = select i1 %cmp, i32 0, i32 2
  br label %loop.1

loop.1:
  %state.1 = phi i32 [ %sel, %entry ], [ %state.1.be2, %loop.1.backedge ]
  br label %loop.2

loop.2:
  %state.2 = phi i32 [ %state.1, %loop.1 ], [ %state.2.be, %loop.2.backedge ]
  br label %loop.3

loop.3:
  %state = phi i32 [ %state.2, %loop.2 ], [ 3, %case2 ]
  switch i32 %state, label %infloop.i [
    i32 2, label %case2
    i32 3, label %case3
    i32 4, label %case4
    i32 0, label %case0
    i32 1, label %case1
  ]

infloop.i:
  br label %infloop.i

case2:
  br i1 %cmp, label %loop.3, label %loop.1.backedge

case3:
  br i1 %cmp, label %loop.2.backedge, label %case4

case4:
  br i1 %cmp, label %loop.2.backedge, label %loop.1.backedge

loop.2.backedge:
  %state.2.be = phi i32 [ 3, %case4 ], [ 0, %case3 ]
  br label %loop.2

loop.1.backedge:
  %state.1.be = phi i32 [ 2, %case4 ], [ 4, %case2 ]
  %state.1.be2 = select i1 %cmp, i32 1, i32 %state.1.be
  br label %loop.1

case0:
  br label %exit

case1:
  br label %exit

exit:
  ret i32 0
}
=>
define i32 @test2(i32 %init) {
entry:
  %cmp = icmp eq i32 %init, 0
  br i1 %cmp, label %loop.1, label %sel.si.unfold.false

sel.si.unfold.false:
  %.si.unfold.phi = phi i32 [ 2, %entry ]
  br label %loop.1

loop.1:
  %state.1 = phi i32 [ 0, %entry ], [ %.si.unfold.phi, %sel.si.unfold.false ]
  br label %loop.2

loop.2:
  %state.2 = phi i32 [ %state.1, %loop.1 ]
  br label %loop.3

loop.3:
  %state = phi i32 [ %state.2, %loop.2 ]
  switch i32 %state, label %infloop.i [
    i32 2, label %case2
    i32 3, label %case3
    i32 4, label %case4
    i32 0, label %case0
    i32 1, label %case1
  ]

infloop.i:
  br label %infloop.i

case4:
  br i1 %cmp, label %loop.2.backedge.jt3, label %loop.1.backedge.jt2

loop.2.backedge.jt3:
  br label %loop.2.jt3

loop.2.jt3:
  br label %loop.3.jt3

loop.1.backedge.jt2:
  br i1 %cmp, label %loop.1.jt1, label %state.1.be2.si.unfold.false.jt2

state.1.be2.si.unfold.false.jt2:
  br label %loop.1.jt2

loop.1.jt2:
  br label %loop.2.jt2

loop.2.jt2:
  br label %loop.3.jt2

loop.3.jt2:
  br label %case2

case2:
  br i1 %cmp, label %loop.3.jt3, label %loop.1.backedge.jt4

loop.3.jt3:
  br label %case3

case3:
  br i1 %cmp, label %loop.2.backedge.jt0, label %case4

loop.2.backedge.jt0:
  br label %loop.2.jt0

loop.2.jt0:
  br label %loop.3.jt0

loop.3.jt0:
  br label %case0

loop.1.backedge.jt4:
  br i1 %cmp, label %loop.1.jt1, label %state.1.be2.si.unfold.false.jt4

loop.1.jt1:
  br label %loop.2.jt1

loop.2.jt1:
  br label %loop.3.jt1

loop.3.jt1:
  br label %case1

state.1.be2.si.unfold.false.jt4:
  br label %loop.1.jt4

loop.1.jt4:
  br label %loop.2.jt4

loop.2.jt4:
  br label %loop.3.jt4

loop.3.jt4:
  br label %case4

case0:
  br label %exit

case1:
  br label %exit

exit:
  ret i32 0
}
Transformation seems to be correct!

-- 8. PassManager<Function> : Skipping NOP
-- 9. PassManager<Function> : Skipping NOP
-- 10. DFAJumpThreadingPass

----------------------------------------
define void @pr78059_bitwidth() {
.split.preheader:
  br label %.split

.split:
  %#0 = phi i128 [ 0, %.split.preheader ], [ 340282366920938463463374607431768211455, %.split ]
  switch i128 %#0, label %end [
    i128 340282366920938463463374607431768211455, label %end
    i128 0, label %.split
  ]

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

-- 11. DFAJumpThreadingPass

----------------------------------------
define void @pr78059_bitwidth() {
.split.preheader:
  br label %.split

.split:
  %#0 = phi i128 [ 0, %.split.preheader ], [ 340282366920938463463374607431768211455, %.split ]
  switch i128 %#0, label %end [
    i128 340282366920938463463374607431768211455, label %end
    i128 0, label %.split
  ]

end:
  ret void
}
=>
define void @pr78059_bitwidth() {
.split.preheader:
  br label %.split

.split:
  %#0 = phi i128 [ 0, %.split.preheader ]
  switch i128 %#0, label %end [
    i128 340282366920938463463374607431768211455, label %end
    i128 0, label %.split.jt18446744073709551615
  ]

.split.jt18446744073709551615:
  br label %end

end:
  ret void
}

****************************************
WARNING: Source function is always UB.
It can be refined by any target function.
Please make sure this is what you wanted.
****************************************

Transformation doesn't verify! (not unsound)
ERROR: The source program doesn't reach a return instruction.
Consider increasing the unroll factor if it has loops
-- 12. PassManager<Function> : Skipping NOP
-- 13. PassManager<Function> : Skipping NOP
-- 14. DFAJumpThreadingPass

----------------------------------------
define void @self-reference() {
.split.preheader:
  br label %.split

.split:
  %#0 = phi i32 [ 0, %.split.preheader ], [ 4294967295, %.split ]
  switch i32 %#0, label %end [
    i32 4294967295, label %end
    i32 0, label %.split
  ]

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

-- 15. DFAJumpThreadingPass

----------------------------------------
define void @self-reference() {
.split.preheader:
  br label %.split

.split:
  %#0 = phi i32 [ 0, %.split.preheader ], [ 4294967295, %.split ]
  switch i32 %#0, label %end [
    i32 4294967295, label %end
    i32 0, label %.split
  ]

end:
  ret void
}
=>
define void @self-reference() {
.split.preheader:
  br label %.split

.split:
  %#0 = phi i32 [ 0, %.split.preheader ]
  switch i32 %#0, label %end [
    i32 4294967295, label %end
    i32 0, label %.split.jt4294967295
  ]

.split.jt4294967295:
  br label %end

end:
  ret void
}

****************************************
WARNING: Source function is always UB.
It can be refined by any target function.
Please make sure this is what you wanted.
****************************************

Transformation doesn't verify! (not unsound)
ERROR: The source program doesn't reach a return instruction.
Consider increasing the unroll factor if it has loops
-- 16. PassManager<Function> : Skipping NOP
-- 17. PassManager<Function> : Skipping NOP
-- 18. DFAJumpThreadingPass

----------------------------------------
define void @pr106083_invalidBBarg_fold(i1 %cmp1, i1 %cmp2, i1 %not, ptr %d) {
bb:
  %sel = select i1 %cmp1, i32 0, i32 1
  br label %BB1

BB1:
  %i = phi i16 [ 0, %BB1.backedge ], [ 0, %bb ], [ 1, %BB7 ]
  br i1 %not, label %BB7, label %BB2

BB2:
  store i16 0, ptr %d, align 2
  %spec.select = select i1 %cmp2, i32 %sel, i32 0
  br label %BB7

BB7:
  %d.promoted4 = phi i16 [ 0, %BB1 ], [ 1, %BB2 ]
  %_3 = phi i32 [ 0, %BB1 ], [ %spec.select, %BB2 ]
  switch i32 %_3, label %BB1.backedge [
    i32 0, label %BB1
    i32 1, label %BB8
  ]

BB1.backedge:
  br label %BB1

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

-- 19. DFAJumpThreadingPass

----------------------------------------
define void @pr106083_invalidBBarg_fold(i1 %cmp1, i1 %cmp2, i1 %not, ptr %d) {
bb:
  %sel = select i1 %cmp1, i32 0, i32 1
  br label %BB1

BB1:
  br i1 %not, label %BB7, label %BB2

BB2:
  store i16 0, ptr %d, align 2
  %spec.select = select i1 %cmp2, i32 %sel, i32 0
  br label %BB7

BB7:
  %_3 = phi i32 [ 0, %BB1 ], [ %spec.select, %BB2 ]
  switch i32 %_3, label %BB1.backedge [
    i32 0, label %BB1
    i32 1, label %BB8
  ]

BB1.backedge:
  br label %BB1

BB8:
  ret void
}
=>
define void @pr106083_invalidBBarg_fold(i1 %cmp1, i1 %cmp2, i1 %not, ptr %d) {
bb:
  br i1 %cmp1, label %BB1, label %sel.si.unfold.false

sel.si.unfold.false:
  %.si.unfold.phi1 = phi i32 [ 1, %bb ]
  br label %BB1

BB1:
  %sel.si.unfold.phi = phi i32 [ %sel.si.unfold.phi, %BB1.backedge ], [ %sel.si.unfold.phi, %BB7 ], [ 0, %bb ], [ %.si.unfold.phi1, %sel.si.unfold.false ], [ %sel.si.unfold.phi, %BB7.jt0 ]
  br i1 %not, label %BB7.jt0, label %BB2

BB2:
  store i16 0, ptr %d, align 2
  br i1 %cmp2, label %BB7, label %spec.select.si.unfold.false.jt0

BB7:
  %_3 = phi i32 [ %sel.si.unfold.phi, %BB2 ]
  switch i32 %_3, label %BB1.backedge [
    i32 0, label %BB1
    i32 1, label %BB8
  ]

BB1.backedge:
  br label %BB1

BB8:
  ret void

spec.select.si.unfold.false.jt0:
  br label %BB7.jt0

BB7.jt0:
  br label %BB1
}
Transformation seems to be correct!

-- 20. PassManager<Function> : Skipping NOP
-- 21. PassManager<Function> : Skipping NOP
-- 22. DFAJumpThreadingPass

----------------------------------------
define void @pr106083_select_dead_uses(i1 %cmp1, i1 %not, ptr %p) {
bb:
  %spec.select = select i1 %cmp1, i32 0, i32 1
  br label %.loopexit6

.loopexit6:
  br i1 %not, label %select.unfold, label %bb1

bb1:
  %i = load i32, ptr %p, align 4
  %not2 = icmp eq i32 0, 0
  %spec.select7 = select i1 %not2, i32 %spec.select, i32 0
  br label %select.unfold

select.unfold:
  %_2 = phi i32 [ 0, %.loopexit6 ], [ %spec.select7, %bb1 ]
  switch i32 %_2, label %bb2 [
    i32 0, label %.preheader.preheader
    i32 1, label %.loopexit6
  ]

bb2:
  assume i1 0

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

-- 23. DFAJumpThreadingPass

----------------------------------------
define void @pr106083_select_dead_uses(i1 %cmp1, i1 %not, ptr %p) {
bb:
  %spec.select = select i1 %cmp1, i32 0, i32 1
  br label %.loopexit6

.loopexit6:
  br i1 %not, label %select.unfold, label %bb1

bb1:
  %i = load i32, ptr %p, align 4
  %not2 = icmp eq i32 0, 0, offsetonly
  %spec.select7 = select i1 %not2, i32 %spec.select, i32 0
  br label %select.unfold

select.unfold:
  %_2 = phi i32 [ 0, %.loopexit6 ], [ %spec.select7, %bb1 ]
  switch i32 %_2, label %bb2 [
    i32 0, label %.preheader.preheader
    i32 1, label %.loopexit6
  ]

bb2:
  assume i1 0

.preheader.preheader:
  ret void
}
=>
define void @pr106083_select_dead_uses(i1 %cmp1, i1 %not, ptr %p) {
bb:
  br i1 %cmp1, label %.loopexit6, label %spec.select.si.unfold.false

spec.select.si.unfold.false:
  %.si.unfold.phi1 = phi i32 [ 1, %bb ]
  br label %.loopexit6

.loopexit6:
  %spec.select.si.unfold.phi = phi i32 [ %spec.select.si.unfold.phi, %select.unfold ], [ 0, %bb ], [ %.si.unfold.phi1, %spec.select.si.unfold.false ]
  br i1 %not, label %select.unfold.jt0, label %bb1

bb1:
  %i = load i32, ptr %p, align 4
  %not2 = icmp eq i32 0, 0, offsetonly
  br i1 %not2, label %select.unfold, label %spec.select7.si.unfold.false.jt0

select.unfold:
  %_2 = phi i32 [ %spec.select.si.unfold.phi, %bb1 ]
  switch i32 %_2, label %bb2 [
    i32 0, label %.preheader.preheader
    i32 1, label %.loopexit6
  ]

bb2:
  assume i1 0

spec.select7.si.unfold.false.jt0:
  br label %select.unfold.jt0

select.unfold.jt0:
  br label %.preheader.preheader

.preheader.preheader:
  ret void
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
i1 %cmp1 = undef
i1 %not = #x1 (1)
ptr %p = poison

Source:
i32 %spec.select = #x00000001 (1)	[based on undef value]
  >> Jump to %.loopexit6
  >> Jump to %select.unfold
i32 %_2 = #x00000000 (0)
  >> Jump to %.preheader.preheader

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 4	alloc type: 0	alive: false	address: 0
Block 1 >	size: 0	align: 1	alloc type: 0	alive: true	address: 2

Target:
UB triggered on br


Pass: DFAJumpThreadingPass
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' '-S' '-passes=dfa-jump-threading' '/bitbucket/nlopes/llvm/llvm/test/Transforms/DFAJumpThreading/dfa-jump-threading-transform.ll' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/dfa-jump-threading-transform_5CL9Nt8W_ztsQ.bc"


------------------- SMT STATS -------------------
Num queries: 34
Num invalid: 0
Num skips:   0
Num trivial: 23 (40.4%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     28 (82.4%)
Num UNSAT:   6 (17.6%)
Alive2: Transform doesn't verify; aborting!

stderr:

RUN: at line 2: /home/nlopes/alive2/build/opt-alive.sh -S -passes=dfa-jump-threading /bitbucket/nlopes/llvm/llvm/test/Transforms/DFAJumpThreading/dfa-jump-threading-transform.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/DFAJumpThreading/dfa-jump-threading-transform.ll
+ /home/nlopes/alive2/build/opt-alive.sh -S -passes=dfa-jump-threading /bitbucket/nlopes/llvm/llvm/test/Transforms/DFAJumpThreading/dfa-jump-threading-transform.ll
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/DFAJumpThreading/dfa-jump-threading-transform.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/DFAJumpThreading/dfa-jump-threading-transform.ll

<-- Back