-
Notifications
You must be signed in to change notification settings - Fork 108
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
X86: add support for SSE2/AVX2 intrinsics #1128
X86: add support for SSE2/AVX2 intrinsics #1128
Conversation
Add X86 vector SSE2/AVX2 intrinsics to the IR, complete with formal semantics for the verification flow. The work was originally authored by Zhengyang Liu <[email protected]>, and was motivated by the development of the Minotaur project [https://arxiv.org/abs/2306.00229].
We have 4 LLVM tests failing now (2 are duplicates). Could you please have a look? ; Transforms/InstCombine/X86/x86-pshufb-inseltpoison.ll
define <16 x i8> @splat_test(<16 x i8> %InVec) {
%#1 = x86_ssse3_pshuf_b_128 <16 x i8> %InVec, <16 x i8> { 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 }
ret <16 x i8> %#1
}
=>
define <16 x i8> @splat_test(<16 x i8> %InVec) {
%#1 = shufflevector <16 x i8> %InVec, <16 x i8> poison, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
ret <16 x i8> %#1
}
Transformation doesn't verify! (unsound)
ERROR: Value mismatch
Example:
<16 x i8> %InVec = < undef, poison, poison, poison, poison, poison, poison, poison, poison, poison, poison, poison, poison, poison, poison, poison >
Source:
<16 x i8> %#1 = < #x00 (0) [based on undef value], #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) >
Target:
<16 x i8> %#1 = < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x01 (1), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) >
Source value: < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) >
Target value: < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x01 (1), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) > And: ; Transforms/InstCombine/X86/x86-vector-shifts-inseltpoison.ll
define <8 x i16> @sse2_psra_w_128_masked(<8 x i16> %v, <8 x i16> %a) {
%#1 = and <8 x i16> %a, { 15, 0, 0, 0, poison, poison, poison, poison }
%#2 = x86_sse2_psra_w <8 x i16> %v, <8 x i16> %#1
ret <8 x i16> %#2
}
=>
define <8 x i16> @sse2_psra_w_128_masked(<8 x i16> %v, <8 x i16> %a) {
%#1 = and <8 x i16> %a, { 15, poison, poison, poison, poison, poison, poison, poison }
%#2 = shufflevector <8 x i16> %#1, <8 x i16> poison, 0, 0, 0, 0, 0, 0, 0, 0
%#3 = ashr <8 x i16> %v, %#2
ret <8 x i16> %#3
}
Transformation doesn't verify! (unsound)
ERROR: Value mismatch
Example:
<8 x i16> %v = < #x0000 (0), #x0000 (0), #x0000 (0), #x8ccc (36044, -29492), #x0000 (0), #x0000 (0), #x0000 (0), #xe333 (58163, -7373) >
<8 x i16> %a = < undef, #x0000 (0) [based on undef value], #x0000 (0) [based on undef value], #x0000 (0) [based on undef value], poison, poison, poison, poison >
Source:
<8 x i16> %#1 = < #x0000 (0) [based on undef value], #x0000 (0), #x0000 (0), #x0000 (0), poison, poison, poison, poison >
<8 x i16> %#2 = < #x0000 (0), #x0000 (0), #x0000 (0), #x8ccc (36044, -29492), #x0000 (0), #x0000 (0), #x0000 (0), #xe333 (58163, -7373) >
Target:
<8 x i16> %#1 = < #x0000 (0), poison, poison, poison, poison, poison, poison, poison >
<8 x i16> %#2 = < #x0000 (0), #x0000 (0), #x0000 (0), #x0002 (2), #x0000 (0), #x0000 (0), #x0000 (0), #x0000 (0) >
<8 x i16> %#3 = < #x0000 (0), #x0000 (0), #x0000 (0), #xe333 (58163, -7373), #x0000 (0), #x0000 (0), #x0000 (0), #xe333 (58163, -7373) >
Source value: < #x0000 (0), #x0000 (0), #x0000 (0), #x8ccc (36044, -29492), #x0000 (0), #x0000 (0), #x0000 (0), #xe333 (58163, -7373) >
Target value: < #x0000 (0), #x0000 (0), #x0000 (0), #xe333 (58163, -7373), #x0000 (0), #x0000 (0), #x0000 (0), #xe333 (58163, -7373) > |
I think this is a legitimate bug in the pshuf.b code in its handling of poison. Will investigate more soon.
I think this one is an undef-only bug in upstream LLVM, so I think it's a WONTFIX from upstream. If you disable-undef-input for this one, I think it should verify. |
Another one from x86-pshufb-inseltpoison.ll (no undef involved): define <32 x i8> @identity_test_avx2(<32 x i8> %InVec) {
#0:
%#1 = x86_avx2_pshuf_b <32 x i8> %InVec, <32 x i8> { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 }
ret <32 x i8> %#1
}
=>
define <32 x i8> @identity_test_avx2(<32 x i8> %InVec) {
#0:
ret <32 x i8> %InVec
}
Transformation doesn't verify! (unsound)
ERROR: Target is more poisonous than source
Example:
<32 x i8> %InVec = < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), poison, #x00 (0) >
Source:
<32 x i8> %#1 = < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) >
Target:
Source value: < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0) >
Target value: < #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), #x00 (0), poison, #x00 (0) > |
Co-authored-by: Zhengyang Liu <[email protected]>
So I spent a lot of time on this one, before figuring out that it's an undef-only upstream bug. |
Spent a lot of time on this one too, chasing false leads. I'm very confused now because this verifies:
|
well, and llc crashes when trying to compile this intrinsic... |
Please ignore this test. Somehow I had a bad llvm or z3 version, sorry 😔 |
Add X86 vector SSE2/AVX2 intrinsics to the IR, complete with formal semantics for the verification flow.
The work was originally authored by Zhengyang Liu [email protected], and was motivated by the development of the Minotaur project [https://arxiv.org/abs/2306.00229].