[clang] [analyzer] Switch to PostStmt callbacks in ArrayBoundV2 (PR #72107)

[via cfe-commits]

=?utf-8?q?Donát?= Nagy <donat.nagy at ericsson.com>,
=?utf-8?q?Donát?= Nagy <donat.nagy at ericsson.com>,
=?utf-8?q?Donát?= Nagy <donat.nagy at ericsson.com>,
=?utf-8?q?Donát?= Nagy <donat.nagy at ericsson.com>
Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/72107 at github.com>


================
@@ -350,17 +383,38 @@ void ArrayBoundCheckerV2::checkLocation(SVal Location, bool IsLoad,
     if (ExceedsUpperBound) {
       if (!WithinUpperBound) {
         // We know that the index definitely exceeds the upper bound.
-        std::string RegName = getRegionName(Reg);
-        std::string Msg = getExceedsMsg(C.getASTContext(), RegName, ByteOffset,
-                                        *KnownSize, Location);
-        reportOOB(C, ExceedsUpperBound, OOB_Exceeds, ByteOffset, RegName, Msg);
+        if (isa<ArraySubscriptExpr>(E) && isInAddressOf(E, C.getASTContext())) {
+          // ...but this is within an addressof expression, so we need to check
+          // for the exceptional case that `&array[size]` is valid.
+          auto [EqualsToThreshold, NotEqualToThreshold] =
+              compareValueToThreshold(ExceedsUpperBound, ByteOffset, *KnownSize,
+                                      SVB, /*CheckEquality=*/true);
+          if (EqualsToThreshold && !NotEqualToThreshold) {
+            // We are definitely in the exceptional case, so return early
+            // instead of reporting a bug.
+            C.addTransition(EqualsToThreshold);
----------------
DonatNagyE wrote:

You're right that `EqualsToThreshold` does not contain new information compared to `State`, but I'm using it because I'm trying to follow the pattern that I'm always using the _most recent_ state variable.

On the other hand, the variable `State` may contain new information compared to the state of the node before the start of this callback: e.g. if we start with a range set like $[-\infty, -1] \cup \\{ 10\\}$ for the index variable, then we first test for underflow and update the variable `State` when we assume that there is no underflow.

I think it's valuable to record these assumptions with a state transition, because they improve the accuracy of the modeling. (Otherwise the analyzer could produce bug reports that rely on assumptions that contradict each other.) Currently the assumptions of this checker are added silently but I'll add note tags like "Assuming index is non-negative" for them in a followup commit.

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