[LLVMdev] verification methods for correctness of a compiler

[Criswell, John T]

Dear Jyoti,

You might want to check out LLVM M.D. at http://llvm-md.org.  It is a system that converts unoptimized code and optimized code into eSSA form and then applies rewriting rules to normalize the eSSA form.  If the unoptimized and optimized code normalize to the same thing, then they are semantically equivalent and the optimization(s) are correct.

LLVM M.D. source code is available, but it works for an older version of LLVM and isn't integrated into the LLVM tool chain as well as it could be.  It's also a research prototype, so it needs some additional work to handle optimizations on floating point code, vectors, and so forth.

I recommend you read the LLVM M.D. papers at http://llvm-md.org.

-- John T.

________________________________________
From: llvmdev-bounces at cs.uiuc.edu [llvmdev-bounces at cs.uiuc.edu] on behalf of Jyoti [jyoti.yalamanchili at gmail.com]
Sent: Friday, December 28, 2012 2:44 AM
To: llvmdev at cs.uiuc.edu
Subject: [LLVMdev] verification methods for correctness of a compiler

Hello,

Are there any translation validation tools available to check the correctness of a compiler after each stage, or any tool to check the correction of translation after some particular stage like AST  or .ll
generation or after optimization ? I would like to know if any of those are being used in clang's development and if any such tools exist in first place. I have come across certain papers explaining about "CoVaC: Compiler Validation by Program Analysis of the cross-product" which explains how it can be achieved, however source code or tools aren't available. As far as i know, till date the best ways to validate any compiler is by running a host of regression test suites explicitly hand written to verify language compliance, various types of optimization so on and so forth. Just wondering if i am missing something relevant that's out there.

Thanks in advance.