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.
To compile the development, the following software is required:
./configure ia32-linux # with the aforementioned dependences, should be alright, otherwise please contact me makeThis compilation takes quite a lot of time (about 30 minutes)
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
./ccomp -interp file.c
If anything's wrong with the software, please email me at pierre.wilke@yale.edu.