[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [csmith-dev] compcert support

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:


Brian Campbell

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