A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data

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 guarantees that the target program behaves as the source program. Yet, source programs without a defined semantics do not benefit from this guarantee and could therefore be miscompiled. To reduce the possibility of a miscompilation, we propose a novel memory model for CompCert which gives a defined semantics to challenging features such as bitwise pointer arithmetics and access to uninitialised data. We evaluate our memory model both theoretically and experimentally. In our experiments, we identify pervasive low-level C idioms that require the additional expressiveness provided by our memory model. We also show that our memory model provably subsumes the existing CompCert memory model thus cross-validating both semantics. Our memory model relies on the core concepts of symbolic value and normalisa-tion. A symbolic value models a delayed computation and the normalisation turns, when possible, a symbolic value into a genuine value. We show how to tame the expressive power of the normalisation so that the memory model fits the proof framework of CompCert. We also adapt the proofs of correctness of the compiler passes performed by CompCert's front-end, thus demonstrating that our model is well-suited for proving compiler transformations.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2017, pp.1-48. 〈10.1007/s10817-017-9439-z〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01656895
Contributeur : Frédéric Besson <>
Soumis le : mercredi 6 décembre 2017 - 10:47:09
Dernière modification le : jeudi 15 novembre 2018 - 11:58:59

Fichier

jar-besson-blazy-wilke.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. Journal of Automated Reasoning, Springer Verlag, 2017, pp.1-48. 〈10.1007/s10817-017-9439-z〉. 〈hal-01656895〉

Partager

Métriques

Consultations de la notice

552

Téléchargements de fichiers

41