3 ms·
In this case, the semantics of the C subset chosen are captured perfectly by the assembly produced by the compiler. Seems like that's the intent of a compiler
by njs12345 15y ago
In this case, the semantics of the C subset chosen are captured perfectly by the assembly produced by the compiler.
Seems like that's the intent of a compiler to me :)
- shasta 15y agoRight, but first you have to specify "the semantics of C" and "the semantics of assembly". How do you prove you did that right?
- njs12345 15y agoThe semantics of the dialect of C that CompCert accepts are precisely defined, as are the semantics of the assembly outputted (that is, it's not strictly x86/PPC/ARM or whatever but some subset with defined semantics which happen to line up perfectly with observed behaviour). The first is fine I think (accepting a subset you define formally); the second is an issue but it's currently impossible to do any better. Still, if you look at this compared to the backends of LLVM and GCC it's certainly an improvement.
- cwzwarich 15y agoCompcert uses small-step operational semantics for both the source language and the assembly output (and intermediate languages that are irrelevant to the final statement of the semantic preservation theorem). Specifying such a semantics is basically like writing a very simple functional interpreter for the language. I don't see how it could get much simpler. Here is the description of the semantics for their input language: http://compcert.inria.fr/doc/html/Csem.html http://compcert.inria.fr/doc/html/Csem.html and their PPC output: http://compcert.inria.fr/doc/html/Asm.html http://compcert.inria.fr/doc/html/Asm.html
- shasta 15y agoYes. The approach is probably as good as it can get. And yet, it's not perfect. That functional interpreter could have a bug. And thus Knuth's quote is applicable. Testing the compiler could reveal to you that your specification wasn't really what you intended.