New:
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.git | Wednesday, 09-May-2012 16:44:58 BST |
| tarball including git history | Wednesday, 09-May-2012 16:31:51 BST |
| patch against 1.8.2 | Wednesday, 09-May-2012 16:31:33 BST |
Last modified Wednesday, 19-Dec-2012 11:33:02 GMT.