Verifying InstCombine optimizations

Project Infrastructure LLVM Dev List Archives
#1

Hi,

We built a prototype, named ALIVe, for *automatically* verifying the
correctness of InstCombine optimizations.
Curently, ALIVe is able to verify transformations involving arithmetic
operations, and we are working to add support for the remaining operations.

You can read more about the the tool in: ALIVe: Automatic LLVM InstCombine Verifier – Embedded in Academia

The tool is open-source, so please use it before adding a new transformation
to InstCombine :slight_smile:

Please let us know if you have any question/comment/feedback.

Thanks,
Nuno

#2

From: "Nuno Lopes" <nuno.lopes@ist.utl.pt>
To: llvmdev@cs.uiuc.edu
Sent: Thursday, July 24, 2014 3:47:27 AM
Subject: [LLVMdev] Verifying InstCombine optimizations

Hi,

We built a prototype, named ALIVe, for *automatically* verifying the
correctness of InstCombine optimizations.
Curently, ALIVe is able to verify transformations involving
arithmetic
operations, and we are working to add support for the remaining
operations.

You can read more about the the tool in:
http://blog.regehr.org/archives/1170

The tool is open-source, so please use it before adding a new
transformation
to InstCombine :slight_smile:

This looks spectacular, thank you! (and thanks for clarifying the relative Z3 licensing issues).

-Hal