17 ms·

The CompCert C Compiler

203 points by nequo 2y ago

lisper 2y ago
A cautionary tale for anyone relying on formal proofs of correctness: https://spinroot.com/spin/Doc/rax.pdf https://spinroot.com/spin/Doc/rax.pdf TL;DR: in the 1990s NASA flew an autonomous control system that was formally verified, tested out the wazoo, but which nonetheless failed in flight. [UPDATE] I did not mean to imply that the formal verification failed. It did not. The formal verification worked as advertised. The cause of the failure was much more subtle and nuanced.
- elteto 2y ago
  You make it seem like the formal verification missed an issue. Not quite what happened: "The first effort consisted of analyzing part of the RA autonomous space craft software using the SPIN model checker. One of the errors found with SPIN, a missing critical section around a conditional wait statement, was in fact reintroduced in a different subsystem that was not verified in this first pre-flight effort. This error caused a real deadlock in the RA during flight in space." The model actually found an issue that was later reintroduced in a different part of the system that was not formally verified. If anything, it tells us we need _more_ formal verification!
  - lisper 2y ago
    > You make it seem like the formal verification missed an issue. Sorry, that was not my intent. I added a clarification.
    - sobkas 2y ago
      > > You make it seem like the formal verification missed an issue. > Sorry, that was not my intent. I added a clarification. I'm sorry but it didn't. Without reading next comment I wouldn't know why it failed.
- cwzwarich 2y ago
  I’m confused. Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? Isn’t this more of a cautionary tale for someone not relying on formal verification?
  - lisper 2y ago
    > Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? No, it was quite a bit more subtle than that. The problem was that there was no mechanism to enforce the use of the formally verified API, and an application programmer put in a direct call to a system function that bypassed that API. Source: I was the technical lead on the RAX executive.
    - extrabajs 2y ago
      It sounds more like a cautionary tale against bypassing APIs. What part of this is related to formal verification?
    - Quekid5 2y ago
      This is why friends don't let friends use unsafePerformIO ... or whatever the equivalent was here :) I'm still a bit confused about the point though. I feel like an adequate rejoinder would be to enforce formal methods at all the levels? I'm obviously not talking specifics (because I don't know them! ... and you do), but this seems like a failure of process or lack of enforcement of formal methods "all the way down" as it were. I dunno, color me confused...
      - wucke13 2y ago
        Which almost reads as a cautionary tale about mechanisms like Dust's `unsafe`. Not necessarily the specifics of the Rust, but the overall idea of having a safe (by whatever means) sunset of operations and and additional unsafe operations, which eases code analysis tremendously. You can't got without unsafe in most embedded systems. But it's good to very explicitly mark in the code wherever the unknown depths of UB lurk if not the most attention is exercised.
- tombert 2y ago
  Honestly, I don't think you're wrong, and this is from a guy who is getting a PhD in formal methods. Formal methods are super cool, and formal verification is even cool, but it can be really easy to think it's always perfect. It gives you such amazing guardrails most of the time that it can be easy to stop looking for when there aren't any. For example, model checking is cool and useful, but sort of by definition it is exhaustive and as a result you end up having to restrict scope in a lot of cases (For example, redefining the INTEGERS set to {-1000...1000} in TLA+). This is almost always perfectly fine and can catch a lot of weird cases, but it's easy to forget that "nearly everything" is not the same thing as "everything". Obviously I still think formal methods are worth it, but they're not a substitute for being careful.
  - lisper 2y ago
    > formal methods are worth it, but they're not a substitute for being careful. Yes. Exactly this. I hereby dub this Tombert's law. :-)
    - tombert 2y ago
      I'm honored! I always thought Tombert's Law would end up being something about cartoon trivia, so this is much better.
      - lisper 2y ago
        I'm going to start listing it alongside my other favorite aphorism: Furious activity is no substitute for understanding. -- H.H. Williams
- aidenn0 2y ago
  IIRC Regehr found a bug when testing compcert. It turned out to be a bug in a standard header file. Similar idea of bugs due to incomplete verification.
lisper 2y ago
I have never understood why the C community does not rally around what seems to me to be the obvious answer to the main problem with C: stop conflating pointers and arrays, or at least deprecate it. Make arrays a separate data type, not a synonym for a pointer, and require the system to track the size of arrays either at compile time or at run time (or both). Make a[x] be a bounds-checked array reference rather than a synonym for an unchecked dereference of a+x. It seems stupidly obvious to me that this is the Right Thing. Yes, it would be a non-backwards-compatible change, but the benefits seem to me to vastly outweigh the costs.
- elteto 2y ago
  Because you can't do that and still call the resulting language C. It would be a different language incompatible will _all_ existing C code. Pointer decay is a fundamental mechanic in C. If you use arrays in C, and you pass said arrays as an argument to a function, then you are dealing with pointer decay.
  - lisper 2y ago
    > Because you can't do that and still call the resulting language C. Says who? Non-backwards-compatible changes are made to language standards all the time. It's not pain-free, but neither is the status quo. Besides, who cares what the language is called? Change the name if that's what it takes, but stop conflating pointers and arrays. The cost of that has been literally billions of dollars in losses due to buffer overflows over the decades.
    - usrnm 2y ago
      > The cost of that has been literally billions of dollars in losses due to buffer overflows over the decades. How much, do you think, would rewriting all existing C code cost?
      - junon 2y ago
        Nothing, if new standards are opted in via a #pragma.
dang 2y ago
Related: CompCert – Formally-verified C compiler - https://news.ycombinator.com/item?id=27648735 https://news.ycombinator.com/item?id=27648735 - June 2021 (123 comments) CompCert C a formally verified optimizing compiler for a large subset of C99 - https://news.ycombinator.com/item?id=27644356 https://news.ycombinator.com/item?id=27644356 - June 2021 (1 comment) CompCert – A formally verified C compiler - https://news.ycombinator.com/item?id=18968125 https://news.ycombinator.com/item?id=18968125 - Jan 2019 (57 comments) Closing the Gap – The Formally Verified Optimizing Compiler CompCert [pdf] - https://news.ycombinator.com/item?id=13046449 https://news.ycombinator.com/item?id=13046449 - Nov 2016 (10 comments) CompCert: A formally verified optimizing C compiler - https://news.ycombinator.com/item?id=9130934 https://news.ycombinator.com/item?id=9130934 - March 2015 (62 comments) CompCert - Compilers you can formally trust - https://news.ycombinator.com/item?id=2619650 https://news.ycombinator.com/item?id=2619650 - June 2011 (28 comments)
tombert 2y ago
When I was writing my proposal to get into a PhD program, I had to do a crash course in formally verified applications. The focus of the program is actually in Isabelle, but Coq is similar enough (in a hand-wavey kind of way) to where it was relevant to what I was writing about, and I stumbled across a few formally verified things with Coq. I became slightly obsessed with CompCert, but it felt like a "real" program that was utilizing proper formal verification techniques. It seemed so cool to me that there can be (to some extent), and "objectively correct" version of a C compiler. I still think it's very cool; I wish people would geek out about this stuff as much as I would sometimes.
nullifidian 2y ago
I think it's important to note that you can't use it commercially. "The INRIA Non-Commercial License Agreement is a non-free license that grants you the right to use the CompCert verified compiler for educational, research or evaluation purposes only, but prohibits any commercial use. For commercial use you need a Software Usage Agreement from AbsInt Angewandte Informatik GmbH."
- f1shy 2y ago
  The name of the company is joke, for those who do bot know, it is read same as absinthe in german, where the company is.
  - drdrey 2y ago
    it's also short for Abstract Interpretation, right?
JohnCClarke 2y ago
This is very cool. Can the work involved in creating the proof-of-correctness be leveraged to create similar proofs for compilers of more modern languages?
jack1243star 2y ago
> longjmp and setjmp are not guaranteed to work. Curious why the author words it like this, rather than just "not supported".
- user2342 2y ago
  They may work as expected (and probably will), but they are not covered by the proof.
rurban 2y ago
I wonder how many projects actually do use ccert in its pipeline. I've tried on some big library of mine (25Mb compiled), but it usually runs out of memory. And it's a hassle to fix all the extensions which ccert doesn't support. Esp. __FILE__ and __LINE__
- gergo_barany 2y ago
  __FILE__ and __LINE__ are not extensions, they are standard C constructs. They are typically resolved by the preprocessor, just like #include and whatever, so the actual CompCert compiler should never see them. Maybe you're doing something weird, applying it to non-preprocessed files in a mode where it thinks the input is already preprocessed? EDIT: In fact, here is CompCert preprocessing and then compiling a file containing __FILE__ and __LINE__ just fine: https://gcc.godbolt.org/z/E8sMPPTs4 https://gcc.godbolt.org/z/E8sMPPTs4
JonChesterfield 2y ago
I think compcert uses this https://github.com/jhjourdan/C11parser https://github.com/jhjourdan/C11parser as the parser. It's a lalr grammar with hooks for the usual lexer hack. I suspect that with a symbol table would make a cheap and reliable C to AST compiler. Somewhere on my todo list.
- gergo_barany 2y ago
  What would you want to use it for, and why not use an existing solution? My first choice would be Frama-C (frama-c.com), which has served me well in the past.
  - JonChesterfield 2y ago
    Personally, I want to compile C with vector types to x64 and to amdgpu at the same time, for running code on APUs like the MI300A. I have a suspicion checking that idea works in practice will be easier building from a grammar than from clang.
    - gergo_barany 2y ago
      So you want to add new builtin types for vectors? Yes, building on a parser sounds like a good approach. Otherwise, Frama-C would give you a nice detailed AST, but it might be complicated to extend this way. Sounds like a cool project, good luck!
      - JonChesterfield 2y ago
        The vector types are straightforward and already implemented in clang - it's twisting llvm to represent two different triples in a single module and handling calls between them that I think will be extremely tedious to implement. Frama-c / libfirm / other-compiler-here means getting started quickly and then an uphill battle against the existing implementation. Grammar plus symbol table should yield ast, C doesn't need that much sema checking after the parse, build ssa form cranelift-style then write out asm. Should be a cheap enough exercise to walk through but the unknown unknowns will mess up the schedule and there's a day job in the way. One for a week's vacation I think.
Alifatisk 2y ago
First I stumbled upon Xr0, and now this! I really enjoy these attempts at safe C. Kinda wish I didn't have to recompile this myself though. But the procedure doesn't look that challenging anyways.
- naasking 2y ago
  CompCert isn't about a safe C, it's a verified C compiler. This means it has proofs that verify that the compiler correctly implements the C standard and that the binary code it produces is a faithful implementation of the original program as determined by C's semantics. This is used, for example, as part of the verification for the high-integrity, high-security seL4 microkernel.
  - Alifatisk 2y ago
    Ohhh okey!
sydbarrett74 2y ago
I would like to see Checked C (coming out of Microsoft Research) gain more traction.

203 points by nequo 2y ago

A cautionary tale for anyone relying on formal proofs of correctness: https://spinroot.com/spin/Doc/rax.pdf https://spinroot.com/spin/Doc/rax.pdf TL;DR: in the 1990s NASA flew an autonomous control system that was formally verified, tested out the wazoo, but which nonetheless failed in flight. [UPDATE] I did not mean to imply that the formal verification failed. It did not. The formal verification worked as advertised. The cause of the failure was much more subtle and nuanced.

elteto 2y ago
You make it seem like the formal verification missed an issue. Not quite what happened: "The first effort consisted of analyzing part of the RA autonomous space craft software using the SPIN model checker. One of the errors found with SPIN, a missing critical section around a conditional wait statement, was in fact reintroduced in a different subsystem that was not verified in this first pre-flight effort. This error caused a real deadlock in the RA during flight in space." The model actually found an issue that was later reintroduced in a different part of the system that was not formally verified. If anything, it tells us we need _more_ formal verification!
- lisper 2y ago
  > You make it seem like the formal verification missed an issue. Sorry, that was not my intent. I added a clarification.
  - sobkas 2y ago
    > > You make it seem like the formal verification missed an issue. > Sorry, that was not my intent. I added a clarification. I'm sorry but it didn't. Without reading next comment I wouldn't know why it failed.
cwzwarich 2y ago
I’m confused. Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? Isn’t this more of a cautionary tale for someone not relying on formal verification?
- lisper 2y ago
  > Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? No, it was quite a bit more subtle than that. The problem was that there was no mechanism to enforce the use of the formally verified API, and an application programmer put in a direct call to a system function that bypassed that API. Source: I was the technical lead on the RAX executive.
  - extrabajs 2y ago
    It sounds more like a cautionary tale against bypassing APIs. What part of this is related to formal verification?
  - Quekid5 2y ago
    This is why friends don't let friends use unsafePerformIO ... or whatever the equivalent was here :) I'm still a bit confused about the point though. I feel like an adequate rejoinder would be to enforce formal methods at all the levels? I'm obviously not talking specifics (because I don't know them! ... and you do), but this seems like a failure of process or lack of enforcement of formal methods "all the way down" as it were. I dunno, color me confused...
    - wucke13 2y ago
      Which almost reads as a cautionary tale about mechanisms like Dust's `unsafe`. Not necessarily the specifics of the Rust, but the overall idea of having a safe (by whatever means) sunset of operations and and additional unsafe operations, which eases code analysis tremendously. You can't got without unsafe in most embedded systems. But it's good to very explicitly mark in the code wherever the unknown depths of UB lurk if not the most attention is exercised.
tombert 2y ago
Honestly, I don't think you're wrong, and this is from a guy who is getting a PhD in formal methods. Formal methods are super cool, and formal verification is even cool, but it can be really easy to think it's always perfect. It gives you such amazing guardrails most of the time that it can be easy to stop looking for when there aren't any. For example, model checking is cool and useful, but sort of by definition it is exhaustive and as a result you end up having to restrict scope in a lot of cases (For example, redefining the INTEGERS set to {-1000...1000} in TLA+). This is almost always perfectly fine and can catch a lot of weird cases, but it's easy to forget that "nearly everything" is not the same thing as "everything". Obviously I still think formal methods are worth it, but they're not a substitute for being careful.
- lisper 2y ago
  > formal methods are worth it, but they're not a substitute for being careful. Yes. Exactly this. I hereby dub this Tombert's law. :-)
  - tombert 2y ago
    I'm honored! I always thought Tombert's Law would end up being something about cartoon trivia, so this is much better.
    - lisper 2y ago
      I'm going to start listing it alongside my other favorite aphorism: Furious activity is no substitute for understanding. -- H.H. Williams
aidenn0 2y ago
IIRC Regehr found a bug when testing compcert. It turned out to be a bug in a standard header file. Similar idea of bugs due to incomplete verification.

lisper 2y ago

I have never understood why the C community does not rally around what seems to me to be the obvious answer to the main problem with C: stop conflating pointers and arrays, or at least deprecate it. Make arrays a separate data type, not a synonym for a pointer, and require the system to track the size of arrays either at compile time or at run time (or both). Make a[x] be a bounds-checked array reference rather than a synonym for an unchecked dereference of a+x. It seems stupidly obvious to me that this is the Right Thing. Yes, it would be a non-backwards-compatible change, but the benefits seem to me to vastly outweigh the costs.

elteto 2y ago
Because you can't do that and still call the resulting language C. It would be a different language incompatible will _all_ existing C code. Pointer decay is a fundamental mechanic in C. If you use arrays in C, and you pass said arrays as an argument to a function, then you are dealing with pointer decay.
- lisper 2y ago
  > Because you can't do that and still call the resulting language C. Says who? Non-backwards-compatible changes are made to language standards all the time. It's not pain-free, but neither is the status quo. Besides, who cares what the language is called? Change the name if that's what it takes, but stop conflating pointers and arrays. The cost of that has been literally billions of dollars in losses due to buffer overflows over the decades.
  - usrnm 2y ago
    > The cost of that has been literally billions of dollars in losses due to buffer overflows over the decades. How much, do you think, would rewriting all existing C code cost?
    - junon 2y ago
      Nothing, if new standards are opted in via a #pragma.

dang 2y ago

Related: CompCert – Formally-verified C compiler - https://news.ycombinator.com/item?id=27648735 https://news.ycombinator.com/item?id=27648735 - June 2021 (123 comments) CompCert C a formally verified optimizing compiler for a large subset of C99 - https://news.ycombinator.com/item?id=27644356 https://news.ycombinator.com/item?id=27644356 - June 2021 (1 comment) CompCert – A formally verified C compiler - https://news.ycombinator.com/item?id=18968125 https://news.ycombinator.com/item?id=18968125 - Jan 2019 (57 comments) Closing the Gap – The Formally Verified Optimizing Compiler CompCert [pdf] - https://news.ycombinator.com/item?id=13046449 https://news.ycombinator.com/item?id=13046449 - Nov 2016 (10 comments) CompCert: A formally verified optimizing C compiler - https://news.ycombinator.com/item?id=9130934 https://news.ycombinator.com/item?id=9130934 - March 2015 (62 comments) CompCert - Compilers you can formally trust - https://news.ycombinator.com/item?id=2619650 https://news.ycombinator.com/item?id=2619650 - June 2011 (28 comments)

tombert 2y ago

When I was writing my proposal to get into a PhD program, I had to do a crash course in formally verified applications. The focus of the program is actually in Isabelle, but Coq is similar enough (in a hand-wavey kind of way) to where it was relevant to what I was writing about, and I stumbled across a few formally verified things with Coq. I became slightly obsessed with CompCert, but it felt like a "real" program that was utilizing proper formal verification techniques. It seemed so cool to me that there can be (to some extent), and "objectively correct" version of a C compiler. I still think it's very cool; I wish people would geek out about this stuff as much as I would sometimes.

nullifidian 2y ago

I think it's important to note that you can't use it commercially. "The INRIA Non-Commercial License Agreement is a non-free license that grants you the right to use the CompCert verified compiler for educational, research or evaluation purposes only, but prohibits any commercial use. For commercial use you need a Software Usage Agreement from AbsInt Angewandte Informatik GmbH."

f1shy 2y ago
The name of the company is joke, for those who do bot know, it is read same as absinthe in german, where the company is.
- drdrey 2y ago
  it's also short for Abstract Interpretation, right?

JohnCClarke 2y ago

This is very cool. Can the work involved in creating the proof-of-correctness be leveraged to create similar proofs for compilers of more modern languages?

jack1243star 2y ago

> longjmp and setjmp are not guaranteed to work. Curious why the author words it like this, rather than just "not supported".

user2342 2y ago
They may work as expected (and probably will), but they are not covered by the proof.

rurban 2y ago

I wonder how many projects actually do use ccert in its pipeline. I've tried on some big library of mine (25Mb compiled), but it usually runs out of memory. And it's a hassle to fix all the extensions which ccert doesn't support. Esp. __FILE__ and __LINE__

gergo_barany 2y ago
__FILE__ and __LINE__ are not extensions, they are standard C constructs. They are typically resolved by the preprocessor, just like #include and whatever, so the actual CompCert compiler should never see them. Maybe you're doing something weird, applying it to non-preprocessed files in a mode where it thinks the input is already preprocessed? EDIT: In fact, here is CompCert preprocessing and then compiling a file containing __FILE__ and __LINE__ just fine: https://gcc.godbolt.org/z/E8sMPPTs4 https://gcc.godbolt.org/z/E8sMPPTs4

JonChesterfield 2y ago

I think compcert uses this https://github.com/jhjourdan/C11parser https://github.com/jhjourdan/C11parser as the parser. It's a lalr grammar with hooks for the usual lexer hack. I suspect that with a symbol table would make a cheap and reliable C to AST compiler. Somewhere on my todo list.

gergo_barany 2y ago
What would you want to use it for, and why not use an existing solution? My first choice would be Frama-C (frama-c.com), which has served me well in the past.
- JonChesterfield 2y ago
  Personally, I want to compile C with vector types to x64 and to amdgpu at the same time, for running code on APUs like the MI300A. I have a suspicion checking that idea works in practice will be easier building from a grammar than from clang.
  - gergo_barany 2y ago
    So you want to add new builtin types for vectors? Yes, building on a parser sounds like a good approach. Otherwise, Frama-C would give you a nice detailed AST, but it might be complicated to extend this way. Sounds like a cool project, good luck!
    - JonChesterfield 2y ago
      The vector types are straightforward and already implemented in clang - it's twisting llvm to represent two different triples in a single module and handling calls between them that I think will be extremely tedious to implement. Frama-c / libfirm / other-compiler-here means getting started quickly and then an uphill battle against the existing implementation. Grammar plus symbol table should yield ast, C doesn't need that much sema checking after the parse, build ssa form cranelift-style then write out asm. Should be a cheap enough exercise to walk through but the unknown unknowns will mess up the schedule and there's a day job in the way. One for a week's vacation I think.

Alifatisk 2y ago

First I stumbled upon Xr0, and now this! I really enjoy these attempts at safe C. Kinda wish I didn't have to recompile this myself though. But the procedure doesn't look that challenging anyways.

naasking 2y ago
CompCert isn't about a safe C, it's a verified C compiler. This means it has proofs that verify that the compiler correctly implements the C standard and that the binary code it produces is a faithful implementation of the original program as determined by C's semantics. This is used, for example, as part of the verification for the high-integrity, high-security seL4 microkernel.
- Alifatisk 2y ago
  Ohhh okey!

sydbarrett74 2y ago

I would like to see Checked C (coming out of Microsoft Research) gain more traction.