llvm dev - Jul 2014 - [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 :)

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

Thanks,
Nuno

----- Original Message -----
> From: "Nuno Lopes" <nuno.lopes at ist.utl.pt>
> To: llvmdev at 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 :)
This looks spectacular, thank you! (and thanks for clarifying the relative Z3
licensing issues).

 -Hal
> 
> Please let us know if you have any question/comment/feedback.
> 
> Thanks,
> Nuno
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
> 
-- 
Hal Finkel
Assistant Computational Scientist
Leadership Computing Facility
Argonne National Laboratory