Can You Trust Your C Compiler?
If you are writing a hello world program, you probably aren’t too concerned about how the compiler translates your source code to machine code. However, if your code runs on something that people’s lives depend on, you will want to be a bit pickier and use something like the COMPCERT compiler. It’s a formally verified compiler, meaning there is a mathematical proof that what you write in C will be correctly translated to machine code. The compiler can generate for PowerPC, ARM, RISC-V, and x86, accepting a subset of ISO C 99 with a few extensions. While it doesn’t produce code that runs as fast as gcc, you can be sure the generated code will do what you asked it to do.
Of course, this still provides no assurance that your code will work. It just means that if you write something such as “x=0;” the generated code will set x to zero and will not do anything else. You can apply formal methods to verify your source code and be assured that the compiler doesn’t introduce possible failures. Cases where code like “x=0;” does extra things or incorrect things are very hard to figure out because the source code is correct and an examination of the generated code would be necessary to find the compiler’s code generation bug.
All this does come with a few restrictions. For example, variable-length array types are not available and you should not use longjmp and setjmp. There are also restrictions on how you can code a switch statement. There are also a variety of options that allow you to examine your code under an interpreter.
You may think your compiler doesn’t need verification, but you might be surprised. The compiler documentation references several papers ranging from 1995 to 2011 that have found many incorrect compilation problems with popular compilers.
COMPCERT operates on observable behaviors of a program, such as calls to I/O functions or accesses to volatile memory locations. The compiler is allowed to improve a program’s observable behavior — for example, resolving a divide by zero error — but must not change other behaviors. Note, however, that while you could argue that execution time and memory usage are externally observable, they don’t count in this context.
To make the proof manageable, the Coq proof assistant does automated checking on the compiler proofs and the compiler itself uses 15 passes, each proved correct. As of today, there is still about 10% of the compiler that is not proven correct. Researchers dedicated 6 CPU-years to finding compiler bugs using Csmith and could not find any errors (which was not true of other compilers).
Of course, it is still up to you to make your program do what you want it to do. All this does is ensures the compiler does what you asked it to do. Luckily, there are tools to help formally verify your code, too.
from Hackaday http://bit.ly/2S8zvM2
via IFTTT