What is the practicality of actually using CompCert? And what does it actually defend against?
All I know is that it tries to ensure that the behavior of the program is the same as the input, meaning that the compiler itself does not have bugs. But how does that actually interact with undefined behavior in the language? What happens to an array out of bounds?
And what are the limitations imposed, since it only works on a subset of the C language?
It seems unlikely that I could just switch compilers and suddenly have a safe program written in C.
It looks like CompCert explicitly does not attempt to prevent UB from resulting in unpredictable behavior; all it guarantees is that "the observable behavior of [the compiled code] C improves on one of the allowed observable behaviors of [the source program] S", where "improving on" allows for arbitrary behavior on UB [0]:
> Third, the compiler is allowed to improve the behavior of the source program. Here, to improve means to convert a run-time error (such as crashing on an integer division by zero) into a more defined behavior. This can happen if the run-time error (e.g. division by zero) was optimized away (e.g. removed because the result of the division is unused). However, if the source program is known to be free of run-time errors, perhaps because it was verified using static analyzers or deductive program provers, improvement as described above never takes place, and the generated code behaves exactly as one of the allowed behaviors of the source program.
So you still have to prove your program's correctness by some other means.
You have to scroll down a bit, but see here[1]. Also searching [site:regehr.org compcert] will find more. CompCert C makes it impossible to reproduce at least some UB bugs:
For CompCert, the high-level correctness theorems I proved are all of the first kind above: if the source program goes wrong, nothing is guaranteed about the behavior of the compiled code. It happens, however, that the stepwise simulation lemmas I build on actually prove property 2 above: the compiled code cannot crash "earlier" than the source code, and will produce the same pre-crash observables, then possibly more. So maybe I should strengthen my high-level correctness theorems...
That was over a decade ago, so perhaps it's been done. I confess I haven't closely followed CompCert in some time, due to having priorities elsewhere. As you can see elsewhere in that reference CompCert C will fail to generate the example UB code.
But yes, mechanically proving additional properties with some kind of SAT solver is also an open area of research. Dafny is the example I’m familiar with. Its conditions and invariants allow things like automatically proved binary search[2]. Converting CompCert C statements to SMTLibv2 assertions (which is, to an extremely rough first approximation what Dafny does) would certainly be considerably easier than it would be for most other languages. It would still be a serious effort of course.
Apart from compiler bugs, this issue with "time-traveling UB" shouldn't really occur in practice with any side effects other than volatile accesses. As noted by Martin Uecker [0],
> In portable C code I/O is performed using function calls of the standard library. A compiler can generally not assume that a function returns to the caller, because the function could call ‘exit’, ‘abort’, ‘longjmp’, or enter an infinite loop. For this reason, it is never allowed for a compiler to use any information derived from an operation with potential UB that comes after a function call in a way that could affect observable behavior before the function call. Consequently, observable behavior that is accessed via function calls (i.e. all except volatile accesses) can not be affected by time-traveling optimizations even when using the abstract interpretation. In principle, a compiler could use special knowledge about C library functions and use the fact those functions always return to the caller, but we are not aware of any compiler which does this (and it hardly seems worthwhile).
I believe LLVM has a "mustreturn" attribute expressing this, but as noted, no standard C library messes with any such attributes for functions that cause observable behavior.
So time-traveling UB really only affects programs which use volatile accesses for MMIO, and it might eventually be banned entirely from the C standard if the linked proposal N3128 goes through. I'd say that even "some C bugs" is a overstatement outside of embedded programming, given the rarity of MMIO in a hosted environment.
> through. I'd say that even "some C bugs" is a overstatement outside of embedded programming, given the rarity of MMIO in a hosted environment.
I don’t concede your claims, but I’m enough out of the loop that I won’t attempt to refute them either. However, for what it’s worth, embedded programming is exactly where I most want that.
Furthermore, I don’t know of any other popular bare metal language that’s even close to having a compiler offering mechanically provable assertions about its compiled behavior. Do you?
> Furthermore, I don’t know of any other popular bare metal language that’s even close to having a compiler offering mechanically provable assertions about its compiled behavior. Do you?
Well, if you ask the question that narrowly, then I suppose not, unless CakeML's GC is lightweight enough to be stuffed onto some board or another.
But 99% of the time (i.e., when I am not doing something intentionally strange to test the language's limits), the correctness of the program I'm writing, or at least of its dependencies (including the standard library), is far more questionable than the correctness of the compiler; after all, the output of, say, GCC and LLVM has been tested by oodles of real-world software. Even if I'm really paranoid, I can disable all optimizations and reenable any less-questionable ones individually.
Thus the GP's complaint, that C is filled to the brim with undefined behavior that will silently cause corruption in production code instead of failing loudly, since all the runtime sanitizers (AFAIK) swear up and down that they aren't very secure.
I do hope that that formal verification on the program's side becomes more accessible in the future, though, either via dedicated systems like Daphny or via "gradual verification" as permitted by things like Why3 frontends for different languages. (In particular, I've been meaning to look into the Creusot project for Rust.) But short of formal verification, robust runtime assertions and guardrails are generally the best bet, and C as a language simply doesn't provide very good tools for those.
> Furthermore, I don’t know of any other popular bare metal language that’s even close to having a compiler offering mechanically provable assertions about its compiled behavior. Do you?
You can automatically extract low level code out of certain high level, provable languages. I think some of them might offer the guarantee you asked for (assuming you eg use a certified C compiler for the last leg).
[1] https://compcert.org/