[DA] Rewrite the formula in the Strong SIV test (#179665)
In the Strong SIV test, given two addrecs `{c0,+,a}` and `{c1,+,a}`, the
following inequality is evaluated:
`|c0 - c1| >s |a| * BTC`, where `BTC` is the backedge-taken count of the
loop.
To evaluate this correctly, at least the following checks are necessary.
- `c0 - c1` doesn't overflow
- For all absolute-value calculations `|x|`, `x` is not the signed
minimum value
- `|a| * BTC` doesn't overflow
- `0 <=s BTC`, which is currently missed
- The addrecs have `nsw`, which is also currently missed
Enumerating these conditions and inserting them one by one is risky, and
I believe it makes the software flaky, so it should be avoided. It's
also unclear if these conditions are sufficient.
This patch replaces the current implementation with one that uses
`ConstantRange` so that we don't need to check any condition by
ourselves.
Fixes the test case for the Strong SIV test added in #179664. I believe
a similar fix can be applied for other tests as well.
