[PATCH] D104634: [SCEV] Generalize MatchBinaryAddToConst to support non-add expressions.

[Florian Hahn via Phabricator via llvm-commits]

fhahn added inline comments.


================
Comment at: llvm/lib/Analysis/ScalarEvolution.cpp:10106
   case ICmpInst::ICMP_SLE:
-    // X s<= (X + C)<nsw> if C >= 0
-    if (MatchBinaryAddToConst(RHS, LHS, C, SCEV::FlagNSW) && C.isNonNegative())
+    // (X + C1)<nsw> s<= (X + C2) if C1 s<= C2.
+    if (MatchBinaryAddToConst(LHS, RHS, C1, C2, SCEV::FlagNSW) && C1.sle(C2))
----------------
mkazantsev wrote:
> mkazantsev wrote:
> > Is lack of `nsw` in `(X + C2)` intentional? If yes, the counter-example to this is
> > 
> > ```
> > X = SINT_MIN
> > C1 = 1
> > C2 = -1
> > ```
> > `(X + C1)<nsw> = SINT_MIN + 1 <= (X - 1) = SINT_MAX`, but obviously `C1 > C2`.
> > 
> > 
> I'm not sure whether two-ways implication is required here, or one way implication is enough. It was two-ways in old code. If I'm wrong here, please let me know.
The comment is missing `<nsw>` from the second expression, the actual checks enforce `nsw` for both (same for `nuw` below). I updated the comment.

> I'm not sure whether two-ways implication is required here, or one way implication is enough. It was two-ways in old code. If I'm wrong here, please let me know.

The new reasoning should handle both previous checks I think , as, `X s<= (X + C)` treated as `X + 0 s<= (X + C)` and `(X + C) s<= X` is treated as `(X + C) s<= X + 0`




Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D104634/new/

https://reviews.llvm.org/D104634