KIT | KIT-Bibliothek | Impressum

Synthesizing Instruction Selection

Buchwald, Sebastian; Fried, Andreas; Hack, Sebastian

Abstract: 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.


Zugehörige Institution(en) am KIT Lehrstuhl IPD Snelting (Lehrstuhl IPD Snelting)
Publikationstyp Forschungsbericht
Jahr 2017
Sprache Englisch
Identifikator DOI(KIT): 10.5445/IR/1000066092
ISSN: 2194-1629
URN: urn:nbn:de:swb:90-660921
KITopen ID: 1000066092
Verlag KIT, Karlsruhe
Umfang 15 S.
Serie KIT Scientific Working Papers ; 59
Lizenz CC BY-NC-SA 4.0: Creative Commons Namensnennung – Nicht kommerziell – Weitergabe unter gleichen Bedingungen 4.0 International
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page