Miscompilation – A Thing of the Past

A compiler translates the source code written in a given programming language into executable object code of the target processor. Even in recent years scientific studies have found numerous bugs in all investigated open source and commercial compilers, including compiler crashes and miscompilation issues. Miscompilation means that the compiler silently generates incorrect machine code from a correct source program. In safety-critical systems this is a serious problem since it can cause erroneous or erratic behaviors including memory corruption and program crashes. CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. Source code and proofs are publicly available and are amenable to independent verification. This article gives an overview of the design and proof concept of CompCert. We will also report on experience gained at MTU Friedrichshafen in the context of a safety-critical industry application. The use of CompCert helped not only to improve the performance of the generated code, but also considerably reduced the (qualification) costs: using CompCert was a key factor for qualifying the engine control software according to IEC 60880, category A and IEC 61508-3:2010, SCL 3.