5 ms·

Closing the Gap – The Formally Verified Optimizing Compiler CompCert [pdf]

66 points by panic 10y ago

cryptarch 10y ago
Weird, the print dialog opened directly when I clicked the above link. Is that a "normal" PDF feature, or was it triggered from someplace else?
- eximius 10y ago
  Same on Linux + Chrome
  - hrjet 10y ago
    And even with uMatrix installed + JS disabled for that domain! Edit: raised an issue in uMatrix: https://github.com/gorhill/uMatrix/issues/672 https://github.com/gorhill/uMatrix/issues/672
- j_s 10y ago
  Semi-normal (PDF JavaScript) http://superuser.com/a/263875 http://superuser.com/a/263875
debatem1 10y ago
I'm sorry, I won't read this until I can do so on a formally verified pdf renderer or an attacker might hack me further upstream. Oh no, I'm commenting using an unverified browser! runs screaming into the middle distance
- tombone12 10y ago
  Pff, amateur. The only safe way to read pdfs is by getting a bunch of smartphones by dumpster diving and then discarding them once you've read the pdf once.
Animats 10y ago
Wow. That's an achievement. The key to getting the problem down to a manageable size for verification seems to have been using a large number of passes, so that each pass performs a well-defined transformation on a sequential file.
- whateveracct 10y ago
  That's a good software pattern in general, and as you use more and more powerfully typed languages, the Coq analogy becomes even more obvious. If you write small modules, it's easier to statically prove more behavior. Then all you need is to compose the modules, and thanks to composition being a small, well-defined, and lawful operation, the correctness of your program becomes the sum of its proofs :)
whatismyip 10y ago
There's been at least one attempt to make LLVM verifiable, however it's largely stalled: http://www.cis.upenn.edu/~stevez/vellvm/ http://www.cis.upenn.edu/~stevez/vellvm/
SloopJon 10y ago
A few things I notice from skimming the paper and perusing related sites: 1. Although the source is available free of charge, CompCert is not free software. I couldn't find pricing on the AbsInt site or the North American vendor's site ("Ask for a quote"). 2. Currently targets IA32, 32-bit PowerPC, and ARMv6. 3. Covers most of C99, except VLAs and certain abuses of switch statements (e.g., Duff's device). 4. Faster and smaller code than GCC -O0, reasonably close to -O1 and -O2. John Regehr points out: "If we want better code out of [GCC et al.] we can turn on their optimizers, but at that point they would fail to be capable of translating 1,000,000 random programs without miscompiling a few times." http://blog.regehr.org/archives/1052 http://blog.regehr.org/archives/1052 I'm less inclined to use C as time goes by, but for the embedded market that CompCert targets, it seems like a really useful tool.

66 points by panic 10y ago

Weird, the print dialog opened directly when I clicked the above link. Is that a "normal" PDF feature, or was it triggered from someplace else?

eximius 10y ago
Same on Linux + Chrome
- hrjet 10y ago
  And even with uMatrix installed + JS disabled for that domain! Edit: raised an issue in uMatrix: https://github.com/gorhill/uMatrix/issues/672 https://github.com/gorhill/uMatrix/issues/672
j_s 10y ago
Semi-normal (PDF JavaScript) http://superuser.com/a/263875 http://superuser.com/a/263875

debatem1 10y ago

I'm sorry, I won't read this until I can do so on a formally verified pdf renderer or an attacker might hack me further upstream. Oh no, I'm commenting using an unverified browser! runs screaming into the middle distance

tombone12 10y ago
Pff, amateur. The only safe way to read pdfs is by getting a bunch of smartphones by dumpster diving and then discarding them once you've read the pdf once.

Animats 10y ago

Wow. That's an achievement. The key to getting the problem down to a manageable size for verification seems to have been using a large number of passes, so that each pass performs a well-defined transformation on a sequential file.

whateveracct 10y ago
That's a good software pattern in general, and as you use more and more powerfully typed languages, the Coq analogy becomes even more obvious. If you write small modules, it's easier to statically prove more behavior. Then all you need is to compose the modules, and thanks to composition being a small, well-defined, and lawful operation, the correctness of your program becomes the sum of its proofs :)

whatismyip 10y ago

There's been at least one attempt to make LLVM verifiable, however it's largely stalled: http://www.cis.upenn.edu/~stevez/vellvm/ http://www.cis.upenn.edu/~stevez/vellvm/

SloopJon 10y ago

A few things I notice from skimming the paper and perusing related sites: 1. Although the source is available free of charge, CompCert is not free software. I couldn't find pricing on the AbsInt site or the North American vendor's site ("Ask for a quote"). 2. Currently targets IA32, 32-bit PowerPC, and ARMv6. 3. Covers most of C99, except VLAs and certain abuses of switch statements (e.g., Duff's device). 4. Faster and smaller code than GCC -O0, reasonably close to -O1 and -O2. John Regehr points out: "If we want better code out of [GCC et al.] we can turn on their optimizers, but at that point they would fail to be capable of translating 1,000,000 random programs without miscompiling a few times." http://blog.regehr.org/archives/1052 http://blog.regehr.org/archives/1052 I'm less inclined to use C as time goes by, but for the embedded market that CompCert targets, it seems like a really useful tool.