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.
You can also browse the development online here
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.