HOME | ENGLISH | IMPRESSUM | KIT

Konferenzartikel: Verified Construction of Static Single Assignment Form

[buchwald16cc]Sebastian Buchwald, Denis Lohner, Sebastian Ullrich, Verified Construction of Static Single Assignment Form, Hermenegildo, Manuel (Ed.), 25th International Conference on Compiler Construction, pp. 67--76, ACM, 2016.

Zusammenfassung

Modern compilers use intermediate representations in static single assignment (SSA) form, which simplifies many optimizations. However, the high implementation complexity of efficient SSA construction algorithms poses a challenge to verified compilers. In this paper, we consider a variant of the recent SSA construction algorithm by Braun et al. that combines simplicity and efficiency, and is therefore a promising candidate to tackle this challenge. We prove the correctness of the algorithm using the theorem prover Isabelle/HOL. Furthermore, we prove that the algorithm constructs pruned SSA form and, in case of a reducible control flow graph, minimal SSA form. To the best of our knowledge, these are the first formal proofs regarding the quality of an SSA construction algorithm. Finally, we replace the SSA construction of the CompCertSSA project with code extracted by Isabelle's code generator to demonstrate the applicability to real world programs.

Download

  [PDF]   [DOI]   [Vortragsfolien]

BibTeX

Institutsinterne Autoren

Wissenschaftliche Mitarbeiter
Sebastian Buchwald
Denis Lohner
Sebastian Ullrich

Projekte

Projekt
InvasIC
libFirm
Quis-Custodiet
Verified Construction of Static Single Assignment Form