Add csyntaxgen tool for exporting CompCert C (Csyntax) AST as .v file #404
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adds the
csyntaxgen
tool, which takes a.c
file and exports the CompCert C AST (as defined inCsyntax.v
) to a.v
file.Produced by copy-pasting and adapting the
exportclight
andtests/clightgen
directories. I left these steps as separate commits to ease reviewing; of course, these should be squashed.Motivation
The Clight AST, as exported by the
clightgen
tool, is most appropriate when a human user needs to directly interact with the AST, such as when using the Verified Software Toolchain. For certain other use cases, however, the CompCert C AST may be more appropriate.Specifically, we want to prove soundness of CH2O with respect to CompCert C, and then obtain theorems about CompCert-compiled assembly code by first verifying the
.c
program using our VeriFast verification tool, which will eventually emit a Coq proof of correctness with respect to CH2O, and then porting this correctness statement to CompCert C using the soundness theorem, and then applying the CompCert correctness proof.The CH2O-CompCert soundness theorem will be based on a relation linking a CH2O Core C program to a corresponding CompCert C program. This relation is easier to define between CH2O Core C and CompCert C than between CH2O Core C and Clight, and easier to prove for the CH2O Core C AST generated from a .c file and the CompCert C AST generated from that .c file, because CompCert C is closer to the source code (and closer to CH2O Core C) than Clight.
In any case, we want to prove soundness of CH2O with respect to CompCert C, not Clight, because the former is a stronger statement.