Instruction selection in compiler backends traditionally depends on huge handwritten rule libraries that map IR patterns to target instruction sequences. Porting to new architectures or extending them for new hardware features is a very error-prone process,results in a significant development effort of a dedicated expert and even requires long-term commitment to apply patches for previously introduced bugs.

Automatic synthesis of these rule libraries from formal ISA and IR specifications eliminates the initial development effort and reduces the long-term maintenance effort, as synthesized rules are correct by construction. Prior work on synthesizing instruction selectors either requires synthesis times of multiple days or significantly falls behind the code quality of an optimizing handwritten backend - in both cases not applicable in practice.

We introduce a term canonicalization and indexing approach that accelerates finding rules on syntactically-similar bitvector terms while returning to SMT solving to ensure completeness in all other cases. Combined with search bounds derived from LLVM's existing pattern base, this reduces synthesis times from multiple days to under two hours for AArch64 and RISC-V.

We integrated the synthesized instruction selection rules for AArch64 and RISC-V into LLVM's GlobalISel backend and achieved almost on-par performance with the existing, industry-standard code generation backends in LLVM on the SPEC 2017 Integer benchmark suite (within 4% of LLVM GlobalISel).