Test Failure: Transforms/InstCombine/assume.ll

Test source: git

Log:

Source: <stdin>
ERROR: Unsupported instruction:   tail call void @llvm.assume(i1 true) [ "ignore"(i32* undef) ]

----------------------------------------
define i32 @foo1(* %a) {
%0:
  %t0 = load i32, * %a, align 4
  %ptrint = ptrtoint * %a to i64
  %maskedptr = and i64 %ptrint, 31
  %maskcond = icmp eq i64 %maskedptr, 0
  assume i1 %maskcond
  ret i32 %t0
}
=>
define i32 @foo1(* %a) {
%0:
  %t0 = load i32, * %a, align 32
  %ptrint = ptrtoint * %a to i64
  %maskedptr = and i64 %ptrint, 31
  %maskcond = icmp eq i64 %maskedptr, 0
  assume i1 %maskcond
  ret i32 %t0
}
Transformation seems to be correct!


----------------------------------------
define i32 @foo2(* %a) {
%0:
  %ptrint = ptrtoint * %a to i64
  %maskedptr = and i64 %ptrint, 31
  %maskcond = icmp eq i64 %maskedptr, 0
  assume i1 %maskcond
  %t0 = load i32, * %a, align 4
  ret i32 %t0
}
=>
define i32 @foo2(* %a) {
%0:
  %ptrint = ptrtoint * %a to i64
  %maskedptr = and i64 %ptrint, 31
  %maskcond = icmp eq i64 %maskedptr, 0
  assume i1 %maskcond
  %t0 = load i32, * %a, align 32
  ret i32 %t0
}
Transformation seems to be correct!


----------------------------------------
define i32 @simple(i32 %a) {
%0:
  %cmp = icmp eq i32 %a, 4
  assume i1 %cmp
  ret i32 %a
}
=>
define i32 @simple(i32 %a) {
%0:
  %cmp = icmp eq i32 %a, 4
  assume i1 %cmp
  ret i32 4
}
Transformation seems to be correct!


----------------------------------------
define i32 @can1(i1 %a, i1 %b, i1 %c) {
%0:
  %and1 = and i1 %a, %b
  %and = and i1 %and1, %c
  assume i1 %and
  ret i32 5
}
=>
define i32 @can1(i1 %a, i1 %b, i1 %c) {
%0:
  assume i1 %a
  assume i1 %b
  assume i1 %c
  ret i32 5
}
Transformation seems to be correct!


----------------------------------------
define i32 @can1_logical(i1 %a, i1 %b, i1 %c) {
%0:
  %and1 = select i1 %a, i1 %b, i1 0
  %and = select i1 %and1, i1 %c, i1 0
  assume i1 %and
  ret i32 5
}
=>
define i32 @can1_logical(i1 %a, i1 %b, i1 %c) {
%0:
  assume i1 %a
  assume i1 %b
  assume i1 %c
  ret i32 5
}
Transformation seems to be correct!


----------------------------------------
define i32 @can2(i1 %a, i1 %b, i1 %c) {
%0:
  %v = or i1 %a, %b
  %w = xor i1 %v, 1
  assume i1 %w
  ret i32 5
}
=>
define i32 @can2(i1 %a, i1 %b, i1 %c) {
%0:
  %1 = xor i1 %a, 1
  assume i1 %1
  %2 = xor i1 %b, 1
  assume i1 %2
  ret i32 5
}
Transformation seems to be correct!


----------------------------------------
define i32 @can2_logical(i1 %a, i1 %b, i1 %c) {
%0:
  %v = select i1 %a, i1 1, i1 %b
  %w = xor i1 %v, 1
  assume i1 %w
  ret i32 5
}
=>
define i32 @can2_logical(i1 %a, i1 %b, i1 %c) {
%0:
  %1 = xor i1 %a, 1
  assume i1 %1
  %2 = xor i1 %b, 1
  assume i1 %2
  ret i32 5
}
Transformation seems to be correct!


----------------------------------------
define i32 @bar1(i32 %a) {
%0:
  %and1 = and i32 %a, 3
  %and = and i32 %a, 7
  %cmp = icmp eq i32 %and, 1
  assume i1 %cmp
  ret i32 %and1
}
=>
define i32 @bar1(i32 %a) {
%0:
  %and = and i32 %a, 7
  %cmp = icmp eq i32 %and, 1
  assume i1 %cmp
  ret i32 1
}
Transformation seems to be correct!


----------------------------------------
define i32 @bar2(i32 %a) {
%0:
  %and = and i32 %a, 7
  %cmp = icmp eq i32 %and, 1
  assume i1 %cmp
  %and1 = and i32 %a, 3
  ret i32 %and1
}
=>
define i32 @bar2(i32 %a) {
%0:
  %and = and i32 %a, 7
  %cmp = icmp eq i32 %and, 1
  assume i1 %cmp
  ret i32 1
}
Transformation seems to be correct!


----------------------------------------
define i32 @bar3(i32 %a, i1 %x, i1 %y) {
%entry:
  %and1 = and i32 %a, 3
  assume i1 %x
  %and = and i32 %a, 7
  %cmp = icmp eq i32 %and, 1
  assume i1 %cmp
  assume i1 %y
  ret i32 %and1
}
=>
define i32 @bar3(i32 %a, i1 %x, i1 %y) {
%entry:
  assume i1 %x
  %and = and i32 %a, 7
  %cmp = icmp eq i32 %and, 1
  assume i1 %cmp
  assume i1 %y
  ret i32 1
}
Transformation seems to be correct!


----------------------------------------
define i32 @bar4(i32 %a, i32 %b) {
%entry:
  %and1 = and i32 %b, 3
  %and = and i32 %a, 7
  %cmp = icmp eq i32 %and, 1
  assume i1 %cmp
  %cmp2 = icmp eq i32 %a, %b
  assume i1 %cmp2
  ret i32 %and1
}
=>
define i32 @bar4(i32 %a, i32 %b) {
%entry:
  %and = and i32 %a, 7
  %cmp = icmp eq i32 %and, 1
  assume i1 %cmp
  %cmp2 = icmp eq i32 %a, %b
  assume i1 %cmp2
  ret i32 1
}
Transformation seems to be correct!


----------------------------------------
define i32 @icmp1(i32 %a) {
%0:
  %cmp = icmp sgt i32 %a, 5
  assume i1 %cmp
  %conv = zext i1 %cmp to i32
  ret i32 %conv
}
=>
define i32 @icmp1(i32 %a) {
%0:
  %cmp = icmp sgt i32 %a, 5
  assume i1 %cmp
  ret i32 1
}
Transformation seems to be correct!


----------------------------------------
define i32 @icmp2(i32 %a) {
%0:
  %cmp = icmp sgt i32 %a, 5
  assume i1 %cmp
  %t0 = zext i1 %cmp to i32
  %lnot.ext = xor i32 %t0, 1
  ret i32 %lnot.ext
}
=>
define i32 @icmp2(i32 %a) {
%0:
  %cmp = icmp sgt i32 %a, 5
  assume i1 %cmp
  ret i32 0
}
Transformation seems to be correct!


----------------------------------------
define i1 @assume_not(i1 %cond) {
%0:
  %notcond = xor i1 %cond, 1
  assume i1 %notcond
  ret i1 %cond
}
=>
define i1 @assume_not(i1 %cond) {
%0:
  %notcond = xor i1 %cond, 1
  assume i1 %notcond
  ret i1 0
}
Transformation seems to be correct!


----------------------------------------
define i32 @bundle1(* %P) {
%0:
  assume_nonnull * %P
  assume i1 1
  %load = load i32, * %P, align 4
  ret i32 %load
}
=>
define i32 @bundle1(* %P) {
%0:
  assume_nonnull * %P
  assume i1 1
  %load = load i32, * %P, align 4
  ret i32 %load
}
Transformation seems to be correct!

ERROR: Unsupported metadata: 11

----------------------------------------
define i1 @nonnull2(* %a) {
%0:
  %load = load i32, * %a, align 4
  %cmp = icmp ne i32 %load, 0
  assume i1 %cmp
  %rval = icmp eq i32 %load, 0
  ret i1 %rval
}
=>
define i1 @nonnull2(* %a) {
%0:
  %load = load i32, * %a, align 4
  %cmp = icmp ne i32 %load, 0
  assume i1 %cmp
  ret i1 0
}
Transformation seems to be correct!


----------------------------------------
define i1 @nonnull3(* %a, i1 %control) {
%entry:
  %load = load *, * %a, align 8
  %cmp = icmp ne * %load, null
  br i1 %control, label %taken, label %not_taken

%not_taken:
  %rval.2 = icmp sgt * %load, null
  ret i1 %rval.2

%taken:
  assume i1 %cmp
  %rval = icmp eq * %load, null
  ret i1 %rval
}
=>
define i1 @nonnull3(* %a, i1 %control) {
%entry:
  %load = load *, * %a, align 8
  %cmp = icmp ne * %load, null
  br i1 %control, label %taken, label %not_taken

%not_taken:
  %rval.2 = icmp sgt * %load, null
  ret i1 %rval.2

%taken:
  assume i1 %cmp
  ret i1 0
}
Transformation seems to be correct!


----------------------------------------
define i1 @nonnull4(* %a) {
%0:
  %load = load *, * %a, align 8
  call void @escape(* %load)
  %cmp = icmp ne * %load, null
  assume i1 %cmp
  %rval = icmp eq * %load, null
  ret i1 %rval
}
=>
define i1 @nonnull4(* %a) {
%0:
  %load = load *, * %a, align 8
  call void @escape(* %load)
  %cmp = icmp ne * %load, null
  assume i1 %cmp
  ret i1 0
}
Transformation seems to be correct!


----------------------------------------
define i1 @nonnull5(* %a) {
%0:
  %load = load *, * %a, align 8
  call void @escape(* %load)
  %integral = ptrtoint * %load to i64
  %cmp = icmp slt i64 %integral, 0
  assume i1 %cmp
  %rval = icmp eq * %load, null
  ret i1 %rval
}
=>
define i1 @nonnull5(* %a) {
%0:
  %load = load *, * %a, align 8
  call void @escape(* %load)
  %cmp = icmp slt * %load, null
  assume i1 %cmp
  ret i1 0
}
Transformation doesn't verify!
ERROR: Source is more defined than target

Example:
* %a = pointer(non-local, block_id=1, offset=0)

Source:
* %load = pointer(non-local, block_id=2, offset=-9223372036854775808)
i64 %integral = #x8000000000000004 (9223372036854775812, -9223372036854775804)
i1 %cmp = #x1 (1)
i1 %rval = #x0 (0)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 1	alloc type: 0	address: 0
Block 1 >	size: 4611686018427387904	align: 2	alloc type: 0	address: 8
Block 2 >	align: 8	alloc type: 2	address: 4
Block 3 >	size: 2203280442434510843	align: 4	alloc type: 0	address: 6670569784910807042

Target:
* %load = pointer(non-local, block_id=2, offset=-9223372036854775808)
i1 %cmp = #x0 (0)



------------------- SMT STATS -------------------
Num queries: 48
Num invalid: 0
Num skips:   0
Num trivial: 80 (62.5%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     20 (41.7%)
Num UNSAT:   28 (58.3%)

stderr:

+ : 'RUN: at line 2'
+ /home/nlopes/alive2/build/opt-alive.sh -instcombine -S -instcombine-infinite-loop-threshold=2 -instcombine-unsafe-select-transform=0
+ /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/InstCombine/assume.ll

Alive2: Transform doesn't verify; aborting!
FileCheck error: '<stdin>' is empty.
FileCheck command line:  /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/InstCombine/assume.ll

<-- Back