Test Failure: Transforms/InstCombine/assume.ll

Test source: git

Log:

Source: <stdin>

----------------------------------------
define i32 @foo1(* %a) {
%entry:
  %0 = 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 %0
}
=>
define i32 @foo1(* %a) {
%entry:
  %0 = 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 %0
}
Transformation seems to be correct!


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


----------------------------------------
define i32 @simple(i32 %a) {
%entry:
  %cmp = icmp eq i32 %a, 4
  assume i1 %cmp
  ret i32 %a
}
=>
define i32 @simple(i32 %a) {
%entry:
  %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) {
%entry:
  %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) {
%entry:
  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) {
%entry:
  %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) {
%entry:
  %0 = xor i1 %a, 1
  assume i1 %0
  %1 = xor i1 %b, 1
  assume i1 %1
  ret i32 5
}
Transformation seems to be correct!


----------------------------------------
define i32 @bar1(i32 %a) {
%entry:
  %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) {
%entry:
  %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) {
%entry:
  %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) {
%entry:
  %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 i1 1
  %load = load i32, * %P, align 4
  ret i32 %load
}
=>
define i32 @bundle1(* %P) {
%0:
  assume i1 1
  %load = load i32, * %P, align 4
  ret i32 %load
}
Transformation seems to be correct!


----------------------------------------
define i32 @bundle2(* %P) {
%0:
  assume i1 1
  %load = load i32, * %P, align 4
  ret i32 %load
}
=>
define i32 @bundle2(* %P) {
%0:
  %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=2147483640)

Source:
* %load = pointer(non-local, block_id=4, offset=-7381115287405330432)
i64 %integral = #x999102c0d0000000 (11065628786572656640, -7381115287136894976)
i1 %cmp = #x1 (1)
i1 %rval = #x0 (0)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 64	alloc type: 0	address: 0
Block 1 >	size: 1152921504606846982	align: 0	alloc type: 0	address: 288230376151711744
Block 2 >	size: 2533283730662944	align: 4	alloc type: 0	address: 18063137816238142
Block 3 >	size: 439170037373854726	align: 2	alloc type: 0	address: 5818791456051036160
Block 4 >	size: 18013811976960510	align: 2	alloc type: 0	address: 268435456

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



------------------- SMT STATS -------------------
Num queries: 52
Num invalid: 0
Num skips:   0
Num trivial: 35 (40.2%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     19 (36.5%)
Num UNSAT:   33 (63.5%)

stderr:

+ : 'RUN: at line 2'
+ /home/nlopes/alive2/scripts/opt-alive.sh -instcombine -S
+ /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