Test source: git
Comments: Alive2 bug in input ptr refinement
Source: <stdin>
ERROR: Unsupported instruction: %a = addrspacecast %T* %A to i8 addrspace(1)*
ERROR: Unsupported instruction: call void @llvm.memcpy.p0i8.p1i8.i64(i8* align 4 %a, i8 addrspace(1)* align 4 addrspacecast (i8* getelementptr inbounds (%T, %T* @G, i32 0, i32 0) to i8 addrspace(1)*), i64 124, i1 false)
ERROR: Unsupported instruction: call void @llvm.memcpy.p0i8.p1i8.i64(i8* align 4 %a, i8 addrspace(1)* align 4 addrspacecast (i8* bitcast (%U* getelementptr inbounds ([2 x %U], [2 x %U]* @H, i64 0, i32 1) to i8*) to i8 addrspace(1)*), i64 20, i1 false)
ERROR: Unsupported instruction: call void @llvm.memcpy.p0i8.p1i8.i64(i8* align 4 %a, i8 addrspace(1)* align 4 addrspacecast (i8* bitcast (%U* getelementptr inbounds ([2 x %U], [2 x %U]* @H, i64 0, i32 1) to i8*) to i8 addrspace(1)*), i64 20, i1 false)
----------------------------------------
@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(nonnull * %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: %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 nofree
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 nofree
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: 1 alloc type: 0
Block 1 > size: 124 align: 16 alloc type: 0
Block 2 > size: 0 align: 1 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)
------------------- SMT STATS -------------------
Num queries: 8
Num invalid: 0
Num skips: 0
Num trivial: 17 (68.0%)
Num timeout: 1 (12.5%)
Num errors: 0 (0.0%)
Num SAT: 5 (62.5%)
Num UNSAT: 2 (25.0%)
Alive2: Transform doesn't verify; aborting!
+ : 'RUN: at line 2' + /home/nlopes/alive2/build/opt-alive.sh -instcombine -S + /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/InstCombine/memcpy-from-global.ll 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