3 ms·
The idea seems to be a bit broader than that: we can test any group of compilers, none of whom we trust to be correct, by comparing their outputs against each o
by setr 7y ago
The idea seems to be a bit broader than that: we can test any group of compilers, none of whom we trust to be correct, by comparing their outputs against each other.
Though it won't tell us who is wrong, it tells us one of the pairs is (or both).
- WalterBright 7y ago> Though it won't tell us who is wrong, it tells us one of the pairs is (or both). If it's implementation-defined behavior, it won't even tell you that.
- recursivecaveat 7y agoCSmith is carefully designed to only generate fully defined programs. That obviously limits the scope of bugs it covers quite a lot, but it still managed to uncover quite a few. Its biggest weakness is the difficulty of minimizing and root-causing bugs.
- zellyn 7y agoregehr's posts on program minimization are quite fascinating in their own right: https://blog.regehr.org/archives/1679 https://blog.regehr.org/archives/1679
- kazinator 7y agoThat doesn't matter though; if there is any difference, we can sort out the root cause by inspection. There are also false negatives: either, or both compilers are wrong, or else the test program is wrong (undefined behavior or non-portable), or some combination of these, yet by fluke the results agree. That's no big loss; if you're fuzzing, you're generating a lot of this stuff. If this geneated program won't catch a problem, maybe another one will. Individually, the test cases are cheap.
- hoseja 7y agoUnless all are wrong in the same way, which doesn't seem too impossible.
- tuukkah 7y agoOne of their compilers is never wrong: "Formal Methods as Bugscreen [--] the formally-verified CompCert compiler"
- jcranmer 7y agoJohn Regehr did find 11 bugs in CompCert (the unverified portion).
- tuukkah 7y agoIf I've understood correctly, the compiling step is verified but the parsing and assembly steps are not, and no bugs have been found where valid input would have been compiled to valid but wrong assembly. I didn't see a statement about this on CompCert's web site though.
- setr 7y agoThere were no bugs that their program could find; not that there are no bugs at all :-)
- setr 7y agoThe tool isn't meant to find all bugs, but rather to suggest that bugs exist. That there exist limitations to the kinds of bugs it can find is probably acceptable. Also if everyone implements something the same way, incorrectly according to the standard, then perhaps the standard itself is wrong. But otherwise, you just need one compiler to implement more strictly according to the standard for the bug to be suggested