<div dir="ltr"><div><div>Hi Nuno,<br><br></div>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>}<br><br></div>(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> )<br><div><br></div><div>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>}<br><br></div><div>As a first hack, I did this:<br><a href="http://rise4fun.com/Alive/qG">http://rise4fun.com/Alive/qG</a><br></div><div><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)<br><br></div><div>...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?<br></div><div><br><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 5, 2017 at 3:42 PM, Nuno Lopes via llvm-dev <span dir="ltr"><<a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
Just a short email to announce that Alive is now available online: <a href="http://rise4fun.com/Alive" rel="noreferrer" 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" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/llvm-dev</a><br>
</blockquote></div><br></div>