[Analyzer][VLASizeChecker] Fix problem with zero index assumption.

[balazske]

Summary

See https://bugs.llvm.org/show_bug.cgi?id=46128
The crash was caused by incorect assumptions on a and a + 1
that resulted in knowing something about a (that it is exactly -1)
and only knowing about a + 1 that it is non-zero.

"constraints": [
  { "symbol": "reg_$0<int a>", "range": "{ [-1, -1] }" },
  { "symbol": "(reg_$0<int a>) + 1", "range": "{ [-2147483648, -1], [1, 2147483647] }" }
],

The problem was fixed by replacing plain assume on symbol with assume on
binary operator (test for "a==0" instead of "a").
An additional check was inserted at place of the assertion to prevent
similar crashes.

A test that triggers this last case is missing now.
The added test causes no problem because at start of the second loop
"c" can not be zero because the previous assumption made by the checker
(that did not work correct before the fix).

[balazske]

There may be still a problem somewhere else. I think assume of "a" and "a==0" should have the same results.

[NoQ]

clang/lib/StaticAnalyzer/Checkers/VLASizeChecker.cpp

127–129

If we aim for a better fix, can we reduce the number of assumptions we make from 2 to 1? Like, it's ok if it's imperfect; 1 imperfect assumption is better than 2 imperfect assumptions.

The mental model i'm following here is that every path-sensitive bug can be thought of as a single formula over symbolic expressions. Eg., division by zero is the formula "$denominator == 0" is definitely true, double close is "is_closed($file_being_closed)", division by tainted value is "$denominator == 0" is possibly true AND "is_tainted($denominator)". I'd like you to write down the single formula that represents your bug and perform a single assume() over that and use the result of such assume as an ultimate source of truth. If such assume is not working correctly, let's think how to fix the assume rather than pile up more assumes in every checker to manually cross-check each other.

[balazske]

Improved assumption on array size.

[balazske]

clang/lib/StaticAnalyzer/Checkers/VLASizeChecker.cpp

127–129

Based on this the assumptions could be really simplified. Now the check is made only for positive array size.
One question is if it is good to leave the assert here. This condition shows internal inconsistency, it may be better to abort the checker instead of making probably bad state changes (in the bad case array extent was changed to a nonzero but probably negative value range).

[NoQ]

clang/lib/StaticAnalyzer/Checkers/VLASizeChecker.cpp

130–131

Why not do the same in checkVLAIndexSize then?

201–202

The type of binary operator >= is bool, not size_t.

[balazske]

clang/lib/StaticAnalyzer/Checkers/VLASizeChecker.cpp

130–131

The only reason for this is was that at this place the known index value is already computed but not in checkVLAIndexSize.

[balazske]

• Rebase
• Using condition type for evalBinOp
• Comments updated

[balazske]

Ping
This is a better fix for the previous problem, and makes the code better too.

[Szelethus]

I don't have much to say here, this goes a bit outside my expertise. @NoQ?

clang/lib/StaticAnalyzer/Checkers/VLASizeChecker.cpp

for (const Expr *SizeE : VLASizes) {
     SVal Mul = SVB.evalBinOpNN(State, BO_Mul, ArrSize, IndexLength, SizeTy);
     if (auto MulNonLoc = Mul.getAs<NonLoc>())
       ArrSize = *MulNonLoc;
     else
       // Extent could not be determined.
       return State;
 
     if (const llvm::APSInt *IndexLVal = SVB.getKnownValue(State, IndexLength)) {
+      uint64_t IndexL = IndexLVal->getZExtValue();
+      if (IndexL == 0) {
+        // Despite the previous assumptions for non-zero and positiveness,
+        // this value might be zero or negative.
+        // At least check for zero again.
+        // Assume that this is a more exact fact than the previous assumptions
+        // (in checkVLAIndexSize), so report error too.
+        reportBug(VLA_Zero, SizeE, State, C);
+        return nullptr;
+      }
       // Check if the array size will overflow.
       // Size overflow check does not work with symbolic expressions because a
       // overflow situation can not be detected easily.
-      uint64_t IndexL = IndexLVal->getZExtValue();
-      assert(IndexL > 0 && "Index length should have been checked for zero.");
       if (KnownSize <= SizeMax / IndexL) {
         KnownSize *= IndexL;
       } else {
         // Array size does not fit into size_t.
         reportBug(VLA_Overflow, SizeE, State, C);
         return nullptr;
       }
     } else {
ProgramStateRef VLASizeChecker::checkVLAIndexSize(CheckerContext &C,
 
   // Check if the size is tainted.
   if (isTainted(State, SizeV)) {
     reportBug(VLA_Tainted, SizeE, nullptr, C,
               std::make_unique<TaintBugVisitor>(SizeV));
     return nullptr;
   }
 
-  // Check if the size is zero.
+  QualType SizeTy = SizeE->getType();
   DefinedSVal SizeD = SizeV.castAs<DefinedSVal>();
+  SValBuilder &SVB = C.getSValBuilder();
+  DefinedOrUnknownSVal Zero = SVB.makeZeroVal(SizeTy);
 
-  ProgramStateRef StateNotZero, StateZero;
-  std::tie(StateNotZero, StateZero) = State->assume(SizeD);
+  // Check if the size is zero.
+
+  SVal IsZeroVal = SVB.evalBinOp(State, BO_EQ, SizeD, Zero, SizeTy);
+  if (Optional<DefinedSVal> IsZeroDVal = IsZeroVal.getAs<DefinedSVal>()) {
+    ProgramStateRef StateZero, StateNotZero;
 
+    std::tie(StateZero, StateNotZero) = State->assume(*IsZeroDVal);
     if (StateZero && !StateNotZero) {
-    reportBug(VLA_Zero, SizeE, StateZero, C);
+      reportBug(VLA_Zero, SizeE, State, C);
       return nullptr;
     }
-
-  // From this point on, assume that the size is not zero.
     State = StateNotZero;
+  }
 
   // Check if the size is negative.
-  SValBuilder &SVB = C.getSValBuilder();
-
-  QualType SizeTy = SizeE->getType();
-  DefinedOrUnknownSVal Zero = SVB.makeZeroVal(SizeTy);
 
   SVal LessThanZeroVal = SVB.evalBinOp(State, BO_LT, SizeD, Zero, SizeTy);
   if (Optional<DefinedSVal> LessThanZeroDVal =
           LessThanZeroVal.getAs<DefinedSVal>()) {
-    ConstraintManager &CM = C.getConstraintManager();
     ProgramStateRef StatePos, StateNeg;
 
-    std::tie(StateNeg, StatePos) = CM.assumeDual(State, *LessThanZeroDVal);
+    std::tie(StateNeg, StatePos) = State->assume(*LessThanZeroDVal);
     if (StateNeg && !StatePos) {
       reportBug(VLA_Negative, SizeE, State, C);
       return nullptr;
     }
     State = StatePos;
   }
 
   return State;

clang/test/Analysis/vla.c

void check_VLA_extent() {
   int vla2m[2][x];
   clang_analyzer_eval(clang_analyzer_getExtent(&vla2m) == 2 * x * sizeof(int));
   // expected-warning@-1{{TRUE}}
 
   int vla3m[2][x][4];
   clang_analyzer_eval(clang_analyzer_getExtent(&vla3m) == 2 * x * 4 * sizeof(int));
   // expected-warning@-1{{TRUE}}
 }
+
+// https://bugs.llvm.org/show_bug.cgi?id=46128
+// Analyzer doesn't handle more than simple symbolic expressions correct.
+// Just don't crash.
+extern void foo(void);
+int a;
+void b() {
+  int c = a + 1;
+  for (;;) {
+    int d[c];
+    for (; 0 < c;)
+      foo();
+  }
+} // no-crash