CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics

Frédéric Besson 1 Sandrine Blazy 1 Pierre Wilke 2
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The CompCert C compiler provides the formal guarantee that the observable behaviour of the compiled code improves on the observable behaviour of the source code. In this paper, we present a formally verified C compiler, CompCertS, which is essentially the CompCert compiler, albeit with a stronger formal guarantee: it gives a semantics to more programs and ensures that the memory consumption is preserved by the compiler. CompCertS is based on an enhanced memory model where, unlike CompCert but like Gcc, the binary representation of pointers can be manipulated much like integers and where, unlike CompCert, allocation may fail if no memory is available. The whole proof of CompCertS is a significant proof-effort and we highlight the crux of the novel proofs of 12 passes of the back-end and a challenging proof of an essential optimising pass of the front-end.
Type de document :
Communication dans un congrès
ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. Springer, LNCS, 10499, pp.81-97, ITP 2017: Interactive Theorem Proving. 〈http://itp2017.cic.unb.br/〉. 〈10.1007/978-3-319-66107-0_6〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01656875
Contributeur : Frédéric Besson <>
Soumis le : mercredi 6 décembre 2017 - 10:34:43
Dernière modification le : jeudi 11 janvier 2018 - 06:28:14

Fichier

compcerts.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Frédéric Besson, Sandrine Blazy, Pierre Wilke. CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics. ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. Springer, LNCS, 10499, pp.81-97, ITP 2017: Interactive Theorem Proving. 〈http://itp2017.cic.unb.br/〉. 〈10.1007/978-3-319-66107-0_6〉. 〈hal-01656875〉

Partager

Métriques

Consultations de la notice

40

Téléchargements de fichiers

7