A Precise and Abstract Memory Model for C Using Symbolic Values

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 : Real life C programs are often written using C dialects which, for the ISO C standard, have undefined behaviours. In particular, according to the ISO C standard, reading an uninitialised variable has an undefined behaviour and low-level pointer operations are implementation defined. We propose a formal semantics which gives a well-defined meaning to those behaviours for the C dialect of the CompCert compiler. Our semantics builds upon a novel memory model leveraging a notion of symbolic values. Symbolic values are used by the semantics to delay the evaluation of operations and are normalised lazily to genuine values when needed. We show that the most precise normalisation is computable and that a slightly relaxed normalisation can be efficiently implemented using an SMT solver. The semantics is executable and our experiments show that the enhancements of our semantics are mandatory to give a meaning to low-levels idioms such as those found in the allocation functions of a C standard library.
Type de document :
Communication dans un congrès
12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. Springer, 8858, pp.449 - 468, 2014, LNCS. 〈10.1007/978-3-319-12736-1_24〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01093312
Contributeur : Frédéric Besson <>
Soumis le : mercredi 10 décembre 2014 - 14:54:16
Dernière modification le : mardi 16 janvier 2018 - 15:54:15
Document(s) archivé(s) le : mercredi 11 mars 2015 - 11:15:14

Fichier

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

Identifiants

Citation

Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Precise and Abstract Memory Model for C Using Symbolic Values. 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. Springer, 8858, pp.449 - 468, 2014, LNCS. 〈10.1007/978-3-319-12736-1_24〉. 〈hal-01093312〉

Partager

Métriques

Consultations de la notice

580

Téléchargements de fichiers

106