[llvm] r285729 - [InstCombine] Fold nuw left-shifts in `ugt`/`ule` comparisons.

Nuno Lopes via llvm-commits llvm-commits at lists.llvm.org
Thu Jan 5 14:34:44 PST 2017


> On 01/05/2017 03:26 AM, Nuno Lopes via llvm-commits wrote:
>> Sorry for digging up this old email, but just wanted to announce that 
>> Alive is now available online!
>> I've transcribed your example and Alive confirms that it is correct: 
>> http://rise4fun.com/Alive/R
>>
>> BTW your proof in Z3 is not sufficient to ensure soundness of the 
>> transformation.  It needs an additional proof that the transformed 
>> expression is 1) as defined as the original (no introduction of UB 
>> allowed), and 2) is not more poisonous than the original.
>>
>> Alive does all these proofs for you automatically (modulo bugs in the 
>> implementation..). You can also get a permalink and share the proof 
>> with others :)
>>
>> Please let me know if you run into problems with this online version.  
>> It's still in tests.
> 
> This sounds really neat! Can you announce this on llvm-dev instead of 
> just in this thread?
> 
>   -Hal

Thanks, will do!
Nuno


More information about the llvm-commits mailing list