<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">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_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><div>Nice! I'll draft a patch for the transform.<br></div><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_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@<wbr>gmail.com</a><br><b>Subject:</b> Re: [llvm-dev] Alive now available online<u></u><u></u></span></p><div><div class="h5"><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/<wbr>rL285729</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_<wbr>bug.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><br></div></div>