[llvm] [DA] Rewrite BanerjeeMIV test with safe APInt interval arithmetic (PR #207662)

[Ruoyu Qiu via llvm-commits]

cabbaken wrote:

Using the old native-width SCEV arithmetic unchanged would retain the overflow problem.

I agree that SCEV expressions could be explicitly extended to WideBits before constructing the Banerjee formulas. The WideBits proof would then guarantee that the widened SCEV arithmetic does not wrap, while __preserving symbolic cases__ that the current APInt implementation rejects.

APInt was chosen to make the arithmetic and infinity representation self-contained, rather than because SCEV fundamentally cannot be used.

For this initial version, I intentionally use APInt and accept only constant affine expressions so that the overflow reasoning remains simple and explicit. Unsupported symbolic cases bail out conservatively, so this is a precision limitation rather than a correctness issue.
I suggest considering widened symbolic SCEV support as follow-up work.

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