Test Failure: Transforms/SandboxVectorizer/bottomup_basic.ll

Test source: git

Log:

Source: /bitbucket/nlopes/llvm/llvm/test/Transforms/SandboxVectorizer/bottomup_basic.ll
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. SandboxVectorizerPass

----------------------------------------
define void @store_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  store float %ld0, ptr %ptr0, align 4
  store float %ld1, ptr %ptr1, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 3. SandboxVectorizerPass

----------------------------------------
define void @store_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  store float %ld0, ptr %ptr0, align 4
  store float %ld1, ptr %ptr1, align 4
  ret void
}
=>
define void @store_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %VecL = load <2 x float>, ptr %ptr0, align 4
  store <2 x float> %VecL, ptr %ptr0, align 4
  ret void
}
Transformation seems to be correct!

-- 4. PassManager<Function> : Skipping NOP
-- 5. PassManager<Function> : Skipping NOP
-- 6. SandboxVectorizerPass

----------------------------------------
define void @store_fpext_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ptrd0 = gep ptr %ptr, 8 x i32 0
  %ptrd1 = gep ptr %ptr, 8 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  %fpext0 = fpext float %ld0 to double
  %fpext1 = fpext float %ld1 to double
  store double %fpext0, ptr %ptrd0, align 8
  store double %fpext1, ptr %ptrd1, align 8
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 7. SandboxVectorizerPass

----------------------------------------
define void @store_fpext_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ptrd0 = gep ptr %ptr, 8 x i32 0
  %ptrd1 = gep ptr %ptr, 8 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  %fpext0 = fpext float %ld0 to double
  %fpext1 = fpext float %ld1 to double
  store double %fpext0, ptr %ptrd0, align 8
  store double %fpext1, ptr %ptrd1, align 8
  ret void
}
=>
define void @store_fpext_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptrd0 = gep ptr %ptr, 8 x i32 0
  %VecL = load <2 x float>, ptr %ptr0, align 4
  %VCast = fpext <2 x float> %VecL to <2 x double>
  store <2 x double> %VCast, ptr %ptrd0, align 8
  ret void
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 8. PassManager<Function> : Skipping NOP
-- 9. PassManager<Function> : Skipping NOP
-- 10. SandboxVectorizerPass

----------------------------------------
define void @store_fcmp_zext_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ptrb0 = gep ptr %ptr, 4 x i32 0
  %ptrb1 = gep ptr %ptr, 4 x i32 1
  %ldB0 = load float, ptr %ptr0, align 4
  %ldB1 = load float, ptr %ptr1, align 4
  %ldA0 = load float, ptr %ptr0, align 4
  %ldA1 = load float, ptr %ptr1, align 4
  %fcmp0 = fcmp ogt float %ldA0, %ldB0
  %fcmp1 = fcmp ogt float %ldA1, %ldB1
  %zext0 = zext i1 %fcmp0 to i32
  %zext1 = zext i1 %fcmp1 to i32
  store i32 %zext0, ptr %ptrb0, align 4
  store i32 %zext1, ptr %ptrb1, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 11. SandboxVectorizerPass

----------------------------------------
define void @store_fcmp_zext_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ptrb0 = gep ptr %ptr, 4 x i32 0
  %ptrb1 = gep ptr %ptr, 4 x i32 1
  %ldB0 = load float, ptr %ptr0, align 4
  %ldB1 = load float, ptr %ptr1, align 4
  %ldA0 = load float, ptr %ptr0, align 4
  %ldA1 = load float, ptr %ptr1, align 4
  %fcmp0 = fcmp ogt float %ldA0, %ldB0
  %fcmp1 = fcmp ogt float %ldA1, %ldB1
  %zext0 = zext i1 %fcmp0 to i32
  %zext1 = zext i1 %fcmp1 to i32
  store i32 %zext0, ptr %ptrb0, align 4
  store i32 %zext1, ptr %ptrb1, align 4
  ret void
}
=>
define void @store_fcmp_zext_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptrb0 = gep ptr %ptr, 4 x i32 0
  %VecL1 = load <2 x float>, ptr %ptr0, align 4
  %VecL = load <2 x float>, ptr %ptr0, align 4
  %VCmp = fcmp ogt <2 x float> %VecL, %VecL1
  %VCast = zext <2 x i1> %VCmp to <2 x i32>
  store <2 x i32> %VCast, ptr %ptrb0, align 4
  ret void
}
Transformation seems to be correct!

-- 12. PassManager<Function> : Skipping NOP
-- 13. PassManager<Function> : Skipping NOP
-- 14. SandboxVectorizerPass

----------------------------------------
define void @store_fadd_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ldA0 = load float, ptr %ptr0, align 4
  %ldA1 = load float, ptr %ptr1, align 4
  %ldB0 = load float, ptr %ptr0, align 4
  %ldB1 = load float, ptr %ptr1, align 4
  %fadd0 = fadd float %ldA0, %ldB0
  %fadd1 = fadd float %ldA1, %ldB1
  store float %fadd0, ptr %ptr0, align 4
  store float %fadd1, ptr %ptr1, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 15. SandboxVectorizerPass

----------------------------------------
define void @store_fadd_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ldA0 = load float, ptr %ptr0, align 4
  %ldA1 = load float, ptr %ptr1, align 4
  %ldB0 = load float, ptr %ptr0, align 4
  %ldB1 = load float, ptr %ptr1, align 4
  %fadd0 = fadd float %ldA0, %ldB0
  %fadd1 = fadd float %ldA1, %ldB1
  store float %fadd0, ptr %ptr0, align 4
  store float %fadd1, ptr %ptr1, align 4
  ret void
}
=>
define void @store_fadd_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %VecL = load <2 x float>, ptr %ptr0, align 4
  %VecL1 = load <2 x float>, ptr %ptr0, align 4
  %Vec = fadd <2 x float> %VecL, %VecL1
  store <2 x float> %Vec, ptr %ptr0, align 4
  ret void
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 16. PassManager<Function> : Skipping NOP
-- 17. PassManager<Function> : Skipping NOP
-- 18. SandboxVectorizerPass

----------------------------------------
define void @store_fneg_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  %fneg0 = fneg float %ld0
  %fneg1 = fneg float %ld1
  store float %fneg0, ptr %ptr0, align 4
  store float %fneg1, ptr %ptr1, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 19. SandboxVectorizerPass

----------------------------------------
define void @store_fneg_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  %fneg0 = fneg float %ld0
  %fneg1 = fneg float %ld1
  store float %fneg0, ptr %ptr0, align 4
  store float %fneg1, ptr %ptr1, align 4
  ret void
}
=>
define void @store_fneg_load(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %VecL = load <2 x float>, ptr %ptr0, align 4
  %Vec = fneg <2 x float> %VecL
  store <2 x float> %Vec, ptr %ptr0, align 4
  ret void
}
Transformation seems to be correct!

-- 20. PassManager<Function> : Skipping NOP
-- 21. PassManager<Function> : Skipping NOP
-- 22. SandboxVectorizerPass

----------------------------------------
define float @scalars_with_external_uses_not_dead(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  store float %ld0, ptr %ptr0, align 4
  store float %ld1, ptr %ptr1, align 4
  %user = fneg float %ld1
  ret float %ld0
}
Transformation seems to be correct! (syntactically equal)

-- 23. SandboxVectorizerPass

----------------------------------------
define float @scalars_with_external_uses_not_dead(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  store float %ld0, ptr %ptr0, align 4
  store float %ld1, ptr %ptr1, align 4
  ret float %ld0
}
=>
define float @scalars_with_external_uses_not_dead(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  %VecL = load <2 x float>, ptr %ptr0, align 4
  store <2 x float> %VecL, ptr %ptr0, align 4
  ret float %ld0
}
Transformation seems to be correct!

-- 24. PassManager<Function> : Skipping NOP
-- 25. PassManager<Function> : Skipping NOP
-- 26. SandboxVectorizerPass

----------------------------------------
define void @pack_scalars(ptr %ptr, ptr %ptr2) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr2, align 4
  store float %ld0, ptr %ptr0, align 4
  store float %ld1, ptr %ptr1, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 27. SandboxVectorizerPass

----------------------------------------
define void @pack_scalars(ptr %ptr, ptr %ptr2) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr2, align 4
  store float %ld0, ptr %ptr0, align 4
  store float %ld1, ptr %ptr1, align 4
  ret void
}
=>
define void @pack_scalars(ptr %ptr, ptr %ptr2) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr2, align 4
  %Pack = insertelement <2 x float> poison, float %ld0, i32 0
  %Pack1 = insertelement <2 x float> %Pack, float %ld1, i32 1
  store <2 x float> %Pack1, ptr %ptr0, align 4
  ret void
}
Transformation seems to be correct!

-- 28. PassManager<Function> : Skipping NOP
-- 29. PassManager<Function> : Skipping NOP
-- 30. SandboxVectorizerPass

----------------------------------------
declare void @foo()

define void @cant_vectorize_seeds(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  store float %ld1, ptr %ptr1, align 4
  call void @foo()
  store float %ld1, ptr %ptr1, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 31. SandboxVectorizerPass

----------------------------------------
declare void @foo()

define void @cant_vectorize_seeds(ptr %ptr) {
#0:
  %ptr0 = gep ptr %ptr, 4 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 1
  %ld0 = load float, ptr %ptr0, align 4
  %ld1 = load float, ptr %ptr1, align 4
  store float %ld1, ptr %ptr1, align 4
  call void @foo()
  store float %ld1, ptr %ptr1, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 32. PassManager<Function> : Skipping NOP
-- 33. PassManager<Function> : Skipping NOP
-- 34. SandboxVectorizerPass

----------------------------------------
define void @pack_vectors(ptr %ptr, ptr %ptr2) {
#0:
  %ptr0 = gep ptr %ptr, 8 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 2
  %ld0 = load <2 x float>, ptr %ptr0, align 8
  %ld1 = load float, ptr %ptr2, align 4
  store <2 x float> %ld0, ptr %ptr0, align 8
  store float %ld1, ptr %ptr1, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 35. SandboxVectorizerPass

----------------------------------------
define void @pack_vectors(ptr %ptr, ptr %ptr2) {
#0:
  %ptr0 = gep ptr %ptr, 8 x i32 0
  %ptr1 = gep ptr %ptr, 4 x i32 2
  %ld0 = load <2 x float>, ptr %ptr0, align 8
  %ld1 = load float, ptr %ptr2, align 4
  store <2 x float> %ld0, ptr %ptr0, align 8
  store float %ld1, ptr %ptr1, align 4
  ret void
}
=>
define void @pack_vectors(ptr %ptr, ptr %ptr2) {
#0:
  %ptr0 = gep ptr %ptr, 8 x i32 0
  %ld0 = load <2 x float>, ptr %ptr0, align 8
  %ld1 = load float, ptr %ptr2, align 4
  %VPack = extractelement <2 x float> %ld0, i32 0
  %VPack1 = insertelement <3 x float> poison, float %VPack, i32 0
  %VPack2 = extractelement <2 x float> %ld0, i32 1
  %VPack3 = insertelement <3 x float> %VPack1, float %VPack2, i32 1
  %Pack = insertelement <3 x float> %VPack3, float %ld1, i32 2
  store <3 x float> %Pack, ptr %ptr0, align 8
  ret void
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
ptr %ptr = pointer(non-local, block_id=1, offset=0) / Address=#x08
ptr %ptr2 = pointer(non-local, block_id=1, offset=0) / Address=#x08

Source:
ptr %ptr0 = pointer(non-local, block_id=1, offset=0) / Address=#x08
ptr %ptr1 = pointer(non-local, block_id=1, offset=8) / Address=#x10
<2 x float> %ld0 = < poison, poison >
float %ld1 = poison

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 4	alloc type: 0	alive: false	address: 0
Block 1 >	size: 12	align: 1	alloc type: 0	alive: true	address: 8
Block 2 >	size: 0	align: 2	alloc type: 0	alive: true	address: 8

Target:
ptr %ptr0 = pointer(non-local, block_id=1, offset=0) / Address=#x08
<2 x float> %ld0 = < poison, poison >
float %ld1 = poison
float %VPack = poison
<3 x float> %VPack1 = < poison, poison, poison >
float %VPack2 = poison
<3 x float> %VPack3 = < poison, poison, poison >
<3 x float> %Pack = < poison, poison, poison >
void = UB triggered!


Pass: SandboxVectorizerPass
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=sandbox-vectorizer' '-sbvec-passes=bottom-up-vec<>' '/bitbucket/nlopes/llvm/llvm/test/Transforms/SandboxVectorizer/bottomup_basic.ll' '-S' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/bottomup_basic_CpF2w6Ch_JctH.bc"


------------------- SMT STATS -------------------
Num queries: 68
Num invalid: 0
Num skips:   0
Num trivial: 33 (32.7%)
Num timeout: 2 (2.9%)
Num errors:  0 (0.0%)
Num SAT:     41 (60.3%)
Num UNSAT:   25 (36.8%)
Alive2: Transform doesn't verify; aborting!

stderr:

RUN: at line 2: /home/nlopes/alive2/build/opt-alive.sh -passes=sandbox-vectorizer -sbvec-passes="bottom-up-vec<>" /bitbucket/nlopes/llvm/llvm/test/Transforms/SandboxVectorizer/bottomup_basic.ll -S | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/SandboxVectorizer/bottomup_basic.ll
+ /home/nlopes/alive2/build/opt-alive.sh -passes=sandbox-vectorizer '-sbvec-passes=bottom-up-vec<>' /bitbucket/nlopes/llvm/llvm/test/Transforms/SandboxVectorizer/bottomup_basic.ll -S
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/SandboxVectorizer/bottomup_basic.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/SandboxVectorizer/bottomup_basic.ll

<-- Back