[llvm] [DA] Add tests for nsw doesn't hold on entier iteration (PR #162281)

Ehsan Amiri via llvm-commits llvm-commits at lists.llvm.org
Fri Nov 21 11:51:27 PST 2025


amehsan wrote:

> Case 1: `a1 * N1 < c2 – c1` and so we (supposedly incorrectly) proved independence. Note that from our assumptions about non-overflowing computations we can conclude `a1 * x + c1 <= a1 * N1 + c1 ` (`x` cannot be more than `N1`) So we have `a1 * N1 + c1 < c2` it is ok to move `c1` because we know there is no overflow in the left hand side computations. But since `a1, N1, and x` are non-negative numbers we have `a1 * x + c1 < c2`. And since `a2 and y` are non-negative numbers we conclude `a1 * x + c1 < a2 * y+ c2`.

There is a minor mistake. Let me correct it:

We know `a1 * x  < a1 *N` and we know `a1 * N1 < c2 – c1` . So we conclude `a1 * x  < c2 - c1`. Now we can move `c1` to left side and conclude `a1 * x + c1 < c2`

https://github.com/llvm/llvm-project/pull/162281


More information about the llvm-commits mailing list