[llvm-dev] Alive now available online

[Sanjay Patel via llvm-dev]

On Fri, Jan 6, 2017 at 2:30 AM, Nuno Lopes <nuno.lopes at ist.utl.pt> wrote:

> Hi Sanjay,
>
>
>
> You used Alive correctly, of course :)
>
> At this moment we cannot give you the best precondition. It’s on the todo
> list, but it’s not even started yet. It’s a much harder problem to
> solve.  We do have a mode to compute the best set of nsw/nuw/exact
> attributes in the transformed expression, but it’s not enabled on the web
> interface yet (InstCombine was missing quite a few cases last time I
> checked).
>
>
>
> I played a bit with your example and realized that it doesn’t even need a
> precondition :)  Check this out: http://rise4fun.com/Alive/j
>
> (btw, > is signed comparison, and u> is unsigned).
>
>
Nice! I'll draft a patch for the transform.




>
>
> Nuno
>
>
>
>
>
> *From:* Sanjay Patel [mailto:spatel at rotateright.com]
> *Sent:* 6 de janeiro de 2017 00:35
> *To:* Nuno Lopes <nuno.lopes at ist.utl.pt>
> *Cc:* llvm-dev <llvm-dev at lists.llvm.org>; John Regehr <regehr at cs.utah.edu>;
> 3.14472+reviews.llvm.org at gmail.com
> *Subject:* Re: [llvm-dev] Alive now available online
>
>
>
> Hi Nuno,
>
> This is great. I just stumbled onto a problem that's similar to the one
> that Bryant solved in:
> https://reviews.llvm.org/rL285729
>
> define i1 @foo(i32 %x) {
>   %shl = shl nsw i32 %x, 4
>   %cmp = icmp sgt i32 %shl, 1
>   ret i1 %cmp
> }
>
> (For more background, see PR30773 - https://llvm.org/bugs/show_
> bug.cgi?id=30773 )
>
>
>
> So I'm staring at that wondering why instcombine can't see that it's
> really just:
> define i1 @foo(i32 %x) {
>   %cmp = icmp sgt i32 %x, 0
>   ret i1 %cmp
> }
>
> As a first hack, I did this:
> http://rise4fun.com/Alive/qG
>
>
> Name: sgt
> Pre: C0 > 0
> %a = shl nsw i8 %x, C1
> %b = icmp sgt %a, C0
>   =>
> %b = icmp sgt %x, (C0 >> C1)
>
> ...and success! Assuming I used Alive correctly. :)
>
> But is there a way to tell if I've chosen the most liberal constraint? Ie,
> is C0 > 0 the best pre-condition?
>
>
>
>
>
> On Thu, Jan 5, 2017 at 3:42 PM, Nuno Lopes via llvm-dev <
> llvm-dev at lists.llvm.org> wrote:
>
> Hi,
>
> Just a short email to announce that Alive is now available online:
> http://rise4fun.com/Alive
>
> The site includes a few examples (both correct and buggy). You can also
> create a "permalink" to send the proof to someone else.
>
> The execution time is limited to 30 seconds for now.  You may want to
> constrain the operand's types if the tool times out, for example.
>
> The service is still in tests.  Please let me know if you run into
> problems and/or if you have comments or feature requests.
>
> Nuno
>
> P.S.: The semantics implemented in this release is the one I've presented
> at the last LLVM dev meeting.  I've kept undef for now, though, but there's
> a poison value.  There's (very) limited support for branches as well.
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20170106/bfa0491c/attachment-0001.html>