Formal Verification of an SSA-based Middle-end for CompCert - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2011

Formal Verification of an SSA-based Middle-end for CompCert

Résumé

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 that is used by many compilers. In fact, it has remained an open problem to verify formally an 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 in 2009: giving a simple and intuitive formal semantics to SSA, and leveraging the global properties of SSA to reason locally about program optimizations.

Domaines

Informatique
Fichier principal
Vignette du fichier
BDPreport.pdf (1.32 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00634702 , version 1 (22-10-2011)
inria-00634702 , version 2 (10-01-2012)
inria-00634702 , version 3 (02-04-2013)

Identifiants

  • HAL Id : inria-00634702 , version 3

Citer

Gilles Barthe, Delphine Demange, David Pichardie. Formal Verification of an SSA-based Middle-end for CompCert. [University works] 2011. ⟨inria-00634702v3⟩
974 Consultations
659 Téléchargements

Partager

Gmail Facebook X LinkedIn More