[PATCH] D31886: [analyzer] Simplify values in binary operations more aggressively

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In https://reviews.llvm.org/D31886#724796, @xazax.hun wrote:

> maybe we want to skip this kind of simplification in case of Z3?


Hmm, that depends on how would we want to use it eventually.

- If Z3 acts all alone and fires only over actual bug reports, then yeah, it turns this simplification procedure into a dry-run no-op. However, the much bigger performance problem would be the increased path explosion from not removing infeasible paths early on.
- If we try to filter out infeasible paths continuously, either by employing RangeConstraintManager as a filter, or by employing Z3 as a filter, then Z3 would anyway benefit from simpler symbolic expressions. In the worst case ("that's what Z3 would have done itself anyway), we'd, i guess, have little effect on quality *or* performance

Generally, i've a feeling that simplifying SVals is a safe thing to do.


https://reviews.llvm.org/D31886