[llvm] r285729 - [InstCombine] Fold nuw left-shifts in `ugt`/`ule` comparisons.
Hal Finkel via llvm-commits
llvm-commits at lists.llvm.org
Thu Jan 5 06:27:43 PST 2017
On 01/05/2017 03:26 AM, Nuno Lopes via llvm-commits wrote:
> Sorry for digging up this old email, but just wanted to announce that
> Alive is now available online!
> I've transcribed your example and Alive confirms that it is correct:
> http://rise4fun.com/Alive/R
>
> 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.
>
> 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 :)
>
> Please let me know if you run into problems with this online version.
> It's still in tests.
This sounds really neat! Can you announce this on llvm-dev instead of
just in this thread?
-Hal
>
> Thanks,
> Nuno
>
>
> Quoting Sanjay Patel via llvm-commits <llvm-commits at lists.llvm.org>:
>
>> Author: spatel
>> Date: Tue Nov 1 14:19:29 2016
>> New Revision: 285729
>>
>> URL: http://llvm.org/viewvc/llvm-project?rev=285729&view=rev
>> Log:
>> [InstCombine] Fold nuw left-shifts in `ugt`/`ule` comparisons.
>>
>> This transforms
>>
>> %a = shl nuw %x, c1
>> %b = icmp {ugt|ule} %a, c0
>>
>> into
>>
>> %b = icmp {ugt|ule} %x, (c0 >> c1)
>>
>> z3:
>>
>> (declare-const x (_ BitVec 64))
>> (declare-const c0 (_ BitVec 64))
>> (declare-const c1 (_ BitVec 64))
>>
>> (push)
>> (assert (= x (bvlshr (bvshl x c1) c1))) ; nuw
>> (assert (not (= (bvugt (bvshl x c1) c0)
>> (bvugt x
>> (bvlshr c0 c1)))))
>> (check-sat)
>> (get-model)
>> (pop)
>>
>> (push)
>> (assert (= x (bvlshr (bvshl x c1) c1))) ; nuw
>> (assert (not (= (bvule (bvshl x c1) c0)
>> (bvule x
>> (bvlshr c0 c1)))))
>> (check-sat)
>> (get-model)
>> (pop)
>>
>> Patch by bryant!
>>
>> Differential Revision: https://reviews.llvm.org/D25913
>>
>> Modified:
>> llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp
>> llvm/trunk/test/Transforms/InstCombine/icmp-shl-nuw.ll
>>
>> Modified: llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp
>> URL:
>> http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp?rev=285729&r1=285728&r2=285729&view=diff
>> ==============================================================================
>>
>> --- llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp
>> (original)
>> +++ llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp Tue
>> Nov 1 14:19:29 2016
>> @@ -1950,6 +1950,23 @@ Instruction *InstCombiner::foldICmpShlCo
>> And, Constant::getNullValue(And->getType()));
>> }
>>
>> + // When the shift is nuw and pred is >u or <=u, comparison only
>> really happens
>> + // in the pre-shifted bits. Since InstSimplify canoncalizes <=u
>> into <u, the
>> + // <=u case can be further converted to match <u (see below).
>> + if (Shl->hasNoUnsignedWrap() &&
>> + (Pred == ICmpInst::ICMP_UGT || Pred == ICmpInst::ICMP_ULT)) {
>> + // Derivation for the ult case:
>> + // (X << S) <=u C is equiv to X <=u (C >> S) for all C
>> + // (X << S) <u (C + 1) is equiv to X <u (C >> S) + 1 if C <u ~0u
>> + // (X << S) <u C is equiv to X <u ((C - 1) >> S) + 1 if C >u 0
>> + assert((Pred != ICmpInst::ICMP_ULT || C->ugt(0)) &&
>> + "Encountered `ult 0` that should have been eliminated by "
>> + "InstSimplify.");
>> + APInt ShiftedC = Pred == ICmpInst::ICMP_ULT ? (*C -
>> 1).lshr(*ShiftAmt) + 1
>> + : C->lshr(*ShiftAmt);
>> + return new ICmpInst(Pred, X, ConstantInt::get(X->getType(),
>> ShiftedC));
>> + }
>> +
>> // Transform (icmp pred iM (shl iM %v, N), C)
>> // -> (icmp pred i(M-N) (trunc %v iM to i(M-N)), (trunc (C>>N))
>> // Transform the shl to a trunc if (trunc (C>>N)) has no loss and
>> M-N.
>>
>> Modified: llvm/trunk/test/Transforms/InstCombine/icmp-shl-nuw.ll
>> URL:
>> http://llvm.org/viewvc/llvm-project/llvm/trunk/test/Transforms/InstCombine/icmp-shl-nuw.ll?rev=285729&r1=285728&r2=285729&view=diff
>> ==============================================================================
>>
>> --- llvm/trunk/test/Transforms/InstCombine/icmp-shl-nuw.ll (original)
>> +++ llvm/trunk/test/Transforms/InstCombine/icmp-shl-nuw.ll Tue Nov 1
>> 14:19:29 2016
>> @@ -3,8 +3,7 @@
>>
>> define i1 @icmp_ugt_32(i64) {
>> ; CHECK-LABEL: @icmp_ugt_32(
>> -; CHECK-NEXT: [[C:%.*]] = shl nuw i64 %0, 32
>> -; CHECK-NEXT: [[D:%.*]] = icmp ugt i64 [[C]], 4294967295
>> +; CHECK-NEXT: [[D:%.*]] = icmp ne i64 %0, 0
>> ; CHECK-NEXT: ret i1 [[D]]
>> ;
>> %c = shl nuw i64 %0, 32
>> @@ -14,8 +13,7 @@ define i1 @icmp_ugt_32(i64) {
>>
>> define i1 @icmp_ule_64(i128) {
>> ; CHECK-LABEL: @icmp_ule_64(
>> -; CHECK-NEXT: [[C:%.*]] = shl nuw i128 %0, 64
>> -; CHECK-NEXT: [[D:%.*]] = icmp ult i128 [[C]], 18446744073709551616
>> +; CHECK-NEXT: [[D:%.*]] = icmp eq i128 %0, 0
>> ; CHECK-NEXT: ret i1 [[D]]
>> ;
>> %c = shl nuw i128 %0, 64
>> @@ -25,8 +23,7 @@ define i1 @icmp_ule_64(i128) {
>>
>> define i1 @icmp_ugt_16(i64) {
>> ; CHECK-LABEL: @icmp_ugt_16(
>> -; CHECK-NEXT: [[C:%.*]] = shl nuw i64 %0, 16
>> -; CHECK-NEXT: [[D:%.*]] = icmp ugt i64 [[C]], 1048575
>> +; CHECK-NEXT: [[D:%.*]] = icmp ugt i64 %0, 15
>> ; CHECK-NEXT: ret i1 [[D]]
>> ;
>> %c = shl nuw i64 %0, 16
>> @@ -36,8 +33,7 @@ define i1 @icmp_ugt_16(i64) {
>>
>> define <2 x i1> @icmp_ule_16x2(<2 x i64>) {
>> ; CHECK-LABEL: @icmp_ule_16x2(
>> -; CHECK-NEXT: [[C:%.*]] = shl nuw <2 x i64> %0, <i64 16, i64 16>
>> -; CHECK-NEXT: [[D:%.*]] = icmp ult <2 x i64> [[C]], <i64 65536,
>> i64 65536>
>> +; CHECK-NEXT: [[D:%.*]] = icmp eq <2 x i64> %0, zeroinitializer
>> ; CHECK-NEXT: ret <2 x i1> [[D]]
>> ;
>> %c = shl nuw <2 x i64> %0, <i64 16, i64 16>
>> @@ -45,10 +41,29 @@ define <2 x i1> @icmp_ule_16x2(<2 x i64>
>> ret <2 x i1> %d
>> }
>>
>> +define <2 x i1> @icmp_ule_16x2_nonzero(<2 x i64>) {
>> +; CHECK-LABEL: @icmp_ule_16x2_nonzero(
>> +; CHECK-NEXT: [[D:%.*]] = icmp ult <2 x i64> %0, <i64 4, i64 4>
>> +; CHECK-NEXT: ret <2 x i1> [[D]]
>> +;
>> + %c = shl nuw <2 x i64> %0, <i64 16, i64 16>
>> + %d = icmp ule <2 x i64> %c, <i64 196608, i64 196608> ; 0x03_0000
>> + ret <2 x i1> %d
>> +}
>> +
>> +define <2 x i1> @icmp_ule_12x2(<2 x i64>) {
>> +; CHECK-LABEL: @icmp_ule_12x2(
>> +; CHECK-NEXT: [[D:%.*]] = icmp ult <2 x i64> %0, <i64 4, i64 4>
>> +; CHECK-NEXT: ret <2 x i1> [[D]]
>> +;
>> + %c = shl nuw <2 x i64> %0, <i64 12, i64 12>
>> + %d = icmp ule <2 x i64> %c, <i64 12288, i64 12288> ; 0x3000
>> + ret <2 x i1> %d
>> +}
>> +
>> define i1 @icmp_ult_8(i64) {
>> ; CHECK-LABEL: @icmp_ult_8(
>> -; CHECK-NEXT: [[C:%.*]] = shl nuw i64 %0, 8
>> -; CHECK-NEXT: [[D:%.*]] = icmp ult i64 [[C]], 4095
>> +; CHECK-NEXT: [[D:%.*]] = icmp ult i64 %0, 16
>> ; CHECK-NEXT: ret i1 [[D]]
>> ;
>> %c = shl nuw i64 %0, 8
>> @@ -58,8 +73,7 @@ define i1 @icmp_ult_8(i64) {
>>
>> define <2 x i1> @icmp_uge_8x2(<2 x i16>) {
>> ; CHECK-LABEL: @icmp_uge_8x2(
>> -; CHECK-NEXT: [[C:%.*]] = shl nuw <2 x i16> %0, <i16 8, i16 8>
>> -; CHECK-NEXT: [[D:%.*]] = icmp ugt <2 x i16> [[C]], <i16 4094,
>> i16 4094>
>> +; CHECK-NEXT: [[D:%.*]] = icmp ugt <2 x i16> %0, <i16 15, i16 15>
>> ; CHECK-NEXT: ret <2 x i1> [[D]]
>> ;
>> %c = shl nuw <2 x i16> %0, <i16 8, i16 8>
>> @@ -69,8 +83,7 @@ define <2 x i1> @icmp_uge_8x2(<2 x i16>)
>>
>> define <2 x i1> @icmp_ugt_16x2(<2 x i32>) {
>> ; CHECK-LABEL: @icmp_ugt_16x2(
>> -; CHECK-NEXT: [[C:%.*]] = shl nuw <2 x i32> %0, <i32 16, i32 16>
>> -; CHECK-NEXT: [[D:%.*]] = icmp ugt <2 x i32> [[C]], <i32 1048575,
>> i32 1048575>
>> +; CHECK-NEXT: [[D:%.*]] = icmp ugt <2 x i32> %0, <i32 15, i32 15>
>> ; CHECK-NEXT: ret <2 x i1> [[D]]
>> ;
>> %c = shl nuw <2 x i32> %0, <i32 16, i32 16>
>>
>>
>> _______________________________________________
>> llvm-commits mailing list
>> llvm-commits at lists.llvm.org
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-commits
>
> _______________________________________________
> llvm-commits mailing list
> llvm-commits at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-commits
--
Hal Finkel
Lead, Compiler Technology and Programming Languages
Leadership Computing Facility
Argonne National Laboratory
More information about the llvm-commits
mailing list