Executable semantics for CompCert C


The paper An Executable Semantics for CompCert C was presented at Certified Programs and Proofs 2012. Here are slides from the presentation and a preprint version of the paper. The original publication is available at www.springerlink.com, in LNCS 7679.

A set of slides from the November 2011 Scottish Programming Languages Seminar are available. They are a slightly better version of the slides below.

CompCert 1.9 has been released, which now features a interpreter with soundness and completeness proofs with respect to the non-deterministic semantics. Note that this is a fresh implementation which implements more external functions and features less hacks than the semantics here. Several of the bugs found with the work below have been fixed, too.

Also, I've recently added a -fcstrategy option, which implements the deterministic strategy from Cstrategy.v, and a completeness proof for it.

A set of slides from an internal talk are available, but read the ones above instead.

This work started after I noticed a problem in my executable semantics for Clight language developed for the CerCo project. I wanted to reproduce the problem with CompCert's semantics, and explore writing executable semantics for the more demanding CompCert C language. The semantics makes use of existing executable parts of CompCert, in particular for environments and the memory model.

Building the development will produce a cexec executable as well as the compiler, which executes CompCert C following a leftmost-innermost evaluation strategy, with the exception of external functions other than malloc and free (and minimal hacks for memcpy and printf to allow Csmith generated programs to be run). The options for controlling preprocessing featured in the compiler are also available in the interpreter. The error reporting is very basic, although it is easy to use the Caml debugger to identify expressions that get stuck.

Individual successful steps of the executable semantics are shown to be equivalent to a step in the non-deterministic semantics, and steps of expression evaluation in the non-deterministic semantics are shown to be executed successfully with a suitable choice of evaluation strategy.

Other evaluation strategies can be plugged in, but are at present limited to those which can be expressed by a function which splits an expression into a subexpression and context. I'd like to change this in future.

The executable semantics are based on CompCert 1.8.2, and can be downloaded using one of the methods below. Note that a fix to the existing C semantics is included that allows calls using function pointers. A partial workaround for bugs involving e1 ? e2 : e3 conditional statements and void casts can be turned on with the -dworkaround option.

git clone http://homepages.inf.ed.ac.uk/bcampbe2/compcert/compcert-exec.gitWednesday, 09-May-2012 16:44:58 BST
tarball including git historyWednesday, 09-May-2012 16:31:51 BST
patch against 1.8.2Wednesday, 09-May-2012 16:31:33 BST


Last modified Wednesday, 19-Dec-2012 11:33:02 GMT.