Design overview
CompCert is structured as a pipeline of 20 compilation passes that bridge the gap between C source files and object code, going through 11 intermediate languages. The passes can be grouped in 4 successive phases:
Parsing
This phase comprises preprocessing, tokenization, parsing into an ambiguous abstract syntax tree (AST), type-checking and scope resolution to obtain a precise, unambiguous AST and produce error and warning messages as appropriate. The LR(1) parser is automatically generated from the grammar of the C language by the Menhir parser generator, along with a Coq proof of correctness of the parser.
Frontend compiler
This phase re-checks the types inferred for expressions and determines an evaluation order among the several permitted by the C standard. Implicit type conversions, operator overloading, address computations, and other type-dependent behaviors are made explicit; loops are simplified. The output is code in Cminor, a simple untyped intermediate language featuring both structured (
if/else, loops) and unstructured (goto) control.Backend compiler
This phase comprises twelve passes, including all optimizations and most dependencies on the target architecture. The most important optimization performed is register allocation, which uses the sophisticated Iterated Register Coalescing algorithm. Other optimizations include function inlining, instruction selection, constant propagation, common subexpression elimination (CSE), and redundancy elimination. These optimizations implement several strategies to eliminate computations that are useless or redundant, or to turn them into equivalent but cheaper instruction sequences.
Assembling
The final phase takes the AST for assembly language produced by the backend, prints it in concrete assembly syntax, adds DWARF debugging information coming from the parser, and calls into an off-the-shelf assembler and linker to produce object files and executable files. For additional confidence, CompCert provides an independent tool called Valex that re-checks the ELF executable file produced by the linker against the assembly language AST produced by the backend.
The CompCert proof
The CompCert frontend and backend compilation passes are all formally proved to be free of miscompilation errors; as a consequence, so is their composition.
To state this property with mathematical precision, formal semantics are given for every source, intermediate and target language, from C to assembly. These semantics associate to each program the set of all its possible behaviors. Behaviors indicate whether the program terminates (normally by exiting, or abnormally by causing a runtime error such as dereferencing the null pointer) or runs forever.
Behaviors also contain a trace of all observable input/output actions performed by the program, such as system calls and accesses to “volatile” memory areas that could correspond to a memory-mapped I/O device.
To a first approximation, a compiler preserves semantics if the generated code has exactly the same set of observable behaviors as the source code (same termination properties, same I/O actions). This first approximation fails to account for two important degrees of freedom left to the compiler.
- First, the source program can have several possible behaviors: this is the case for C, which permits several evaluation orders for expressions. A compiler is allowed to reduce this non-determinism by picking one specific evaluation order.
- Second, a C compiler can “optimize away” runtime errors present in the source code, replacing them by any behavior of its choice. (This is the essence of the notion of “undefined behavior” in the ISO C standards.)
As an example, consider this out-of-bounds array access:
int main(void)
{
int t[2];
t[2] = 1; // out of bounds
return 0;
}
This is undefined behavior according to ISO C, and
a runtime error according to the formal semantics of CompCert C.
The generated assembly code does not check array bounds and therefore
writes 1 in a stack location. This location can be padding,
in which case the compiled program terminates normally, or can contain
the return address for main, smashing the stack
and causing execution to continue at PC 1, with unpredictable
effects. Finally, an optimizing compiler like CompCert can notice that the assignment
to t[2] is useless (the t array is not used afterwards) and remove
it from the generated code, causing the compiled program to terminate normally.
To address the two degrees of flexibility above, CompCert’s formal verification uses the following definition of semantic preservation, viewed as a refinement over observable behaviors:
If the compiler produces compiled code C from source code S, without reporting compile-time errors, then every observable behavior of C is either identical to an allowed behavior of S, or improves over such an allowed behavior of S by replacing undefined behaviors with more defined behaviors.
The semantic preservation property is a corollary of a stronger property, called a simulation diagram that relates the transitions that C can make with those that S can make. First, the simulation diagrams are proved independently, one for each pass of the frontend and backend compilers. Then, the diagrams are composed together, establishing semantic preservation for the whole compiler.
The proofs are very large, owing to the many passes and the many cases to be considered — too large to be carried using pencil and paper. We therefore use machine assistance in the form of the Coq proof assistant. Coq gives us the means to write precise, unambiguous specifications; conduct proofs in interaction with the tool; and automatically re-check the proofs for soundness and completeness. We therefore achieve very high levels of confidence in the proof.
At 100 000 lines of Coq and six person-years of effort, CompCert’s proof is among the largest ever performed with a proof assistant.
Proving the absence of runtime errors
Behaviors undefined according to the C semantics are not covered by the formal correctness proof of CompCert. Only code that exhibits no numeric overflows, division by zero, invalid memory accesses or any other undefined behavior can possibly be functionally correct.
In safety-critical embedded systems, the use of dynamic memory allocation and recursions is typically forbidden or limited. This simplifies the task of static analysis such that it is possible to report all potential runtime errors that are still present in the program, or formally prove the complete absence thereof.
The sound static analyzer Astrée does just that. It reports runtime errors caused by unspecified and undefined behaviors according to the C norm ISO/IEC 9899:1999 (E), program defects caused by invalid concurrent behavior, violations of user-specified programming guidelines, and computes program properties relevant for functional safety.
Errors reported by Astrée include integer/floating-point division by zero, out-of-bounds array indexing, erroneous pointer manipulation and dereferencing (buffer overflows, null pointer dereferencing, dangling pointers, etc.), data races, lock/unlock problems, deadlocks, integer and floating-point arithmetic overflows, read accesses to uninitialized variables, unreachable code, non-terminating loops, and violations of optional user-defined static assertions. Astrée also provides a module for checking coding rules that supports various coding guidelines (MISRA 2004 and 2012, ISO/IEC TS 17961, SEI CERT, CWE), computes code metrics and checks code metric thresholds.
Astrée is based on the theory of abstract interpretation, a mathematically rigorous formalism providing a semantics-based methodology for static program analysis.
Abstract interpretation supports formal correctness proofs. It can be proved that an analysis will terminate and that it is sound, i.e. that it computes an over-approximation of the concrete semantics:
- If no potential error is signaled, definitely no runtime error can occur. There are no false negatives.
- If a potential error is reported, the analyzer cannot exclude that there is a concrete program execution triggering the error. If there is no such execution, this is a false alarm (false positive).
This imprecision is on the safe side: there can never be a runtime error that is not reported.
Who uses CompCert?
The Institute of Flight System Dynamics at the Technical University of Munich uses CompCert in the development of flight control and navigation algorithms.
In November 2017 CompCert was successfully qualified by MTU Friedrichshafen according to IEC 60880, category A and IEC 61508-3:2010, SCL 3 for a certification project in the nuclear energy domain. The use of CompCert reduced development time and costs.
Airbus is employing CompCert at the Toulouse plant for a number of currently undisclosed projects.
In the civil-aviation research project QSMA by the German Federal Ministry for Economic Affairs and Energy, CompCert is being used to develop a TSO-C151b Terrain Avoidance and Warning System in accordance with DAL-C. The project is carried out by emmtrix, the German Aerospace Center DLR, Validas, TU Clausthal, and AbsInt.
Translation validation
Currently the verified part of the compilation tool chain ends at the generated assembly code. In order to bridge this gap AbsInt has developed a tool for automatic translation validation, called Valex. It validates the assembling and linking stages à posteriori.
Valex checks the correctness of the assembling and linking of a statically and fully linked executable file PE against the internal abstract assembly representation PA produced by CompCert from the source C program PS. The internal abstract assembly as well as the linked executable are passed as arguments to the Valex tool.
The main goal is to verify that every function defined in a C source file compiled by CompCert and not optimized away by it can be found in the linked executable and that its disassembled machine instructions match the abstract assembly code.
To that end, after parsing the abstract assembly code Valex extracts
the symbol table and all sections from the linked executable. Then the functions contained in the abstract
assembly code are disassembled. Extraction and disassembling is done by two invocations of exec2crl,
the well-established and robust executable reader of aiT WCET Analyzers
and StackAnalyzer.
Apart from matching the instructions in the abstract assembly code against the instructions contained in the linked executable, Valex also checks whether symbols are used consistently, whether variable size and initialization data correspond and whether variables are placed in the right sections in the executable.
Currently Valex can check linked PowerPC executables that have been produced from C source code by the CompCert C compiler using the Diab assembler and linker from Wind River Systems, or the GCC tool chain (version 4.8, together with GNU binutils 2.24).
Further information
The above overview is based on excerpts from the paper CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler (PDF, 600kB) by D. Kästner, J. Barrho, U. Wünsche, M. Schlickling, B. Schommer et al., in ERTS² 2018 — Embedded Real Time Software and Systems, January 2018, Toulouse, France. <hal-01643290>.
Other recent papers on CompCert include:
- D. Kästner, X. Leroy, S. Blazy, B. Schommer, M. Schmidt, C. Ferdinand. Closing the Gap — The Formally Verified Optimizing Compiler CompCert. In Proceedings of the 25th Safety-Critical System Symposium SSS 2017, Feb 2017, Bristol, UK.
- K. Nürnberger, M. Hochstrasser and F. Holzapfel, Execution time analysis and optimisation techniques in the model-based development of a flight control software (PDF, 1.9MB), in IET Cyber-Physical Systems: Theory & Applications (2017), 2 (2):57, ISSN 2398-3396, 10.1049/iet-cps.2016.0046.
- X. Leroy, S. Blazy, D. Kästner, B. Schommer, M. Pister, C. Ferdinand. CompCert — A Formally Verified Optimizing Compiler (Best Paper Award). In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Jan 2016, Toulouse, France.
Free trial
Request your free trial package today, complete with training and support via WebEx and email.