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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
