[PATCH] D148355: [analyzer] Fix comparison logic in ArrayBoundCheckerV2

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

This subject haunted us for quite some time now, and there is more behind what it seems at first.

If I'm not mistaken, this patch is pretty much what is in D86874 <https://reviews.llvm.org/D86874> except that it doesn't give up and still checks the upper-bound in this edge case - which is good.

I had other attempts at fixing this, from a different angle though, such as in D88359 <https://reviews.llvm.org/D88359> - where the idea was to do the //simplification// in the math domain (so not in the c++ language model). During this process, we would have the opportunity of explaining what assumptions were taken during the process where we finally constrain the (root, aka. `x`) symbol. Actually, these missing notes (explanations) are the reason why this checker is `alpha`. But yes, the other reason is this FP that you fixed.
Do you plan to explore ways to improve the readability of the reports explaining the constraints in the future?

At SonarSource, we had a fix for this issue for ~1.5 years now with great success.F27176964: sonarsource-CPP-2376.patch <https://reviews.llvm.org/F27176964>
We decided to keep it downstream, due to the failure of similar attempts :D
Our implementation and your have a lot in common.

The only difference (I think) is that we detect this case:

  void alwaysOverflow(unsigned long long s) {
    int x[20];
    x[s + 21] = 0; // Ours warn!
   // Hmm, it should work for `x + 20` as well.
  }

I haven't done an extensive differential analysis between this and our patches.
Do you think it would make sense to consider both implementations and forge them? Would you be up for that?
We could also say of course that we fix the FP first as a baby step.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D148355