KIT | KIT-Bibliothek | Impressum | Datenschutz

Synthesizing Instruction Selection

Buchwald, Sebastian; Fried, Andreas; Hack, Sebastian

Instruction selection is the part in a compiler that transforms 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 using template-based counter-example guided synthesis (CEGIS). Thereby, we overcome several shortcomings of an existing SMT-based CEGIS approach, which was not applicable to our setting in the first place.We propose a novel way of handling memory operations and show how the search space can be iteratively explored to synthesize rules that are relevant for instruction selection.
Our approach 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. With respect to the runtime of the compiled programs, we show that the synthesized rules are close to a manually-tuned instruction selector.

Open Access Logo

Volltext §
DOI: 10.5445/IR/1000066092
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 2017
Sprache Englisch
Identifikator ISSN: 2194-1629
KITopen-ID: 1000066092
Verlag KIT, Karlsruhe
Umfang 15 S.
Serie KIT Scientific Working Papers ; 59
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page