A Formally Verified SSA-based Middle-end: Static Single Assignment meets CompCert

Gilles Barthe 1 Delphine Demange 2 David Pichardie 2
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : CompCert is a formally verified compiler that generates compact and efficient PowerPC, ARM and x86 code for a large and realistic subset of the C language. However, CompCert foregoes using Static Single Assignment (SSA), an intermediate representation that allows for writing simpler and faster optimizers, and is used by many compilers. In fact, it has remained an open problem to verify formally a SSA-based compiler middle-end. We report on a formally verified, SSA-based, middle-end for CompCert. Our middle-end performs conversion from CompCert intermediate form to SSA form, optimization of SSA programs, including Global Value Numbering, and transforming out of SSA to intermediate form. In addition to provide the first formally verified SSA-based middle-end, we address two problems raised by Leroy [13]: giving a simple and intuitive formal semantics to SSA, and leveraging the global properties of SSA to reason locally about program optimizations.
Type de document :
Communication dans un congrès
21th European Symposium on Programming, ESOP 2012, Mar 2012, Tallin, Estonia. Springer, 7211, pp.47-66, 2012, LNCS Programming Languages and Systems. 〈10.1007/978-3-642-28869-2_3〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01110783
Contributeur : Delphine Demange <>
Soumis le : mercredi 28 janvier 2015 - 22:01:20
Dernière modification le : jeudi 15 novembre 2018 - 11:57:41

Lien texte intégral

Identifiants

Citation

Gilles Barthe, Delphine Demange, David Pichardie. A Formally Verified SSA-based Middle-end: Static Single Assignment meets CompCert. 21th European Symposium on Programming, ESOP 2012, Mar 2012, Tallin, Estonia. Springer, 7211, pp.47-66, 2012, LNCS Programming Languages and Systems. 〈10.1007/978-3-642-28869-2_3〉. 〈hal-01110783〉

Partager

Métriques

Consultations de la notice

844