[PATCH] [analyzer][Bugfix/improvement] Fix for PR16833

[Jordan Rose]

Sorry it's taken a while to get back to this. I still have a few concerns here (see inline comments), but overall I think this approach is all right. Please add several more tests, though, showing that we're actually modeling this correctly, and including cases where we take the case and cases where we don't.

================
Comment at: lib/StaticAnalyzer/Core/ExprEngine.cpp:1675
@@ -1668,42 +1674,3 @@
 
-    // FIXME: Eventually we should replace the logic below with a range
-    //  comparison, rather than concretize the values within the range.
-    //  This should be easy once we have "ranges" for NonLVals.
-
-    do {
-      nonloc::ConcreteInt CaseVal(getBasicVals().getValue(V1));
-      DefinedOrUnknownSVal Res = svalBuilder.evalEQ(DefaultSt ? DefaultSt : state,
-                                               CondV, CaseVal);
-
-      // Now "assume" that the case matches.
-      if (ProgramStateRef stateNew = state->assume(Res, true)) {
-        builder.generateCaseStmtNode(I, stateNew);
-
-        // If CondV evaluates to a constant, then we know that this
-        // is the *only* case that we can take, so stop evaluating the
-        // others.
-        if (CondV.getAs<nonloc::ConcreteInt>())
-          return;
-      }
-
-      // Now "assume" that the case doesn't match.  Add this state
-      // to the default state (if it is feasible).
-      if (DefaultSt) {
-        if (ProgramStateRef stateNew = DefaultSt->assume(Res, false)) {
-          defaultIsFeasible = true;
-          DefaultSt = stateNew;
-        }
-        else {
-          defaultIsFeasible = false;
-          DefaultSt = nullptr;
-        }
-      }
-
-      // Concretize the next value in the range.
-      if (V1 == V2)
-        break;
-
-      ++V1;
-      assert (V1 <= V2);
-
-    } while (true);
+    ProgramStateRef stateNew;
+    assert(CondV.getAs<NonLoc>());
----------------
Please follow the LLVM naming conventions (http://llvm.org/docs/CodingStandards.html#name-types-functions-variables-and-enumerators-properly).

================
Comment at: lib/StaticAnalyzer/Core/ExprEngine.cpp:1681
@@ +1680,3 @@
+
+    // Now "assume" that the case matches.
+    if (stateNew)
----------------
This comment is no longer quite correct; the "assume" part has already been done in assumeBoundDual.

================
Comment at: lib/StaticAnalyzer/Core/ExprEngine.cpp:1691
@@ +1690,3 @@
+      defaultIsFeasible = false;
+      break;
+    }
----------------
I don't think this `break` is correct. Cases are not guaranteed to be in order.

================
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:84-85
@@ -83,1 +83,4 @@
 
+  /// Create a new set with all ranges of this set and RS
+  /// Possible intersections are not checked here
+  RangeSet addRange(Factory &F, const RangeSet &RS) {
----------------
Nitpick: please include periods ('.') in your doc comments.

================
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:88-89
@@ +87,4 @@
+    PrimRangeSet Ranges(RS.ranges);
+    for (iterator I = begin(), E = end(); I != E; I++)
+      Ranges = F.add(Ranges, *I);
+    return RangeSet(Ranges);
----------------
You might as well use a C++11 for-each loop here.

================
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:324-327
@@ -314,1 +323,6 @@
 
+  ProgramStateRef assumeSymInBound(ProgramStateRef state, SymbolRef sym,
+                                   const llvm::APSInt& From,
+                                   const llvm::APSInt& To,
+                                   const llvm::APSInt& Adjustment) override;
+
----------------
Please follow the LLVM naming conventions (capital letters, here and elsewhere) and put the `&` next to the variable name.

================
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:604-605
@@ +603,4 @@
+                                            const llvm::APSInt& Adjustment) {
+  ProgramStateRef St1 = assumeSymLT(state, sym, From, Adjustment);
+  ProgramStateRef St2 = assumeSymGT(state, sym, To, Adjustment);
+  RangeSet Range1 = St1 ? GetRange(St1, sym) : F.getEmptySet();
----------------
These are expensive operations. Is it possible to do this at a lower level? Or are there good reasons to do this extra work?

One reason I'm not so happy with this is that some day we could have constraints on one symbol affect another symbol, but this doesn't preserve that. Then again, neither would a lower-level solution.

http://reviews.llvm.org/D5102