A Concrete Memory Model for CompCert

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 properties of the binary encoding of pointers can be reasoned about.
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.

Page last updated on: 2015-03-17

Paper

This work has been submitted to the 6th conference on Interactive Theorem Proving (ITP 2015).

Coq Development

Download the last stable version of the Coq development: [distrib.tar.gz]
(tested with OCaml 4.01.0 and Coq 8.4pl4)

You can also browse the development online here

Requirements

To compile our interpreter, you need to have OCaml and Coq installed on your machine.
You also need to have Z3 installed, if you want to run the interpreter.

Installation instructions

Note: You need OCaml and Coq installed on your machine.
  1. Download and extract the archive (tar xvzf distrib.tar.gz).
  2. Run ./configure ia32-linux, then run make to actually compile the code (this takes several minutes).

Usage

You can compile a C file into Cminor code with the following command: ./ccomp file.c. The output Cminor code is in the file file.cm.

You can also execute a C file in the interpreter with the following command: ./ccomp -interp file.c. This will run the C semantics on the program and return its output value.
You can trace all the semantic steps with the -trace option.