Test Failure: Transforms/SLPVectorizer/vectorizable-functions-inseltpoison.ll

Test source: git

Comments: Alive2: no support for "vector-function-abi-variant"

Log:

Source: /bitbucket/nlopes/llvm/llvm/test/Transforms/SLPVectorizer/vectorizable-functions-inseltpoison.ll
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. SLPVectorizerPass

----------------------------------------
declare float @memread(float) nofree willreturn memory(read)

define <4 x float> @memread_4x(ptr %a) {
entry:
  %#0 = load <4 x float>, ptr %a, align 16
  %vecext = extractelement <4 x float> %#0, i32 0
  %#1 = tail call float @memread(float %vecext) NNaN nofree willreturn memory(read)
  %vecins = insertelement <4 x float> poison, float %#1, i32 0
  %vecext.1 = extractelement <4 x float> %#0, i32 1
  %#2 = tail call float @memread(float %vecext.1) NNaN nofree willreturn memory(read)
  %vecins.1 = insertelement <4 x float> %vecins, float %#2, i32 1
  %vecext.2 = extractelement <4 x float> %#0, i32 2
  %#3 = tail call float @memread(float %vecext.2) NNaN nofree willreturn memory(read)
  %vecins.2 = insertelement <4 x float> %vecins.1, float %#3, i32 2
  %vecext.3 = extractelement <4 x float> %#0, i32 3
  %#4 = tail call float @memread(float %vecext.3) NNaN nofree willreturn memory(read)
  %vecins.3 = insertelement <4 x float> %vecins.2, float %#4, i32 3
  ret <4 x float> %vecins.3
}
Transformation seems to be correct! (syntactically equal)

-- 3. SLPVectorizerPass

----------------------------------------
declare float @memread(float) nofree willreturn memory(read)

define <4 x float> @memread_4x(ptr %a) {
entry:
  %#0 = load <4 x float>, ptr %a, align 16
  %vecext = extractelement <4 x float> %#0, i32 0
  %#1 = tail call float @memread(float %vecext) NNaN nofree willreturn memory(read)
  %vecins = insertelement <4 x float> poison, float %#1, i32 0
  %vecext.1 = extractelement <4 x float> %#0, i32 1
  %#2 = tail call float @memread(float %vecext.1) NNaN nofree willreturn memory(read)
  %vecins.1 = insertelement <4 x float> %vecins, float %#2, i32 1
  %vecext.2 = extractelement <4 x float> %#0, i32 2
  %#3 = tail call float @memread(float %vecext.2) NNaN nofree willreturn memory(read)
  %vecins.2 = insertelement <4 x float> %vecins.1, float %#3, i32 2
  %vecext.3 = extractelement <4 x float> %#0, i32 3
  %#4 = tail call float @memread(float %vecext.3) NNaN nofree willreturn memory(read)
  %vecins.3 = insertelement <4 x float> %vecins.2, float %#4, i32 3
  ret <4 x float> %vecins.3
}
=>
declare <4 x float> @vmemread(<4 x float>)

define <4 x float> @memread_4x(ptr %a) {
entry:
  %#0 = load <4 x float>, ptr %a, align 16
  %#1 = call <4 x float> @vmemread(<4 x float> %#0) NNaN
  ret <4 x float> %#1
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

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

Source:
<4 x float> %#0 = < poison, poison, poison, poison >
float %vecext = poison
float %#1 = #x00000000 (+0.0)
<4 x float> %vecins = < #x00000000 (+0.0), poison, poison, poison >
float %vecext.1 = poison
float %#2 = #x00000000 (+0.0)
<4 x float> %vecins.1 = < #x00000000 (+0.0), #x00000000 (+0.0), poison, poison >
float %vecext.2 = poison
float %#3 = #x00000000 (+0.0)
<4 x float> %vecins.2 = < #x00000000 (+0.0), #x00000000 (+0.0), #x00000000 (+0.0), poison >
float %vecext.3 = poison
float %#4 = #x00000000 (+0.0)
<4 x float> %vecins.3 = < #x00000000 (+0.0), #x00000000 (+0.0), #x00000000 (+0.0), #x00000000 (+0.0) >

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

Target:
<4 x float> %#0 = < poison, poison, poison, poison >
Function @vmemread triggered UB

TARGET MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 8	alloc type: 0	alive: false	address: #x00
Block 1 >	size: 8	align: 64	alloc type: 0	alive: true	address: #x40
Block 2 >	size: 0	align: 1	alloc type: 4	alive: true	address: #x02


Pass: SLPVectorizerPass
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=slp-vectorizer' '-S' '/bitbucket/nlopes/llvm/llvm/test/Transforms/SLPVectorizer/vectorizable-functions-inseltpoison.ll' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'

Wrote bitcode to: "/home/nlopes/alive2/build/logs/vectorizable-functions-inseltpoison_nWHTJsSq_273N.bc"

------------------- SMT STATS -------------------
Num queries: 48
Num invalid: 0
Num skips:   0
Num trivial: 15 (23.8%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     37 (77.1%)
Num UNSAT:   11 (22.9%)
Alive2: Transform doesn't verify; aborting!

stderr:

Transforms/SLPVectorizer/vectorizable-functions-inseltpoison.ll' FAILED ********************
Exit Code: 2

Command Output (stdout):
--
# RUN: at line 2
/home/nlopes/alive2/build/opt-alive.sh -passes=slp-vectorizer -S /bitbucket/nlopes/llvm/llvm/test/Transforms/SLPVectorizer/vectorizable-functions-inseltpoison.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/SLPVectorizer/vectorizable-functions-inseltpoison.ll
# executed command: /home/nlopes/alive2/build/opt-alive.sh -passes=slp-vectorizer -S /bitbucket/nlopes/llvm/llvm/test/Transforms/SLPVectorizer/vectorizable-functions-inseltpoison.ll
# .---command stderr------------
# `-----------------------------
# error: command failed with exit status: 1
# executed command: /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/SLPVectorizer/vectorizable-functions-inseltpoison.ll
# .---command stderr------------
# | FileCheck error: '<stdin>' is empty.
# | FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/SLPVectorizer/vectorizable-functions-inseltpoison.ll
# `-----------------------------
# error: command failed with exit status: 2

--

<-- Back