[llvm] [DA] Rewrite the formula in the Strong SIV test (PR #179665)

[Ehsan Amiri via llvm-commits]

amehsan wrote:

> As for the accessibility, I think that's reasonable point, but I cannot fully agree with the rest. Yes, as you said, adding a BTC check could be a trivial change. However, what I want to emphasize here is that this is a completely separate issue from overflows. The condition `0 <=s BTC` is a really subtle one. I'm not trying to boast about it, but this case is something I happened to come up with one day, and it's really quite an obscure edge case. The fact that this check is necessary means that, with this approach, we need to take care of things other than overflows. I see this as a kind of technical debt. A small code change in the future could introduce other subtle corner cases. I'm still not sure if adding a BTC check is sufficient to cover all the edge cases in the current implementation in the first place.

These are not corner cases discovered by trial and error. They come from investigation of the inequalities required. I was aware of the BTC condition before you mention it. If you look at the history of my proof, you can see that it says all the numbers should be interpreted as signed and it does say that non-nagtive values are less than BTC. I do give you credit for the example that you raised. Not because I didn't know BTC must be non-negative, but because I didn't know we need the check even with the existing SCEV behavior. But even then (and I believe I mentioned this to you before) my plan was to add test for BTC >= 0. Because I wanted to make sure the code will be correct when SCEV behavior changes.

That said, the point here is that, no, this test is not a technical debt and a small code change in the future is not going to introduce another subtle corner case. That is why we need a proof. Otherwise , this kind of cocern is applicable to any implemention including the one proposed here.

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