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
  %t3 = shl i32 %hash, 2
  %t5 = and i32 %t3, 124
  %t753 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %t5
  %t9 = load float, ptr %t753, align 4
  %t11 = fmul float %t9, %x
  %t13 = fadd float %t11, 0.000000
  %t17.sum52 = or i32 %t5, 1
  %t1851 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %t17.sum52
  %t19 = load float, ptr %t1851, align 4
  %t21 = fmul float %t19, %y
  %t23 = fadd float %t21, %t13
  %t27.sum50 = or i32 %t5, 2
  %t2849 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %t27.sum50
  %t29 = load float, ptr %t2849, align 4
  %t31 = fmul float %t29, %z
  %t33 = fadd float %t31, %t23
  %t37.sum48 = or i32 %t5, 3
  %t3847 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %t37.sum48
  %t39 = load float, ptr %t3847, align 4
  %t41 = fmul float %t39, %w
  %t43 = fadd float %t41, %t33
  ret float %t43
}
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
  %t3 = shl i32 %hash, 2
  %t5 = and i32 %t3, 124
  %t753 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %t5
  %t9 = load float, ptr %t753, align 4
  %t11 = fmul float %t9, %x
  %t13 = fadd float %t11, 0.000000
  %t17.sum52 = or i32 %t5, 1
  %t1851 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %t17.sum52
  %t19 = load float, ptr %t1851, align 4
  %t21 = fmul float %t19, %y
  %t23 = fadd float %t21, %t13
  %t27.sum50 = or i32 %t5, 2
  %t2849 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %t27.sum50
  %t29 = load float, ptr %t2849, align 4
  %t31 = fmul float %t29, %z
  %t33 = fadd float %t31, %t23
  %t37.sum48 = or i32 %t5, 3
  %t3847 = gep ptr %lookupTable, 512 x i32 0, 4 x i32 %t37.sum48
  %t39 = load float, ptr %t3847, align 4
  %t41 = fmul float %t39, %w
  %t43 = fadd float %t41, %t33
  ret float %t43
}
=>
@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:
  %t3 = shl i32 %hash, 2
  %t5 = and i32 %t3, 124
  %#0 = zext nneg i32 %t5 to i64
  %t753 = gep ptr @C.0.1248, 512 x i64 0, 4 x i64 %#0
  %t9 = load float, ptr %t753, align 4
  %t11 = fmul float %t9, %x
  %t13 = fadd float %t11, 0.000000
  %t17.sum52 = or disjoint i32 %t5, 1
  %#1 = zext nneg i32 %t17.sum52 to i64
  %t1851 = gep ptr @C.0.1248, 512 x i64 0, 4 x i64 %#1
  %t19 = load float, ptr %t1851, align 4
  %t21 = fmul float %t19, %y
  %t23 = fadd float %t21, %t13
  %t27.sum50 = or disjoint i32 %t5, 2
  %#2 = zext nneg i32 %t27.sum50 to i64
  %t2849 = gep ptr @C.0.1248, 512 x i64 0, 4 x i64 %#2
  %t29 = load float, ptr %t2849, align 4
  %t31 = fmul float %t29, %z
  %t33 = fadd float %t31, %t23
  %t37.sum48 = or disjoint i32 %t5, 3
  %#3 = zext nneg i32 %t37.sum48 to i64
  %t3847 = gep ptr @C.0.1248, 512 x i64 0, 4 x i64 %#3
  %t39 = load float, ptr %t3847, align 4
  %t41 = fmul float %t39, %w
  %t43 = fadd float %t41, %t33
  ret float %t43
}
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:
UB triggered on br

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

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

Target:
UB triggered on br


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_G0GNwYxo_s4Ex.bc"


------------------- SMT STATS -------------------
Num queries: 17
Num invalid: 0
Num skips:   0
Num trivial: 12 (41.4%)
Num timeout: 2 (11.8%)
Num errors:  0 (0.0%)
Num SAT:     15 (88.2%)
Num UNSAT:   0 (0.0%)
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