[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