Viele Analysen in einem Compiler lassen sich als Datenflussanalyse (DFA) ausdrücken (siehe z. B. Abschnitt 27 hier):
- Konstantenpropagation: Welche Werte sind schon zur Compilezeit bekannt?
- Value Range Propagation: In welchem Bereich wird ein Wert liegen?
- Const-Bit-Analyse: Ist etwas über die einzelnen Bits eines Wertes bekannt? Ist er z. B. gerade, passt in 16 Bit, …?
Aus theoretischer Sicht lassen sich DFAs als Instanz von abstrakter Interpretation begreifen. Die abstrakte Interpretation liefert sogar ein Verfahren, um eine optimale DFA zu konstruieren, das aber wegen seiner Ineffizienz nicht praktisch einsetzbar ist. Mit den Techniken der Programmsynthese (unterstützt durch immer bessere SMT-Solver und ähnliche Tools) ist es in einigen Fällen aber möglich, dieses Problem zu umgehen.
Das Thema dieser Arbeit ist bewusst offen gehalten. Folgende Forschungsrichtungen sind denkbar:
- Automatische Analyse der in einem bestehenden Compiler implementierten DFAs: Sind sie korrekt und so präzise wie möglich? Falls nicht, findet man Gegenbeispiele?
- Bei welchen Mustern im Code lohnt es sich, eine Sonderregel in der DFA einzuführen? Zum Beispiel ist das unterste Bit des Ergebnisses von x & (x - 1) immer 0, aber die Const-Bit-Analyse findet das nicht heraus, wenn sie die Operationen & und - getrennt betrachtet.
- Generieren einer effizienten DFA: Man kann die von der Theorie gegebene ineffiziente Implementierung als Spezifikation benutzen um mit Techniken der Programmsynthese eine effiziente DFA zu erzeugen.
Aufgabe:
- SMT-Solver-gestützte Analyse von DFAs als abstrakte Interpretationen
- Anwendung auf den Compilerbau
Voraussetzungen
- Interesse für Logik und formale Systeme
- Bereitschaft, sich in eine neue Theorie einzuarbeiten
- Vorkenntnisse in SAT-/SMT-Solving vorteilhaft
-
Neugierde statt Angst beim Anblick dieses kommutativen Diagramms:
Schlüsselworte
Compiler, Programmsynthese, Datenflussanalyse Betreuer
| Ehemalige Mitarbeiter |
|---|
| M.Sc. Andreas Fried |