Test Failure: Transforms/Scalarizer/min-bits.ll

Test source: git

Log:

Source: /bitbucket/nlopes/llvm/llvm/test/Transforms/Scalarizer/min-bits.ll
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. ScalarizerPass

----------------------------------------
define void @load_add_store_v2i16(ptr %pa, ptr %pb) {
#0:
  %a = load <2 x i16>, ptr %pa, align 8
  %b = load <2 x i16>, ptr %pb, align 8
  %c = add <2 x i16> %a, %b
  store <2 x i16> %c, ptr %pa, align 8
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 3. ScalarizerPass

----------------------------------------
define void @load_add_store_v2i16(ptr %pa, ptr %pb) {
#0:
  %a = load <2 x i16>, ptr %pa, align 8
  %b = load <2 x i16>, ptr %pb, align 8
  %c = add <2 x i16> %a, %b
  store <2 x i16> %c, ptr %pa, align 8
  ret void
}
=>
define void @load_add_store_v2i16(ptr %pa, ptr %pb) {
#0:
  %pb.i1 = gep ptr %pb, 2 x i32 1
  %a.i0 = load i16, ptr %pa, align 8
  %pa.i1 = gep ptr %pa, 2 x i32 1
  %a.i1 = load i16, ptr %pa.i1, align 2
  %b.i0 = load i16, ptr %pb, align 8
  %b.i1 = load i16, ptr %pb.i1, align 2
  %c.i0 = add i16 %a.i0, %b.i0
  %c.i1 = add i16 %a.i1, %b.i1
  store i16 %c.i0, ptr %pa, align 8
  store i16 %c.i1, ptr %pa.i1, align 2
  ret void
}
Transformation seems to be correct!

-- 4. DCEPass

----------------------------------------
define void @load_add_store_v2i16(ptr %pa, ptr %pb) {
#0:
  %pb.i1 = gep ptr %pb, 2 x i32 1
  %a.i0 = load i16, ptr %pa, align 8
  %pa.i1 = gep ptr %pa, 2 x i32 1
  %a.i1 = load i16, ptr %pa.i1, align 2
  %b.i0 = load i16, ptr %pb, align 8
  %b.i1 = load i16, ptr %pb.i1, align 2
  %c.i0 = add i16 %a.i0, %b.i0
  %c.i1 = add i16 %a.i1, %b.i1
  store i16 %c.i0, ptr %pa, align 8
  store i16 %c.i1, ptr %pa.i1, align 2
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 5. DCEPass

----------------------------------------
define void @load_add_store_v2i16(ptr %pa, ptr %pb) {
#0:
  %pb.i1 = gep ptr %pb, 2 x i32 1
  %a.i0 = load i16, ptr %pa, align 8
  %pa.i1 = gep ptr %pa, 2 x i32 1
  %a.i1 = load i16, ptr %pa.i1, align 2
  %b.i0 = load i16, ptr %pb, align 8
  %b.i1 = load i16, ptr %pb.i1, align 2
  %c.i0 = add i16 %a.i0, %b.i0
  %c.i1 = add i16 %a.i1, %b.i1
  store i16 %c.i0, ptr %pa, align 8
  store i16 %c.i1, ptr %pa.i1, align 2
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 6. PassManager<Function> : Skipping NOP
-- 7. PassManager<Function> : Skipping NOP
-- 8. ScalarizerPass

----------------------------------------
define void @load_add_store_v3i16(ptr %pa, ptr %pb) {
#0:
  %a = load <3 x i16>, ptr %pa, align 8
  %b = load <3 x i16>, ptr %pb, align 8
  %c = add <3 x i16> %a, %b
  store <3 x i16> %c, ptr %pa, align 8
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 9. ScalarizerPass

----------------------------------------
define void @load_add_store_v3i16(ptr %pa, ptr %pb) {
#0:
  %a = load <3 x i16>, ptr %pa, align 8
  %b = load <3 x i16>, ptr %pb, align 8
  %c = add <3 x i16> %a, %b
  store <3 x i16> %c, ptr %pa, align 8
  ret void
}
=>
define void @load_add_store_v3i16(ptr %pa, ptr %pb) {
#0:
  %pb.i1 = gep ptr %pb, 2 x i32 1
  %pb.i2 = gep ptr %pb, 2 x i32 2
  %a.i0 = load i16, ptr %pa, align 8
  %pa.i1 = gep ptr %pa, 2 x i32 1
  %a.i1 = load i16, ptr %pa.i1, align 2
  %pa.i2 = gep ptr %pa, 2 x i32 2
  %a.i2 = load i16, ptr %pa.i2, align 4
  %b.i0 = load i16, ptr %pb, align 8
  %b.i1 = load i16, ptr %pb.i1, align 2
  %b.i2 = load i16, ptr %pb.i2, align 4
  %c.i0 = add i16 %a.i0, %b.i0
  %c.i1 = add i16 %a.i1, %b.i1
  %c.i2 = add i16 %a.i2, %b.i2
  store i16 %c.i0, ptr %pa, align 8
  store i16 %c.i1, ptr %pa.i1, align 2
  store i16 %c.i2, ptr %pa.i2, align 4
  ret void
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 10. DCEPass

----------------------------------------
define void @load_add_store_v3i16(ptr %pa, ptr %pb) {
#0:
  %pb.i1 = gep ptr %pb, 2 x i32 1
  %pb.i2 = gep ptr %pb, 2 x i32 2
  %a.i0 = load i16, ptr %pa, align 8
  %pa.i1 = gep ptr %pa, 2 x i32 1
  %a.i1 = load i16, ptr %pa.i1, align 2
  %pa.i2 = gep ptr %pa, 2 x i32 2
  %a.i2 = load i16, ptr %pa.i2, align 4
  %b.i0 = load i16, ptr %pb, align 8
  %b.i1 = load i16, ptr %pb.i1, align 2
  %b.i2 = load i16, ptr %pb.i2, align 4
  %c.i0 = add i16 %a.i0, %b.i0
  %c.i1 = add i16 %a.i1, %b.i1
  %c.i2 = add i16 %a.i2, %b.i2
  store i16 %c.i0, ptr %pa, align 8
  store i16 %c.i1, ptr %pa.i1, align 2
  store i16 %c.i2, ptr %pa.i2, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 11. DCEPass

----------------------------------------
define void @load_add_store_v3i16(ptr %pa, ptr %pb) {
#0:
  %pb.i1 = gep ptr %pb, 2 x i32 1
  %pb.i2 = gep ptr %pb, 2 x i32 2
  %a.i0 = load i16, ptr %pa, align 8
  %pa.i1 = gep ptr %pa, 2 x i32 1
  %a.i1 = load i16, ptr %pa.i1, align 2
  %pa.i2 = gep ptr %pa, 2 x i32 2
  %a.i2 = load i16, ptr %pa.i2, align 4
  %b.i0 = load i16, ptr %pb, align 8
  %b.i1 = load i16, ptr %pb.i1, align 2
  %b.i2 = load i16, ptr %pb.i2, align 4
  %c.i0 = add i16 %a.i0, %b.i0
  %c.i1 = add i16 %a.i1, %b.i1
  %c.i2 = add i16 %a.i2, %b.i2
  store i16 %c.i0, ptr %pa, align 8
  store i16 %c.i1, ptr %pa.i1, align 2
  store i16 %c.i2, ptr %pa.i2, align 4
  ret void
}
Transformation seems to be correct! (syntactically equal)

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

----------------------------------------
define void @load_add_store_v4i16(ptr %pa, ptr %pb) {
#0:
  %a = load <4 x i16>, ptr %pa, align 8
  %b = load <4 x i16>, ptr %pb, align 8
  %c = add <4 x i16> %a, %b
  store <4 x i16> %c, ptr %pa, align 8
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 15. ScalarizerPass

----------------------------------------
define void @load_add_store_v4i16(ptr %pa, ptr %pb) {
#0:
  %a = load <4 x i16>, ptr %pa, align 8
  %b = load <4 x i16>, ptr %pb, align 8
  %c = add <4 x i16> %a, %b
  store <4 x i16> %c, ptr %pa, align 8
  ret void
}
=>
define void @load_add_store_v4i16(ptr %pa, ptr %pb) {
#0:
  %pb.i1 = gep ptr %pb, 2 x i32 1
  %pb.i2 = gep ptr %pb, 2 x i32 2
  %pb.i3 = gep ptr %pb, 2 x i32 3
  %a.i0 = load i16, ptr %pa, align 8
  %pa.i1 = gep ptr %pa, 2 x i32 1
  %a.i1 = load i16, ptr %pa.i1, align 2
  %pa.i2 = gep ptr %pa, 2 x i32 2
  %a.i2 = load i16, ptr %pa.i2, align 4
  %pa.i3 = gep ptr %pa, 2 x i32 3
  %a.i3 = load i16, ptr %pa.i3, align 2
  %b.i0 = load i16, ptr %pb, align 8
  %b.i1 = load i16, ptr %pb.i1, align 2
  %b.i2 = load i16, ptr %pb.i2, align 4
  %b.i3 = load i16, ptr %pb.i3, align 2
  %c.i0 = add i16 %a.i0, %b.i0
  %c.i1 = add i16 %a.i1, %b.i1
  %c.i2 = add i16 %a.i2, %b.i2
  %c.i3 = add i16 %a.i3, %b.i3
  store i16 %c.i0, ptr %pa, align 8
  store i16 %c.i1, ptr %pa.i1, align 2
  store i16 %c.i2, ptr %pa.i2, align 4
  store i16 %c.i3, ptr %pa.i3, align 2
  ret void
}
Transformation seems to be correct!

-- 16. DCEPass

----------------------------------------
define void @load_add_store_v4i16(ptr %pa, ptr %pb) {
#0:
  %pb.i1 = gep ptr %pb, 2 x i32 1
  %pb.i2 = gep ptr %pb, 2 x i32 2
  %pb.i3 = gep ptr %pb, 2 x i32 3
  %a.i0 = load i16, ptr %pa, align 8
  %pa.i1 = gep ptr %pa, 2 x i32 1
  %a.i1 = load i16, ptr %pa.i1, align 2
  %pa.i2 = gep ptr %pa, 2 x i32 2
  %a.i2 = load i16, ptr %pa.i2, align 4
  %pa.i3 = gep ptr %pa, 2 x i32 3
  %a.i3 = load i16, ptr %pa.i3, align 2
  %b.i0 = load i16, ptr %pb, align 8
  %b.i1 = load i16, ptr %pb.i1, align 2
  %b.i2 = load i16, ptr %pb.i2, align 4
  %b.i3 = load i16, ptr %pb.i3, align 2
  %c.i0 = add i16 %a.i0, %b.i0
  %c.i1 = add i16 %a.i1, %b.i1
  %c.i2 = add i16 %a.i2, %b.i2
  %c.i3 = add i16 %a.i3, %b.i3
  store i16 %c.i0, ptr %pa, align 8
  store i16 %c.i1, ptr %pa.i1, align 2
  store i16 %c.i2, ptr %pa.i2, align 4
  store i16 %c.i3, ptr %pa.i3, align 2
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 17. DCEPass

----------------------------------------
define void @load_add_store_v4i16(ptr %pa, ptr %pb) {
#0:
  %pb.i1 = gep ptr %pb, 2 x i32 1
  %pb.i2 = gep ptr %pb, 2 x i32 2
  %pb.i3 = gep ptr %pb, 2 x i32 3
  %a.i0 = load i16, ptr %pa, align 8
  %pa.i1 = gep ptr %pa, 2 x i32 1
  %a.i1 = load i16, ptr %pa.i1, align 2
  %pa.i2 = gep ptr %pa, 2 x i32 2
  %a.i2 = load i16, ptr %pa.i2, align 4
  %pa.i3 = gep ptr %pa, 2 x i32 3
  %a.i3 = load i16, ptr %pa.i3, align 2
  %b.i0 = load i16, ptr %pb, align 8
  %b.i1 = load i16, ptr %pb.i1, align 2
  %b.i2 = load i16, ptr %pb.i2, align 4
  %b.i3 = load i16, ptr %pb.i3, align 2
  %c.i0 = add i16 %a.i0, %b.i0
  %c.i1 = add i16 %a.i1, %b.i1
  %c.i2 = add i16 %a.i2, %b.i2
  %c.i3 = add i16 %a.i3, %b.i3
  store i16 %c.i0, ptr %pa, align 8
  store i16 %c.i1, ptr %pa.i1, align 2
  store i16 %c.i2, ptr %pa.i2, align 4
  store i16 %c.i3, ptr %pa.i3, align 2
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 18. PassManager<Function> : Skipping NOP
-- 19. PassManager<Function> : Skipping NOP
-- 20. ScalarizerPass

----------------------------------------
define void @load_add_store_v4i10(ptr %pa, ptr %pb) {
#0:
  %a = load <4 x i10>, ptr %pa, align 8
  %b = load <4 x i10>, ptr %pb, align 8
  %c = add <4 x i10> %a, %b
  store <4 x i10> %c, ptr %pa, align 8
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 21. ScalarizerPass

----------------------------------------
define void @load_add_store_v4i10(ptr %pa, ptr %pb) {
#0:
  %a = load <4 x i10>, ptr %pa, align 8
  %b = load <4 x i10>, ptr %pb, align 8
  %c = add <4 x i10> %a, %b
  store <4 x i10> %c, ptr %pa, align 8
  ret void
}
=>
define void @load_add_store_v4i10(ptr %pa, ptr %pb) {
#0:
  %a = load <4 x i10>, ptr %pa, align 8
  %a.i0 = extractelement <4 x i10> %a, i64 0
  %a.i1 = extractelement <4 x i10> %a, i64 1
  %a.i2 = extractelement <4 x i10> %a, i64 2
  %a.i3 = extractelement <4 x i10> %a, i64 3
  %b = load <4 x i10>, ptr %pb, align 8
  %b.i0 = extractelement <4 x i10> %b, i64 0
  %c.i0 = add i10 %a.i0, %b.i0
  %b.i1 = extractelement <4 x i10> %b, i64 1
  %c.i1 = add i10 %a.i1, %b.i1
  %b.i2 = extractelement <4 x i10> %b, i64 2
  %c.i2 = add i10 %a.i2, %b.i2
  %b.i3 = extractelement <4 x i10> %b, i64 3
  %c.i3 = add i10 %a.i3, %b.i3
  %c.upto0 = insertelement <4 x i10> poison, i10 %c.i0, i64 0
  %c.upto1 = insertelement <4 x i10> %c.upto0, i10 %c.i1, i64 1
  %c.upto2 = insertelement <4 x i10> %c.upto1, i10 %c.i2, i64 2
  %c = insertelement <4 x i10> %c.upto2, i10 %c.i3, i64 3
  store <4 x i10> %c, ptr %pa, align 8
  ret void
}
Transformation seems to be correct!

-- 22. DCEPass

----------------------------------------
define void @load_add_store_v4i10(ptr %pa, ptr %pb) {
#0:
  %a = load <4 x i10>, ptr %pa, align 8
  %a.i0 = extractelement <4 x i10> %a, i64 0
  %a.i1 = extractelement <4 x i10> %a, i64 1
  %a.i2 = extractelement <4 x i10> %a, i64 2
  %a.i3 = extractelement <4 x i10> %a, i64 3
  %b = load <4 x i10>, ptr %pb, align 8
  %b.i0 = extractelement <4 x i10> %b, i64 0
  %c.i0 = add i10 %a.i0, %b.i0
  %b.i1 = extractelement <4 x i10> %b, i64 1
  %c.i1 = add i10 %a.i1, %b.i1
  %b.i2 = extractelement <4 x i10> %b, i64 2
  %c.i2 = add i10 %a.i2, %b.i2
  %b.i3 = extractelement <4 x i10> %b, i64 3
  %c.i3 = add i10 %a.i3, %b.i3
  %c.upto0 = insertelement <4 x i10> poison, i10 %c.i0, i64 0
  %c.upto1 = insertelement <4 x i10> %c.upto0, i10 %c.i1, i64 1
  %c.upto2 = insertelement <4 x i10> %c.upto1, i10 %c.i2, i64 2
  %c = insertelement <4 x i10> %c.upto2, i10 %c.i3, i64 3
  store <4 x i10> %c, ptr %pa, align 8
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 23. DCEPass

----------------------------------------
define void @load_add_store_v4i10(ptr %pa, ptr %pb) {
#0:
  %a = load <4 x i10>, ptr %pa, align 8
  %a.i0 = extractelement <4 x i10> %a, i64 0
  %a.i1 = extractelement <4 x i10> %a, i64 1
  %a.i2 = extractelement <4 x i10> %a, i64 2
  %a.i3 = extractelement <4 x i10> %a, i64 3
  %b = load <4 x i10>, ptr %pb, align 8
  %b.i0 = extractelement <4 x i10> %b, i64 0
  %c.i0 = add i10 %a.i0, %b.i0
  %b.i1 = extractelement <4 x i10> %b, i64 1
  %c.i1 = add i10 %a.i1, %b.i1
  %b.i2 = extractelement <4 x i10> %b, i64 2
  %c.i2 = add i10 %a.i2, %b.i2
  %b.i3 = extractelement <4 x i10> %b, i64 3
  %c.i3 = add i10 %a.i3, %b.i3
  %c.upto0 = insertelement <4 x i10> poison, i10 %c.i0, i64 0
  %c.upto1 = insertelement <4 x i10> %c.upto0, i10 %c.i1, i64 1
  %c.upto2 = insertelement <4 x i10> %c.upto1, i10 %c.i2, i64 2
  %c = insertelement <4 x i10> %c.upto2, i10 %c.i3, i64 3
  store <4 x i10> %c, ptr %pa, align 8
  ret void
}
Transformation seems to be correct! (syntactically equal)

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

----------------------------------------
define <2 x half> @select_uniform_condition_v2f16(<2 x half> %a, <2 x half> %b, i1 %cc) {
#0:
  %r = select i1 %cc, <2 x half> %a, <2 x half> %b
  ret <2 x half> %r
}
Transformation seems to be correct! (syntactically equal)

-- 27. ScalarizerPass

----------------------------------------
define <2 x half> @select_uniform_condition_v2f16(<2 x half> %a, <2 x half> %b, i1 %cc) {
#0:
  %r = select i1 %cc, <2 x half> %a, <2 x half> %b
  ret <2 x half> %r
}
=>
define <2 x half> @select_uniform_condition_v2f16(<2 x half> %a, <2 x half> %b, i1 %cc) {
#0:
  %a.i0 = extractelement <2 x half> %a, i64 0
  %b.i0 = extractelement <2 x half> %b, i64 0
  %r.i0 = select i1 %cc, half %a.i0, half %b.i0
  %a.i1 = extractelement <2 x half> %a, i64 1
  %b.i1 = extractelement <2 x half> %b, i64 1
  %r.i1 = select i1 %cc, half %a.i1, half %b.i1
  %r.upto0 = insertelement <2 x half> poison, half %r.i0, i64 0
  %r = insertelement <2 x half> %r.upto0, half %r.i1, i64 1
  ret <2 x half> %r
}
Transformation doesn't verify! (unsound)
ERROR: Target is more poisonous than source

Example:
<2 x half> %a = < #x0000 (+0.0)	[based on undef value], poison >
<2 x half> %b = < poison, #x0000 (+0.0)	[based on undef value] >
i1 %cc = undef

Source:
<2 x half> %r = < poison, poison >

Target:
half %a.i0 = #x0000 (+0.0)
half %b.i0 = poison
half %r.i0 = poison
half %a.i1 = poison
half %b.i1 = #x0000 (+0.0)
half %r.i1 = poison
<2 x half> %r.upto0 = < poison, poison >
<2 x half> %r = < poison, poison >
Source value: < poison, poison >
Target value: < poison, poison >

Pass: ScalarizerPass
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' '/bitbucket/nlopes/llvm/llvm/test/Transforms/Scalarizer/min-bits.ll' '-passes=function(scalarizer<load-store;min-bits=16>,dce)' '-S' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/min-bits_d78lDHvN_p2Jg.bc"


------------------- SMT STATS -------------------
Num queries: 30
Num invalid: 0
Num skips:   0
Num trivial: 25 (45.5%)
Num timeout: 1 (3.3%)
Num errors:  0 (0.0%)
Num SAT:     20 (66.7%)
Num UNSAT:   9 (30.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/Scalarizer/min-bits.ll -passes='function(scalarizer<load-store;min-bits=16>,dce)' -S | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Scalarizer/min-bits.ll --check-prefixes=CHECK,MIN16
+ /home/nlopes/alive2/build/opt-alive.sh /bitbucket/nlopes/llvm/llvm/test/Transforms/Scalarizer/min-bits.ll '-passes=function(scalarizer<load-store;min-bits=16>,dce)' -S
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Scalarizer/min-bits.ll --check-prefixes=CHECK,MIN16

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Scalarizer/min-bits.ll --check-prefixes=CHECK,MIN16

NOTE: This test would pass if undef didn't exist!

<-- Back