[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In https://reviews.llvm.org/D35110#1117401, @baloghadamsoftware wrote:

> Sorry, Artem, but it does not work this way. Even if the symbolic expressions are constrained to `[-MAX/4..MAX/4]`, after rearrangement the difference still uses the whole range, thus `m>n` becomes `m-n>0`, where in the false branch the range for `m-n` is `[MIN..0]`. Then if we check `n>=m` the range set is reversed to `[MIN..MIN]U[0..MAX]` which results `UNKNOWN` for `n-m`. It does not solve any of our problems and there is no remedy on the checker's side.


Which expressions are constrained? Why does the difference use the whole range? Is it something that could have been fixed by the "enforce that separately" part in my old comment:

> iterator-related symbols are all planned to be within range [-2²⁹, -2²⁹], right? So if we subtract one such symbol from another, it's going to be in range [-2³⁰, 2³⁰]. Can we currently infer that? Or maybe we should make the iterator checker to enforce that separately?

?


https://reviews.llvm.org/D35110