A verified compiler for a linear imperative / functional intermediate language

Abstract

This thesis describes the design of the verified compiler LVC. LVC's main novelty is the way its first-order, term-based intermediate language IL realizes the advantages of static single assignment (SSA) for verified compilation. IL is a term-based language not based on a control-flow graph (CFG) but defined in terms of an inductively defined syntax with lexically scoped mutually recursive function definitions. IL replaces the usual dominance-based SSA definition found in unverified and verified compilers with the novel notion of coherence. The main research question this thesis studies is whether IL with coherence offers a faithful implementation of SSA, and how the design influences the correctness invariants and the proofs in the verified compiler LVC. To study this question, we verify dead code elimination, several SSA-based value optimizations including sparse conditional constant propagation and SSA-based register allocation approach including spilling. In these case studies, IL with coherence provides the usual advantages of SSA and improves modularity of proofs. Furthermore, we propose a novel SSA construction algorithm based on coherence, and leverage the term structure of IL to obtain an inductive proof method for simulation proofs. LVC is implemented and verified with over 50,000 lines of code using the proof assistant Coq. To underline practicability of our approach, we integrate LVC with CompCert to obtain an executable compiler that generates PowerPC assembly code.

Diese Arbeit beschreibt das Design des verifizierten Compilers LVC. Die Hauptneuerung von LVC ist seine term-basierte Zwischensprache IL, die die Vorteile von static single assignment (SSA) für Verifikation nutzbar macht. IL ist eine term-basierte Sprache, die nicht auf einem Kontrollflussgraphen basiert, sondern auf einer induktiv definierten Syntax mit lexikalischen Variablen und verschränkt rekursiven Funktionen. IL ersetzt die übliche, dominanz-basierte SSA-Definition, die man in verifizierten und unverifizierten Compilern gleichermaßen findet, durch das neuartige Konzept der \emph{Kohärenz (coherence)}. Die Hauptforschungsfragen dieser Arbeit sind, ob IL zusammen mit Kohärenz als Implementierung von SSA geeignet ist, und wie ein IL-basiertes Design Korrektheitsinvarianten und Beweise am Beispiel von LVC beeinflusst. Um diese Fragen zu klären verifizieren wir verschiedene SSA-basierte Wertoptimierungen, wie beispielsweise sparse conditional constant propagation, und einen SSA-basierten Registerallokationsansatz mit spilling. In diesen Fallbeispielen bietet IL mit Kohärenz die üblichen Vorteile von SSA und verbessert die Modularität der Beweise. Darüberhinaus schlagen wir einen neuen, kohärenzbasierten SSA Aufbaualgorithmus vor und nutzen die Struktur von IL aus, um ein induktives Beweisverfahren für Simulationsbeweise zu entwickeln. LVC ist mit über 50.000 Zeilen mithilfe des Beweisassistenten Coq implementiert und verifiziert. Um die praktische Anwendbarkeit unseres Ansatzes zu zeigen, integrieren wir LVC mit dem verifizierten Compiler CompCert, wodurch wir einen ausführbaren Compiler erhalten, der PowerPC assembly code generiert.