[PATCH] D35109: [Analyzer] SValBuilder Comparison Rearrangement

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

A breakthrough with credit going to Devin: Note that whenever we're not dealing with `>`/`<`/`<=`/`>=` (but only with additive ops and `==` and `!=`, and we have everything of the same type) we can rearrange regardless of constraints, simply because Z/nZ is an abelian group.

First of all, it means that we definitely do not need to check constraints in those cases.

Then the question is - would it be enough to limit rearrangements to additive and equality comparisons? `operator<()` is rarely redefined for iterator objects. You rely on `>`/`<` comparisons to compare symbolic iterators to `.begin()` or `.end()`, but how much more does it give in practice, compared to straightforwardly matching, say, `i == i.container.end` where `N` is non-negative, given that the rest of our solver barely solves anything? Like, let's say that "iterator `i` is past end" from now on literally means "//there exists a non-negative `N` for which `i` is-the-same-symbol-as `i.container.end + N`//" rather than "//`i >= i.container.end`//". Would the checker lose much from such change? If not, we can completely screw all checks and gain a lot more value from the rearrangements.


https://reviews.llvm.org/D35109