search for: rise4fun

Craig I know it's a pain compared to the web interface but Alive is pretty easy to install and run from a shell. John On 9/22/17 11:41 AM, Craig Topper via llvm-dev wrote: > And now rise4fun.com <http://rise4fun.com> doesn't work at all? > > ~Craig > > On Wed, Sep 20, 2017 at 9:53 AM, Nuno Lopes <nunoplopes at sapo.pt > <mailto:nunoplopes at sapo.pt>> wrote: > > Alive is now working again. There was a migration to a new server. > P...

And now rise4fun.com doesn't work at all? ~Craig On Wed, Sep 20, 2017 at 9:53 AM, Nuno Lopes <nunoplopes at sapo.pt> wrote: > Alive is now working again. There was a migration to a new server. > Permalinks are still being copied from backup; they will work again > shortly as well. (I would p...

...oon? :) On Fri, Sep 22, 2017 at 2:48 PM, John Regehr via llvm-dev <llvm-dev at lists.llvm.org> wrote: Craig I know it's a pain compared to the web interface but Alive is pretty easy to install and run from a shell. John On 9/22/17 11:41 AM, Craig Topper via llvm-dev wrote: And now rise4fun.com <http://rise4fun.com> doesn't work at all? ~Craig On Wed, Sep 20, 2017 at 9:53 AM, Nuno Lopes <nunoplopes at sapo.pt <mailto:nunoplopes at sapo.pt>> wrote: Alive is now working again. There was a migration to a new server. Permalinks are still being copied from...

...t; I'm investigating; thanks for the heads up. Sorry for the trouble. > Nuno > > > -----Original Message----- > From: Craig Topper via llvm-dev > Sent: Tuesday, September 19, 2017 11:52 PM > Subject: [llvm-dev] Where did Alive go? > > > This no longer works http://rise4fun.com/Alive > > > > ~Craig > _______________________________________________ > LLVM Developers mailing list > llvm-dev at lists.llvm.org > http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev

...expression, but it’s not enabled on the >> web interface yet (InstCombine was missing quite a few cases last time I >> checked). >> >> >> >> I played a bit with your example and realized that it doesn’t even need >> a precondition :) Check this out: http://rise4fun.com/Alive/j >> >> (btw, > is signed comparison, and u> is unsigned). >> >> > Nice! I'll draft a patch for the transform. > > > > >> >> >> Nuno >> >> >> >> >> >> *From:* Sanjay Patel [mailto:spatel...

...he best set of nsw/nuw/exact attributes in the transformed expression, but it’s not enabled on the web interface yet (InstCombine was missing quite a few cases last time I checked). I played a bit with your example and realized that it doesn’t even need a precondition :) Check this out: http://rise4fun.com/Alive/j (btw, > is signed comparison, and u> is unsigned). Nuno From: Sanjay Patel [mailto:spatel at rotateright.com] Sent: 6 de janeiro de 2017 00:35 To: Nuno Lopes <nuno.lopes at ist.utl.pt> Cc: llvm-dev <llvm-dev at lists.llvm.org>; John Regehr <regehr at cs...

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 se...

...transforms for select-of-select were added here: https://reviews.llvm.org/rL228409 But Alive says this is more poisonous: Name: selsel %s1 = select i1 %cond1, i8 C1, i8 C2 %s2 = select i1 %cond2, i8 %s1, i8 C2 => %andcond = and i1 %cond1, %cond2 %s2 = select i1 %andcond, i8 C1, i8 C2 http://rise4fun.com/Alive/JT6 Are those transforms legal? -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20170522/bbc53c66/attachment.html>

This no longer works http://rise4fun.com/Alive ~Craig -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20170919/1a9c951b/attachment.html>

No concerns from me. I use Alive2 all the time, and it would be fantastic to have it available online reliably. If we can get Alive1 up there too, that would be even better. I still use that to try to prove things where it's not obvious how to express the relationships in pure LLVM IR: https://rise4fun.com/Alive/NDu On Wed, Jun 17, 2020 at 4:05 PM Chris Lattner via llvm-dev < llvm-dev at lists.llvm.org> wrote: > This seems pretty clear cut to me - alive2 is a great tool, and I’d love > to see it get more visibility in the LLVM world. Would it make sense to > add a web page and...

...John Regehr via llvm-dev <llvm-dev at lists.llvm.org> wrote: > > > If we can get Alive1 up there too, that would be even better. I still > > use that to try to prove things where it's not obvious how to express > > the relationships in pure LLVM IR: > > https://rise4fun.com/Alive/NDu > > I don't expect it would be real hard to shoehorn alive1 into Compiler > Explorer, but Nuno and I will have to talk about whether we (or he, more > accurately) wants to keep supporting it. We might prefer to try to just > support use cases such as your example in...

...39;m teaching ConstantRange how no-wrap flags affect the range of `mul` instruction, with end goal of exploiting this in LVI/CVP. There are certain combinations of ranges and no-wrap flags that result in always-overflowing `mul`. For example, `mul nuw nsw i4 [2,0), [4,0)` always overflows: https://rise4fun.com/Alive/1aK so for such ranges the ideal answer is `empty set`; although it wouldn't be incorrect to return a more pessimistic range (e.g. full-set) that contains more than the ideal result. The problem is, unlike the case of `add`, where intersection between plain `add` range and `saturatin...

...t y) { return (x>y) - (x<y); } define i32 @neg101_cmp_sub(i32, i32) { %3 = icmp sgt i32 %0, %1 %4 = zext i1 %3 to i32 %5 = icmp slt i32 %0, %1 %6 = zext i1 %5 to i32 %7 = sub nsw i32 %4, %6 ret i32 %7 } https://godbolt.org/g/UnM9H7 Show these are logically equivalent: http://rise4fun.com/Alive/b4D Recent patch related to this pattern: https://reviews.llvm.org/D34278 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20170701/ee76109b/attachment.html>

I'm investigating; thanks for the heads up. Sorry for the trouble. Nuno -----Original Message----- From: Craig Topper via llvm-dev Sent: Tuesday, September 19, 2017 11:52 PM Subject: [llvm-dev] Where did Alive go? This no longer works http://rise4fun.com/Alive ~Craig

.../reviews.llvm.org/D46336> - enhance -instcombine to do more reassociation/factoring [3] D45842 <https://reviews.llvm.org/D45842> - add to the existing -reassociate pass to enable factoring Here's a basic motivating example that we fail to optimize: https://godbolt.org/g/64NmJM https://rise4fun.com/Alive/wec Currently, responsibility for reassociative transforms is split between -reassociate and -instcombine. I don't know if that split is intentional or just how the code evolved. Debug stats for test-suite compiled with -O3 show: 78K "reassociations" by -instcombine. 58K &q...

...rg/rL228409 > > But Alive says this is more poisonous: > > Name: selsel > %s1 = select i1 %cond1, i8 C1, i8 C2 > %s2 = select i1 %cond2, i8 %s1, i8 C2 > => > %andcond = and i1 %cond1, %cond2 > %s2 = select i1 %andcond, i8 C1, i8 C2 > > <http://rise4fun.com/Alive/JT6> http://rise4fun.com/Alive/JT6 > > Are those transforms legal? -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20170523/f98ceab6/attachment.html>

...ance -instcombine to do > more reassociation/factoring > [3] D45842 <https://reviews.llvm.org/D45842> - add to the existing > -reassociate pass to enable factoring > > Here's a basic motivating example that we fail to optimize: > https://godbolt.org/g/64NmJM > https://rise4fun.com/Alive/wec > > Currently, responsibility for reassociative transforms is split between > -reassociate and -instcombine. I don't know if that split is intentional or > just how the code evolved. Debug stats for test-suite compiled with -O3 > show: > 78K "reassociations&...

...; do more reassociation/factoring >> [3] D45842 <https://reviews.llvm.org/D45842> - add to the existing >> -reassociate pass to enable factoring >> >> Here's a basic motivating example that we fail to optimize: >> https://godbolt.org/g/64NmJM >> https://rise4fun.com/Alive/wec >> >> Currently, responsibility for reassociative transforms is split between >> -reassociate and -instcombine. I don't know if that split is intentional or >> just how the code evolved. Debug stats for test-suite compiled with -O3 >> show: >> 7...

...ext i8 %6 to i32 %o1 = sub i32 32, %o0 %r = shl i32 %5, %o1 While int shl1(int x, unsigned char y) { return x << (32 - y); } produces %n0 = zext i8 %6 to i32 %n1 = sub i32 32, %n0 %r = shl i32 %5, %n1 (as one would expect) And here we again don't need sign-extension: https://rise4fun.com/Alive/ymk In my eyes, that doesn't completely invalidate https://reviews.llvm.org/D68150 approach, i still think it is a good idea, but clearly we *also* need something else, more generic. My first thought would be CVP and LVI, but i did not look yet.. Roman > > >> > >...

Hi Roman, Thanks for your good idea. I think it can solve the abs issue very well. I can continue with my work now^-^. But if it is not abs and there is no select, %res = OP i32 %b, %a %sub = sub i32 0, %b %res2 = OP i32 %sub, %a theoretically, we can still do the following transform for the above pattern: %res2 = OP i32 %sub, %a ==> %res2 = sub i32 0, %res Not sure whether we can do it