[PATCH] D35109: [Analyzer] SValBuilder Comparison Rearrangement
Artem Dergachev via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Mon Nov 6 03:48:28 PST 2017
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.
More information about the cfe-commits