[PATCH] D25913: [InstCombine] Fold nuw left-shifts in `ugt`/`ule` comparisons.

[bryant via llvm-commits]

bryant added inline comments.


================
Comment at: lib/Transforms/InstCombine/InstCombineCompares.cpp:1955
+  // comparison only really happens in the pre-shifted bits. This also holds for
+  // <=u and >u, but the latter two are canonicalized into the former.
+  if (Shl->hasNoUnsignedWrap()) {
----------------
spatel wrote:
> ">u" should be ">=u"
So, just to recap: This transformation only works for all c when `ugt` and `ule` (cf. the z3 in my opening post) and fails for `uge`:

```z3
(push)
(declare-const s (_ BitVec 8))
(declare-const c (_ BitVec 8))
(declare-const x (_ BitVec 8))

(assert (= (bvlshr (bvshl x s) s) x))

(assert (not (= (bvuge (bvshl x s) c) (bvuge x (bvlshr c s)))))
(check-sat)
(get-model)
(pop)

sat
(model 
  (define-fun s () (_ BitVec 8)
    #x10)
  (define-fun x () (_ BitVec 8)
    #x00)
  (define-fun c () (_ BitVec 8)
    #x01)
)
```

But the original rule can be transformed from ugt to uge:

```
(x << s) ugt c = x ugt (c >> s)
(x << s) uge (c + 1) = x ugt (c >> s) if c < -1
(x << s) uge (c + 1) = x uge (c >> s) + 1 if c < -1
(x << s) uge c = x uge ((c - 1) >> s) + 1 if c > 0
```

The exact same holds for ule to ult, but c has to be non-zero.

Maybe I'll add this derivation to the comments.


================
Comment at: lib/Transforms/InstCombine/InstCombineCompares.cpp:1961
+
+    if (C->ugt(0) && Pred == ICmpInst::ICMP_ULT)
+      return new ICmpInst(ICmpInst::ICMP_ULE, X,
----------------
spatel wrote:
> I don't think you need to check that the constant is ugt(0) here because:
> icmp ult %x, 0
> must always be simplified to 'false' ahead of this.
> Let me know if I've misunderstood that check.
It's a safety check that doesn't seem so expensive. If C is zero by some chance for whatever reason, then this transformation is incorrect and really mustn't happen. Are you really sure that I should remove it? Better safe than slow.


Repository:
  rL LLVM

https://reviews.llvm.org/D25913