Test Failure: Transforms/SimpleLoopUnswitch/guards.ll

Test source: git

Log:

Source: <stdin>
ERROR: Unsupported instruction:   invoke void @may_throw(i32 %iv)
          to label %loop unwind label %exit

----------------------------------------
define void @test_simple_case(i1 %cond, i32 %N) {
%entry:
  br label %loop

%loop:
  %iv = phi i32 [ 0, %entry ], [ %iv.next, %loop ]
  call void @llvm.experimental.guard(i1 %cond) nofree
  %iv.next = add i32 %iv, 1
  %loop.cond = icmp slt i32 %iv.next, %N
  br i1 %loop.cond, label %loop, label %exit

%exit:
  ret void
}
=>
define void @test_simple_case(i1 %cond, i32 %N) {
%entry:
  br i1 %cond, label %entry.split.us, label %entry.split

%entry.split:
  br label %loop

%loop:
  br label %deopt

%deopt:
  call void @llvm.experimental.guard(i1 0) nofree
  assume i1 0

%entry.split.us:
  br label %loop.us

%loop.us:
  %iv.us = phi i32 [ 0, %entry.split.us ], [ %iv.next.us, %guarded.us ]
  br label %guarded.us

%guarded.us:
  %iv.next.us = add i32 %iv.us, 1
  %loop.cond.us = icmp slt i32 %iv.next.us, %N
  br i1 %loop.cond.us, label %loop.us, label %exit.split.us

%exit.split.us:
  br label %exit

%exit:
  ret void
}
Transformation doesn't verify!
ERROR: Couldn't prove the correctness of the transformation
Alive2 approximated the semantics of the programs and therefore we
cannot conclude whether the bug found is valid or not.

Approximations done:
 - Unknown libcall: @llvm.experimental.guard



----------------------------------------
define void @test_two_guards(i1 %cond1, i1 %cond2, i32 %N) {
%entry:
  br label %loop

%loop:
  %iv = phi i32 [ 0, %entry ], [ %iv.next, %loop ]
  call void @llvm.experimental.guard(i1 %cond1) nofree
  call void @llvm.experimental.guard(i1 %cond2) nofree
  %iv.next = add i32 %iv, 1
  %loop.cond = icmp slt i32 %iv.next, %N
  br i1 %loop.cond, label %loop, label %exit

%exit:
  ret void
}
=>
define void @test_two_guards(i1 %cond1, i1 %cond2, i32 %N) {
%entry:
  br i1 %cond1, label %entry.split.us, label %entry.split

%entry.split:
  br label %loop

%loop:
  br label %deopt

%deopt:
  call void @llvm.experimental.guard(i1 0) nofree
  assume i1 0

%entry.split.us:
  br i1 %cond2, label %entry.split.us.split.us, label %entry.split.us.split

%entry.split.us.split.us:
  br label %loop.us.us

%loop.us.us:
  %iv.us.us = phi i32 [ 0, %entry.split.us.split.us ], [ %iv.next.us.us, %guarded.us2 ]
  br label %guarded.us.us

%guarded.us.us:
  br label %guarded.us2

%guarded.us2:
  %iv.next.us.us = add i32 %iv.us.us, 1
  %loop.cond.us.us = icmp slt i32 %iv.next.us.us, %N
  br i1 %loop.cond.us.us, label %loop.us.us, label %exit.split.us.split.us

%exit.split.us.split.us:
  br label %exit.split.us

%exit.split.us:
  br label %exit

%exit:
  ret void

%entry.split.us.split:
  br label %loop.us

%loop.us:
  br label %guarded.us

%guarded.us:
  br label %deopt1

%deopt1:
  call void @llvm.experimental.guard(i1 0) nofree
  assume i1 0
}
Transformation doesn't verify!
ERROR: Couldn't prove the correctness of the transformation
Alive2 approximated the semantics of the programs and therefore we
cannot conclude whether the bug found is valid or not.

Approximations done:
 - Unknown libcall: @llvm.experimental.guard



----------------------------------------
define void @test_conditional_guards(i1 %cond, i32 %N) {
%entry:
  br label %loop

%loop:
  %iv = phi i32 [ 0, %entry ], [ %iv.next, %backedge ]
  %condition = icmp eq i32 %iv, 123
  br i1 %condition, label %guard, label %backedge

%guard:
  call void @llvm.experimental.guard(i1 %cond) nofree
  br label %backedge

%backedge:
  %iv.next = add i32 %iv, 1
  %loop.cond = icmp slt i32 %iv.next, %N
  br i1 %loop.cond, label %loop, label %exit

%exit:
  ret void
}
=>
define void @test_conditional_guards(i1 %cond, i32 %N) {
%entry:
  br i1 %cond, label %entry.split.us, label %entry.split

%entry.split:
  br label %loop

%loop:
  %iv = phi i32 [ 0, %entry.split ], [ %iv.next, %backedge ]
  %condition = icmp eq i32 %iv, 123
  br i1 %condition, label %guard, label %backedge

%guard:
  br label %deopt

%deopt:
  call void @llvm.experimental.guard(i1 0) nofree
  assume i1 0

%backedge:
  %iv.next = add i32 %iv, 1
  %loop.cond = icmp slt i32 %iv.next, %N
  br i1 %loop.cond, label %loop, label %exit.split

%exit.split:
  br label %exit

%entry.split.us:
  br label %loop.us

%loop.us:
  %iv.us = phi i32 [ 0, %entry.split.us ], [ %iv.next.us, %backedge.us ]
  %condition.us = icmp eq i32 %iv.us, 123
  br i1 %condition.us, label %guard.us, label %backedge.us

%guard.us:
  br label %guarded.us

%guarded.us:
  br label %backedge.us

%backedge.us:
  %iv.next.us = add i32 %iv.us, 1
  %loop.cond.us = icmp slt i32 %iv.next.us, %N
  br i1 %loop.cond.us, label %loop.us, label %exit.split.us

%exit.split.us:
  br label %exit

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

Example:
i1 %cond = undef
i32 %N = #x00000001 (1)

Source:
i32 %iv = #x00000000 (0)
i1 %condition = #x0 (0)
i32 %iv.next = #x00000001 (1)
i1 %loop.cond = #x0 (0)

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

Target:
i32 %iv = #x00000000 (0)
i1 %condition = #x0 (0)
i32 %iv.next = #x00000001 (1)
i1 %loop.cond = #x0 (0)
i32 %iv.us = #x00000000 (0)
i1 %condition.us = #x0 (0)
i32 %iv.next.us = #x00000001 (1)
i1 %loop.cond.us = #x0 (0)



------------------- SMT STATS -------------------
Num queries: 6
Num invalid: 0
Num skips:   0
Num trivial: 14 (70.0%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     6 (100.0%)
Num UNSAT:   0 (0.0%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 1'
+ /home/nlopes/alive2/build/opt-alive.sh '-passes=loop(simple-loop-unswitch<nontrivial>),verify<loops>' -simple-loop-unswitch-guards -S
+ /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/SimpleLoopUnswitch/guards.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/SimpleLoopUnswitch/guards.ll

<-- Back