11 ms·

CompCert – Formally-verified C compiler

227 points by mbrodersen 5y ago

userbinator 5y ago
I think a lot of others here are going to have the question "what does it do with UB", which is partially answered in the doc: https://compcert.org/man/manual005.html#language-reference 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.
- tialaramex 5y ago
  There was a CPPCon talk [I think?] about changes in this direction for C++ and the "problem" with this approach goes like this: 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.
  - wruza 5y ago
    A program correctness is not just yes-or-no if you take consequences into account and state that there is some room for errors and that we deal with them instead of just meeting our fate. One thing is an incorrect value that is catched few assertions later (we check our invariants, don’t we?). A completely another thing is entire blocks of code missing from an executable and flow control broken so bad that the program is now a binary equivalent of a triggered psychopath. 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.
    - tialaramex 5y ago
      > One thing is an incorrect value that is catched few assertions later (we check our invariants, don’t we?). 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.
      - wruza 5y ago
        Is this rocket example real or imaginary? If latter, rockets do not have explode-on-assertion-fail schematics, afaik. I’m not a rocket engineer, but I find that at least restarting a subsystem is more appropriate than letting it explode “because yeah anyway”. The difference between a regular error and UB is that you can’t handle UB by definition.
        tialaramex 5y ago
        Ariane 5's test flight self-destructed 37 seconds after launch. Its horizontal velocity was outside the range that could be represented in a 16-bit variable. In fact this check wasn't appropriate for Ariane 5 and so was removed in subsequent versions, but that's hindsight. 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.
- mannykannot 5y ago
  Am I right in thinking that all undefined behavior must have a defined outcome in the implementation? Otherwise, I would guess that "proven correct" is only relevant for the compilation of programs that cannot enter UB territory. 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.
  - tialaramex 5y ago
    No. There's "Implementation Defined" behaviour where the compiler vendor is expected to explain what their compiler (and maybe operating system, hardware architecture, site installation) does in these cases. 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.
- a1369209993 5y ago
  > but it's unclear what happens for other types of UB. 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.
- edwcross 5y ago
  CompCert's main theorem is that the compiled code maintains or improves the behavior of the source code, as in, it can only maintain or remove erroneous behaviors. So, it can remove a division by zero, for instance, but it will never add one. Otherwise, the compiler does not guarantee the absence of UB; for that, you need Verasco (http://compcert.inria.fr/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.
bombcar 5y ago
The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, x86 and RISC-V processors. I suspect that large subset is doing a lot of lifting.
- macleginn 5y ago
  On their website, the claim is more ambitious: "The main result of the project is the CompCert C verified compiler, a high-assurance compiler for _almost all_ of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors." (https://compcert.org/ https://compcert.org/)
  - bombcar 5y ago
    That makes me wonder even more what the missing parts are.
    - anonydsfsfs 5y ago
      The differences are documented at https://compcert.org/man/manual001.html#sec13 https://compcert.org/man/manual001.html#sec13
      - hvdijk 5y ago
        Interesting that only a restricted switch is supported, but goto is apparently available unrestricted. Any switch should be trivially translatable to if-goto-else-if-goto-etc, so I wonder what the reason for that might be.
        MaxBarraclough 5y ago
        Just a guess, but perhaps they don't bother supporting 'unstructured switch' because they expect that input programs will most likely be written in the MISRA C subset of C anyway? 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.
rock_artist 5y ago
> CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
- Faaak 5y ago
  and ?
  - david_draco 5y ago
    Isn't that against Github rules? And doesn't that mean the 150 forks (republishings) are in legal danger?
    - CodesInChaos 5y ago
      There is no requirement for software on github to be open source. The github ToS just demand some basic rights needed for github to function (e.g. forking and downloading must be allowed)
    - ylyn 5y ago
      > Isn't that against Github rules? 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).
    - shakna 5y ago
      No. GitHub's Terms of Service cover certain rights, allowing them to do certain things like fork, and view the code. 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-of-service#3-ownership-of-content-right-to-post-and-license-grants https://docs.github.com/en/github/site-policy/github-terms-o...
exikyut 5y ago
As noted in the License section of the readme, > 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 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?
- bombcar 5y ago
  It appears that the LGPL does NOT cover the "meat" of the codebase (see the directories arm, x86, etc) and instead covers the "edges" where their code may interact with other code. 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.
- alfu 5y ago
  >The files in question are, from a formal verification standpoint, the interface to CompCert. They are licensed under the non-commercial license (NCL) so that they can be used together with the rest of CompCert (the implementation of the compiler, so to speak), which is NCL-only. >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/ http://vst.cs.princeton.edu/) that connect with CompCert. at https://github.com/AbsInt/CompCert/issues/140 https://github.com/AbsInt/CompCert/issues/140 (2016); GPL -> LGPL in a later commit.
Cu3PO42 5y ago
I have had the pleasure of visiting AbsInt and hearing talks on, amongst other things, CompCert. It really is a fascinating piece of software. I would highly recommend looking at the 2016 paper [1] for a bit more detail on how it works. If you're interested you can find other publications as well. 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. [1] https://hal.inria.fr/hal-01238879 https://hal.inria.fr/hal-01238879
- moonchild 5y ago
  > 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.
  - Cu3PO42 5y ago
    I wholeheartedly agree. I didn't mean to say that the translation of the specification was a big problem, merely that all others are even more insignificant.
    - MaxBarraclough 5y ago
      Also, this has been studied empirically, and CompCert holds up well: • https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf • https://compcert.org/motivations.html 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.
etaioinshrdlu 5y ago
It would be nice if Tesla would use something like this for certain parts of the car. But you just know they won’t. Love to hear if anyone knows of any formal methods are used at all, and not talking about the self driving stack, but stuff like throttle control.
- epgui 5y ago
  Relevance??
  - etaioinshrdlu 5y ago
    If all you think about is Tesla, every comment thread is a relevant place to post.
  - mtts 5y ago
    Not usually in the habit of giving much thought to Tesla, but suggesting that a proven correct C compiler created by a company that builds transportation devices that contain lots of computers might be interesting for another company that builds transportation devices that use lots of computers seems to me to be perfectly sensible. 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.
    - 7thaccount 5y ago
      Ada/Spark is also supposed to be pretty good here.
    - robbrown451 5y ago
      I was like, since when does Airbnb build transportation devices? Oh. Nevermind.
  - 5y ago
runeks 5y ago
I wonder how often a C program does something wrong because of a compiler bug versus a program bug. I’d think the former is extraordinarily rare for e.g. gcc. Although, if you spend an hour studying every line of code (as is customary when writing safety-critical code), it’s possible you may arrive at a point where the primary source of bugs is the compiler. However, for non safety-critical software I’d say buying a proven correct C compiler would be a waste of money.
- Agingcoder 5y ago
  Compiler bugs are not rare - it's just that most people never notice them.
- crubier 5y ago
  I was lucky enough to work with people working on CompCert in French public aerospace research labs. 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.
  - occamrazor 5y ago
    Did they fix or report the bugs upstream?
    - archi42 5y ago
      They're usually at least reported. At least that was the case for all the compiler-bug related papers I've read.
    - crubier 5y ago
      Yes I think they systematically reported it, and explained that their work was beneficial to all C compilers as a consequence. They did not fix them though, that would have needed a team 10x larger
tankfeeder 5y ago
Btw, Monocypher passed Compcert in -interp mode.
moonchild 5y ago
CakeML[0] is another formally verified compiler. Notably, unlike compcert, it is open source. 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. 0. https://github.com/CakeML/cakeml https://github.com/CakeML/cakeml
rwmj 5y ago
I gave an introductory talk to Red Hat about proving C code with Frama-C, which touched on CompCert. (Coq, Frama-C, CompCert and OCaml are all written by an overlapping set of the same people.) Note I'm very much a beginner here myself. http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4
globuous 5y ago
Xavier Leroy, who is a big contributor to this project, was an INRIA senior researcher and was the main Ocaml développer. He’s got a lecture (in french) at the college de France where he introduces the formal verification of a basic compiler for an imperative language: https://www.college-de-france.fr/site/xavier-leroy/course-2019-12-12-09h30.htm https://www.college-de-france.fr/site/xavier-leroy/course-20..., very interesting !
belter 5y ago
Also relevant: "Verifiable C" https://vst.cs.princeton.edu/ https://vst.cs.princeton.edu/ "Cyclone a safe dialect of C" https://cyclone.thelanguage.org/ https://cyclone.thelanguage.org/ "Checked C" https://www.microsoft.com/en-us/research/project/checked-c/ https://www.microsoft.com/en-us/research/project/checked-c/ "Frama C" https://frama-c.com/ https://frama-c.com/
anonymousiam 5y ago
Some caveats in this compiler: "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.
PaulHoule 5y ago
Yeah, it even gets the undefined behavior right.
tinganho 5y ago
Couldnt this problem be dealt with unit tests?
- au8er 5y ago
  You cannot use unit tests for everything, since the number of unit tests required is basically infinity. Logically, unit tests can only prove an error exists and cannot show the program is correct. What they most likely did was mathematically showed that all possible edge cases (potentially inifinitely many) are all considered.
  - tinganho 5y ago
    I have never heard of verified compiler before. Not entirely sure if I understand everything from their docs either. But here are my thoughts. 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?
sobriquet9 5y ago
Not completely: > 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

227 points by mbrodersen 5y ago

I think a lot of others here are going to have the question "what does it do with UB", which is partially answered in the doc: https://compcert.org/man/manual005.html#language-reference 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.

tialaramex 5y ago
There was a CPPCon talk [I think?] about changes in this direction for C++ and the "problem" with this approach goes like this: 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.
- wruza 5y ago
  A program correctness is not just yes-or-no if you take consequences into account and state that there is some room for errors and that we deal with them instead of just meeting our fate. One thing is an incorrect value that is catched few assertions later (we check our invariants, don’t we?). A completely another thing is entire blocks of code missing from an executable and flow control broken so bad that the program is now a binary equivalent of a triggered psychopath. 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.
  - tialaramex 5y ago
    > One thing is an incorrect value that is catched few assertions later (we check our invariants, don’t we?). 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.
    - wruza 5y ago
      Is this rocket example real or imaginary? If latter, rockets do not have explode-on-assertion-fail schematics, afaik. I’m not a rocket engineer, but I find that at least restarting a subsystem is more appropriate than letting it explode “because yeah anyway”. The difference between a regular error and UB is that you can’t handle UB by definition.
      - tialaramex 5y ago
        Ariane 5's test flight self-destructed 37 seconds after launch. Its horizontal velocity was outside the range that could be represented in a 16-bit variable. In fact this check wasn't appropriate for Ariane 5 and so was removed in subsequent versions, but that's hindsight. 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.
mannykannot 5y ago
Am I right in thinking that all undefined behavior must have a defined outcome in the implementation? Otherwise, I would guess that "proven correct" is only relevant for the compilation of programs that cannot enter UB territory. 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.
- tialaramex 5y ago
  No. There's "Implementation Defined" behaviour where the compiler vendor is expected to explain what their compiler (and maybe operating system, hardware architecture, site installation) does in these cases. 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.
a1369209993 5y ago
> but it's unclear what happens for other types of UB. 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.
edwcross 5y ago
CompCert's main theorem is that the compiled code maintains or improves the behavior of the source code, as in, it can only maintain or remove erroneous behaviors. So, it can remove a division by zero, for instance, but it will never add one. Otherwise, the compiler does not guarantee the absence of UB; for that, you need Verasco (http://compcert.inria.fr/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.

bombcar 5y ago

The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, x86 and RISC-V processors. I suspect that large subset is doing a lot of lifting.

macleginn 5y ago
On their website, the claim is more ambitious: "The main result of the project is the CompCert C verified compiler, a high-assurance compiler for _almost all_ of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors." (https://compcert.org/ https://compcert.org/)
- bombcar 5y ago
  That makes me wonder even more what the missing parts are.
  - anonydsfsfs 5y ago
    The differences are documented at https://compcert.org/man/manual001.html#sec13 https://compcert.org/man/manual001.html#sec13
    - hvdijk 5y ago
      Interesting that only a restricted switch is supported, but goto is apparently available unrestricted. Any switch should be trivially translatable to if-goto-else-if-goto-etc, so I wonder what the reason for that might be.
      - MaxBarraclough 5y ago
        Just a guess, but perhaps they don't bother supporting 'unstructured switch' because they expect that input programs will most likely be written in the MISRA C subset of C anyway? 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.

rock_artist 5y ago

> CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.

Faaak 5y ago
and ?
- david_draco 5y ago
  Isn't that against Github rules? And doesn't that mean the 150 forks (republishings) are in legal danger?
  - CodesInChaos 5y ago
    There is no requirement for software on github to be open source. The github ToS just demand some basic rights needed for github to function (e.g. forking and downloading must be allowed)
  - ylyn 5y ago
    > Isn't that against Github rules? 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).
  - shakna 5y ago
    No. GitHub's Terms of Service cover certain rights, allowing them to do certain things like fork, and view the code. 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-of-service#3-ownership-of-content-right-to-post-and-license-grants https://docs.github.com/en/github/site-policy/github-terms-o...

exikyut 5y ago

As noted in the License section of the readme, > 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 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?

bombcar 5y ago
It appears that the LGPL does NOT cover the "meat" of the codebase (see the directories arm, x86, etc) and instead covers the "edges" where their code may interact with other code. 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.
alfu 5y ago
>The files in question are, from a formal verification standpoint, the interface to CompCert. They are licensed under the non-commercial license (NCL) so that they can be used together with the rest of CompCert (the implementation of the compiler, so to speak), which is NCL-only. >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/ http://vst.cs.princeton.edu/) that connect with CompCert. at https://github.com/AbsInt/CompCert/issues/140 https://github.com/AbsInt/CompCert/issues/140 (2016); GPL -> LGPL in a later commit.

Cu3PO42 5y ago

I have had the pleasure of visiting AbsInt and hearing talks on, amongst other things, CompCert. It really is a fascinating piece of software. I would highly recommend looking at the 2016 paper [1] for a bit more detail on how it works. If you're interested you can find other publications as well. 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. [1] https://hal.inria.fr/hal-01238879 https://hal.inria.fr/hal-01238879

moonchild 5y ago
> 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.
- Cu3PO42 5y ago
  I wholeheartedly agree. I didn't mean to say that the translation of the specification was a big problem, merely that all others are even more insignificant.
  - MaxBarraclough 5y ago
    Also, this has been studied empirically, and CompCert holds up well: • https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf • https://compcert.org/motivations.html 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.

etaioinshrdlu 5y ago

It would be nice if Tesla would use something like this for certain parts of the car. But you just know they won’t. Love to hear if anyone knows of any formal methods are used at all, and not talking about the self driving stack, but stuff like throttle control.

epgui 5y ago
Relevance??
- etaioinshrdlu 5y ago
  If all you think about is Tesla, every comment thread is a relevant place to post.
- mtts 5y ago
  Not usually in the habit of giving much thought to Tesla, but suggesting that a proven correct C compiler created by a company that builds transportation devices that contain lots of computers might be interesting for another company that builds transportation devices that use lots of computers seems to me to be perfectly sensible. 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.
  - 7thaccount 5y ago
    Ada/Spark is also supposed to be pretty good here.
  - robbrown451 5y ago
    I was like, since when does Airbnb build transportation devices? Oh. Nevermind.
- 5y ago

runeks 5y ago

I wonder how often a C program does something wrong because of a compiler bug versus a program bug. I’d think the former is extraordinarily rare for e.g. gcc. Although, if you spend an hour studying every line of code (as is customary when writing safety-critical code), it’s possible you may arrive at a point where the primary source of bugs is the compiler. However, for non safety-critical software I’d say buying a proven correct C compiler would be a waste of money.

Agingcoder 5y ago
Compiler bugs are not rare - it's just that most people never notice them.
crubier 5y ago
I was lucky enough to work with people working on CompCert in French public aerospace research labs. 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.
- occamrazor 5y ago
  Did they fix or report the bugs upstream?
  - archi42 5y ago
    They're usually at least reported. At least that was the case for all the compiler-bug related papers I've read.
  - crubier 5y ago
    Yes I think they systematically reported it, and explained that their work was beneficial to all C compilers as a consequence. They did not fix them though, that would have needed a team 10x larger

tankfeeder 5y ago

Btw, Monocypher passed Compcert in -interp mode.

moonchild 5y ago

CakeML[0] is another formally verified compiler. Notably, unlike compcert, it is open source. 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. 0. https://github.com/CakeML/cakeml https://github.com/CakeML/cakeml

rwmj 5y ago

I gave an introductory talk to Red Hat about proving C code with Frama-C, which touched on CompCert. (Coq, Frama-C, CompCert and OCaml are all written by an overlapping set of the same people.) Note I'm very much a beginner here myself. http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4

globuous 5y ago

Xavier Leroy, who is a big contributor to this project, was an INRIA senior researcher and was the main Ocaml développer. He’s got a lecture (in french) at the college de France where he introduces the formal verification of a basic compiler for an imperative language: https://www.college-de-france.fr/site/xavier-leroy/course-2019-12-12-09h30.htm https://www.college-de-france.fr/site/xavier-leroy/course-20..., very interesting !

belter 5y ago

Also relevant: "Verifiable C" https://vst.cs.princeton.edu/ https://vst.cs.princeton.edu/ "Cyclone a safe dialect of C" https://cyclone.thelanguage.org/ https://cyclone.thelanguage.org/ "Checked C" https://www.microsoft.com/en-us/research/project/checked-c/ https://www.microsoft.com/en-us/research/project/checked-c/ "Frama C" https://frama-c.com/ https://frama-c.com/

anonymousiam 5y ago

Some caveats in this compiler: "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.

PaulHoule 5y ago

Yeah, it even gets the undefined behavior right.

tinganho 5y ago

Couldnt this problem be dealt with unit tests?

au8er 5y ago
You cannot use unit tests for everything, since the number of unit tests required is basically infinity. Logically, unit tests can only prove an error exists and cannot show the program is correct. What they most likely did was mathematically showed that all possible edge cases (potentially inifinitely many) are all considered.
- tinganho 5y ago
  I have never heard of verified compiler before. Not entirely sure if I understand everything from their docs either. But here are my thoughts. 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?

sobriquet9 5y ago

Not completely: > 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