intrinsics: add support for X86 vector intrinsics

[artagnon]

This 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]. This is a draft, asking the maintainers of Alive2 if there is interest in having this work be part of Alive2 upstream: if so, some work is required to clean up the patch, and break it up into digestible bits. I've fixed up Minotaur, and checked that all tests pass, when it is based on this work. The motivation to try and upstream this is so that we can get more eyes on this code to iron out the bugs: I plan to build upon this work to also support RISC-V vectors; my employer is very supportive of the project.

CC: @regehr

[regehr]

a few comments about this, in no particular order.

• we've done some focused randomized testing of these semantics, and also used them as part of Minotaur optimizing plenty of real applications, without seeing breakage. so we're decently confident in them, but of course there could still be bugs
• there's some maintenance burden here. I'm not sure if we can count on Zhengyang to help much, he's pretty busy lately. obviously the top-level decision about this rests on Nuno since he's the primary Alive2 developer and maintainer
• previously, when adding code to Alive2 that Nuno was not interested in maintaining, I've tried to make it as easily removable as possible, and then basically told Nuno that I would commit to either maintaining it or removing it. if we decide to proceed with this patch, I would suggest that we do something similar (but it's @artagnon maintaining it, not me)

[regehr]

in particular, the approximation stuff requires some careful thought

[artagnon]

I can't say that I'm familiar with X86 vector intrinsics, but it seems like a small additional burden over the RISC-V vector intrinsics, which I plan to add and maintain. The code is quite independent, and should be easy to strip out if it falls out of maintenance in the future. I will split out the parts that will also be useful for RISC-V vector intrinsics (FP approximation, FakeShuffle), so that the X86-specific parts can be reverted easily. An alternative is to maintain the X86 and RISC-V specific parts downstream, and just get the generic support merged: I'm quite open to this, as I don't think the mechanical intrinsic-matching code needs review.

Like John said, I do need the FP approximation part reviewed.

[nunoplopes]

This would be great to have!
I suggest creating a new file in the ir directory (e.g., x86_intrinsics.cpp) and move the new code there to avoid making the instr.cpp file even longer.
Also, please revert some of the unrelated changes like formatting and etc. And pay attention to missing/extra newlines a bit all over.

I suggest we start with the intrinsics that have precise semantics. Then work over the approximations, as these require more thought.

[artagnon]

I suggest we start with the intrinsics that have precise semantics. Then work over the approximations, as these require more thought.

I think you misunderstood: all the intrinsics have precise semantics, and the FP exactness is a configuration option that's not required for correctness of X86 intrinsics within Alive2: it is used by Minotaur to synthesize certain fp operations correctly.

Thanks for the suggestions; I've put up #1128 and #1129. With both applied, all tests in Minotaur pass. The rest of the code in this draft is unnecessary/dead.

[artagnon]

This option along with all its users is dead code.