Item — HN Reader

Although there seem to have been parts of it that hadn't been formally verified:

"Using Csmith, we found previously unknown bugs in unproved parts of CompCert—bugs that cause this compiler to silently produce incorrect code." (http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf)

The CompCert homepage tells us that the same authors did a study in the same year (2011) without finding any wrong-code errors.

But even if they hadn't; I'd still be excited about CompCert demonstrating that this level of verification is indeed possible. Because then verifying the unverified parts would probably be just as feasible, given enough resources.

1 comments

The Csmith paper notes two types of errors found in CompCert: front-end errors and a misunderstanding of PPC semantics.

The former type of bug was apparently due to a part of the compiler that wasn't verified at the time. According to the Csmith paper, " This bug and five others like it were in CompCert’s unverified front-end code. Partly in response to these bug reports, the main CompCert developer expanded the verified portion of CompCert to include C’s integer promotions and other tricky implicit casts."

Additionally, the CompCert team produced a validated parser which they discussed in their ESOP 2012 paper, "Validating LR(1) Parsers"

The second type of bug (misunderstanding the semantics of the target architecture) is, as far as I know, impossible to avoid. Any verification project can end up with a true proof of the wrong theorem!

> The second type of bug (misunderstanding the semantics of the target architecture) is, as far as I know, impossible to avoid. Any verification project can end up with a true proof of the wrong theorem!

Indeed. However, although it's impossible to avoid, you can still take steps to make it less likely.

When you formally verify code, you are showing that a program has a particular specification.

If you want to eliminate errors in your specification, you should aim to make it as simple as possible, so that people with domain knowledge (in this case, people with a correct understanding of PPC) would be able to tell whether your specification is correct.