[PATCH] D88359: [analyzer][RFC] Complete rewrite of ArrayBoundCheckerV2

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

So, `ArrayBoundCheckerV3` then?

We already have a similar simplification facility in `SValBuilder` created to solve the similar problem with iterator checkers. It fires up when it knows that the values it works with are limited to roughly 1/4 of their type's range and therefore none of the individual operations over them can potentially overflow (cf. D35109 <https://reviews.llvm.org/D35109>). It's currently off by default because performance was not properly evaluated and none of the on-by-default checkers rely on it. This is currently the intended approach to such issues. It was decided that constructing a custom solver for "non-overflowing but still bounded" arithmetic was not the right thing to do, mostly because it absolutely doesn't correspond to the actual run-time behavior of the program that we're supposed to be modeling.

Separately, I'd like to once again bring up that the problem you're solving with this patch is relatively minor compared to bigger problems with this checker. One bigger problem is that this checker amplifies our lack of loop widening (i highly doubt that the existing alpha loop widening feature solves any of these, though i didn't try; it has to be really good loop widening in order to be effective). The checker has massive false positives because of just that. Like, it only deals with small concrete values, not much solving, but even then it's all wrong, just because the loop isn't executed the right number of times.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88359/new/

https://reviews.llvm.org/D88359