Synthesizing an Instruction Selection Rule Library from Semantic Specifications

Our paper “Synthesizing an Instruction Selection Rule Library from Semantic Specifications” has been presented at CGO 2018.

Abstract

Instruction selection is the part of a compiler that transforms intermediate representation (IR) code into machine code. Instruction selectors build on a library of hundreds if not thousands of rules. Creating and maintaining these rules is a tedious and error-prone manual process.

In this paper, we present a fully automatic approach to create provably correct rule libraries from formal specifications of the instruction set architecture and the compiler IR. We use a hybrid approach that combines enumerative techniques with template-based counterexample-guided inductive synthesis (CEGIS). Thereby, we overcome several shortcomings of existing approaches, which were not able to handle complex instructions in a reasonable amount of time. In particular, we efficiently model memory operations.

Our tool synthesized a large part of the integer arithmetic rules for the x86 architecture within a few days where existing techniques could not deliver a substantial rule library within weeks. Using the rule library, we generate a prototype instruction selector that produces code on par with a manually-tuned instruction selector. Furthermore, using 63012 test cases generated from the rule library, we identified 29498 rules that both Clang and GCC miss.

Artifact

Our synthesis tool accompanies the paper as a freely available artifact. The artifact is hosted on Zenodo under the DOI 10.5281/zenodo.1095055. Please see our paper's artifact appendix for documentation.

Unsupported Instruction Selection Rules in State-of-the-Art Compilers

Links to Godbolt's Compiler Explorer