Re: [csmith-dev] compcert support

[Brian Campbell <Brian.Campbell@ed.ac.uk>]

On 11/08/11 05:02, John Regehr wrote:
> I should add that I've been doing some CompCert testing lately w/o the
> special --ccomp flag to Csmith and it works fine. It seems that many
> CompCert limitations have disappeared in the last year or two. I was
> thinking about pulling all of the CompCert-specific code out of Csmith.

This might be a good opportunity for me to point out some work I've been 
doing recently on an executable version of the CompCert C semantics. 
This provides a single-step function in CIC which (with the exception of 
some "external" functions) matches the existing CompCert C semantics. 
More interesting for Csmith is the OCaml driver which runs the program 
using this function until it completes or gets stuck (a little like kcc, 
but specialized to CompCert C).

Using it with Csmith doesn't generate too many surprises (the problems 
are mostly to do with features not supported by CompCert C, such as 
structure passing).  There was an interesting bug in the compiler with 
the evaluation of conditional expressions that will be fixed in the next 
CompCert release - but it was encountered in the safe_math.h functions 
rather than the random code!

One Csmith feature that would be useful for testing this sort of thing 
would be options to turn off struct/union assignments, and structs on 
the left side of a comma operator.  I've had to turn comma off entirely 
because CompCert doesn't support structs on the left side.

If anyone is interested in the semantics, they can be found at the 
following address:

  http://homepages.inf.ed.ac.uk/bcampbe2/compcert/

--
Brian Campbell

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.