[LLVMdev] Verifying InstCombine optimizations

[Hal Finkel]

----- 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