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/20170106/fb8d6992/attachment.html>
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
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>