A Concrete Memory Model for CompCert

Frédéric Besson 1 Sandrine Blazy 1 Pierre Wilke 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Semantics preserving compilation of low-level C programs is challenging because their semantics is implementation defined according to the C standard. This paper presents the proof of an enhanced and more concrete memory model for the CompCert C compiler which assigns a definite meaning to more C programs. In our new formally verified memory model, pointers are still abstract but are nonetheless mapped to concrete 32-bit integers. Hence, the memory is finite and it is possible to reason about the binary encoding of pointers. We prove that the existing memory model is an abstraction of our more concrete model thus validating formally the soundness of CompCert's abstract semantics of pointers. We also show how to adapt the front-end of CompCert thus demonstrating that it should be feasible to port the whole compiler to our novel memory model.
Type de document :
Communication dans un congrès
Springer. ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. Lecture Notes in Computer Science (LNCS) (9236), pp.67-83, 2015, nteractive Theorem Proving. 〈10.1007/978-3-319-22102-1_5〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01194549
Contributeur : Sandrine Blazy <>
Soumis le : lundi 7 septembre 2015 - 11:17:28
Dernière modification le : mercredi 11 avril 2018 - 02:01:17
Document(s) archivé(s) le : mardi 8 décembre 2015 - 11:50:55

Fichier

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

Licence


Copyright (Tous droits réservés)

Identifiants

Citation

Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Concrete Memory Model for CompCert. Springer. ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. Lecture Notes in Computer Science (LNCS) (9236), pp.67-83, 2015, nteractive Theorem Proving. 〈10.1007/978-3-319-22102-1_5〉. 〈hal-01194549〉

Partager

Métriques

Consultations de la notice

614

Téléchargements de fichiers

75