[analyzer] Fix comparison logic in ArrayBoundCheckerV2

[donat.nagy]

Summary

The prototype checker alpha.security.ArrayBoundV2 performs two comparisons to check that in an expression like Array[Index]

0 <= Index < length(Array)

holds. These comparisons are handled by almost identical logic: the inequality is first rearranged by getSimplifiedOffsets(), then evaluated with evalBinOpNN().

However the simplification used "naive" elementary mathematical schematics, while evalBinOpNN() performed the signed -> unsigned conversions described in the C/C++ standards, and these led to wildly inaccurate results: false positives from the lower bound check and false negatives from the upper bound check.

This commit eliminates the code duplication by moving the comparison logic into a separate function, and introduces an explicit check that handles the problematic case separately.

In addition to this, the commit also cleans up a testcase that was demonstrating the presence of this problem. Note that while that testcase was failing with an overflow error, its actual problem was in the underflow handler logic:
(0) The testcase introduces with a five-element array "char a[5]" and an unknown argument "size_t len"; then evaluates "a[len+1]".
(1) The underflow check tries to determine whether "len+1 < 0" holds.
(2) This inequality is rearranged to "len < -1".
(3) evalBinOpNN() evaluates this with the schematics of C/C++ and converts -1 to the size_t value SIZE_MAX.
(4) The engine concludes that len == SIZE_MAX, because otherwise we'd have an underflow here.
(5) The overflow check tries to determine whether "len+1 >= 5".
(6) This inequality is rearranged to "len >= 4".
(7) The engine substitutes len == SIZE_MAX and reports that we have an overflow.

[steakhal]

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 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 - 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.

sonarsource-CPP-2376.patch2 KBDownload

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.

[donat.nagy]

@steakhal Thanks for the background information!

I didn't know about D86874 so I indeed ended up with something very similar to it. I reviewed D88359 and I knew that it's a completely general solution of this issue, but I felt that it's too complicated and wanted to create a patch with shorter code than that.

I really like the "use zero instead of negative numbers" trick in the SonarSource patch; if you would upload that for a review, I'd strongly support merging it.

Another alternative is that I'm working on a new version of my patch, which would eliminate the code duplication between the underflow and overflow checks (by introducing a single function compareValueToThreshold that performs offset simplification when needed, handles the unsigned-vs-negative case, calls evalBinOpNN and invokes state->assume). This would be equivalent to the SonarSource patch (it handles unsigned-vs-negative comparison on "both sides") with the added independent benefit of simplifying the codebase. However, I can also do this code simplification as a separate patch after merging the SonarSource solution for the bug.

Which solution would you prefer (upstream the solution used by SonarSource + separate code quality improvement or the combined refactor-and-check-before-evalBinOpNN variant that I could implement)?

[steakhal]

In D148355#4279866, @donat.nagy wrote:

@steakhal Thanks for the background information!

I didn't know about D86874 so I indeed ended up with something very similar to it. I reviewed D88359 and I knew that it's a completely general solution of this issue, but I felt that it's too complicated and wanted to create a patch with shorter code than that.

I really like the "use zero instead of negative numbers" trick in the SonarSource patch; if you would upload that for a review, I'd strongly support merging it.

Another alternative is that I'm working on a new version of my patch, which would eliminate the code duplication between the underflow and overflow checks (by introducing a single function compareValueToThreshold that performs offset simplification when needed, handles the unsigned-vs-negative case, calls evalBinOpNN and invokes state->assume). This would be equivalent to the SonarSource patch (it handles unsigned-vs-negative comparison on "both sides") with the added independent benefit of simplifying the codebase. However, I can also do this code simplification as a separate patch after merging the SonarSource solution for the bug.

Which solution would you prefer (upstream the solution used by SonarSource + separate code quality improvement or the combined refactor-and-check-before-evalBinOpNN variant that I could implement)?

Right now I don't have the bandwidth for upstreaming our version, and it seems like you already picked up the subject, so it's probably less intrusive for you. But I should speak for my self I know.
So, you can update this revision to our version, or modify or inspire by our version. Anything you want.
The only thing is, if the patch, in the end, is sufficiently similar to ours, I think we should add credit to the original author, who is I think @tomasz-kaminski-sonarsource (Tomasz Kamiński <[e-mail]>).

I can help to review and do measurements at scale but I don't think I can contribute in other ways.

And on the note of doing refinement followup patches. If those are NFC (non-function changes), then those should be separated from semantic changes for sure.
Pure NFC changes make validation much easier, equally so the review process. If not, then it's up to you how you think it's the easiest to review the patch set.

[donat.nagy]

@steakhal Then I'll clean up my own solution, which will be completely independent of the patch of Tomasz (except for the obviously identical changes in the test code).

The de-duplication that I'm planning is not pure NFC, because it'll probably affect some mostly-theoretical corner cases: e.g. the current implementation skips the upper bound check if lowerBound (the result of the first evalBinOpNN) is not a NonLoc, while after the refactor this won't trigger an early return. As it's not a very big change (limited to one function), I'll probably do it in the same commit as the fix of the unsigned-vs-negative bug.

[steakhal]

Sounds good. Thanks for clarifying.

[donat.nagy]

I'm publishing the extended variant of this commit (which I mentioned in earlier comments).

This generalizes the first version of the commit to check for the unsigned-vs-negative comparison on both bound checks (and eliminates the code duplication between the two bound checks by moving their logic into a helper function), so it will behave similarly to Tomasz's solution (which uses the indirect "use 0 instead of negative numbers" trick to avoid unsigned-vs-negative comparisons).

[donat.nagy]

I tested this patch on a few open source projects and it significantly reduced the number of alpha.security.ArrayBoundV2 reports:

Project name	memcached	tmux	curl	twin	vim	openssl	sqlite
Baseline report #	0	2	13	6	12	7	11
Report # with this patch	0	2	0	3	3	0	4

(The patched version did not produce any additional reports, it seems these projects does not contain any bugs where the enhancements of the upper bound check could become significant. As a minor side effect, applying the patch also eliminated an alpha.deadcode.UnreachableCode report -- presumably because the analysis wasn't stopped at some false positive.)

I briefly looked at the eliminated reports, but they are very convoluted and I didn't analyze them to understand their (presumably buggy) logic. It seems that the remaining reports are also false positive (which is not surprising, as we are analyzing released, stable versions), but they are mostly reasonable:

• Several reports complain about expressions like c = fgetc(f), isdigit(c) because fgetc(f) returns tainted output and (at least in glibc) character type macros like isdigit(c) are equivalent to ((*__ctype_b_loc())[(int)(c)] & <some bitmask>. It would be relatively straightforward to fix these reports, perhaps by modelling the behavior of the internal function __ctype_b_loc().
• Several reports are produced by code like s = get_tainted_string(); int n = strlen(s); if (n > 0) return s[n-1]; where the analyzer says that n-1 is a tainted index so this may be an overflow error. To model this correctly we'd need to maintain a connection between the memory region of the string and the symbol conjured as the return value of strlen; my first guess is that this is doable but not too easy.
• There are also some sporadic false positives where the analyzer is confused by code that relies on tricky ad-hoc invariants.

[steakhal]

I like this. Looks really solid.
I only had style nitpicks.

Have you run measurements?
After that we could land it, I think.

FYI: I'll also schedule a test run with this patch. You should expect the results in a week - not because it takes that long, but because I need to find time for evaluating it xD.

clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp

57–59

118–132

133–134

133–137

163–164

I don't think we need an explanation here.
BTW This "optional-like" RegionRawOffsetV2 makes me angry. It should be an std::optional<RegionRawOffsetV2> in the first place.
You don't need to take actions, I'm just ranting...

168

169–170

Good point.

177

189

190–192

I think as we don't plan to overwrite/assign to these states, we could just use structured bindings.
I think that should be preferred over std::tie()-ing think. That is only not widespread because we just recently moved to C++17.

205–209

You just left the guarded block in the previous line.
By moving this statement there you could spare the if.

301–303

[steakhal]

Okay, so you just added some numbers :D
Now it's my turn I guess. I'll compare this version against the version I shared, and use in our product.
Stay tuned.

[donat.nagy]

@steakhal Thanks for the review, it was really instructive :). I'll probably upload the updated commit on Monday.

clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp

163–164

Yes, I was also very annoyed by this "intrustive optional" behavior and I seriously considered refactoring the code to use a real std::optional, but I didn't want to snowball this change into a full-scale rewrite so I ended up with the assert in the constructor and this comment. Perhaps I'll refactor it in a separate NFC...

168

You're completely right, I just blindly copied this test from the needlessly overcomplicated computeExtentBegin().

205–209

Nice catch :)

[steakhal]

clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp

163–164

Please :D

168

Hold on. This would only skip the lower bounds check if it's an UnknownSpaceRegion.
Shouldn't we early return instead?

205–209

On second though no. The outer if guards state_exceedsUpperBound.
So this check seems necessary.

[donat.nagy]

clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp

168

This behavior is inherited from the code before my commit: the old block if ( /*... =*/ extentBegin.getAs<NonLoc>() ) { /* ... */ } is equivalent to if (llvm::isa<UnknownSpaceRegion>(SR)) { /*...*/ } and there was no early return connected to this NonLocness check. (The old code skipped the upper bound check if the result of evalBinOpNN() is unknown, and that's what I changed because I saw no reason to do an early return there.)

After some research into the memory region model, I think that there is no reason to perform an early return -- in fact, the condition of this if seems to be too narrow because we would like to warn about code like

struct foo {
  int tag;
  int array[5];
};
int f(struct foo *p) {
  return p->arr[-1];
}

despite the fact that it's indexing into a FieldRegion inside a SymbolicRegion in UnknownSpaceRegion. That is, instead of checking the top-level MemorySpace, the correct logic would be checking the kind of the memory region and/or perhaps its immediate super-region.

As this is a complex topic and completely unrelated to the main goal of this commit; I'd prefer to keep the old (not ideal, but working) logic in this patch, then revisit this question by creating a separate follow-up commit.

168

Minor nitpick: your suggested change accidentally negated the conditional :) ... and I said that it's "completely right". I'm glad that I noticed this and inserted the "!" before the isa check because otherwise it could've been annoying to debug this...

169–170

For now I'm keeping this comment (with your formatting changes), because it's "approximately correct", but I'll replace or elaborate it when I refine the condition for skipping the lower bound check.

190–192

Good suggestion, applied both here and at the lower bound check.

205–209

Yup, kept it. You had me at first glance... ;)

[steakhal]

Please mark comments "Done" where applicable.

clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp

168

Agreed.

168

Sorry about that. Happens

[donat.nagy]

@steakhal I marked a few comments as Done (I accidentally missed some when I was creating the most recent patch) and now the only not-Done thing is the followup commit for refactoring the optionalness of RegionRawOffsetV2. Do you see anything else to do?

[donat.nagy]

clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp

168

No problem :)

[steakhal]

In D148355#4294738, @donat.nagy wrote:

@steakhal I marked a few comments as Done (I accidentally missed some when I was creating the most recent patch) and now the only not-Done thing is the followup commit for refactoring the optionalness of RegionRawOffsetV2. Do you see anything else to do?

I think it's good. I've just scheduled the measurement now for 180+ OSS projects. Stay tuned!

[steakhal]

In D148355#4294798, @steakhal wrote:

In D148355#4294738, @donat.nagy wrote:

@steakhal I marked a few comments as Done (I accidentally missed some when I was creating the most recent patch) and now the only not-Done thing is the followup commit for refactoring the optionalness of RegionRawOffsetV2. Do you see anything else to do?

I think it's good. I've just scheduled the measurement now for 180+ OSS projects. Stay tuned!

The results are all good. The effect is pretty much equal to the effect of our implementation except for a handful of absent reports - and we are talking about at most 20 issues in total.
I must say, the report diff looks much better than I anticipated.
Thank you for working on this. Feel free to merge this change whenever you want. Thanks.

BTW the issues themselves look terrible. One cannot understand and track the value of the index and the assumed buffer size etc.
So the checker will still remain in alpha.

[donat.nagy]

Committed in rGde2547329b41ad6ea4ea876d12731bde5a6b64c5 (which accidentally refers to a wrong Phabricator review).

clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp

 private:
   const SubRegion *baseRegion;
   SVal byteOffset;
 
   RegionRawOffsetV2()
     : baseRegion(nullptr), byteOffset(UnknownVal()) {}
 
 public:
-  RegionRawOffsetV2(const SubRegion* base, SVal offset)
-    : baseRegion(base), byteOffset(offset) {}
+  RegionRawOffsetV2(const SubRegion *base, NonLoc offset)
+      : baseRegion(base), byteOffset(offset) { assert(base); }
 
   NonLoc getByteOffset() const { return byteOffset.castAs<NonLoc>(); }
   const SubRegion *getRegion() const { return baseRegion; }
 
   static RegionRawOffsetV2 computeOffset(ProgramStateRef state,
                                          SValBuilder &svalBuilder,
                                          SVal location);
 
   void dump() const;
   void dumpToStream(raw_ostream &os) const;
 };
 }
 
-static SVal computeExtentBegin(SValBuilder &svalBuilder,
-                               const MemRegion *region) {
-  const MemSpaceRegion *SR = region->getMemorySpace();
-  if (SR->getKind() == MemRegion::UnknownSpaceRegionKind)
-    return UnknownVal();
-  else
-    return svalBuilder.makeZeroArrayIndex();
-}
-
 // TODO: once the constraint manager is smart enough to handle non simplified
 // symbolic expressions remove this function. Note that this can not be used in
 // the constraint manager as is, since this does not handle overflows. It is
 // safe to assume, however, that memory offsets will not overflow.
+// NOTE: callers of this function need to be aware of the effects of overflows
+// and signed<->unsigned conversions!
 static std::pair<NonLoc, nonloc::ConcreteInt>
 getSimplifiedOffsets(NonLoc offset, nonloc::ConcreteInt extent,
                      SValBuilder &svalBuilder) {
   std::optional<nonloc::SymbolVal> SymVal = offset.getAs<nonloc::SymbolVal>();
   if (SymVal && SymVal->isExpression()) {
     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SymVal->getSymbol())) {
       llvm::APSInt constant =
           APSIntType(extent.getValue()).convert(SIE->getRHS());
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SymVal->getSymbol())) {
         break;
       }
     }
   }
 
   return std::pair<NonLoc, nonloc::ConcreteInt>(offset, extent);
 }
 
+// Evaluate the comparison Value < Threshold with the help of the custom
+// simplification algorithm defined for this checker. Return a pair of states,
+// where the first one corresponds to "value below threshold" and the second
+// corresponds to "value at or above threshold". Returns {nullptr, nullptr} in
+// the case when the evaluation fails.
+static std::pair<ProgramStateRef, ProgramStateRef>
+compareValueToThreshold(ProgramStateRef State, NonLoc Value, NonLoc Threshold,
+                        SValBuilder &SVB) {
+  if (auto ConcreteThreshold = Threshold.getAs<nonloc::ConcreteInt>()) {
+    std::tie(Value, Threshold) = getSimplifiedOffsets(Value, *ConcreteThreshold, SVB);
+  }
+  if (auto ConcreteThreshold = Threshold.getAs<nonloc::ConcreteInt>()) {
+    QualType T = Value.getType(SVB.getContext());
+    if (T->isUnsignedIntegerType() && ConcreteThreshold->getValue().isNegative()) {
+      // In this case we reduced the bound check to a comparison of the form
+      //   (symbol or value with unsigned type) < (negative number)
+      // which is always false. We are handling these cases separately because
+      // evalBinOpNN can perform a signed->unsigned conversion that turns the
+      // negative number into a huge positive value and leads to wildly
+      // inaccurate conclusions.
+      return {nullptr, State};
+    }
+  }
+  auto BelowThreshold =
+      SVB.evalBinOpNN(State, BO_LT, Value, Threshold, SVB.getConditionType()).getAs<NonLoc>();
+
+  if (BelowThreshold)
+    return State->assume(*BelowThreshold);
+
+  return {nullptr, nullptr};
+}
+
 void ArrayBoundCheckerV2::checkLocation(SVal location, bool isLoad,
                                         const Stmt* LoadS,
                                         CheckerContext &checkerContext) const {
 
   // NOTE: Instead of using ProgramState::assumeInBound(), we are prototyping
   // some new logic here that reasons directly about memory region extents.
   // Once that logic is more mature, we can bring it back to assumeInBound()
   // for all clients to use.
   //
   // The algorithm we are using here for bounds checking is to see if the
   // memory access is within the extent of the base region.  Since we
   // have some flexibility in defining the base region, we can achieve
   // various levels of conservatism in our buffer overflow checking.
   ProgramStateRef state = checkerContext.getState();
 
   SValBuilder &svalBuilder = checkerContext.getSValBuilder();
   const RegionRawOffsetV2 &rawOffset =
     RegionRawOffsetV2::computeOffset(state, svalBuilder, location);
 
   if (!rawOffset.getRegion())
     return;
 
-  NonLoc rawOffsetVal = rawOffset.getByteOffset();
+  NonLoc ByteOffset = rawOffset.getByteOffset();
 
-  // CHECK LOWER BOUND: Is byteOffset < extent begin?
-  //  If so, we are doing a load/store
-  //  before the first valid offset in the memory region.
-
-  SVal extentBegin = computeExtentBegin(svalBuilder, rawOffset.getRegion());
-
-  if (std::optional<NonLoc> NV = extentBegin.getAs<NonLoc>()) {
-    if (auto ConcreteNV = NV->getAs<nonloc::ConcreteInt>()) {
-      std::pair<NonLoc, nonloc::ConcreteInt> simplifiedOffsets =
-          getSimplifiedOffsets(rawOffset.getByteOffset(), *ConcreteNV,
-                               svalBuilder);
-      rawOffsetVal = simplifiedOffsets.first;
-      *NV = simplifiedOffsets.second;
-    }
-
-    SVal lowerBound = svalBuilder.evalBinOpNN(state, BO_LT, rawOffsetVal, *NV,
-                                              svalBuilder.getConditionType());
+  // CHECK LOWER BOUND
+  const MemSpaceRegion *SR = rawOffset.getRegion()->getMemorySpace();
+  if (!llvm::isa<UnknownSpaceRegion>(SR)) {
+    // A pointer to UnknownSpaceRegion may point to the middle of
+    // an allocated region.
+
+    auto [state_precedesLowerBound, state_withinLowerBound] =
+        compareValueToThreshold(state, ByteOffset,
+                                svalBuilder.makeZeroArrayIndex(), svalBuilder);
 
-    std::optional<NonLoc> lowerBoundToCheck = lowerBound.getAs<NonLoc>();
-    if (!lowerBoundToCheck)
-      return;
-
-    ProgramStateRef state_precedesLowerBound, state_withinLowerBound;
-    std::tie(state_precedesLowerBound, state_withinLowerBound) =
-      state->assume(*lowerBoundToCheck);
-
-    // Are we constrained enough to definitely precede the lower bound?
     if (state_precedesLowerBound && !state_withinLowerBound) {
+      // We know that the index definitely precedes the lower bound.
       reportOOB(checkerContext, state_precedesLowerBound, OOB_Precedes);
       return;
     }
 
-    // Otherwise, assume the constraint of the lower bound.
-    assert(state_withinLowerBound);
+    if (state_withinLowerBound)
       state = state_withinLowerBound;
   }
 
-  do {
-    // CHECK UPPER BOUND: Is byteOffset >= size(baseRegion)?  If so,
-    // we are doing a load/store after the last valid offset.
-    const MemRegion *MR = rawOffset.getRegion();
-    DefinedOrUnknownSVal Size = getDynamicExtent(state, MR, svalBuilder);
-    if (!isa<NonLoc>(Size))
-      break;
-
-    if (auto ConcreteSize = Size.getAs<nonloc::ConcreteInt>()) {
-      std::pair<NonLoc, nonloc::ConcreteInt> simplifiedOffsets =
-          getSimplifiedOffsets(rawOffset.getByteOffset(), *ConcreteSize,
-                               svalBuilder);
-      rawOffsetVal = simplifiedOffsets.first;
-      Size = simplifiedOffsets.second;
+  // CHECK UPPER BOUND
+  DefinedOrUnknownSVal Size =
+      getDynamicExtent(state, rawOffset.getRegion(), svalBuilder);
+  if (auto KnownSize = Size.getAs<NonLoc>()) {
+    auto [state_withinUpperBound, state_exceedsUpperBound] =
+        compareValueToThreshold(state, ByteOffset, *KnownSize, svalBuilder);
+
+    if (state_exceedsUpperBound) {
+      if (!state_withinUpperBound) {
+        // We know that the index definitely exceeds the upper bound.
+        reportOOB(checkerContext, state_exceedsUpperBound, OOB_Excedes);
+        return;
       }
-
-    SVal upperbound = svalBuilder.evalBinOpNN(state, BO_GE, rawOffsetVal,
-                                              Size.castAs<NonLoc>(),
-                                              svalBuilder.getConditionType());
-
-    std::optional<NonLoc> upperboundToCheck = upperbound.getAs<NonLoc>();
-    if (!upperboundToCheck)
-      break;
-
-    ProgramStateRef state_exceedsUpperBound, state_withinUpperBound;
-    std::tie(state_exceedsUpperBound, state_withinUpperBound) =
-      state->assume(*upperboundToCheck);
-
-    // If we are under constrained and the index variables are tainted, report.
-    if (state_exceedsUpperBound && state_withinUpperBound) {
-      SVal ByteOffset = rawOffset.getByteOffset();
       if (isTainted(state, ByteOffset)) {
+        // Both cases are possible, but the index is tainted, so report.
         reportOOB(checkerContext, state_exceedsUpperBound, OOB_Tainted,
                   std::make_unique<TaintBugVisitor>(ByteOffset));
         return;
       }
-    } else if (state_exceedsUpperBound) {
-      // If we are constrained enough to definitely exceed the upper bound,
-      // report.
-      assert(!state_withinUpperBound);
-      reportOOB(checkerContext, state_exceedsUpperBound, OOB_Excedes);
-      return;
     }
 
-    assert(state_withinUpperBound);
+    if (state_withinUpperBound)
       state = state_withinUpperBound;
   }
-  while (false);
 
   checkerContext.addTransition(state);
 }
 
 void ArrayBoundCheckerV2::reportOOB(
     CheckerContext &checkerContext, ProgramStateRef errorState, OOB_Kind kind,
     std::unique_ptr<BugReporterVisitor> Visitor) const {
 
RegionRawOffsetV2 RegionRawOffsetV2::computeOffset(ProgramStateRef state,
                                                    SVal location)
 {
   const MemRegion *region = location.getAsRegion();
   SVal offset = UndefinedVal();
 
   while (region) {
     switch (region->getKind()) {
       default: {
         if (const SubRegion *subReg = dyn_cast<SubRegion>(region)) {
-          offset = getValue(offset, svalBuilder);
-          if (!offset.isUnknownOrUndef())
-            return RegionRawOffsetV2(subReg, offset);
+          if (auto Offset = getValue(offset, svalBuilder).getAs<NonLoc>())
+            return RegionRawOffsetV2(subReg, *Offset);
         }
         return RegionRawOffsetV2();
       }
       case MemRegion::ElementRegionKind: {
         const ElementRegion *elemReg = cast<ElementRegion>(region);
         SVal index = elemReg->getIndex();
         if (!isa<NonLoc>(index))
           return RegionRawOffsetV2();

clang/test/Analysis/array-bound-v2-constraint-check.c

 // RUN: %clang_analyze_cc1 -analyzer-checker=core,alpha.security.ArrayBoundV2,debug.ExprInspection \
 // RUN:   -analyzer-config eagerly-assume=false -verify %s
 
 void clang_analyzer_eval(int);
 void clang_analyzer_printState(void);
 
 typedef unsigned long long size_t;
 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) {
   (void)a[len]; // no-warning
   // len: [0,4]
   clang_analyzer_eval(len <= 4); // expected-warning {{TRUE}}
   clang_analyzer_eval(len <= 3); // expected-warning {{UNKNOWN}}
 }