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

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to