Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection

Compiling programs to an instruction set architecture (ISA) requires a set of rewrite rules that map patterns consisting of compiler instructions to patterns consisting of ISA instructions. We synthesize such rules by constructing SMT queries, where solutions represent two functionally equivalent programs. These two programs are interpreted as an instruction selection rewrite rule. Furthermore, we address existing work's limitations by developing a set of optimizations that prevent synthesis of duplicate rules, composite rules, and higher-cost rules. We evaluate our algorithm on multiple ISAs. Without our optimizations, the majority of synthesized rewrite rules are either duplicates or higher cost. With our optimizations, we only synthesize unique and lowest-cost rules, resulting in total speedups of up to 212x.