[llvm] [DA] Add tests for nsw doesn't hold on entire iteration space (NFC) (PR #162281)
Ehsan Amiri via llvm-commits
llvm-commits at lists.llvm.org
Mon Dec 1 06:24:22 PST 2025
================
----------------
amehsan wrote:
> * You are conflating signed comparisons with unsigned comparisons. A backedge-taken count can be larger than `2^63 - 1`. So `a * (y - x)`, or even `y - x` may overflow in a signed sense.
> * Therefore `|a| (y - x) = |c - d|` is non-trivial.
> * You are implicitly assuming `|a| * BTC` doesn't overflow.
You have misundersood the proof. The claim is not that for arbitrary `x` and `y` `y-x` or `a(y-x)` won't overflow. Here we have a proof by contradition. Starting from two montonic references. We know `ax` and `ay` so do not overflow. then if `y>x` we conclude `a(y-x) won't overflow.
https://github.com/llvm/llvm-project/pull/162281
More information about the llvm-commits
mailing list