<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 15 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman",serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:12.0pt;
font-family:"Times New Roman",serif;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body lang=EN-US link=blue vlink=purple><div class=WordSection1><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri",sans-serif'>Hi Sanjay,<o:p></o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri",sans-serif'><o:p> </o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri",sans-serif'>You used Alive correctly, of course :)<o:p></o:p></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).<o:p></o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri",sans-serif'><o:p> </o:p></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">http://rise4fun.com/Alive/j</a><o:p></o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri",sans-serif'>(btw, > is signed comparison, and u> is unsigned).<o:p></o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri",sans-serif'><o:p> </o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri",sans-serif'>Nuno<o:p></o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri",sans-serif'><o:p> </o:p></span></p><p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri",sans-serif'><o:p> </o:p></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:spatel@rotateright.com] <br><b>Sent:</b> 6 de janeiro de 2017 00:35<br><b>To:</b> Nuno Lopes <nuno.lopes@ist.utl.pt><br><b>Cc:</b> llvm-dev <llvm-dev@lists.llvm.org>; John Regehr <regehr@cs.utah.edu>; 3.14472+reviews.llvm.org@gmail.com<br><b>Subject:</b> Re: [llvm-dev] Alive now available online<o:p></o:p></span></p><p class=MsoNormal><o:p> </o:p></p><div><div><div><p class=MsoNormal style='margin-bottom:12.0pt'>Hi Nuno,<o:p></o:p></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">https://reviews.llvm.org/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>}<o:p></o:p></p></div><p class=MsoNormal>(For more background, see PR30773 - <a href="https://llvm.org/bugs/show_bug.cgi?id=30773">https://llvm.org/bugs/show_bug.cgi?id=30773</a> )<o:p></o:p></p><div><p class=MsoNormal><o:p> </o:p></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>}<o:p></o:p></p></div><div><p class=MsoNormal>As a first hack, I did this:<br><a href="http://rise4fun.com/Alive/qG">http://rise4fun.com/Alive/qG</a><o:p></o:p></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)<o:p></o:p></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?<o:p></o:p></p></div><div><p class=MsoNormal style='margin-bottom:12.0pt'><o:p> </o:p></p></div></div><div><p class=MsoNormal><o:p> </o:p></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:<o:p></o:p></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>_______________________________________________<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/mailman/listinfo/llvm-dev</a><o:p></o:p></p></blockquote></div><p class=MsoNormal><o:p> </o:p></p></div></div></body></html>