Formally verified compilation for RISC-V

CompCert for RISC-V 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 32-bit and 64-bit RISC-V.

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.

In 2022, the Association for Computing Machinery, ACM, presented the CompCert development team with the prestigious ACM Software System Award. Subsequently, the team also received the ACM SIGPLAN Programming Languages Software Award.

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
Redundant code elimination
Function inlining
Tail call elimination
If-conversion

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.

Execution times of 23 benchmark programs compiled with ■ gcc -O0, ■ CompCert, ■ gcc -O1, and ■ gcc -O2

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.

“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

“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

Supported targets

CompCert for RISC-V supports the base instruction sets RV32I and RV64I, as well as the extensions M, F, and D. Supported target system is Linux with the GNU toolchain. ELF psABI with ILP32D or LP64D calling convention is supported.