[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 15:20:24 PST 2017
Well, the SMT output of Alive/Z3 is not the most readable thing in the
world..
For each value that changes (only %b in your example), Alive checks that the
following constraints are UNSAT:
- def_src /\ not def_tgt
- def_src /\ non_poison_src /\ not non_poison_tgt
- def_src /\ non_poison_src /\ val_src != val_tgt
def_src is the definedness constraint for the src value (it may have flown
from a division by zero, for example).
Then the second proof ensures the target cannot be more poisonous than the
source.
And the third is the one you had.
Our PLDI'15 has a few more details if you are interested. It's non-trivial
to get the whole proof right the first few times (speaking from experience
:)
Nuno
-----Original Message-----
From: Bryant Wong
Sent: Thursday, January 5, 2017 2:55 PM
To: llvm-commits
Cc: Hal Finkel ; Nuno Lopes ; spatel at rotateright.com
Subject: Re: [llvm] r285729 - [InstCombine] Fold nuw left-shifts in
`ugt`/`ule` comparisons.
Hi Nuno,
Could there be an option on the web UI to display the Z3 equivalent to the
Alive input? I'm interested in knowing what the complete proof would look
like and what was missing from my original one. I know that it would be
doable from the Python package, but that would require installing Z3's
bindings, which is a bit...difficult.
Thanks!
Bryant.
On Thu, Jan 5, 2017 at 9:37 AM, Sanjay Patel <spatel at rotateright.com> wrote:
Very cool! And I agree with Hal - please send to the dev list so more people
will know.
cc'ing Bryant's Phab email address (I was just the committer on this one,
not the author).
On Thu, Jan 5, 2017 at 7:27 AM, Hal Finkel <hfinkel at anl.gov> wrote:
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