CompCert - formally verified optimizing C compiler
What is CompCert?
CompCert is a formally verified optimizing C compiler. Its intended use is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It accepts most of the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for ARM, PowerPC, x86, and RISC-V architectures.
What sets CompCert apart?
What sets CompCert apart? CompCert is the only production compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. The code it produces is proved to behave exactly as specified by the semantics of the source C program. This level of confidence in the correctness of the compilation process is unprecedented and contributes to meeting the highest levels of software assurance.
The formal proof covers all transformations from the abstract syntax tree to the generated assembly code. To preprocess and produce object and executable files, an external C preprocessor, assemblers, linkers, and C libraries have to be used. However, these unverified stages are well-understood and robust from an implementation perspective. This was demonstrated on a development version of CompCert in a 2011 study by Regehr, Yang et al.:
“The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.”
Formally verified optimizations
CompCert implements the following optimizations, all of them formally verified:
- Register allocation using graph coloring and iterated register coalescing
- Instruction selection with strength reduction, to take advantage of combined instructions provided by the target architectures
- Constant propagation for integer and floating-point types
- Common subexpression elimination
- Dead code elimination
- Function inlining
-
Tail call elimination
Who uses CompCert
“With CompCert it is possible to decrease the execution time of our flight control algorithms by a significant amount. The reduction of the execution time can be used for additional functionality.” TU Munich, Institute of Flight System Dynamics, 2016
-
MTU Friedrichshafen successfully qualified CompCert in 2017 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.
“The computed WCET bounds lead to a total processor load which is about 28% smaller with the CompCert-generated code than with the code generated by the conventional compiler. The main reason for this behaviour is the improved memory performance. The result is consistent with our expectations and with previously published CompCert research papers.” MTU Friedrichshafen, 2018
Your benefits
Using CompCert is a natural complement to applying formal verification techniques (static analysis, program proof, model checking) at the source-code level. The correctness proof of CompCert guarantees that all safety properties verified on the source code automatically hold for the generated code as well. When using a conventional compiler to compile safety-critical applications, you typically have to disable compiler optimizations and run into resource problems as a result. With CompCert, you can significantly improve your applications’ performance, as you no longer have to switch off optimizations for safety reasons.
Compilation with execution time in mind
On typical embedded processors, code generated by CompCert typically runs twice as fast as code generated by GCC without optimizations, and only 20% slower than GCC code at optimization level 3.
Chart of CompCert vs. GCC execution times for 23 benchmarks :
Supported architectures CompCert produces machine code for:
- ARM / Cortex
- PowerPC (32-bit and 32/64-bit hybrid)
- Intel IA32 (x86 32-bit)
- AMD64 (x86 64-bit)
-
RISC-V (32- and 64-bit)
Supported Tool-chains
To preprocess and produce object and executable files, an external C preprocessor, assembler and linker have to be provided. CompCert is currently tested for compatibility with:
- GNU logo DiabData logo
- GCC (version 4 or newer)
- WindRiver Diab for PowerPC (version 5)
An optional tool called Valex is available for the postpass validation of the assembling and linking steps. It compares the instructions in the abstract assembly code produced by CompCert to the instructions in the linked binary executable, checks whether symbols are used consistently, whether variable size and initialization data match up, and whether variables are placed in the proper sections in the executable.
Free Trail Request your free trial package today here>>
How to buy :
Please do not hesitate to contact Gerard Fianen at INDES-IDS BV to discuss your formal S/W verification requirments
|