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

Test source: git

Comments: Alive2 bug in input ptr refinement

Log:

Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
ERROR: Unsupported instruction:   %a.cast = addrspacecast ptr %A to ptr addrspace(1)
ERROR: Unsupported instruction:   call void @llvm.memcpy.p0.p1.i64(ptr align 4 %A, ptr addrspace(1) align 4 addr
ERROR: Unsupported instruction:   call void @llvm.memcpy.p0.p1.i64(ptr align 4 %Al, ptr addrspace(1) align 4 add
ERROR: Unsupported instruction:   call void @llvm.memcpy.p0.p1.i64(ptr align 4 %A, ptr addrspace(1) align 4 addr
ERROR: Unsupported instruction:   call void @llvm.memcpy.p0.p1.i64(ptr align 4 %a, ptr addrspace(1) align 4 @I, 
ERROR: Unsupported instruction:   call void @llvm.memcpy.p0.p1.i64(ptr align 4 %a, ptr addrspace(1) align 4 @I, 
ERROR: Unsupported attribute: noalias
-- 1. PassManager<Function> : Skipping NOP
-- 2. InstCombinePass

----------------------------------------
@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 }, ptr @C.0.1248, align 32
  br label %entry

entry:
  %lookupTable = alloca i64 512, align 16
  memcpy ptr %lookupTable align 16, ptr @C.0.1248 align 16, i64 512
  %tmp3 = shl i32 %hash, 2
  %tmp5 = and i32 %tmp3, 124
  %tmp753 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %tmp5
  %tmp9 = load float, ptr %tmp753, align 4
  %tmp11 = fmul float %tmp9, %x
  %tmp13 = fadd float %tmp11, 0.000000
  %tmp17.sum52 = or i32 %tmp5, 1
  %tmp1851 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %tmp17.sum52
  %tmp19 = load float, ptr %tmp1851, align 4
  %tmp21 = fmul float %tmp19, %y
  %tmp23 = fadd float %tmp21, %tmp13
  %tmp27.sum50 = or i32 %tmp5, 2
  %tmp2849 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %tmp27.sum50
  %tmp29 = load float, ptr %tmp2849, align 4
  %tmp31 = fmul float %tmp29, %z
  %tmp33 = fadd float %tmp31, %tmp23
  %tmp37.sum48 = or i32 %tmp5, 3
  %tmp3847 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %tmp37.sum48
  %tmp39 = load float, ptr %tmp3847, align 4
  %tmp41 = fmul float %tmp39, %w
  %tmp43 = fadd float %tmp41, %tmp33
  ret float %tmp43
}
Transformation seems to be correct! (syntactically equal)

-- 3. InstCombinePass

----------------------------------------
@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 }, ptr @C.0.1248, align 32
  br label %entry

entry:
  %lookupTable = alloca i64 512, align 16
  memcpy ptr %lookupTable align 16, ptr @C.0.1248 align 32, i64 512
  %tmp3 = shl i32 %hash, 2
  %tmp5 = and i32 %tmp3, 124
  %tmp753 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %tmp5
  %tmp9 = load float, ptr %tmp753, align 4
  %tmp11 = fmul float %tmp9, %x
  %tmp13 = fadd float %tmp11, 0.000000
  %tmp17.sum52 = or i32 %tmp5, 1
  %tmp1851 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %tmp17.sum52
  %tmp19 = load float, ptr %tmp1851, align 4
  %tmp21 = fmul float %tmp19, %y
  %tmp23 = fadd float %tmp21, %tmp13
  %tmp27.sum50 = or i32 %tmp5, 2
  %tmp2849 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %tmp27.sum50
  %tmp29 = load float, ptr %tmp2849, align 4
  %tmp31 = fmul float %tmp29, %z
  %tmp33 = fadd float %tmp31, %tmp23
  %tmp37.sum48 = or i32 %tmp5, 3
  %tmp3847 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %tmp37.sum48
  %tmp39 = load float, ptr %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 }, ptr @C.0.1248, align 32
  br label %entry

entry:
  %tmp3 = shl i32 %hash, 2
  %tmp5 = and i32 %tmp3, 124
  %#0 = zext nneg i32 %tmp5 to i64
  %tmp753 = gep ptr @C.0.1248, 512 x i64 0, 4 x i64 %#0
  %tmp9 = load float, ptr %tmp753, align 4
  %tmp11 = fmul float %tmp9, %x
  %tmp13 = fadd float %tmp11, 0.000000
  %tmp17.sum52 = or disjoint i32 %tmp5, 1
  %#1 = zext nneg i32 %tmp17.sum52 to i64
  %tmp1851 = gep ptr @C.0.1248, 512 x i64 0, 4 x i64 %#1
  %tmp19 = load float, ptr %tmp1851, align 4
  %tmp21 = fmul float %tmp19, %y
  %tmp23 = fadd float %tmp21, %tmp13
  %tmp27.sum50 = or disjoint i32 %tmp5, 2
  %#2 = zext nneg i32 %tmp27.sum50 to i64
  %tmp2849 = gep ptr @C.0.1248, 512 x i64 0, 4 x i64 %#2
  %tmp29 = load float, ptr %tmp2849, align 4
  %tmp31 = fmul float %tmp29, %z
  %tmp33 = fadd float %tmp31, %tmp23
  %tmp37.sum48 = or disjoint i32 %tmp5, 3
  %#3 = zext nneg i32 %tmp37.sum48 to i64
  %tmp3847 = gep ptr @C.0.1248, 512 x i64 0, 4 x i64 %#3
  %tmp39 = load float, ptr %tmp3847, align 4
  %tmp41 = fmul float %tmp39, %w
  %tmp43 = fadd float %tmp41, %tmp33
  ret float %tmp43
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 4. PassManager<Function> : Skipping NOP
-- 5. PassManager<Function> : Skipping NOP
-- 6. InstCombinePass

----------------------------------------
declare void @bar(ptr)

@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 } }, ptr @G, align 16
  br label %#0

#0:
  %A = alloca i64 124, align 8
  %B = alloca i64 124, align 8
  memcpy ptr %A align 4, ptr @G align 4, i64 124
  memcpy ptr %B align 4, ptr %A align 4, i64 124
  call void @bar(ptr %B)
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 7. InstCombinePass

----------------------------------------
declare void @bar(ptr)

@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 } }, ptr @G, align 16
  br label %#0

#0:
  %A = alloca i64 124, align 8
  %B = alloca i64 124, align 8
  memcpy ptr %A align 8, ptr @G align 16, i64 124
  memcpy ptr %B align 8, ptr %A align 8, i64 124
  call void @bar(ptr %B)
  ret void
}
=>
declare void @bar(ptr)

@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 } }, ptr @G, align 16
  br label %#0

#0:
  %B = alloca i64 124, align 8
  memcpy ptr %B align 8, ptr @G align 16, i64 124
  call void @bar(nonnull ptr %B)
  ret void
}
Transformation seems to be correct!

-- 8. PassManager<Function> : Skipping NOP
-- 9. PassManager<Function> : Skipping NOP
-- 10. InstCombinePass

----------------------------------------
declare void @bar(ptr)

@G = constant 124 bytes, align 16

define void @test2_no_null_opt() null_pointer_is_valid {
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 } }, ptr @G, align 16
  br label %#0

#0:
  %A = alloca i64 124, align 8
  %B = alloca i64 124, align 8
  memcpy ptr %A align 4, ptr @G align 4, i64 124
  memcpy ptr %B align 4, ptr %A align 4, i64 124
  call void @bar(ptr %B)
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 11. InstCombinePass

----------------------------------------
declare void @bar(ptr)

@G = constant 124 bytes, align 16

define void @test2_no_null_opt() null_pointer_is_valid {
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 } }, ptr @G, align 16
  br label %#0

#0:
  %A = alloca i64 124, align 8
  %B = alloca i64 124, align 8
  memcpy ptr %A align 8, ptr @G align 16, i64 124
  memcpy ptr %B align 8, ptr %A align 8, i64 124
  call void @bar(ptr %B)
  ret void
}
=>
declare void @bar(ptr)

@G = constant 124 bytes, align 16

define void @test2_no_null_opt() null_pointer_is_valid {
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 } }, ptr @G, align 16
  br label %#0

#0:
  %B = alloca i64 124, align 8
  memcpy ptr %B align 8, ptr @G align 16, i64 124
  call void @bar(nonnull ptr %B)
  ret void
}
Transformation seems to be correct!

-- 12. PassManager<Function> : Skipping NOP
-- 13. PassManager<Function> : Skipping NOP
ERROR: Unsupported instruction:   %a.cast = addrspacecast ptr %A to ptr addrspace(1)
-- 14. InstCombinePass
ERROR: Unsupported instruction:   %a.cast = addrspacecast ptr %A to ptr addrspace(1)
-- 15. InstCombinePass
ERROR: Unsupported instruction:   %b.cast = addrspacecast ptr %B to ptr addrspace(1)
-- 16. PassManager<Function> : Skipping NOP
ERROR: Unsupported instruction:   %b.cast = addrspacecast ptr %B to ptr addrspace(1)
-- 17. PassManager<Function> : Skipping NOP
-- 18. InstCombinePass

----------------------------------------
declare void @bar(ptr)

@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 } }, ptr @G, align 16
  br label %#0

#0:
  %A = alloca i64 124, align 8
  memcpy ptr %A align 4, ptr @G align 4, i64 124
  call void @bar(ptr %A) nofree memory(read)
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 19. InstCombinePass

----------------------------------------
declare void @bar(ptr)

@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 } }, ptr @G, align 16
  br label %#0

#0:
  %A = alloca i64 124, align 8
  memcpy ptr %A align 8, ptr @G align 16, i64 124
  call void @bar(ptr %A) nofree memory(read)
  ret void
}
=>
declare void @bar(ptr)

@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 } }, ptr @G, align 16
  br label %#0

#0:
  call void @bar(nonnull ptr @G) nofree memory(read)
  ret void
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:

Source:
  >> Jump to %#0
ptr %A = null
void = function did not return!

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 1	alloc type: 0	alive: false	address: 0
Block 1 >	size: 124	align: 16	alloc type: 0	alive: true	address: 192	const

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

Target:
  >> Jump to %#0
Function @bar triggered UB


Pass: InstCombinePass
Command line: '/home/nlopes/llvm/build/bin/opt' '-load=/home/nlopes/alive2/build/tv/tv.so' '-load-pass-plugin=/home/nlopes/alive2/build/tv/tv.so' '-tv-exit-on-error' '-passes=instcombine' '-S' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/in_wJ2qC42j_ydwo.bc"


------------------- SMT STATS -------------------
Num queries: 22
Num invalid: 0
Num skips:   0
Num trivial: 13 (37.1%)
Num timeout: 2 (9.1%)
Num errors:  0 (0.0%)
Num SAT:     14 (63.6%)
Num UNSAT:   6 (27.3%)
Alive2: Transform doesn't verify; aborting!

stderr:

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

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

<-- Back