[llvm-dev] Alive now available online

[Sanjay Patel via llvm-dev]

Following up here with a link that Nuno posted in the D29774 review, so I'm
less likely to lose the hint. :)

"You can see the list of predicates/functions here (the syntax highlighting
code):
 https://github.com/nunoplopes/alive/blob/newsema/rise4fun/language
"

Example:
http://rise4fun.com/Alive/plF

Name: slt_overflow
Pre: !WillNotOverflowSignedSub(C2, C1)
%a = add nsw i8 %x, C1
%b = icmp slt %a, C2
  =>
%b = icmp sge C2, 0


On Sun, Jan 8, 2017 at 12:26 PM, Nuno Lopes <nuno.lopes at ist.utl.pt> wrote:

> It's very on topic, certainly. We've ported more than 300 InstCombine
> patterns to Alive ourselves.
> Right now the C++ code generation is not great. Alive produces a linear
> search through the patterns, similar to how InstCombine works today.
> It's on my todo list to improve this part of Alive; I just didn't have
> time to do it yet.  If this year I manage to get an intern with experience
> on graph rewriting, we'll get it done (or try, at least)! :)
>
> Nuno
>
>
> -----Original Message-----
> From: Bryant Wong
> Sent: Friday, January 6, 2017 7:29 PM
> To: Sanjay Patel ; llvm-dev at lists.llvm.org
> Cc: Nuno Lopes ; John Regehr
> Subject: Re: [llvm-dev] Alive now available online
>
>
> Not sure how off-topic this is, but should we consider/have we considered
> porting our InstCombines to Alive? The PLDI '15 paper even demos C++
> extraction from Alive theorems. I think it'd be a small step from that to
> extracting tightly optimized VM code, not unlike what Tablegen emits.
> Everything would be so clean and readable and organized. And edge cases can
> still be handled manually, like ISel.
>
>
>
> On Fri, Jan 6, 2017 at 9:38 AM, Sanjay Patel <spatel at rotateright.com>
> wrote:
>
>
>
> 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/20170213/227b3bfb/attachment.html>