CompCert
The formally-verified C compiler.
Overview
The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, x86 and RISC-V processors.
The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code.
For more information on CompCert (supported platforms, supported C features, installation instructions, using the compiler, etc), please refer to the Web site and especially the user's manual.
Verimag-Kalray version
This is a special version with additions from Verimag and Kalray :
- A backend for the Coolidge VLIW KVX processor.
- Postpass scheduling passes for KVX, ARMv8 (aarch64) and RISC-V along with a preprocessing peephole optimizer.
- Improved subexpression elimination: two passes CSE2 and CSE3. Both go through loops and feature a small alias analysis.
- A generic prepass scheduling optimizer with a multi-purpose preprocessing front-end: rewritings, register renaming, if-lifting and some generic code transformations such as loop-rotation, loop-unrolling, or tail-duplication.
- A profiling system: see
OPTIM_PROFILING.md
for details. - Static branch prediction.
The branch prediction is basic, it annotates each
Icond
node by anoption bool
. ASome true
annotation indicates we predict the branch will be taken.Some false
indicates the fallthrough case is predicted.None
indicates we could not predict anything, and are not sure about which control will be preferred. -ftracelinearize
uses the branch prediction information to linearize LTL basic blocks in a slightly better way (in theLinearize
phase).- And some experimental features that are work in progress.
Please refer to the resources listed below for more information.
The people responsible for this version are
- Sylvain Boulmé (Grenoble-INP, Verimag)
- David Monniaux (CNRS, Verimag)
- Cyril Six (Kalray)
- Léo Gourdin (UGA, Verimag)
with contributions of:
- Justus Fasse (M2R UGA, now at KU Leuven).
- Pierre Goutagny and Nicolas Nardino (L3 ENS-Lyon).
Installing
Please follow the instructions in INSTALL.md
Papers, docs, etc on this CompCert version
- The documentation of the KVX backend Coq sources.
- A 5-minutes video by C. Six, presenting the postpass scheduling and the KVX backend (also on YouTube if you need subtitles).
- Certified and Efficient Instruction Scheduling, an OOPSLA'20 paper, by Six, Boulmé and Monniaux.
- Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion, a LCTES'21 paper, by Monniaux and Six.
- Formally Verified Superblock Scheduling, a CPP'22 paper, by Six, Gourdin, Boulmé, Monniaux, Fasse and Nardino.
- Optimized and formally-verified compilation for a VLIW processor, Phd Thesis of Cyril Six in 2021.
- Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) -- Chapters 1 to 3, Habilitation Thesis of Sylvain Boulmé in 2021.
- Code Transformations to Increase Prepass Scheduling Opportunities in CompCert, MSc Thesis of Justus Fasse in 2021.
- Register-Pressure-Aware Prepass-Scheduling for CompCert, BSc Thesis of Nicolas Nardino in 2021.
- Formally verified postpass scheduling with peephole optimization for AArch64, a short AFADL'21 paper, by Gourdin.
License
CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
A commercial version of CompCert, without this restriction and with
professional support and extra features, can be purchased from
AbsInt. See the file LICENSE
for more
information.
Copyright
The CompCert verified compiler is Copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and AbsInt Angewandte Informatik GmbH.
The additions are Copyright Grenoble-INP, CNRS and Kalray.
Contact
General discussions on CompCert take place on the compcert-users@inria.fr mailing list.
For inquiries on the commercial version of CompCert, please contact info@absint.com
For inquiries on the Verimag-specific additions, contact the researchers.