[llvm-dev] Alive now available online

[Sanjay Patel via llvm-dev]

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/20170105/6d45664a/attachment.html>