CompCert – Formally-verified C compiler
github.com
github.com
The core idea is that every phase of the compiler is proven not to change the behavior of the program. I.e. if you ran any intermediate representation you'd always get the same behavior.
The main limitation is, in my opinion, that the C specification isn't available in any form that a proof assistant can consume. Therefore, they had to translate the specification into that form manually. It is possible that this step contains mistakes. On the upside, every C compiler has this problem.
Most compiler bugs are not in their interpretation of the specification, but in various optimization passes. Compcert's formal verification ensures that all optimizations retain semantics; that alone makes it worth whatever they're charging.
• https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf
• https://compcert.org/motivations.html
I think things may have improved further since the 2011 paper, where they found bugs in parts of CompCert which were not, at the time at least, formally verified.
The formally verified parts of CompCert withstood torture testing admirably.
I work on a large, open-source, industrial-grade compiler for a living and I disagree with this statement unless it is specifically referring to C compilers and not compilers for other languages.
The point of compiler fuzzing like Csmith was that optimization bugs are really hard to find by the kinds of testing that would find more typical conformance bugs. Before these test generators were written one might have thought that optimization bugs were rare, simply because they hadn't been triggered much.
It could be. Another possible explanation could be that I am biased due to mostly working on the frontend of the compiler. I don't think that's the case though, most of the tickets that our customers open seem to be related to the frontend doing something that doesn't match the spec.
The relative frequency of different kinds of bugs can also change over time. Testing has a diminishing returns behavior. If front end bugs are easy to trigger, they will get expunged, and you'll be left with the harder to trigger bugs elsewhere in the compiler. I saw this in writing conformance tests for Common Lisp implementations: after implementations got the little direct tests right (function FOO implements its specified behavior), the remaining defects tended to be deeper and more subtle. Eventually random testing was churning out bizarre compiler interactions (but even that eventually burned through the reachable bugs.)
It would be interesting to study various compiler testing approaches using mutation: introduce bugs to the compiler by mutating its code, then see what fraction the testing can detect. Fully mutating a compiler is likely infeasible, but one could create a random sample of mutations and make estimates.
For correctness, it is most important that the programmer and the compiler agree on the interpretation of the specification. The good thing here is that there is an unambiguous interpretation which the compiler uses, and that anyone can read. The downside is that most C programmers probably can't understand this machine-readable language, and so will simply refer to the original human-readable specification.
What would be quite neat is if they translated the machine-readale specification back into a set of clarifying notes against the original spec.
Reminds me of the farmer who peeks out of the basement after a big storm, and reports back to his wife: "Good news and bad news. The bad news is, our barn blew down. The good news is, all the neighbors' barns blew down too!"
https://compcert.org/man/manual005.html#language-reference
Overflow in arithmetic over signed integer types is defined as taking the mathematically-exact result and reducing it modulo 2^32 or 2^64 to the range of representable signed integers. Bitwise operators (&, |, ^, ~, <<, >>) over signed integer types are interpreted following two’s-complement representation.
...so at least for that case, it behaves sanely, but it's unclear what happens for other types of UB.
Although lots of things blow up (and a few of them literally) due to overflow, very few blew up because it was UB, most of them blew up because it was overflow, and so having the natural two's complement behaviour as CompCert does here would not improve those programs.
If in the modern era you began over from scratch (like Rust) you might choose to (like Rust does in production) define this as having the natural two's complement behaviour because that's unsurprising.
But chances are if a programmer encounters overflow and didn't choose a type which has expressed behaviour for overflow, they did not actually want overflow. So in C++ the result of that argument is C++ should get wrapping and saturating integer types (Rust got these some time ago), so you can say "When counter overflows, just saturate" or "When index overflows, just wrap it" explicitly showing you actually made a decision and the compiler ought to accommodate this.
Wherever possible you actually want to try to flag cases where overflow happened and the programmer apparently hadn't even considered that. Is it better to wrap silently than crash at runtime? Maybe, in some cases, but every single place a language lets you raise 2 to the power 32 and then store it in a generic 32-bit integer at compile time without pointing out what a terrible idea this was is a source of bugs, and "defining" it as zero doesn't fix those bugs.
A lot of UB in C is necessary to compiler optimisation in the face of a language that doesn't do as much as it could to help the compiler tell what is really intended. So it's not really practical for CompCert to abolish some of that.
We know that every program still contains an error, and we want to reduce its snowball effect wherever possible. UB as handled by a modern compiler is completely opposite to this idea.
So like I said, some of them literally blow up.
The assertion happened, it concluded that the system had entered an unpredicted state, the rocket exploded. That was the fail safe condition.
That rocket wasn't actually programmed in C. The nasal demons you've probably imagining infesting everything weren't a factor. Overflow blew the rocket up, like I said, not any associated undefined behaviour. This is very common.
Maybe you find that "restarting" a rocket would be "more appropriate" but any people who die when an entire rocket full of explosive fuel crashes into their home because it's "restarting" wouldn't agree. Once the rocket ceases to be inside its design conditions, the safest thing to do is blow it up, so that's what happens.
Historically a "range safety officer", a human, would be watching the launch and, if it seems to deviate from their expectations they remotely trigger destruction. This is tricky to do correctly, the remote trigger might malfunction, and humans react slowly, so this is not the preferred option for today's unmanned rockets which are full of computers anyway.
The designers recycled the Ariane 4's "inertial platform" IMU but neither adjusted its parameters for expected Ariane 5 conditions, nor bothered to test it in such conditions. When flight accelerations exceeded Ariane 4's design parameters, the inertial platform sent debug messages down the channel meant for input to the engine gimbals. The engine gimbals interpreted those error messages as measurements, and steered accordingly, triggering destruction of the rocket and its payload of two (then) $200M+ satellites.
Many things could have prevented the failure. Checking the IMU specs against, or actually testing the IMU under, projected flight conditions would have revealed the problem. Not building the code in debug-mode, or not sending debug messages down some random control channel, or (on the receiving end) ignoring ill-formed input to the steering system, would have allowed the mission to complete.
In subsequent flights the software on the IMU was adjusted to expect accelerations that had been originally projected and did occur, and all was well. I don't know whether it will still send debug messages to the engines in case of a booboo, or whether the engines would ignore debug messages now.
Note that there was no actual need for the checks that resulted in the error messages. They were assertions of the sort that most Europeans of the time believed should be left in production code. I doubt this experience changed many of their minds.
A few years later, the code is pulled out for re-use in the Ariane 5. Apparently the kludge wasn't documented and no one bothered to confirm that the Ariane 4 code was actually up to the Ariane 4 spec. Had the Ariane 4 code been up to spec, the code reuse would have been fine.
If you check for overflow in a slightly wrong way, you'll accidentally "prove" to the compiler that the overflow check can be optimized out entirely. There's no explicit saturating or checked arithmetic. Even when you use only unsigned types, you still need to be paranoid about implicit integer promotion that can make intermediate operations signed.
These things could be fixed with relatively small changes to the spec or stdlib, but I don't think there's a will for it among C users.
But I agree with you these wouldn't be difficult to implement and are worth the appropriate committee looking at so that at least the programmers who realise they have a problem also have a solution.
C like C++ and Ada standards are actually a product of a JTC1 sub-(sub-?)-committee and so it's not so much about the will of C users in general as it is about the will of advocates to justify this to that committee and push it through all the bureaucracy.
Anyone actually interested in this should definitely engage with the people trying to get stuff done for C++ because the two languages know that they both benefit from the relatively good mutual compatibility, so neither would appreciate a pointless divergence on this work.
The real problem is when a compiler deletes code due to UB. The poster example being that you can't check for overflow by adding two numbers and examining if overflow occurred, since overflow is undefined. Strict aliasing can similarly break specific memory management code, because it often has to juggle raw memory and an unfortunate inlining can produce a function where a pointer exists simultaneously as two different incompatible types. Another favourite of mine is the fact you can't check if a reference in C++ is null, because it can't be, even though it can happen. The compiler just deletes code like "if (&x)".
This all happens silently, and only with full optimisations, making it possibly the worst footgun in all of C and C++, and it's not even the fault of the language, but a choice by the implementers.
At work we just don't write standard C, we use -fwrapv, -fno-strict-aliasing and a couple of others. Writing software at scale is simply impossible with UB looming over your head all the time.
X& x = *p; // p might be 0.
Y& y = p->y;
If p is a null pointer, dereferencing it is Undefined Behaviour and you lose immediately.
1. Require the programmer to prove to the compiler that the pointer is not null.
2. Insert null checks and abort the program if the pointer is null.
Both of those are deficient for me, because it's possible for some other bug to cause the memory holding the reference to be overwritten with 0, so I really favour:
3. Treat references as immutable pointers that can be null, but disallow creating them from pointers that are obviously constantly null.
Obviously currently all ways to obtain a null reference are UB, but at the same time the compiler happily produces a program that creates a null reference, but deletes the check for it. Which is the absolute worst possible way to do it. It's a needless optimisation that requires you to solve the halting problem to be safe.
Given Moonchild's comment about all optimizations retaining semantics, this leaves me wondering what happens with some of the more notorious UB-with-optimization footguns, such as the elimination of a chunk of code because an unsigned variable cannot go negative. If such optimizations are performed by this compiler, does the "all optimizations retain semantics" rule mean that this code elimination would be applied before any optimization (to avoid there being a difference between the before and after semantics)? I am not saying that would be wrong, but I am curious about how these cases are handled.
But "Undefined Behaviour" says that anything might happen. The reason to be so vague is that this frees the compiler to conclude that it can ignore this scenario. Whatever it does can't be wrong for Undefined Behaviour, so, it needn't consider any cases that trigger this. This makes it actually practical to produce reasonable object code for good programs that don't actually have Undefined Behaviour.
The practical alternative is that you can just outlaw a huge amount of stuff so that there's no problem for the compiler. For example you could say OK, my language refuses to admit that pointers are just an integer which happens to correspond to a machine address. Anything that depends on that is just removed from the language entirely. But now you can't do a lot of clever tricks, so, you abandon C and move to a language where you can get your job done.
Rust's approach is to put all that stuff that - if you get it wrong - is horribly unsafe and require its "unsafe" keyword. So in one sense it's actually two very similar languages, the safe language which you would have abandoned for a lower-level language because it can't get what you need done, and the low-level language where if you screw up everything catches fire. This would not have been practical in the 1970s but it is practical today.
The semantics of undefined behaviour are exactly the same before and after any transformation of the program, because any behaviour is a semantically reasonable implementation of your program. You screwed up, not the compiler.
1. In Rust I have a type named OnewayLess that insists it has equivalence (implements the Eq trait) and is totally ordered (implements the Ord trait), yet, in defiance of reason, it also insists that any of its members are less than anything when asked, even themselves.
This is incoherent nonsense, but it's safe under Rust. Rust promises that even though I am clearly a lunatic who doesn't understand what equivalence and ordering mean, my programs do not have Undefined Behaviour. If I try to sort a vector of this type, that won't reformat my hard disk, or more practically change unrelated data in the program. However, it very well might take forever (the sort keeps looking for the smallest object and never finds it) or run out of memory (the sort might try to keep references to the infinitely many "lesser" items from the vector) and that isn't undefined, that's just consequences of my reprehensible type design.
2. In our RDF storage engine written in C an older version contained a mistake in which an array of temporary pointers might get partially overwritten.
In C there is no safety checking, these are raw memory addresses, and dereferencing a pointer that now might be garbage is Undefined Behaviour so all bets are off. It could do absolutely anything. If the compiler is instead required to somehow check, when referencing them, that these are still good pointers, the performance of many C programs is ruined, even though our bug was in unrelated code.
"The semantics of undefined behaviour are exactly the same before and after any transformation of the program"
[emphasis added]
I think you've got this idea that Undefined Behaviour somehow means that the behaviour is defined but is being kept secret from you. It isn't. The behaviour really is Undefined. Doing further transformations to it is therefore always harmless.
I don’t think you are getting that Undefined is a concept in the language specification domain, that is not literally implemented. Consequently, you don’t even see yet what my question is about. When I think of a way to make it clearer, I will follow up.
The C standard Appendix J.2 contains an incomplete list of undefined behavior causes. Note that some of them simply cannot be checked at compile time, eg "The execution of a program contains a data race (5.1.2.4)" cannot have the semantics of the resulting program defined by the compiler. C does not provide the compiler with enough information to statically prevent data races. I'm not familiar with CompCert, but it should be possible to go through appendix J.2 and find the UB causes which are detectable at compile time, and then go through CompCert and see what it does for each. What it does will likely depend on the particular program it's compiling, of course.
In these cases, it is important to distinguish between what the standard defines, and what the implementation does. The standard says, in effect, that we cannot assume any specific outcome from UB, but in any particular case in a specific implementation, something definite (and often deterministic, though context-dependent) will happen. This, of course, is often a source of problems, when programmers know (or think they know) what will happen, and depend on it.
Consider WUFFS https://github.com/google/wuffs
WUFFS will give you a C library that can turn PNG data into raw image data and is definitely correct. It's not exactly idiomatic C, you'd assume if a person wrote this code it's probably wrong, but WUFFS promises it's correct. CompCert should turn that C library into executable code which is therefore also definitely correct.
Now, maybe you will screw up code that reads the PNG data from a disk file, or draws the image on a screen, or a million other things, but the WUFFS library components are definitely fine, not just "Bill wrote it and he's got 20 years experience" fine or "It passed the unit tests" fine but "Four Color Theorem" fine.
With respect to what standard of correctness? If the answer is that the object code is guaranteed to behave according to the source according to the C standard that is a useless guarantee because of the possibility that there is UB in the source code, in which case the compiler could release the kraken and it would still be "correct".
WUFFs promises that you can't write unsafe things. For example you can't have arithmetic overflow in WUFFS. Every time it sees arithmetic in your code the compiler is trying to decide why this operation might overflow. If you add together two 8-bit variables and put the result in a 16-bit variable, that doesn't overflow, but if you try to put the result in another 8-bit integer variable the compiler assumes unless it can see otherwise that this is an overflow, which is forbidden, so your code doesn't compile.
Buffer overflows are the same, if you're indexing into a buffer with an 8-bit unsigned variable and the buffer has 400 entries it's cool. If it has 100 entries but the compiler has concluded this variable can only be between say, 20 and 48 then that's cool too. But if the compiler can't prove this variable isn't 100 then you've got a potential buffer overflow and the code does not compile.
The C code is an output from WUFFS. WUFFS says "This C code is definitely safe" and then CompCert says "This object code is definitely a correct implementation of your C code" so the result is WUFFS compiled by CompCert is definitely safe object code.
> you can't have arithmetic overflow in WUFFS
That seems improbable. Can I write x++? Because if I can, then I can have an arithmetic overflow.
> Buffer overflows are the same
That seems improbable. Can I write *p++? Because if I can then I can overflow a buffer.
It's fairly straightforward to provide a proof, given a definition of division by zero, that 1 = 0. It's often done in first-year introduction to algebra classes.
It would be correct, then for a compiler to substitute the value 1 everywhere the programmer used the value 0 (or NULL, or '\0') and still produce a valid program with the same behaviour because 1 and 0 have been proven to be equivalent.
So no, you are not right in thinking all implementations must define undefined behaviour. Undefined is undefined. C code containing undefined behaviour is not valid C code and the compiler to only required to produce correct output when the input is valid C code.
To clarify, what I am interested in here is the interaction of C-standard UB with any guarantee this compiler may give with regard to semantics preservation under optimization.
[1] In reality, the hardware will do something, and deterministically in every case that I am aware of, when the divide operation is invoked with zero as the divisor. Computer division is not an exact implementation of mathematical division.
To clarify my point: undefined behaviour has any semantics you might want it to have. Anything and everything is semantically correct even under optimization. Even if the compiler says it will do one thing and then does another: it's correct either way.
The computer may "do something" with division by zero. Or the compiler might completely elide the code and replace it with a picture of a teapot before it even gets as far as hitting a register in anger. It's still valid, semantically, because you're dividing by zero from which you can prove anything and everything.
No, it is not. It's fairly straightforward to provide a proof, given the false[0] premise that x*y/y = x, that 1 = 0.
0: Hell, I don't even need division by zero for that one:
uint8_t x = 2;
x = x*128;
// x is now (uint8_t)(2<<7) == (uint8_t)256 == 0
x = x/128;
// x is now 0>>7 == 0
// x is now x*y/y is 2*y/y is 2
if(x == 2) printf("it's two\n");
printf("it's %i\n",(int)x);Yeah, strictly speaking we don't care as much what it does in specific cases of undefined behaviour (eg signed integer overflow), since compiler bugs in any specific case, while infuriating, can be worked around on a case-by-case basis (eg, warning on any null pointer check that comes after a dereference). The real concern is what happens in the arbitrarily-large number of cases that don't get specific attention.
Otherwise, the compiler does not guarantee the absence of UB; for that, you need Verasco (http://compcert.inria.fr/verasco/), a static analyzer that tries to prove that a given code is UB-free. If it succeeds, then combined with CompCert's semantic guarantee, you get a compiled code that is as UB-free as the source code.
Verasco was a research project and it's not clear it's still being developed.
The language it implements (an sml dialect) is high-level and garbage collected, meaning that it is not usable in all of the same domains, but work is ongoing to reuse much of the compiler infrastructure for 'pancake', a low-level language.
> CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. A commercial version of CompCert, without this restriction and with professional support and extra features, can be purchased from AbsInt. See the file LICENSE for more information.
However, https://github.com/AbsInt/CompCert/blob/master/LICENSE goes onto say that
> The following files in this distribution are dual-licensed both under the INRIA Non-Commercial License Agreement and under the Free Software Foundation GNU Lesser General Public License, either version 2.1 or (at your option) any later version: ...
and then lists a bunch of specific files and paths, which may or may not (this is the key question) constitute a majority of the repo. Looking around, I see a few references to the LGPL and LGPLv3.
The LICENSE also makes clear (immediately following the file list) that
> If you opt for the GNU Lesser General Public License, these files are free software and can be used both in commercial and non-commercial contexts, subject to the terms of the GNU Lesser General Public License.
So, broadly speaking: am I just looking at a standard smoke-and-mirrors routine (creating just enough uncertainty that most commercial operations would reasonably pursue the custom license) or are there any actual intuition-violating footguns hiding anywhere in the codebase?
A comment indicates they relicensed some of it GPL->LGPL so I assume they hold the copyright.
The BSD licensed stuff seems to be imported code.
>Additionally, the interface files in question are also licensed under the GPL so that they can be used in other, open-source projects such as VST (http://vst.cs.princeton.edu/) that connect with CompCert.
at https://github.com/AbsInt/CompCert/issues/140 (2016); GPL -> LGPL in a later commit.
As far as I read your evaluation, probably it is gpl. But without the gpl linker exception you cannot create non gpl binaries.
Right. It's about a compiler with a GPL license but without a similar exception. I was making a comparison.
[1] https://github.com/AbsInt/CompCert/commit/04f499c632a76e4605...
From GPLv2:
"These requirements apply to the modified work as a whole. If identifiable sections of that work are not derived from the Program, and can be reasonably considered independent and separate works in themselves, then this License, and its terms, do not apply to those sections when you distribute them as separate works. But when you distribute the same sections as part of a whole which is a work based on the Program, the distribution of the whole must be on the terms of this License, whose permissions for other licensees extend to the entire whole, and thus to each and every part regardless of who wrote it."
On the other hand, if someone forms it under the GPL, and adds some additional features, the original code base cannot pull those features back in the original closed source project, without ceasing to distribute the whole thing as closed source.
Choosing GPL effectively forms your code, and further code added by others can no longer be added to the “proprietary” branch. But you can continue adding code yourself in parallel in both branches.
One thing to keep in mind, if you sign over your copyright by agreeing to contribute using a Contributor License Agreement (CLA), the person or organization can take your contributions proprietary.
LGPL is not GPL. You are for example allowed to dynamic link from proprietary code to LGPL libraries. This is not the case with GPL shared libraries. You should take look at the LGPL license agreement and then see how the code is used.
But of course it's not a "majority" decision, nor are all files equally important.
"Verifiable C"
"Cyclone a safe dialect of C"
https://cyclone.thelanguage.org/
"Checked C"
https://www.microsoft.com/en-us/research/project/checked-c/
"Frama C"
"In C source files, attribute qualifiers can occur anywhere a standard type qualifier (const, volatile) can occur, and also just after the struct and union keywords. For partial compatibility with GCC, the CompCert parser allows attributes to occur in several other places, but may silently ignore them.
Warning. Some standard C libraries, when used in conjunction with CompCert, deactivate the __attribute__ keyword: the standard includes, or CompCert itself, define __attribute__ as a macro that erases its argument. This is the case for the Glibc standard library under Linux, and the Xcode header files under macOS. For this reason, please use the __attribute keyword in preference to the __attribute__ keyword."
I learned C in the 80's and did a lot of it for about 10 years. After not doing much software development for another 10 years or so, I wrote an embedded OS and an application (for the MSP430 platform). I was surprised by the advances in compiler optimization while I had been away. I needed to be much more diligent when interacting with hardware and locking. (E.g. Use the volatile qualifier generously, or my code would not work.) I also found some odd compiler bugs (in the TI compiler) related to bit fields.
However, for non safety-critical software I’d say buying a proven correct C compiler would be a waste of money.
I remember a presentation in which they presented the number of bugs they found on other compilers (GCC, Clang, MSVC) while developing test cases and benchmarks, and it was surprisingly high!
I don’t want to say any figures as I don’t remember it enough, but I think it was in the hundreds.
And there are many horror stories on Hacker News of people being impacted by compiler bugs in prod on non-critical software, sometimes with significant financial impact.
But yeah, not sure the price is worth it for non critical software in general.
They did not fix them though, that would have needed a team 10x larger
In Fedora this is all low stakes but it wouldn't be if the software was deployed in a plane.
Especially since that other company has a bit of a reputation for writing shoddy software.
In fact, the more I think about the more relevant this comment becomes. Building computerized transportation devices is hard and apparently one of the things you need to do it well is a proven correct C compiler. A far cry from the type of software development most people do, which involves slapping together some stuff we found on the internet and writing some glue code around it.
Oh.
Nevermind.
I know nothing of Tesla though and have no plans of buying one anytime soon. Still seems pretty relevant to me though if you don't take every topic to be so narrowly defined.
> about 90% of the compiler’s algorithms (including all optimizations and all code generation algorithms) are proved correct in Coq, but the remaining 10% (including elaboration, presimplifications, assembling and linking) are not verified
Even though you cannot unit test everything. I would still prefer it, then to have another compiler pass to ensure C semantics are the same as the compiled code. Even though compiled code is the same as C. C code can be buggy from the start.
I don't understand the use of "mathematically proven" in this context as well. Proving that x86 add instruction or a set of x86 instruction has the same as the semantics of the C code, is just pure computer science problem, not mathematic?
No. There is no rule against proprietary code on GitHub.
> And doesn't that mean the 150 forks (republishings) are in legal danger?
No.
If you actually read the INRIA license:
> The License entitles you to use the Software to conduct research or education and to create Derivative Works solely for academic, non-commercial research endeavors of the Licensee (A "Derivative Work" is a work that is a modification of, enhancement to, derived from, or based upon the Software).
But... The ToS do not suddenly give everyone the right to modify, publish, or reuse the code, however they wish.
> Because you retain ownership of and responsibility for Your Content, we need you to grant us — and other GitHub Users — certain legal permissions, listed in Sections D.4 — D.7. These license grants apply to Your Content. If you upload Content that already comes with a license granting GitHub the permissions we need to run our Service, no additional license is required. You understand that you will not receive any payment for any of the rights granted in Sections D.4 — D.7. The licenses you grant to us will end when you remove Your Content from our servers, unless other Users have forked it. [0]
[0] https://docs.github.com/en/github/site-policy/github-terms-o...
It’s not against GitHub rules. Were you under the impression users could only host repositories on GitHub that have licenses that fulfill the open source definition? How did you get that misimpression?
And of course, once you set a repository as public, then forking and downloading allowed. Because that is, what the public flag means. Now, once you try to use the downloaded code, the actual license terms apply. But that shouldn't concern GitHub.
I suspect that large subset is doing a lot of lifting.
I don't imagine it's due to technical challenges in formal modelling, as 'structured switch' statements still permit the default case to simply break immediately.