[analyzer] Correctly add assumptions based on array bounds.

[xazax.hun]

Summary

Right now due to a missing brace error the assumptions that an index is inbound in case we are under constrained is not added.

[NoQ]

Nice catch!

Now, this needs a test. How about this one:

// enable the debug.ExprInspection checker?
void clang_analyzer_eval(int);

void test_asume_after_access(unsigned long x) {
  char buf[100];
  buf[x] = 1;
  clang_analyzer_eval(x <= 99); // expected-warning{{TRUE}}
}

By the way, if we replace char with int, this test fails even with your patch. The reason is, the assumption is added on (4 * x) rather than on x, and the constraint manager explodes. Does anybody volunteer to fix this (eg. on the checker side - throw easier equations at the solver)?

[xazax.hun]

• Address review comments.

[xazax.hun]

I am not sure that the checker is the appropriate way to fix the remaining issue with this checker. I think generating simpler constraints without loosing any generality is non trivial.

[NoQ]

test/Analysis/out-of-bounds.c

153 ↗

(On Diff #67135)

Yay, there already was a test for this.

/asume/assume/ here and below?

[NoQ]

Whoops, forgot to answer:

In D23112#508333, @xazax.hun wrote:

I am not sure that the checker is the appropriate way to fix the remaining issue with this checker.

Yeah, there are anyway more problems that require this functionality in the RangeConstraintManager (the code throws complicated equations into it anyway, and there are false positives reported), so i think we should try to fix it there anyway, some day.

[xazax.hun]

• Simplifiy generated constraints.

[xazax.hun]

I added a (proof of concept?) implementation to simplify the constraints in the checker. I wonder what do you think.

[NoQ]

On second thought, in RangeConstraintManager we need a different functionality. In particular, from 4 * x < 1000 it does not follow that x < 250 in the general case (due to possible overflows). But in the case of this checker, it doesn't matter - we are always sure that any valid array address is never overflowing even when converted to bytes.

That said, it is still boilerplate. Some day i wish to consider adding the non-overflowing versions of common operations into the SValBuilder's evalBinOp(), so that it could help checkers simplify various symbolic expressions. In my opinion, evalBinOp() should be as user-friendly as possible.

But that's another story, your approach looks good to me!

cfe/trunk/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp

 //
 //===----------------------------------------------------------------------===//
 
 #include "ClangSACheckers.h"
 #include "clang/AST/CharUnits.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
 #include "clang/StaticAnalyzer/Core/Checker.h"
 #include "clang/StaticAnalyzer/Core/CheckerManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/Support/raw_ostream.h"
 
 using namespace clang;
 using namespace ento;
 
switch (region->getKind()) {
         // for symbolic regions.
         return UnknownVal();
       case MemRegion::ElementRegionKind:
         region = cast<SubRegion>(region)->getSuperRegion();
         continue;
     }
 }
 
+// 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.
+static std::pair<NonLoc, nonloc::ConcreteInt>
+getSimplifiedOffsets(NonLoc offset, nonloc::ConcreteInt extent,
+                     SValBuilder &svalBuilder) {
+  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());
+      switch (SIE->getOpcode()) {
+      case BO_Mul:
+        // The constant should never be 0 here, since it the result of scaling
+        // based on the size of a type which is never 0.
+        if ((extent.getValue() % constant) != 0)
+          return std::pair<NonLoc, nonloc::ConcreteInt>(offset, extent);
+        else
+          return getSimplifiedOffsets(
+              nonloc::SymbolVal(SIE->getLHS()),
+              svalBuilder.makeIntVal(extent.getValue() / constant),
+              svalBuilder);
+      case BO_Add:
+        return getSimplifiedOffsets(
+            nonloc::SymbolVal(SIE->getLHS()),
+            svalBuilder.makeIntVal(extent.getValue() - constant), svalBuilder);
+      default:
+        break;
+      }
+    }
+  }
+
+  return std::pair<NonLoc, nonloc::ConcreteInt>(offset, extent);
+}
+
 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();
   ProgramStateRef originalState = state;
 
   SValBuilder &svalBuilder = checkerContext.getSValBuilder();
   const RegionRawOffsetV2 &rawOffset =
     RegionRawOffsetV2::computeOffset(state, svalBuilder, location);
 
   if (!rawOffset.getRegion())
     return;
 
+  NonLoc rawOffsetVal = 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 (Optional<NonLoc> NV = extentBegin.getAs<NonLoc>()) {
-    SVal lowerBound =
-        svalBuilder.evalBinOpNN(state, BO_LT, rawOffset.getByteOffset(), *NV,
+    if (NV->getAs<nonloc::ConcreteInt>()) {
+      std::pair<NonLoc, nonloc::ConcreteInt> simplifiedOffsets =
+          getSimplifiedOffsets(rawOffset.getByteOffset(),
+                               NV->castAs<nonloc::ConcreteInt>(),
+                               svalBuilder);
+      rawOffsetVal = simplifiedOffsets.first;
+      *NV = simplifiedOffsets.second;
+    }
+
+    SVal lowerBound = svalBuilder.evalBinOpNN(state, BO_LT, rawOffsetVal, *NV,
                                               svalBuilder.getConditionType());
 
     Optional<NonLoc> lowerBoundToCheck = lowerBound.getAs<NonLoc>();
     if (!lowerBoundToCheck)
       return;
 
     ProgramStateRef state_precedesLowerBound, state_withinLowerBound;
     std::tie(state_precedesLowerBound, state_withinLowerBound) =
       state->assume(*lowerBoundToCheck);
void ArrayBoundCheckerV2::checkLocation(SVal location, bool isLoad,
   do {
     // CHECK UPPER BOUND: Is byteOffset >= extent(baseRegion)?  If so,
     // we are doing a load/store after the last valid offset.
     DefinedOrUnknownSVal extentVal =
       rawOffset.getRegion()->getExtent(svalBuilder);
     if (!extentVal.getAs<NonLoc>())
       break;
 
-    SVal upperbound
-      = svalBuilder.evalBinOpNN(state, BO_GE, rawOffset.getByteOffset(),
+    if (extentVal.getAs<nonloc::ConcreteInt>()) {
+      std::pair<NonLoc, nonloc::ConcreteInt> simplifiedOffsets =
+          getSimplifiedOffsets(rawOffset.getByteOffset(),
+                               extentVal.castAs<nonloc::ConcreteInt>(),
+                               svalBuilder);
+      rawOffsetVal = simplifiedOffsets.first;
+      extentVal = simplifiedOffsets.second;
+    }
+
+    SVal upperbound = svalBuilder.evalBinOpNN(state, BO_GE, rawOffsetVal,
                                               extentVal.castAs<NonLoc>(),
                                               svalBuilder.getConditionType());
 
     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) {
-      if (state->isTainted(rawOffset.getByteOffset()))
+      if (state->isTainted(rawOffset.getByteOffset())) {
         reportOOB(checkerContext, state_exceedsUpperBound, OOB_Tainted);
         return;
       }
-
-    // If we are constrained enough to definitely exceed the upper bound, report.
-    if (state_exceedsUpperBound) {
+    } 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);
     state = state_withinUpperBound;
   }

cfe/trunk/test/Analysis/out-of-bounds.c

-// RUN: %clang_cc1 -Wno-array-bounds -analyze -analyzer-checker=core,alpha.security.ArrayBoundV2 -verify %s
+// RUN: %clang_cc1 -Wno-array-bounds -analyze -analyzer-checker=core,alpha.security.ArrayBoundV2,debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
 
 // Tests doing an out-of-bounds access after the end of an array using:
 // - constant integer index
 // - constant integer size for buffer
 void test1(int x) {
   int buf[100];
   buf[100] = 1; // expected-warning{{Out of bound memory access}}
 }
void test2_multi_b(int x) {
   buf[-1][0] = 1; // expected-warning{{Out of bound memory access}}
 }
 
 void test2_multi_ok(int x) {
   int buf[100][100];
   buf[0][0] = 1; // no-warning
 }
 
-// *** FIXME ***
-// We don't get a warning here yet because our symbolic constraint solving
-// doesn't handle:  (symbol * constant) < constant
 void test3(int x) {
   int buf[100];
   if (x < 0)
-    buf[x] = 1;
+    buf[x] = 1; // expected-warning{{Out of bound memory access}}
 }
 
-// *** FIXME ***
-// We don't get a warning here yet because our symbolic constraint solving
-// doesn't handle:  (symbol * constant) < constant
 void test4(int x) {
   int buf[100];
   if (x > 99)
-    buf[x] = 1; 
+    buf[x] = 1; // expected-warning{{Out of bound memory access}}
+}
+
+void test_assume_after_access(unsigned long x) {
+  int buf[100];
+  buf[x] = 1;
+  clang_analyzer_eval(x <= 99); // expected-warning{{TRUE}}
 }
 
 // Don't warn when indexing below the start of a symbolic region's whose
 // base extent we don't know.
 int *get_symbolic();
 void test_index_below_symboloc() {
   int *buf = get_symbolic();
   buf[-1] = 0; // no-warning;
 }
 
 void test_incomplete_struct() {
   extern struct incomplete incomplete;
   int *p = (int *)&incomplete;
   p[1] = 42; // no-warning
 }
 
 void test_extern_void() {
   extern void v;
   int *p = (int *)&v;
   p[1] = 42; // no-warning
 }
 
+void test_assume_after_access2(unsigned long x) {
+  char buf[100];
+  buf[x] = 1;
+  clang_analyzer_eval(x <= 99); // expected-warning{{TRUE}}
+}
+