[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

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!

lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp

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;
   }

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

 // 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; 
 }
 
+// *** FIXME ***
+// The result is unknown for the same reason as above.
+void test_asume_after_access(unsigned long x) {
+  int buf[100];
+  buf[x] = 1;
+  clang_analyzer_eval(x <= 99); // expected-warning{{UNKNOWN}}
+}
+
 // 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_asume_after_access2(unsigned long x) {
+  char buf[100];
+  buf[x] = 1;
+  clang_analyzer_eval(x <= 99); // expected-warning{{TRUE}}
+}
+