3 ms·
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 d
by jbapple 12y ago
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!
- DanWaterworth 12y ago> 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.