[llvm] r285729 - [InstCombine] Fold nuw left-shifts in `ugt`/`ule` comparisons.

Nuno Lopes via llvm-commits llvm-commits at lists.llvm.org
Thu Jan 5 01:26:16 PST 2017


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.

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



More information about the llvm-commits mailing list