Structure of CompCert

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:

  1. 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 auto­matically generated from the grammar of the C language by the Menhir parser generator, along with a Coq proof of correct­ness of the parser.

  2. 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.

  3. 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.

  4. 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.

CompCert diagram

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.

The property that is formally verified is semantic preservation between the input code and output code of every pass.

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.

  1. 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.
  2. 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 runtime error analyzer Astrée does just that. It reports program defects 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:

  1. If no potential error is signaled, definitely no runtime error can occur. There are no false negatives.
  2. 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.

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 (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.