<div dir="ltr"><div>Very cool! And I agree with Hal - please send to the dev list so more people will know.<br></div>cc'ing Bryant's Phab email address (I was just the committer on this one, not the author).<br><div><div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 5, 2017 at 7:27 AM, Hal Finkel <span dir="ltr"><<a href="mailto:hfinkel@anl.gov" target="_blank">hfinkel@anl.gov</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span><br>
On 01/05/2017 03:26 AM, Nuno Lopes via llvm-commits wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Sorry for digging up this old email, but just wanted to announce that Alive is now available online!<br>
I've transcribed your example and Alive confirms that it is correct: <a href="http://rise4fun.com/Alive/R" rel="noreferrer" target="_blank">http://rise4fun.com/Alive/R</a><br>
<br>
BTW your proof in Z3 is not sufficient to ensure soundness of the transformation. It needs an additional proof that the transformed expression is 1) as defined as the original (no introduction of UB allowed), and 2) is not more poisonous than the original.<br>
<br>
Alive does all these proofs for you automatically (modulo bugs in the implementation..). You can also get a permalink and share the proof with others :)<br>
<br>
Please let me know if you run into problems with this online version. It's still in tests.<br>
</blockquote>
<br></span>
This sounds really neat! Can you announce this on llvm-dev instead of just in this thread?<br>
<br>
-Hal<div class="m_-7392487016168504930HOEnZb"><div class="m_-7392487016168504930h5"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Thanks,<br>
Nuno<br>
<br>
<br>
Quoting Sanjay Patel via llvm-commits <<a href="mailto:llvm-commits@lists.llvm.org" target="_blank">llvm-commits@lists.llvm.org</a>>:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Author: spatel<br>
Date: Tue Nov 1 14:19:29 2016<br>
New Revision: 285729<br>
<br>
URL: <a href="http://llvm.org/viewvc/llvm-project?rev=285729&view=rev" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-pr<wbr>oject?rev=285729&view=rev</a><br>
Log:<br>
[InstCombine] Fold nuw left-shifts in `ugt`/`ule` comparisons.<br>
<br>
This transforms<br>
<br>
%a = shl nuw %x, c1<br>
%b = icmp {ugt|ule} %a, c0<br>
<br>
into<br>
<br>
%b = icmp {ugt|ule} %x, (c0 >> c1)<br>
<br>
z3:<br>
<br>
(declare-const x (_ BitVec 64))<br>
(declare-const c0 (_ BitVec 64))<br>
(declare-const c1 (_ BitVec 64))<br>
<br>
(push)<br>
(assert (= x (bvlshr (bvshl x c1) c1))) ; nuw<br>
(assert (not (= (bvugt (bvshl x c1) c0)<br>
(bvugt x<br>
(bvlshr c0 c1)))))<br>
(check-sat)<br>
(get-model)<br>
(pop)<br>
<br>
(push)<br>
(assert (= x (bvlshr (bvshl x c1) c1))) ; nuw<br>
(assert (not (= (bvule (bvshl x c1) c0)<br>
(bvule x<br>
(bvlshr c0 c1)))))<br>
(check-sat)<br>
(get-model)<br>
(pop)<br>
<br>
Patch by bryant!<br>
<br>
Differential Revision: <a href="https://reviews.llvm.org/D25913" rel="noreferrer" target="_blank">https://reviews.llvm.org/D2591<wbr>3</a><br>
<br>
Modified:<br>
llvm/trunk/lib/Transforms/Inst<wbr>Combine/InstCombineCompares.cp<wbr>p<br>
llvm/trunk/test/Transforms/Ins<wbr>tCombine/icmp-shl-nuw.ll<br>
<br>
Modified: llvm/trunk/lib/Transforms/Inst<wbr>Combine/InstCombineCompares.cp<wbr>p<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp?rev=285729&r1=285728&r2=285729&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-pr<wbr>oject/llvm/trunk/lib/Transform<wbr>s/InstCombine/InstCombineCompa<wbr>res.cpp?rev=285729&r1=285728&r<wbr>2=285729&view=diff</a><br>
==============================<wbr>==============================<wbr>================== <br>
--- llvm/trunk/lib/Transforms/Inst<wbr>Combine/InstCombineCompares.cp<wbr>p (original)<br>
+++ llvm/trunk/lib/Transforms/Inst<wbr>Combine/InstCombineCompares.cp<wbr>p Tue Nov 1 14:19:29 2016<br>
@@ -1950,6 +1950,23 @@ Instruction *InstCombiner::foldICmpShlCo<br>
And, Constant::getNullValue(And->ge<wbr>tType()));<br>
}<br>
<br>
+ // When the shift is nuw and pred is >u or <=u, comparison only really happens<br>
+ // in the pre-shifted bits. Since InstSimplify canoncalizes <=u into <u, the<br>
+ // <=u case can be further converted to match <u (see below).<br>
+ if (Shl->hasNoUnsignedWrap() &&<br>
+ (Pred == ICmpInst::ICMP_UGT || Pred == ICmpInst::ICMP_ULT)) {<br>
+ // Derivation for the ult case:<br>
+ // (X << S) <=u C is equiv to X <=u (C >> S) for all C<br>
+ // (X << S) <u (C + 1) is equiv to X <u (C >> S) + 1 if C <u ~0u<br>
+ // (X << S) <u C is equiv to X <u ((C - 1) >> S) + 1 if C >u 0<br>
+ assert((Pred != ICmpInst::ICMP_ULT || C->ugt(0)) &&<br>
+ "Encountered `ult 0` that should have been eliminated by "<br>
+ "InstSimplify.");<br>
+ APInt ShiftedC = Pred == ICmpInst::ICMP_ULT ? (*C - 1).lshr(*ShiftAmt) + 1<br>
+ : C->lshr(*ShiftAmt);<br>
+ return new ICmpInst(Pred, X, ConstantInt::get(X->getType(), ShiftedC));<br>
+ }<br>
+<br>
// Transform (icmp pred iM (shl iM %v, N), C)<br>
// -> (icmp pred i(M-N) (trunc %v iM to i(M-N)), (trunc (C>>N))<br>
// Transform the shl to a trunc if (trunc (C>>N)) has no loss and M-N.<br>
<br>
Modified: llvm/trunk/test/Transforms/Ins<wbr>tCombine/icmp-shl-nuw.ll<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/llvm/trunk/test/Transforms/InstCombine/icmp-shl-nuw.ll?rev=285729&r1=285728&r2=285729&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-pr<wbr>oject/llvm/trunk/test/Transfor<wbr>ms/InstCombine/icmp-shl-nuw.ll<wbr>?rev=285729&r1=285728&r2=28572<wbr>9&view=diff</a><br>
==============================<wbr>==============================<wbr>================== <br>
--- llvm/trunk/test/Transforms/Ins<wbr>tCombine/icmp-shl-nuw.ll (original)<br>
+++ llvm/trunk/test/Transforms/Ins<wbr>tCombine/icmp-shl-nuw.ll Tue Nov 1 14:19:29 2016<br>
@@ -3,8 +3,7 @@<br>
<br>
define i1 @icmp_ugt_32(i64) {<br>
; CHECK-LABEL: @icmp_ugt_32(<br>
-; CHECK-NEXT: [[C:%.*]] = shl nuw i64 %0, 32<br>
-; CHECK-NEXT: [[D:%.*]] = icmp ugt i64 [[C]], 4294967295<br>
+; CHECK-NEXT: [[D:%.*]] = icmp ne i64 %0, 0<br>
; CHECK-NEXT: ret i1 [[D]]<br>
;<br>
%c = shl nuw i64 %0, 32<br>
@@ -14,8 +13,7 @@ define i1 @icmp_ugt_32(i64) {<br>
<br>
define i1 @icmp_ule_64(i128) {<br>
; CHECK-LABEL: @icmp_ule_64(<br>
-; CHECK-NEXT: [[C:%.*]] = shl nuw i128 %0, 64<br>
-; CHECK-NEXT: [[D:%.*]] = icmp ult i128 [[C]], 18446744073709551616<br>
+; CHECK-NEXT: [[D:%.*]] = icmp eq i128 %0, 0<br>
; CHECK-NEXT: ret i1 [[D]]<br>
;<br>
%c = shl nuw i128 %0, 64<br>
@@ -25,8 +23,7 @@ define i1 @icmp_ule_64(i128) {<br>
<br>
define i1 @icmp_ugt_16(i64) {<br>
; CHECK-LABEL: @icmp_ugt_16(<br>
-; CHECK-NEXT: [[C:%.*]] = shl nuw i64 %0, 16<br>
-; CHECK-NEXT: [[D:%.*]] = icmp ugt i64 [[C]], 1048575<br>
+; CHECK-NEXT: [[D:%.*]] = icmp ugt i64 %0, 15<br>
; CHECK-NEXT: ret i1 [[D]]<br>
;<br>
%c = shl nuw i64 %0, 16<br>
@@ -36,8 +33,7 @@ define i1 @icmp_ugt_16(i64) {<br>
<br>
define <2 x i1> @icmp_ule_16x2(<2 x i64>) {<br>
; CHECK-LABEL: @icmp_ule_16x2(<br>
-; CHECK-NEXT: [[C:%.*]] = shl nuw <2 x i64> %0, <i64 16, i64 16><br>
-; CHECK-NEXT: [[D:%.*]] = icmp ult <2 x i64> [[C]], <i64 65536, i64 65536><br>
+; CHECK-NEXT: [[D:%.*]] = icmp eq <2 x i64> %0, zeroinitializer<br>
; CHECK-NEXT: ret <2 x i1> [[D]]<br>
;<br>
%c = shl nuw <2 x i64> %0, <i64 16, i64 16><br>
@@ -45,10 +41,29 @@ define <2 x i1> @icmp_ule_16x2(<2 x i64><br>
ret <2 x i1> %d<br>
}<br>
<br>
+define <2 x i1> @icmp_ule_16x2_nonzero(<2 x i64>) {<br>
+; CHECK-LABEL: @icmp_ule_16x2_nonzero(<br>
+; CHECK-NEXT: [[D:%.*]] = icmp ult <2 x i64> %0, <i64 4, i64 4><br>
+; CHECK-NEXT: ret <2 x i1> [[D]]<br>
+;<br>
+ %c = shl nuw <2 x i64> %0, <i64 16, i64 16><br>
+ %d = icmp ule <2 x i64> %c, <i64 196608, i64 196608> ; 0x03_0000<br>
+ ret <2 x i1> %d<br>
+}<br>
+<br>
+define <2 x i1> @icmp_ule_12x2(<2 x i64>) {<br>
+; CHECK-LABEL: @icmp_ule_12x2(<br>
+; CHECK-NEXT: [[D:%.*]] = icmp ult <2 x i64> %0, <i64 4, i64 4><br>
+; CHECK-NEXT: ret <2 x i1> [[D]]<br>
+;<br>
+ %c = shl nuw <2 x i64> %0, <i64 12, i64 12><br>
+ %d = icmp ule <2 x i64> %c, <i64 12288, i64 12288> ; 0x3000<br>
+ ret <2 x i1> %d<br>
+}<br>
+<br>
define i1 @icmp_ult_8(i64) {<br>
; CHECK-LABEL: @icmp_ult_8(<br>
-; CHECK-NEXT: [[C:%.*]] = shl nuw i64 %0, 8<br>
-; CHECK-NEXT: [[D:%.*]] = icmp ult i64 [[C]], 4095<br>
+; CHECK-NEXT: [[D:%.*]] = icmp ult i64 %0, 16<br>
; CHECK-NEXT: ret i1 [[D]]<br>
;<br>
%c = shl nuw i64 %0, 8<br>
@@ -58,8 +73,7 @@ define i1 @icmp_ult_8(i64) {<br>
<br>
define <2 x i1> @icmp_uge_8x2(<2 x i16>) {<br>
; CHECK-LABEL: @icmp_uge_8x2(<br>
-; CHECK-NEXT: [[C:%.*]] = shl nuw <2 x i16> %0, <i16 8, i16 8><br>
-; CHECK-NEXT: [[D:%.*]] = icmp ugt <2 x i16> [[C]], <i16 4094, i16 4094><br>
+; CHECK-NEXT: [[D:%.*]] = icmp ugt <2 x i16> %0, <i16 15, i16 15><br>
; CHECK-NEXT: ret <2 x i1> [[D]]<br>
;<br>
%c = shl nuw <2 x i16> %0, <i16 8, i16 8><br>
@@ -69,8 +83,7 @@ define <2 x i1> @icmp_uge_8x2(<2 x i16>)<br>
<br>
define <2 x i1> @icmp_ugt_16x2(<2 x i32>) {<br>
; CHECK-LABEL: @icmp_ugt_16x2(<br>
-; CHECK-NEXT: [[C:%.*]] = shl nuw <2 x i32> %0, <i32 16, i32 16><br>
-; CHECK-NEXT: [[D:%.*]] = icmp ugt <2 x i32> [[C]], <i32 1048575, i32 1048575><br>
+; CHECK-NEXT: [[D:%.*]] = icmp ugt <2 x i32> %0, <i32 15, i32 15><br>
; CHECK-NEXT: ret <2 x i1> [[D]]<br>
;<br>
%c = shl nuw <2 x i32> %0, <i32 16, i32 16><br>
<br>
<br>
______________________________<wbr>_________________<br>
llvm-commits mailing list<br>
<a href="mailto:llvm-commits@lists.llvm.org" target="_blank">llvm-commits@lists.llvm.org</a><br>
<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-commits" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/llvm-commits</a><br>
</blockquote>
<br>
______________________________<wbr>_________________<br>
llvm-commits mailing list<br>
<a href="mailto:llvm-commits@lists.llvm.org" target="_blank">llvm-commits@lists.llvm.org</a><br>
<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-commits" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/llvm-commits</a><br>
</blockquote>
<br></div></div><span class="m_-7392487016168504930HOEnZb"><font color="#888888">
-- <br>
Hal Finkel<br>
Lead, Compiler Technology and Programming Languages<br>
Leadership Computing Facility<br>
Argonne National Laboratory<br>
<br>
</font></span></blockquote></div><br></div></div></div></div>