Test Failure: Transforms/SimplifyCFG/switch_create.ll

Test source: git

Log:

Source: <stdin>

----------------------------------------
define void @test1(i32 %V) {
%0:
  %C1 = icmp eq i32 %V, 4
  %C2 = icmp eq i32 %V, 17
  %CN = or i1 %C1, %C2
  br i1 %CN, label %T, label %F

%F:
  call void @foo2()
  ret void

%T:
  call void @foo1()
  ret void
}
=>
define void @test1(i32 %V) {
%0:
  switch i32 %V, label %F [
    i32 17, label %T
    i32 4, label %T
  ]

%T:
  call void @foo1()
  ret void

%F:
  call void @foo2()
  ret void
}
Transformation seems to be correct!


----------------------------------------
define void @test1_select(i32 %V) {
%0:
  %C1 = icmp eq i32 %V, 4
  %C2 = icmp eq i32 %V, 17
  %CN = select i1 %C1, i1 1, i1 %C2
  br i1 %CN, label %T, label %F

%F:
  call void @foo2()
  ret void

%T:
  call void @foo1()
  ret void
}
=>
define void @test1_select(i32 %V) {
%0:
  switch i32 %V, label %F [
    i32 17, label %T
    i32 4, label %T
  ]

%T:
  call void @foo1()
  ret void

%F:
  call void @foo2()
  ret void
}
Transformation seems to be correct!


----------------------------------------
define void @test1_ptr(* %V) {
%0:
  %__constexpr_0 = int2ptr i32 4 to *
  %C1 = icmp eq * %V, %__constexpr_0
  %__constexpr_1 = int2ptr i32 17 to *
  %C2 = icmp eq * %V, %__constexpr_1
  %CN = or i1 %C1, %C2
  br i1 %CN, label %T, label %F

%F:
  call void @foo2()
  ret void

%T:
  call void @foo1()
  ret void
}
=>
define void @test1_ptr(* %V) {
%0:
  %magicptr = ptrtoint * %V to i64
  switch i64 %magicptr, label %F [
    i64 17, label %T
    i64 4, label %T
  ]

%T:
  call void @foo1()
  ret void

%F:
  call void @foo2()
  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:
 - inttoptr



----------------------------------------
define void @test2(i32 %V) {
%0:
  %C1 = icmp ne i32 %V, 4
  %C2 = icmp ne i32 %V, 17
  %CN = and i1 %C1, %C2
  br i1 %CN, label %T, label %F

%F:
  call void @foo2()
  ret void

%T:
  call void @foo1()
  ret void
}
=>
define void @test2(i32 %V) {
%0:
  switch i32 %V, label %T [
    i32 17, label %F
    i32 4, label %F
  ]

%F:
  call void @foo2()
  ret void

%T:
  call void @foo1()
  ret void
}
Transformation seems to be correct!


----------------------------------------
define void @test2_select(i32 %V) {
%0:
  %C1 = icmp ne i32 %V, 4
  %C2 = icmp ne i32 %V, 17
  %CN = select i1 %C1, i1 %C2, i1 0
  br i1 %CN, label %T, label %F

%F:
  call void @foo2()
  ret void

%T:
  call void @foo1()
  ret void
}
=>
define void @test2_select(i32 %V) {
%0:
  switch i32 %V, label %T [
    i32 17, label %F
    i32 4, label %F
  ]

%F:
  call void @foo2()
  ret void

%T:
  call void @foo1()
  ret void
}
Transformation seems to be correct!


----------------------------------------
define void @test3(i32 %V) {
%0:
  %C1 = icmp eq i32 %V, 4
  br i1 %C1, label %T, label %N

%N:
  %C2 = icmp eq i32 %V, 17
  br i1 %C2, label %T, label %F

%F:
  call void @foo2()
  ret void

%T:
  call void @foo1()
  ret void
}
=>
define void @test3(i32 %V) {
%0:
  switch i32 %V, label %F [
    i32 4, label %T
    i32 17, label %T
  ]

%T:
  call void @foo1()
  ret void

%F:
  call void @foo2()
  ret void
}
Transformation seems to be correct!


----------------------------------------
define i32 @test4(i8 %c) {
%entry:
  %cmp = icmp eq i8 %c, 62
  br i1 %cmp, label %lor.end, label %lor.lhs.false

%lor.lhs.false:
  %cmp4 = icmp eq i8 %c, 34
  br i1 %cmp4, label %lor.end, label %lor.rhs

%lor.rhs:
  %cmp8 = icmp eq i8 %c, 92
  br label %lor.end

%lor.end:
  %0 = phi i1 [ 1, %lor.lhs.false ], [ 1, %entry ], [ %cmp8, %lor.rhs ]
  %lor.ext = zext i1 %0 to i32
  ret i32 %lor.ext
}
=>
define i32 @test4(i8 %c) {
%entry:
  switch i8 %c, label %lor.rhs [
    i8 62, label %lor.end
    i8 34, label %lor.end
    i8 92, label %lor.end
  ]

%lor.rhs:
  br label %lor.end

%lor.end:
  %0 = phi i1 [ 1, %entry ], [ 0, %lor.rhs ], [ 1, %entry ], [ 1, %entry ]
  %lor.ext = zext i1 %0 to i32
  ret i32 %lor.ext
}
Transformation seems to be correct!


----------------------------------------
define i32 @test5(i8 %c) {
%entry:
  switch i8 %c, label %lor.rhs [
    i8 62, label %lor.end
    i8 34, label %lor.end
    i8 92, label %lor.end
  ]

%lor.rhs:
  %V = icmp eq i8 %c, 92
  br label %lor.end

%lor.end:
  %0 = phi i1 [ 1, %entry ], [ %V, %lor.rhs ], [ 1, %entry ], [ 1, %entry ]
  %lor.ext = zext i1 %0 to i32
  ret i32 %lor.ext
}
=>
define i32 @test5(i8 %c) {
%entry:
  switch i8 %c, label %lor.rhs [
    i8 62, label %lor.end
    i8 34, label %lor.end
    i8 92, label %lor.end
  ]

%lor.rhs:
  br label %lor.end

%lor.end:
  %0 = phi i1 [ 1, %entry ], [ 0, %lor.rhs ], [ 1, %entry ], [ 1, %entry ]
  %lor.ext = zext i1 %0 to i32
  ret i32 %lor.ext
}
Transformation seems to be correct!


----------------------------------------
define i1 @test6(* %I) {
%entry:
  %tmp.1.i = gep * %I, 8 x i64 0, 1 x i64 4
  %tmp.2.i = load i32, * %tmp.1.i, align 4
  %tmp.2 = icmp eq i32 %tmp.2.i, 14
  br i1 %tmp.2, label %shortcirc_done.4, label %shortcirc_next.0

%shortcirc_next.0:
  %tmp.6 = icmp eq i32 %tmp.2.i, 15
  br i1 %tmp.6, label %shortcirc_done.4, label %shortcirc_next.1

%shortcirc_next.1:
  %tmp.11 = icmp eq i32 %tmp.2.i, 16
  br i1 %tmp.11, label %shortcirc_done.4, label %shortcirc_next.2

%shortcirc_next.2:
  %tmp.16 = icmp eq i32 %tmp.2.i, 17
  br i1 %tmp.16, label %shortcirc_done.4, label %shortcirc_next.3

%shortcirc_next.3:
  %tmp.21 = icmp eq i32 %tmp.2.i, 18
  br i1 %tmp.21, label %shortcirc_done.4, label %shortcirc_next.4

%shortcirc_next.4:
  %tmp.26 = icmp eq i32 %tmp.2.i, 19
  br label %UnifiedReturnBlock

%shortcirc_done.4:
  br label %UnifiedReturnBlock

%UnifiedReturnBlock:
  %UnifiedRetVal = phi i1 [ %tmp.26, %shortcirc_next.4 ], [ 1, %shortcirc_done.4 ]
  ret i1 %UnifiedRetVal
}
=>
define i1 @test6(* %I) {
%entry:
  %tmp.1.i = gep * %I, 8 x i64 0, 1 x i64 4
  %tmp.2.i = load i32, * %tmp.1.i, align 4
  %tmp.2.i.off = add i32 %tmp.2.i, 4294967282
  %switch = icmp ult i32 %tmp.2.i.off, 6
  %spec.select = select i1 %switch, i1 1, i1 0
  ret i1 %spec.select
}
Transformation seems to be correct!


----------------------------------------
define void @test7(i8 %c, i32 %x) {
%entry:
  %cmp = icmp ult i32 %x, 32
  %cmp4 = icmp eq i8 %c, 97
  %or.cond = or i1 %cmp, %cmp4
  %cmp9 = icmp eq i8 %c, 99
  %or.cond11 = or i1 %or.cond, %cmp9
  br i1 %or.cond11, label %if.then, label %if.end

%if.end:
  ret void

%if.then:
  call void @foo1()
  ret void
}
=>
define void @test7(i8 %c, i32 %x) {
%entry:
  %cmp = icmp ult i32 %x, 32
  br i1 %cmp, label %if.then, label %switch.early.test

%switch.early.test:
  switch i8 %c, label %if.end [
    i8 99, label %if.then
    i8 97, label %if.then
  ]

%if.end:
  ret void

%if.then:
  call void @foo1()
  ret void
}
Transformation doesn't verify!
ERROR: Source is more defined than target

Example:
i8 %c = #x61 (97)
i32 %x = undef

Source:
i1 %cmp = any
i1 %cmp4 = #x1 (1)
i1 %or.cond = #x1 (1)
i1 %cmp9 = #x0 (0)
i1 %or.cond11 = #x1 (1)

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

Target:
i1 %cmp = any



------------------- SMT STATS -------------------
Num queries: 29
Num invalid: 0
Num skips:   0
Num trivial: 41 (58.6%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     12 (41.4%)
Num UNSAT:   17 (58.6%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 2'
+ /home/nlopes/alive2/build/opt-alive.sh -S -simplifycfg -simplifycfg-require-and-preserve-domtree=1
+ /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/SimplifyCFG/switch_create.ll

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

<-- Back