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

Test source: git

Comments: Alive2 bug in input ptr refinement

Log:

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)
ERROR: Unsupported instruction:   call void @llvm.memcpy.p0i8.p1i8.i64(i8* align 4 %b, i8 addrspace(1)* align 4 bitcast ([4 x float] addrspace(1)* @I to i8 addrspace(1)*), i64 16, i1 false)
ERROR: Unsupported instruction:   call void @llvm.memcpy.p0i8.p1i8.i64(i8* align 4 %b, i8 addrspace(1)* align 4 bitcast ([4 x float] addrspace(1)* @I to i8 addrspace(1)*), i64 16, i1 true)

----------------------------------------
@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, exceptions=ignore
  %tmp13 = fadd float %tmp11, 0.000000, exceptions=ignore
  %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, exceptions=ignore
  %tmp23 = fadd float %tmp21, %tmp13, exceptions=ignore
  %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, exceptions=ignore
  %tmp33 = fadd float %tmp31, %tmp23, exceptions=ignore
  %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, exceptions=ignore
  %tmp43 = fadd float %tmp41, %tmp33, exceptions=ignore
  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, exceptions=ignore
  %tmp13 = fadd float %tmp11, 0.000000, exceptions=ignore
  %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, exceptions=ignore
  %tmp23 = fadd float %tmp21, %tmp13, exceptions=ignore
  %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, exceptions=ignore
  %tmp33 = fadd float %tmp31, %tmp23, exceptions=ignore
  %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, exceptions=ignore
  %tmp43 = fadd float %tmp41, %tmp33, exceptions=ignore
  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:
  >> Jump to %0
* %A = pointer(local, block_id=2, offset=0)
* %a = pointer(local, block_id=2, 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

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

Target:
  >> Jump to %0
* %__constexpr_0 = pointer(non-local, block_id=1, offset=0)
void = UB triggered!



------------------- SMT STATS -------------------
Num queries: 16
Num invalid: 0
Num skips:   0
Num trivial: 17 (51.5%)
Num timeout: 1 (6.2%)
Num errors:  0 (0.0%)
Num SAT:     13 (81.2%)
Num UNSAT:   2 (12.5%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 2'
+ /home/nuno/llvm/build/bin/FileCheck /home/nuno/llvm/llvm/test/Transforms/InstCombine/memcpy-from-global.ll
+ /home/nuno/alive2/build/opt-alive.sh -passes=instcombine -S

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /home/nuno/llvm/build/bin/FileCheck /home/nuno/llvm/llvm/test/Transforms/InstCombine/memcpy-from-global.ll

 

<-- Back