CompCertS companion webpage

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.

The associated Coq development is available here.
You can also browse the development online.

Installation

To compile the development, the following software is required:


(If you are using the Nix package manager, a default.nix file is provided in the archive. All you need to do is launch nix-shell from the root directory, and all the dependencies should be automatically fetched.) The compilation procedure is fairly standard:
./configure ia32-linux # with the aforementioned dependences, should be alright, otherwise please contact me
make
            
This compilation takes quite a lot of time (about 30 minutes)

Running CompCertS

The CompCertS compiler can be called with the following command, where file.c is the C source file and exe is the output executable.

./ccomp file.c -c exe

The interpreter can be run also, provided the z3 SMT solver is installed:
./ccomp -interp file.c

Contact

If anything's wrong with the software, please email me at pierre.wilke@yale.edu.