Ein Compiler ist im Allgemeinen in drei Module unterteilt: Frontend, Middleend und Backend. Das Frontend überführt die Quellsprache in eine Zwischensprache, die von Quellsprache und Zielarchitektur unabhängig ist. Anschließend kann das Middleend eine Reihe von Optimierungen auf der Zwischensprache anwenden. Das Backend transformiert die optimierte Zwischensprache in eine Maschinen-abhängige Darstellung, behandelt die beschränkten Ressourcen der Zielarchitektur und gibt Maschinencode aus.

Während die Zwischensprache aus einfachen Operationen aufgebaut ist, orientieren sich die Operationen der Maschinen-abhängigen Darstellung an den Maschinenbefehlen der Zielarchitektur. Die Aufgabe der Befehlsauswahl ist es, die Operationen der Zwischensprache in Maschinenbefehle zu transformieren. Oft werden dabei mehrere Zwischensprachoperationen zu einem Maschinenbefehl zusammengefasst. Diese Muster von Zwischensprachoperationen werden von den Entwicklern des Compilers händisch spezifiziert und haben somit keinerlei Garantie auf Korrektheit oder Vollständigkeit.

In dieser Arbeit sollen die Muster stattdessen aus einer formalen Spezifikationen von Zwischensprach- und Maschinenoperationen generiert werden. Zur Sicherstellung der Korrektheit soll ein SMT-Solver zum Einsatz kommen. Weiterhin soll aus den erzeugten Mustern eine Befehlsauswahl für den libFirm-Compiler generiert werden, die im Rahmen der Arbeit evaluiert werden soll.



Veröffentlichungen

Veröffentlichung

Synthesizing Instruction Selection

Betreuer

Ehemalige Mitarbeiter
Dipl.-Inform. Sebastian Buchwald

Studenten

Ehemalige Mitarbeiter
M.Sc. Andreas Fried