Test Failure: Transforms/InstCombine/memcpy-from-global.ll

Test source: git

Comments: Alive2 bug in input ptr refinement

Log:

Source: <stdin>

----------------------------------------
@C.0.1248 = constant 512 bytes, align 32

define float @test1(i32 %hash, float %x, float %y, float %z, float %w) {
#init:
  store [128 x float] { -1.000000, -1.000000, -1.000000, 0.000000, -1.000000, -1.000000, 0.000000, -1.000000, -1.000000, -1.000000, 0.000000, 1.000000, -1.000000, -1.000000, 1.000000, 0.000000, -1.000000, 0.000000, -1.000000, -1.000000, -1.000000, 0.000000, -1.000000, 1.000000, -1.000000, 0.000000, 1.000000, -1.000000, -1.000000, 0.000000, 1.000000, 1.000000, -1.000000, 1.000000, -1.000000, 0.000000, -1.000000, 1.000000, 0.000000, -1.000000, -1.000000, 1.000000, 0.000000, 1.000000, -1.000000, 1.000000, 1.000000, 0.000000, 0.000000, -1.000000, -1.000000, -1.000000, 0.000000, -1.000000, -1.000000, 1.000000, 0.000000, -1.000000, 1.000000, -1.000000, 0.000000, -1.000000, 1.000000, 1.000000, 1.000000, -1.000000, -1.000000, 0.000000, 1.000000, -1.000000, 0.000000, -1.000000, 1.000000, -1.000000, 0.000000, 1.000000, 1.000000, -1.000000, 1.000000, 0.000000, 1.000000, 0.000000, -1.000000, -1.000000, 1.000000, 0.000000, -1.000000, 1.000000, 1.000000, 0.000000, 1.000000, -1.000000, 1.000000, 0.000000, 1.000000, 1.000000, 1.000000, 1.000000, -1.000000, 0.000000, 1.000000, 1.000000, 0.000000, -1.000000, 1.000000, 1.000000, 0.000000, 1.000000, 1.000000, 1.000000, 1.000000, 0.000000, 0.000000, 1.000000, -1.000000, -1.000000, 0.000000, 1.000000, -1.000000, 1.000000, 0.000000, 1.000000, 1.000000, -1.000000, 0.000000, 1.000000, 1.000000, 1.000000 }, * @C.0.1248, align 32
  br label %entry

%entry:
  %lookupTable = alloca i64 512, align 16
  %lookupTable1 = bitcast * %lookupTable to *
  %__constexpr_0 = bitcast * @C.0.1248 to *
  memcpy * %lookupTable1 align 16, * %__constexpr_0 align 16, i64 512
  %tmp3 = shl i32 %hash, 2
  %tmp5 = and i32 %tmp3, 124
  %tmp753 = gep * %lookupTable, 512 x i32 0, 4 x i32 %tmp5
  %tmp9 = load float, * %tmp753, align 4
  %tmp11 = fmul float %tmp9, %x
  %tmp13 = fadd float %tmp11, 0.000000
  %tmp17.sum52 = or i32 %tmp5, 1
  %tmp1851 = gep * %lookupTable, 512 x i32 0, 4 x i32 %tmp17.sum52
  %tmp19 = load float, * %tmp1851, align 4
  %tmp21 = fmul float %tmp19, %y
  %tmp23 = fadd float %tmp21, %tmp13
  %tmp27.sum50 = or i32 %tmp5, 2
  %tmp2849 = gep * %lookupTable, 512 x i32 0, 4 x i32 %tmp27.sum50
  %tmp29 = load float, * %tmp2849, align 4
  %tmp31 = fmul float %tmp29, %z
  %tmp33 = fadd float %tmp31, %tmp23
  %tmp37.sum48 = or i32 %tmp5, 3
  %tmp3847 = gep * %lookupTable, 512 x i32 0, 4 x i32 %tmp37.sum48
  %tmp39 = load float, * %tmp3847, align 4
  %tmp41 = fmul float %tmp39, %w
  %tmp43 = fadd float %tmp41, %tmp33
  ret float %tmp43
}
=>
@C.0.1248 = constant 512 bytes, align 32

define float @test1(i32 %hash, float %x, float %y, float %z, float %w) {
#init:
  store [128 x float] { -1.000000, -1.000000, -1.000000, 0.000000, -1.000000, -1.000000, 0.000000, -1.000000, -1.000000, -1.000000, 0.000000, 1.000000, -1.000000, -1.000000, 1.000000, 0.000000, -1.000000, 0.000000, -1.000000, -1.000000, -1.000000, 0.000000, -1.000000, 1.000000, -1.000000, 0.000000, 1.000000, -1.000000, -1.000000, 0.000000, 1.000000, 1.000000, -1.000000, 1.000000, -1.000000, 0.000000, -1.000000, 1.000000, 0.000000, -1.000000, -1.000000, 1.000000, 0.000000, 1.000000, -1.000000, 1.000000, 1.000000, 0.000000, 0.000000, -1.000000, -1.000000, -1.000000, 0.000000, -1.000000, -1.000000, 1.000000, 0.000000, -1.000000, 1.000000, -1.000000, 0.000000, -1.000000, 1.000000, 1.000000, 1.000000, -1.000000, -1.000000, 0.000000, 1.000000, -1.000000, 0.000000, -1.000000, 1.000000, -1.000000, 0.000000, 1.000000, 1.000000, -1.000000, 1.000000, 0.000000, 1.000000, 0.000000, -1.000000, -1.000000, 1.000000, 0.000000, -1.000000, 1.000000, 1.000000, 0.000000, 1.000000, -1.000000, 1.000000, 0.000000, 1.000000, 1.000000, 1.000000, 1.000000, -1.000000, 0.000000, 1.000000, 1.000000, 0.000000, -1.000000, 1.000000, 1.000000, 0.000000, 1.000000, 1.000000, 1.000000, 1.000000, 0.000000, 0.000000, 1.000000, -1.000000, -1.000000, 0.000000, 1.000000, -1.000000, 1.000000, 0.000000, 1.000000, 1.000000, -1.000000, 0.000000, 1.000000, 1.000000, 1.000000 }, * @C.0.1248, align 32
  br label %entry

%entry:
  %tmp3 = shl i32 %hash, 2
  %tmp5 = and i32 %tmp3, 124
  %0 = zext i32 %tmp5 to i64
  %tmp753 = gep * @C.0.1248, 512 x i64 0, 4 x i64 %0
  %tmp9 = load float, * %tmp753, align 16
  %tmp11 = fmul float %tmp9, %x
  %tmp13 = fadd float %tmp11, 0.000000
  %tmp17.sum52 = or i32 %tmp5, 1
  %1 = zext i32 %tmp17.sum52 to i64
  %tmp1851 = gep * @C.0.1248, 512 x i64 0, 4 x i64 %1
  %tmp19 = load float, * %tmp1851, align 4
  %tmp21 = fmul float %tmp19, %y
  %tmp23 = fadd float %tmp21, %tmp13
  %tmp27.sum50 = or i32 %tmp5, 2
  %2 = zext i32 %tmp27.sum50 to i64
  %tmp2849 = gep * @C.0.1248, 512 x i64 0, 4 x i64 %2
  %tmp29 = load float, * %tmp2849, align 8
  %tmp31 = fmul float %tmp29, %z
  %tmp33 = fadd float %tmp31, %tmp23
  %tmp37.sum48 = or i32 %tmp5, 3
  %3 = zext i32 %tmp37.sum48 to i64
  %tmp3847 = gep * @C.0.1248, 512 x i64 0, 4 x i64 %3
  %tmp39 = load float, * %tmp3847, align 4
  %tmp41 = fmul float %tmp39, %w
  %tmp43 = fadd float %tmp41, %tmp33
  ret float %tmp43
}
Transformation doesn't verify!
ERROR: Timeout


----------------------------------------
@G = constant 124 bytes, align 16

define void @test2() {
#init:
  store {i8, [123 x i8]} { 1, { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 } }, * @G, align 16
  br label %0

%0:
  %A = alloca i64 124, align 8
  %B = alloca i64 124, align 8
  %a = bitcast * %A to *
  %b = bitcast * %B to *
  %__constexpr_0 = gep inbounds * @G, 124 x i32 0, 1 x i64 0
  memcpy * %a align 4, * %__constexpr_0 align 4, i64 124
  memcpy * %b align 4, * %a align 4, i64 124
  call void @bar(* %b)
  ret void
}
=>
@G = constant 124 bytes, align 16

define void @test2() {
#init:
  store {i8, [123 x i8]} { 1, { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 } }, * @G, align 16
  br label %0

%0:
  %B1 = alloca i64 124, align 8
  %B1.sub = gep inbounds * %B1, 124 x i64 0, 1 x i64 0
  %__constexpr_0 = gep inbounds * @G, 124 x i64 0, 1 x i64 0
  memcpy * %B1.sub align 8, * %__constexpr_0 align 16, i64 124
  call void @bar(* %B1.sub)
  ret void
}
Transformation seems to be correct!


----------------------------------------
@G = constant 124 bytes, align 16

define void @test2_no_null_opt() {
#init:
  store {i8, [123 x i8]} { 1, { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 } }, * @G, align 16
  br label %0

%0:
  %A = alloca i64 124, align 8
  %B = alloca i64 124, align 8
  %a = bitcast * %A to *
  %b = bitcast * %B to *
  %__constexpr_0 = gep inbounds * @G, 124 x i32 0, 1 x i64 0
  memcpy * %a align 4, * %__constexpr_0 align 4, i64 124
  memcpy * %b align 4, * %a align 4, i64 124
  call void @bar(* %b)
  ret void
}
=>
@G = constant 124 bytes, align 16

define void @test2_no_null_opt() {
#init:
  store {i8, [123 x i8]} { 1, { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 } }, * @G, align 16
  br label %0

%0:
  %B1 = alloca i64 124, align 8
  %B1.sub = gep inbounds * %B1, 124 x i64 0, 1 x i64 0
  %__constexpr_0 = gep inbounds * @G, 124 x i64 0, 1 x i64 0
  memcpy * %B1.sub align 8, * %__constexpr_0 align 16, i64 124
  call void @bar(* %B1.sub)
  ret void
}
Transformation seems to be correct!

ERROR: Unsupported instruction:   %a = addrspacecast %T* %A to i8 addrspace(1)*
ERROR: Unsupported instruction:   %b = addrspacecast i8* %B1.sub to i8 addrspace(1)*

----------------------------------------
@G = constant 124 bytes, align 16

define void @test3() {
#init:
  store {i8, [123 x i8]} { 1, { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 } }, * @G, align 16
  br label %0

%0:
  %A = alloca i64 124, align 8
  %a = bitcast * %A to *
  %__constexpr_0 = gep inbounds * @G, 124 x i32 0, 1 x i64 0
  memcpy * %a align 4, * %__constexpr_0 align 4, i64 124
  call void @bar(* %a) nowrite
  ret void
}
=>
@G = constant 124 bytes, align 16

define void @test3() {
#init:
  store {i8, [123 x i8]} { 1, { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 } }, * @G, align 16
  br label %0

%0:
  %__constexpr_0 = gep inbounds * @G, 124 x i64 0, 1 x i64 0
  call void @bar(* %__constexpr_0) nowrite
  ret void
}
Transformation doesn't verify!
ERROR: Source is more defined than target

Example:

Source:
* %A = pointer(local, block_id=4, offset=0)
* %a = pointer(local, block_id=4, offset=0)
* %__constexpr_0 = pointer(non-local, block_id=1, offset=0)

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

LOCAL BLOCKS:
Block 4 >	size: 124	align: 8	alloc type: 1

Target:
* %__constexpr_0 = pointer(non-local, block_id=1, offset=0)

TARGET MEMORY STATE
===================
LOCAL BLOCKS:
Block 4 >	size: 0	align: 64	alloc type: 0



------------------- SMT STATS -------------------
Num queries: 15
Num invalid: 0
Num skips:   0
Num trivial: 4 (21.1%)
Num timeout: 1 (6.7%)
Num errors:  0 (0.0%)
Num SAT:     5 (33.3%)
Num UNSAT:   9 (60.0%)

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/memcpy-from-global.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/memcpy-from-global.ll

<-- Back