[PATCH] D86874: [analyzer] Fix ArrayBoundCheckerV2 false positive regarding size_t indexer

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

steakhal created this revision.
steakhal added reviewers: NoQ, vsavchenko, Szelethus, martong, balazske, baloghadamsoftware.
Herald added subscribers: cfe-commits, ASDenysPetrov, Charusso, dkrupp, donat.nagy, arphaman, mikhail.ramalho, a.sidorin, rnkovacs, szepet, xazax.hun, whisperity.
Herald added a project: clang.
steakhal requested review of this revision.

Fixes the bug <https://bugs.llvm.org/show_bug.cgi?id=45148>.

  typedef unsigned long long size_t;
  const char a[] = "aabbcc";
  char f1(size_t len) {
    return a[len+1]; // false-positive warning: Out of bound memory access (access exceeds upper limit of memory block)
  }

Previousl, the analyzer did these things:

1. Calculates the RawOffset of the access, resulting in: BaseRegion: `a` and ByteOffset: `len + 1`
2. Checks the lower bound via transforming (//simplifying//) the question `len + 1 < 0` into `len < -1`. However, the analyzer can not prove nor disprove this, so it `assume`s that it holds. This assumption will constrain the `len` to be `UINT_MAX` since the `<` operator will promote the `-1` into `UINT_MAX`.
3. Checks the upper bound via transforming (//simplifying//) the question `len + 1 >= 7` into `len < 6`. Since the analyzer perfectly constrained `len` at the previous step, we wrongly diagnose an out-of-bound error.

Proposed solution:
Skip the lower bound check if the //simplified// root expression (in the current example `len`) is `unsigned` and the //simplified// index holds a negative value.
We know for sure that no out-of-bound error can happen in this part, since how could an unsigned symbolic value be less than a negative constant?
Note that we **don't** deal with wrapping here.

I hope that this fix gets this checker closer to the stage when it can leave alpha.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D86874

Files:
  clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp
  clang/test/Analysis/out-of-bounds-false-positive.c


Index: clang/test/Analysis/out-of-bounds-false-positive.c
===================================================================
--- clang/test/Analysis/out-of-bounds-false-positive.c
+++ clang/test/Analysis/out-of-bounds-false-positive.c
@@ -8,12 +8,11 @@
 const char a[] = "abcd"; // extent: 5 bytes
 
 void symbolic_size_t_and_int0(size_t len) {
-  // FIXME: Should not warn for this.
-  (void)a[len + 1]; // expected-warning {{Out of bound memory access}}
+  (void)a[len + 1]; // no-warning
   // We infered that the 'len' must be in a specific range to make the previous indexing valid.
   // len: [0,3]
-  clang_analyzer_eval(len <= 3); // expected - warning {{TRUE}}
-  clang_analyzer_eval(len <= 2); // expected - warning {{UNKNOWN}}
+  clang_analyzer_eval(len <= 3); // expected-warning {{TRUE}}
+  clang_analyzer_eval(len <= 2); // expected-warning {{UNKNOWN}}
 }
 
 void symbolic_size_t_and_int1(size_t len) {
Index: clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp
+++ clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp
@@ -222,6 +222,12 @@
   std::tie(RootNonLoc, ConstantFoldedRHS) =
       simplify(SVB, RawOffset.getByteOffset(), Zero);
 
+  // No unsigned symbolic value can be less then a negative constant.
+  if (const auto SymbolicRoot = RootNonLoc.getAs<SymbolVal>())
+    if (SymbolicRoot->getSymbol()->getType()->isUnsignedIntegerType() &&
+        ConstantFoldedRHS.castAs<ConcreteInt>().getValue().isNegative())
+      return State;
+
   NonLoc LowerBoundCheck =
       SVB.evalBinOpNN(State, BO_LT, RootNonLoc.castAs<NonLoc>(),
                       ConstantFoldedRHS.castAs<ConcreteInt>(),


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D86874.288926.patch
Type: text/x-patch
Size: 1762 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200831/6ffb1cec/attachment.bin>