llvm dev - Dec 2012 - [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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20121228/224c840a/attachment.html>

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.