[clang] [analyzer] Suppress out of bounds reports after weak loop assumptions (PR #109804)

[Donát Nagy via cfe-commits]

NagyDonat wrote:

> If I understand it correctly, we want to use (very likely) incorrect assumptions to suppress false positives produced by an alpha checker, which receives otherwise wrong assumptions. [...] I think the correct solution to this problem is to investigate why the specific checker receives wrong existing assumptions and make those assumptions correct.

No, the situation is significantly more complex.

The "wrong existing assumptions" are caused by a fundamental limitation of the path-sensitive analysis approach, namely that we need to follow one concrete execution path, which in a loop means modeling one particular iteration count. (See below for more detailed explanation.)

To "make those assumptions correct" we would need to implement a complex invalidation/widening procedure -- I wasted several months on it and didn't manage to make it work. If you write an accurate loop widening logic for the analyzer, then after that I'd happily remove the heuristic workaround added by this commit, but I don't want to wait years with bringing this checker out of the alpha state.

**Justified and wrong of assumptions in the analyzer:**

The analyzer makes _lots_ of assumptions: at each conditional expression, short-circuiting operator, loop etc. it must pick one of the multiple branches (by the way, this is implemented in `ExprEngine::processBranch()` and the related functions).

If the condition of the `if` statement is ambiguous (it can be both true and false in the current `State`), then **both choices are justified** because we can say that "the programmer wrote an `if` here, so he thinks that both cases are possible".

`<offtopic>` This "justification" is not entirely correct because there are paranoid defensive checks (and we try to filter them out with heuristics) and there are many know false positives that look like
```cpp
void do_something(/* some arguments */, bool flag1, bool flag2) {
  if (flag1) {
    // BLOCK1
  }
  // ...
  if (flag2) {
    // BLOCK2
  }
}
```
where it's semantically very clear for the programmer that `flag1` and `flag2` won't be used together, and the nonsense combination of BLOCK1 + BLOCK2 triggers some error. (Here the presence of "`if (flag2)`" implies that the programmer thinks that `flag2` can be true _in some situations_, but the analyzer is wrong when it assumes that `flag2` can be true _on the branch where BLOCK1 was executed_.) However this "correlated if" problem is a separate unrelated mostly-unsolvable limitation of the analyzer, so we shouldn't discuss it here. `</offtopic>`

If the condition of a loop is ambiguous (and e.g remains ambiguous each time it's evaluated), then that's a more complex issue: when programmers write a loop, then **it's justified to assume that "in some situations there can be at least two iterations"** (because otherwise the loop is an overkill and they should've just written an `if`) -- but **more concrete assumptions are all unjustified**, because the presence of the loop (with the ambiguous condition) doesn't imply anything like "there won't be any iterations", "there will be 1 iteration" or "there will be at least 3 iterations" etc.

Note: your inline comments suggest that the analyzer should assume and analyze e.g. the "there won't be any iterations" case unless something (e.g. an assertion) rules it out explicitly, but I strongly disagree with this philosophy because:
- There are situations where there is no natural place for the `assert()`: e.g. if the loop looks like `while (we_have_time() && !algorithm_finished(foo, bar, baz)) {...}` where would you put the assertion?
- The analyzer must aim for accepting all normal code, because it's not reasonable to demand that when a project starts to use static analyzer, they immediately introduce hundreds of assertions to fulfill the demands of our tyrannical tool.
Requiring assertions in situations where (e.g.) the zero-iteration case is impossible may be an useful design rule, but it's far from being universally accepted so we shouldn't enforce it in a general-purpose checker. (If you want to implement it as an off-by-default flag, then that would be OK, but I'm not interested in covering it.)

So, to summarize these, when we encounter a loop and the evaluations of the condition are ambiguous:
- The analyzer architecture can only follow concrete code paths like "skip the loop", "perform 1 iteration then leave", "perform 2 iterations then leave", ..., "perform 6457 iterations then leave" etc.
- It's (mostly - see the offtopic block near the beginning) justified to stay in the loop for 2 iterations, because if the programmer expected just one iteration, then they would've written an `if` instead of a loop.
- It's not justified to stay in the loop for more than two iterations, because the normal way to implement "loop that can execute $\le 2$ iterations" is the same as "loop that can execute many iterations" (and no, you cannot demand that short loops must be marked with assumptions, that's just one particular coding style).
- Theoretically speaking, it's never completely justified to assume a loop exit: for example I can imagine graph algorithms that gradually flood a certain array, where it's clear for the programmer that there will be at least `array_size` steps (but perhaps more).
  - In practice, it's unjustified to assume that the loop is completely skipped -- those branches produce many really ugly false positives.
  - In practice, it's usually OK to assume a loop exit when at least one iteration is completed -- in some cases that can still lead to false positives (e.g. [here](https://sonarsource.atlassian.net/browse/CPP-5698) is a false positive caused by assuming an exit after one iteration), but they are significantly rarer.
Based on this my patch aims to use the code paths that spend one or two iterations within the loops that they encounter. (This is currently limited to ArrayBoundV2, because that's where I've seen the overwhelming amount of false positives, but I think probably it'd be useful to generalize this kind of suppression to all the checkers.)

https://github.com/llvm/llvm-project/pull/109804