<div dir="ltr">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.<br><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jan 6, 2017 at 9:38 AM, Sanjay Patel <span dir="ltr"><<a href="mailto:spatel@rotateright.com" target="_blank">spatel@rotateright.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote"><span>On Fri, Jan 6, 2017 at 2:30 AM, Nuno Lopes <span dir="ltr"><<a href="mailto:nuno.lopes@ist.utl.pt" target="_blank">nuno.lopes@ist.utl.pt</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div link="blue" vlink="purple" lang="EN-US"><div class="m_-8008695695818998755m_-918163879514393090m_6176011440152916242WordSection1"><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">Hi Sanjay,<u></u><u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif"><u></u> <u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">You used Alive correctly, of course :)<u></u><u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">At this moment we cannot give you the best precondition. It</span><span style="font-size:11.0pt">’</span><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">s on the todo list, but it</span><span style="font-size:11.0pt">’</span><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">s not even started yet. It</span><span style="font-size:11.0pt">’</span><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">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</span><span style="font-size:11.0pt">’</span><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">s not enabled on the web interface yet (InstCombine was missing quite a few cases last time I checked).<u></u><u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif"><u></u> <u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">I played a bit with your example and realized that it doesn</span><span style="font-size:11.0pt">’</span><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">t even need a precondition :)  Check this out: <a href="http://rise4fun.com/Alive/j" target="_blank">http://rise4fun.com/Alive/j</a><u></u><u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">(btw, > is signed comparison, and u> is unsigned).<u></u><u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif"><u></u></span></p></div></div></blockquote><div><br></div></span><div>Nice! I'll draft a patch for the transform.<br></div><div><div class="m_-8008695695818998755h5"><div><br><br> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div link="blue" vlink="purple" lang="EN-US"><div class="m_-8008695695818998755m_-918163879514393090m_6176011440152916242WordSection1"><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif"> <u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">Nuno<u></u><u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif"><u></u> <u></u></span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif"><u></u> <u></u></span></p><p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">From:</span></b><span style="font-size:11.0pt;font-family:"Calibri",sans-serif"> Sanjay Patel [mailto:<a href="mailto:spatel@rotateright.com" target="_blank">spatel@rotateright.com</a><wbr>] <br><b>Sent:</b> 6 de janeiro de 2017 00:35<br><b>To:</b> Nuno Lopes <<a href="mailto:nuno.lopes@ist.utl.pt" target="_blank">nuno.lopes@ist.utl.pt</a>><br><b>Cc:</b> llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a>>; John Regehr <<a href="mailto:regehr@cs.utah.edu" target="_blank">regehr@cs.utah.edu</a>>; <a href="mailto:3.14472%2Breviews.llvm.org@gmail.com" target="_blank">3.14472+reviews.llvm.org@gmail<wbr>.com</a><br><b>Subject:</b> Re: [llvm-dev] Alive now available online<u></u><u></u></span></p><div><div class="m_-8008695695818998755m_-918163879514393090h5"><p class="MsoNormal"><u></u> <u></u></p><div><div><div><p class="MsoNormal" style="margin-bottom:12.0pt">Hi Nuno,<u></u><u></u></p></div><p class="MsoNormal" style="margin-bottom:12.0pt">This is great. I just stumbled onto a problem that's similar to the one that Bryant solved in:<br><a href="https://reviews.llvm.org/rL285729" target="_blank">https://reviews.llvm.org/rL285<wbr>729</a><br><br>define i1 @foo(i32 %x) {<br>  %shl = shl nsw i32 %x, 4<br>  %cmp = icmp sgt i32 %shl, 1<br>  ret i1 %cmp<br>}<u></u><u></u></p></div><p class="MsoNormal">(For more background, see PR30773 - <a href="https://llvm.org/bugs/show_bug.cgi?id=30773" target="_blank">https://llvm.org/bugs/show_bug<wbr>.cgi?id=30773</a> )<u></u><u></u></p><div><p class="MsoNormal"><u></u> <u></u></p></div><div><p class="MsoNormal" style="margin-bottom:12.0pt">So I'm staring at that wondering why instcombine can't see that it's really just:<br>define i1 @foo(i32 %x) {<br>  %cmp = icmp sgt i32 %x, 0<br>  ret i1 %cmp<br>}<u></u><u></u></p></div><div><p class="MsoNormal">As a first hack, I did this:<br><a href="http://rise4fun.com/Alive/qG" target="_blank">http://rise4fun.com/Alive/qG</a><u></u><u></u></p></div><div><p class="MsoNormal" style="margin-bottom:12.0pt"><br>Name: sgt<br>Pre: C0 > 0<br>%a = shl nsw i8 %x, C1<br>%b = icmp sgt %a, C0<br>  =><br>%b = icmp sgt %x, (C0 >> C1)<u></u><u></u></p></div><div><p class="MsoNormal">...and success! Assuming I used Alive correctly. :)<br><br>But is there a way to tell if I've chosen the most liberal constraint? Ie, is C0 > 0 the best pre-condition?<u></u><u></u></p></div><div><p class="MsoNormal" style="margin-bottom:12.0pt"><u></u> <u></u></p></div></div><div><p class="MsoNormal"><u></u> <u></u></p><div><p class="MsoNormal">On Thu, Jan 5, 2017 at 3:42 PM, Nuno Lopes via llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a>> wrote:<u></u><u></u></p><blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm"><p class="MsoNormal">Hi,<br><br>Just a short email to announce that Alive is now available online: <a href="http://rise4fun.com/Alive" target="_blank">http://rise4fun.com/Alive</a><br><br>The site includes a few examples (both correct and buggy). You can also create a "permalink" to send the proof to someone else.<br><br>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.<br><br>The service is still in tests.  Please let me know if you run into problems and/or if you have comments or feature requests.<br><br>Nuno<br><br>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. <br>______________________________<wbr>_________________<br>LLVM Developers mailing list<br><a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a><br><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/llvm-dev</a><u></u><u></u></p></blockquote></div><p class="MsoNormal"><u></u> <u></u></p></div></div></div></div></div></blockquote></div></div></div><br></div></div>
</blockquote></div><br></div></div>