Crellvm: Verified Credible Compilation for LLVM

sf.snu.ac.kr

72 points·fuklief··4 comments

"no previous systematic approaches including random testing have found any bugs in the mem2reg and gvn passes"

Uh? This is demonstrably false. A quick trip to llvm bugzilla will show you that. Zhengdong Su's C fuzzing has found basically endless bugs in GVN (and we fuzz NewGVN as well), and many bugs in GVN are well known at this point.

We just told him to not waste his time on GVN because they aren't sanely fixable without rearchitecting (hence, NewGVN).

Things like this frustrate me because a simple question on the llvm dev mailing list would have also elicited the correct answer.

(and yes, i already emailed the paper authors about this after i wrote this comment :P)

For information, links to all the bugs that we reported so far (in GCC/LLVM/CompCert/ICC and Scala) can be found at http://web.cs.ucdavis.edu/~su/emi-project/: 728 in Clang/LLVM (~250 were miscompilations); 783 in GCC.

(Also refer to http://helloqirun.github.io/projects/spe/spe.html for additional bugs reported so far in Rust and Rust bindgen.)

I do thank you for saying something since I found the claim so unbelievable I bookmarked it with a note to run every model checker and test generator I know of on those two components. All prior results Ive seen on compiler tech mean good QA tools usually find something. If the tool finds nothing, it's often a defective tool or a component already analyzed/tested to death by other tools. Now folks know it's better to invest effort in other parts of LLVM codebase.

It'd be interesting to find out if the paper's authors get back to you, and what they say.

Reply on news.ycombinator.com