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

Mon Sep 28 01:37:01 PDT 2020

steakhal added a comment.

In D88359#2297074 <https://reviews.llvm.org/D88359#2297074>, @NoQ wrote:

> So, `ArrayBoundCheckerV3` then?

:D

> 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>).

I know, I have seen that patch, even proved the correctness of the main idea in Z3.
Essentially I'm trying to do the same, but with an ad-hoc calculated upper and lower bound. Constraining any subexpressions of the subscript expression to be in a made-up range like 1/4 (or anything else) would result in unsound constraints and assumptions. So I still think my approach is the only sound one [*].

> 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.

What if we don't want to model the langue but rearrange an inequality to have a different form?
This checker did always this rearrange, expressing `x` in `0 <= x * 2 + 3 < 8` via transforming into `-1 <= x < 3`. Using this the checker could have infered that `x` must be in range `[-1, 2]` to make the dereference valid.
However, we can not make such a transformation without having the appropriate constraints. Such as that no subexpression can overflow/underflow during the transformation AND we must evaluate the constant folding in a mathematical sense (signed, no-wrapping).

> 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.

I haven't touched loop-widening, I will have a look.
By the same token, I also wanted to evaluate some reports.

[X] Assuming that no overflow/underflow could happen in any subexpression (as a heuristic) might introduce false assumptions especially if `-fwrapv` compiler option made signed wrapping well defined or the expression is of unsigned type which is by definition could wrap.

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D88359