[PATCH] D35109: [Analyzer] SValBuilder Comparison Rearrangement

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

The unconstrained rearrangements for `+`/`-`/`==`/`!=` are definitely good to go regardless of anything else.

Within the checker, we propose to manually simplify both `$x - N < $x` and `$x + N > $x` to true (where N is positive), because in general this is unsound (due to potential overflows), but for iterator position symbols this is **the** intended behavior (if `container.end() + N` overflows, it's even worse than a regular past-end access).

For the rest of the cases (`>`/`<` with mixed symbols), we propose to delay the decision for now. For now simply admit that the solver is not awesome. If we had a perfect solver, we wouldn't have to rearrange anything, so the root cause of the problem is in the solver, and we shouldn't be fixing it on the checker side. If, before turning the checker on by default, we prove through evaluation that this shortcoming of the solver is indeed a bigger problem for this checker than for the rest of the analyzer, and is also the biggest problem with the checker, we can still come up with something (eg. the already-existing max/4 approach). But let's delay this until we see how bad this part of the problem actually is.


https://reviews.llvm.org/D35109