Minotaur is a superoptimizer for LLVM's intermediate representation that focuses on integer SIMD instructions, both portable and specific to x86-64. We created it to attack problems in finding missing peephole optimizations for SIMD instructions-this is challenging because there are many such instructions and they can be semantically complex. Minotaur runs a hybrid synthesis algorithm where instructions are enumerated concretely, but literal constants are generated by the solver. We use Alive2 as a verification engine; to do this we modified it to support synthesis and also to support a large subset of Intel's vector instruction sets (SSE, AVX, AVX2, and AVX-512). Minotaur finds many profitable optimizations that are missing from LLVM. It achieves limited speedups on the integer parts of SPEC CPU2017, around 1.3%, and it speeds up the test suite for the libYUV library by 2.2%, on average, and by 1.64x maximum, when targeting an Intel Cascade Lake processor.

翻译：Minotaur 是一款针对LLVM中间表示的超优化器，专注于整数SIMD指令，既支持可移植指令也支持x86-64特定指令。我们开发该工具旨在解决SIMD指令缺失窥孔优化的难题——此类指令数量众多且语义复杂。Minotaur 采用混合综合算法：枚举具体指令，但字面常量由求解器生成。我们使用Alive2作为验证引擎，对其进行了改进以支持综合过程，并支持英特尔向量指令集（SSE、AVX、AVX2和AVX-512）的较大部分。Minotaur 发现了LLVM中缺失的多项高效优化方案。在SPEC CPU2017整数测试集上可实现约1.3%的有限加速；针对Intel Cascade Lake处理器时，对libYUV库的测试集平均加速2.2%，最高加速达1.64倍。