[analyzer][Bugfix/improvement] Fix for PR16833

[a.sidorin]

Summary

Create one state for a range switch case instead of multiple.
This is an attempt to fix PR16833 (http://llvm.org/bugs/show_bug.cgi?id=16833).
Please tell me if I'm going in the right direction.

[a.sidorin]

Remove debug output; fix handling of Unknown values.

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

lib/StaticAnalyzer/Core/ExprEngine.cpp

1675–1691

Please follow the LLVM naming conventions (http://llvm.org/docs/CodingStandards.html#name-types-functions-variables-and-enumerators-properly).

1681

This comment is no longer quite correct; the "assume" part has already been done in assumeBoundDual.

1691

I don't think this break is correct. Cases are not guaranteed to be in order.

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

84–85

Nitpick: please include periods ('.') in your doc comments.

88–89

You might as well use a C++11 for-each loop here.

324–327

Please follow the LLVM naming conventions (capital letters, here and elsewhere) and put the & next to the variable name.

604–605

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.

[a.sidorin]

Thank you Jordan. I have fixed some issues (will post later) but I left some questions in replies.

[a.sidorin]

lib/StaticAnalyzer/Core/ExprEngine.cpp

1691

Does the order really affect this code? The fact that DefaultSt is null means that all possible cases for switch were already covered (range-by-range), there is nothing left to consider and we can break out of loop. Or am I missed something?

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

604–605

Jordan, could you explain what do you mean here?
If you mean removing of creation of new states (creating ranges only), that could be done easily.
But it seems that you mean something else that I cannot understand correctly.
BTW, does the code in previous function need correction too?

[a.sidorin]

Some review issues were fixed.

[jordan_rose]

lib/StaticAnalyzer/Core/ExprEngine.cpp

1691

Hm, that's true—that means a case matched definitively. Okay, I stand corrected.

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

604–605

The creation of new states is the expensive part. I'm kind of okay with the previous function doing it because it keeps things simple, it does exactly what it's specified to do, and it only has one intermediate state. (But yes, avoiding that would be nice if it can still be done tidily.)

For the second, I guess I was concerned about a hypothetical constraint manager that can handle things like this:

Given: ($x * 2) < 20 - we do handle this today, opaquely
Assume: $x outside of (0, 10)
Then: ($x * 2) < 0

Exactly what $x is is still not known because the analyzer operates under -fwrapv semantics. But we could make the above assumption about ($x * 2).

That said, we don't do anything like that today, and this is within RangeConstraintManager, not a general-purpose implementation in ConstraintManager or SimpleConstraintManager. So maybe this is all right, though I still think it would be a good idea to do it at the RangeSet level rather than the ProgramState level.

[a.sidorin]

Remove creation of new states; add two more tests.

[jordan_rose]

Oh, that's a nice way to refactor RangeConstraintManager::assumeSymLT. Now I'm wondering if it makes sense to do the same for RangeConstraintManager::assumeSymInBound. What do you think?

I discussed this offline with Anna and Ted and one other thing that came up was that this is very specifically operating on inclusive bounds. Now, the feature is motivated by the GNU switch extension, so it makes sense to do that, but then it also makes sense to make sure that's very clear for anyone who might want to use the same interface for something else in the future. How about naming it as such?

ProgramState::assumeWithinInclusiveRange
SimpleConstraintManager::assumeSymbolWithinInclusiveRange
RangeConstraintManager::assumeSymbolOutOfInclusiveRange

etc.

[a.sidorin]

Thank you Jordan. I have refactored assumeSymInBound. Does it look better?

[a.sidorin]

Give new functions more informative names; add entry in ProgramState.

[jordan_rose]

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

610–614

Unfortunately this logic isn't correct—assumeSymGE does a lot more than this to account for From and To being the min or max values of the symbol type, or completely outside the range of the symbol. I'd be more comfortable with factoring out assumeSymGE into getSymGERange, like you did with assumeSymGT. Or just going back to the simple form from before.

lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

215–220

I believe this ignores the case where the bounds have a different type, and APSInt will assert. I don't know if this can happen in the analyzer, but if you don't want to worry about it for now it at least deserves a comment and possibly an explicit assertion.

[a.sidorin]

Add an assertion; an another attempt to refactor RangeConstraintManager::assumeSymbolWithinInclusiveRange.

[a.sidorin]

Constantify a function parameter.

[a.sidorin]

Ping?

[a.sidorin]

Ping

[a.sidorin]

Gentle ping.

[jordan_rose]

I guess the regular pings didn't work, so it was worth trying the gentle one? Sorry!

This seems mostly ready to me, but I still have a few comments.

lib/StaticAnalyzer/Core/ExprEngine.cpp

1646–1650

What's the purpose of this? As I understand it, a switch condition value will never be reused in later states, so there's no point in adding constraints to it unless it's already symbolic.

(And not bothering to do this would remove the need to pass the NodeBuilderContext through.)

lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

199–200

Will this ever return a null symbol? Maybe add an assertion?

215–220

This is still relevant.

test/Analysis/switch-case.c

1

All tests should include the "core" checkers. At some point we'll probably make that implicit, but for now please add that to the -analyzer-checker list.

24–25

Can you include at least one more check here: clang_analyzer_eval(t > 2)? (Which should be unknown.)

122

Typo: "Brach"

[a.sidorin]

Thank you for reply, Jordan.

I guess the regular pings didn't work, so it was worth trying the gentle one? Sorry!

And it worked :)

I'll fix the issues you pointed.

[a.sidorin]

lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

215–220

Both types are equal for CaseStmt. But I'll check this code anyway because I found an interesting issue in CFG for SwitchStmt and I'm still investigating it.

[a.sidorin]

• Fix review notes
• Add some more tests
• Add a fix and a test for incorrect pruning of trivially unreachable case statements in CFG for SwitchStmt (accidentially found while writing a test).

[a.sidorin]

Remove duplicating assertion.

[jordan_rose]

Thanks for all the changes. This looks good to me! (And good catch for the constant expression case.)

[ygribov]

Folks, could someone commit this for us?

[dcoughlin]

I will commit. Thanks!

include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

     return ProgramStatePair(StTrue, StFalse);
   }
 
+  virtual ProgramStateRef assumeWithinInclusiveRange(ProgramStateRef State,
+                                                     NonLoc Value,
+                                                     const llvm::APSInt &From,
+                                                     const llvm::APSInt &To,
+                                                     bool InBound) = 0;
+
+  virtual ProgramStatePair assumeWithinInclusiveRangeDual(
+      ProgramStateRef State, NonLoc Value, const llvm::APSInt &From,
+      const llvm::APSInt &To) {
+    ProgramStateRef StInRange = assumeWithinInclusiveRange(State, Value, From,
+                                                           To, true);
+
+    // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
+    // because the existing constraints already establish this.
+    if (!StInRange)
+      return ProgramStatePair((ProgramStateRef)nullptr, State);
+
+    ProgramStateRef StOutOfRange = assumeWithinInclusiveRange(State, Value,
+                                                              From, To, false);
+    if (!StOutOfRange) {
+      // We are careful to return the original state, /not/ StTrue,
+      // because we want to avoid having callers generate a new node
+      // in the ExplodedGraph.
+      return ProgramStatePair(State, (ProgramStateRef)nullptr);
+    }
+
+    return ProgramStatePair(StInRange, StOutOfRange);
+  }
+
   /// \brief If a symbol is perfectly constrained to a constant, attempt
   /// to return the concrete value.
   ///

include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h

 namespace ento {
 
 class NodeBuilder;
+struct NodeBuilderContext;
 
 //===----------------------------------------------------------------------===//
 /// CoreEngine - Implements the core logic of the graph-reachability

 
   void HandleBlockEdge(const BlockEdge &E, ExplodedNode *Pred);
   void HandleBlockEntrance(const BlockEntrance &E, ExplodedNode *Pred);
-  void HandleBlockExit(const CFGBlock *B, ExplodedNode *Pred);
+  void HandleBlockExit(const CFGBlock *B, ExplodedNode *Pred,
+                       NodeBuilderContext *Ctx);
   void HandlePostStmt(const CFGBlock *B, unsigned StmtIdx, ExplodedNode *Pred);
 
   void HandleBranch(const Stmt *Cond, const Stmt *Term, const CFGBlock *B,

   const CFGBlock *Src;
   const Expr *Condition;
   ExplodedNode *Pred;
+  NodeBuilderContext *Ctx;
 
 public:
   SwitchNodeBuilder(ExplodedNode *pred, const CFGBlock *src,
-                    const Expr *condition, CoreEngine* eng)
-  : Eng(*eng), Src(src), Condition(condition), Pred(pred) {}
+                    const Expr *condition, CoreEngine* eng,
+                    NodeBuilderContext *C)
+  : Eng(*eng), Src(src), Condition(condition), Pred(pred), Ctx(C) {}
 
   class iterator {
     CFGBlock::const_succ_reverse_iterator I;

   const LocationContext *getLocationContext() const {
     return Pred->getLocationContext();
   }
+
+  const NodeBuilderContext *getBuilderContext() { return Ctx; }
 };
 
 } // end ento namespace

include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h

                                DefinedOrUnknownSVal upperBound,
                                bool assumption,
                                QualType IndexType = QualType()) const;
+
+  /// Assumes that the value of \p Val is bounded with [\p From; \p To]
+  /// (if \p assumption is "true") or it is fully out of this range
+  /// (if \p assumption is "false").
+  ///
+  /// This returns a new state with the added constraint on \p cond.
+  /// If no new state is feasible, NULL is returned.
+  ProgramStateRef assumeWithinInclusiveRange(DefinedOrUnknownSVal Val,
+                                             const llvm::APSInt &From,
+                                             const llvm::APSInt &To,
+                                             bool assumption) const;
+
+  /// Assumes given range both "true" and "false" for \p Val, and returns both
+  /// corresponding states (respectively).
+  ///
+  /// This is more efficient than calling assume() twice. Note that one (but not
+  /// both) of the returned states may be NULL.
+  std::pair<ProgramStateRef, ProgramStateRef>
+  assumeWithinInclusiveRange(DefinedOrUnknownSVal Val, const llvm::APSInt &From,
+                             const llvm::APSInt &To) const;
+
   
   /// \brief Check if the given SVal is constrained to zero or is a zero
   ///        constant.

       ->assumeDual(this, Cond.castAs<DefinedSVal>());
 }
 
+inline ProgramStateRef
+ProgramState::assumeWithinInclusiveRange(DefinedOrUnknownSVal Val,
+                                         const llvm::APSInt &From,
+                                         const llvm::APSInt &To,
+                                         bool Assumption) const {
+  if (Val.isUnknown())
+    return this;
+
+  assert(Val.getAs<NonLoc>() && "Only NonLocs are supported!");
+
+  return getStateManager().ConstraintMgr->assumeWithinInclusiveRange(
+        this, Val.castAs<NonLoc>(), From, To, Assumption);
+}
+
+inline std::pair<ProgramStateRef, ProgramStateRef>
+ProgramState::assumeWithinInclusiveRange(DefinedOrUnknownSVal Val,
+                                         const llvm::APSInt &From,
+                                         const llvm::APSInt &To) const {
+  if (Val.isUnknown())
+    return std::make_pair(this, this);
+
+  assert(Val.getAs<NonLoc>() && "Only NonLocs are supported!");
+
+  return getStateManager().ConstraintMgr
+      ->assumeWithinInclusiveRangeDual(this, Val.castAs<NonLoc>(), From, To);
+}
+
 inline ProgramStateRef ProgramState::bindLoc(SVal LV, SVal V) const {
   if (Optional<Loc> L = LV.getAs<Loc>())
     return bindLoc(*L, V);

lib/StaticAnalyzer/Core/CoreEngine.cpp

   WList->setBlockCounter(Counter);
 
   // Process the entrance of the block.
-  if (Optional<CFGElement> E = L.getFirstElement()) {
-    NodeBuilderContext Ctx(*this, L.getBlock(), Pred);
+  NodeBuilderContext Ctx(*this, L.getBlock(), Pred);
+  if (Optional<CFGElement> E = L.getFirstElement())
     SubEng.processCFGElement(*E, Pred, 0, &Ctx);
-  }
   else
-    HandleBlockExit(L.getBlock(), Pred);
+    HandleBlockExit(L.getBlock(), Pred, &Ctx);
 }
 
-void CoreEngine::HandleBlockExit(const CFGBlock * B, ExplodedNode *Pred) {
+void CoreEngine::HandleBlockExit(const CFGBlock * B, ExplodedNode *Pred,
+                                 NodeBuilderContext *Ctx) {
 
   if (const Stmt *Term = B->getTerminator()) {
     switch (Term->getStmtClass()) {

 
       case Stmt::SwitchStmtClass: {
         SwitchNodeBuilder builder(Pred, B, cast<SwitchStmt>(Term)->getCond(),
-                                    this);
+                                  this, Ctx);
 
         SubEng.processSwitch(builder);
         return;

   assert(B);
   assert(!B->empty());
 
+  NodeBuilderContext Ctx(*this, B, Pred);
   if (StmtIdx == B->size())
-    HandleBlockExit(B, Pred);
-  else {
-    NodeBuilderContext Ctx(*this, B, Pred);
+    HandleBlockExit(B, Pred, &Ctx);
+  else
     SubEng.processCFGElement((*B)[StmtIdx], Pred, StmtIdx, &Ctx);
-  }
 }
 
 /// generateNode - Utility method to generate nodes, hook up successors,

lib/StaticAnalyzer/Core/ExprEngine.cpp

 void ExprEngine::processSwitch(SwitchNodeBuilder& builder) {
   typedef SwitchNodeBuilder::iterator iterator;
   ProgramStateRef state = builder.getState();
+  const LocationContext *LCtx = builder.getLocationContext();
   const Expr *CondE = builder.getCondition();
-  SVal  CondV_untested = state->getSVal(CondE, builder.getLocationContext());
+  SVal  CondV_untested = state->getSVal(CondE, LCtx);
 
   if (CondV_untested.isUndef()) {
     //ExplodedNode* N = builder.generateDefaultCaseNode(state, true);

     return;
   }
   DefinedOrUnknownSVal CondV = CondV_untested.castAs<DefinedOrUnknownSVal>();
+  if (CondV.isUnknown()) {
+    CondV = state->getStateManager().getSValBuilder().conjureSymbolVal(nullptr,
+          CondE, LCtx, builder.getBuilderContext()->blockCount());
+    state = state->BindExpr(CondE, LCtx, CondV);
+  }
 
   ProgramStateRef DefaultSt = state;
   

     else
       V2 = V1;
 
-    // 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 StateCase;
+    assert(CondV.getAs<NonLoc>());
+    NonLoc NL = CondV.castAs<NonLoc>();
+    std::tie(StateCase, DefaultSt) =
+        DefaultSt->assumeWithinInclusiveRange(NL, V1, V2);
+
+    if (StateCase)
+      builder.generateCaseStmtNode(I, StateCase);
+
+    // Now "assume" that the case doesn't match.  Add this state
+    // to the default state (if it is feasible).
+    if (DefaultSt)
+      defaultIsFeasible = true;
+    else {
+      defaultIsFeasible = false;
+      break;
+    }
   }
 
   if (!defaultIsFeasible)

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 
   RangeSet(PrimRangeSet RS) : ranges(RS) {}
 
+  /// 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) {
+    PrimRangeSet Ranges(RS.ranges);
+    for (auto range : ranges)
+      Ranges = F.add(Ranges, range);
+    return RangeSet(Ranges);
+  }
+
   iterator begin() const { return ranges.begin(); }
   iterator end() const { return ranges.end(); }
 

                              const llvm::APSInt& Int,
                              const llvm::APSInt& Adjustment) override;
 
+  ProgramStateRef assumeSymbolWithinInclusiveRange(
+        ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+        const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+
+  ProgramStateRef assumeSymbolOutOfInclusiveRange(
+        ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+        const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+
   const llvm::APSInt* getSymVal(ProgramStateRef St,
                                 SymbolRef sym) const override;
   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;

 
 private:
   RangeSet::Factory F;
+  RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
+                         const llvm::APSInt &Int,
+                         const llvm::APSInt &Adjustment);
+  RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym,
+                         const llvm::APSInt &Int,
+                         const llvm::APSInt &Adjustment);
+  RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym,
+                         const llvm::APSInt &Int,
+                         const llvm::APSInt &Adjustment);
+  RangeSet getSymLERange(const RangeSet &RS, const llvm::APSInt &Int,
+                         const llvm::APSInt &Adjustment);
+  RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym,
+                         const llvm::APSInt &Int,
+                         const llvm::APSInt &Adjustment);
 };
 
 } // end anonymous namespace

 
 /// Scan all symbols referenced by the constraints. If the symbol is not alive
 /// as marked in LSymbols, mark it as dead in DSymbols.
-ProgramStateRef 
+ProgramStateRef
 RangeConstraintManager::removeDeadBindings(ProgramStateRef state,
                                            SymbolReaper& SymReaper) {
 

 // As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
 // UINT_MAX, 0, 1, and 2.
 
-ProgramStateRef 
+ProgramStateRef
 RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {

   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
-ProgramStateRef 
+ProgramStateRef
 RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {

   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
-ProgramStateRef 
-RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
+RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St,
+                                               SymbolRef Sym,
                                                const llvm::APSInt &Int,
                                                const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
-    return nullptr;
+    return F.getEmptySet();
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
-    return St;
+    return GetRange(St, Sym);
   }
 
   // Special case for Int == Min. This is always false.
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Min = AdjustmentType.getMinValue();
   if (ComparisonVal == Min)
-    return nullptr;
+    return F.getEmptySet();
 
-  llvm::APSInt Lower = Min-Adjustment;
-  llvm::APSInt Upper = ComparisonVal-Adjustment;
+  llvm::APSInt Lower = Min - Adjustment;
+  llvm::APSInt Upper = ComparisonVal - Adjustment;
   --Upper;
 
-  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
-  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
-ProgramStateRef 
-RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
+ProgramStateRef
+RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
+  RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
+  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+}
+
+RangeSet
+RangeConstraintManager::getSymGTRange(ProgramStateRef St, SymbolRef Sym,
+                                      const llvm::APSInt &Int,
+                                      const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
-    return St;
+    return GetRange(St, Sym);
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
-    return nullptr;
+    return F.getEmptySet();
   }
 
   // Special case for Int == Max. This is always false.
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Max = AdjustmentType.getMaxValue();
   if (ComparisonVal == Max)
-    return nullptr;
+    return F.getEmptySet();
 
-  llvm::APSInt Lower = ComparisonVal-Adjustment;
-  llvm::APSInt Upper = Max-Adjustment;
+  llvm::APSInt Lower = ComparisonVal - Adjustment;
+  llvm::APSInt Upper = Max - Adjustment;
   ++Lower;
 
-  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
-  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
-ProgramStateRef 
-RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
+ProgramStateRef
+RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
+  RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
+  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+}
+
+RangeSet
+RangeConstraintManager::getSymGERange(ProgramStateRef St, SymbolRef Sym,
+                                      const llvm::APSInt &Int,
+                                      const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
-    return St;
+    return GetRange(St, Sym);
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
-    return nullptr;
+    return F.getEmptySet();
   }
 
   // Special case for Int == Min. This is always feasible.
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Min = AdjustmentType.getMinValue();
   if (ComparisonVal == Min)
-    return St;
+    return GetRange(St, Sym);
 
   llvm::APSInt Max = AdjustmentType.getMaxValue();
-  llvm::APSInt Lower = ComparisonVal-Adjustment;
-  llvm::APSInt Upper = Max-Adjustment;
+  llvm::APSInt Lower = ComparisonVal - Adjustment;
+  llvm::APSInt Upper = Max - Adjustment;
 
-  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
-  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
-ProgramStateRef 
-RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
+ProgramStateRef
+RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
+  RangeSet New = getSymGERange(St, Sym, Int, Adjustment);
+  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
+}
+
+RangeSet
+RangeConstraintManager::getSymLERange(const RangeSet &RS,
+                                      const llvm::APSInt &Int,
+                                      const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
-    return nullptr;
+    return F.getEmptySet();
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
-    return St;
+    return RS;
   }
 
   // Special case for Int == Max. This is always feasible.
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Max = AdjustmentType.getMaxValue();
   if (ComparisonVal == Max)
-    return St;
+    return RS;
+
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  llvm::APSInt Lower = Min - Adjustment;
+  llvm::APSInt Upper = ComparisonVal - Adjustment;
+
+  return RS.Intersect(getBasicVals(), F, Lower, Upper);
+}
+
+RangeSet
+RangeConstraintManager::getSymLERange(ProgramStateRef St, SymbolRef Sym,
+                                      const llvm::APSInt &Int,
+                                      const llvm::APSInt &Adjustment) {
+  // Before we do any real work, see if the value can even show up.
+  APSIntType AdjustmentType(Adjustment);
+  switch (AdjustmentType.testInRange(Int, true)) {
+  case APSIntType::RTR_Below:
+    return F.getEmptySet();
+  case APSIntType::RTR_Within:
+    break;
+  case APSIntType::RTR_Above:
+    return GetRange(St, Sym);
+  }
+
+  // Special case for Int == Max. This is always feasible.
+  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (ComparisonVal == Max)
+    return GetRange(St, Sym);
 
   llvm::APSInt Min = AdjustmentType.getMinValue();
-  llvm::APSInt Lower = Min-Adjustment;
-  llvm::APSInt Upper = ComparisonVal-Adjustment;
+  llvm::APSInt Lower = Min - Adjustment;
+  llvm::APSInt Upper = ComparisonVal - Adjustment;
+
+  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+}
 
-  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+ProgramStateRef
+RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
+                                    const llvm::APSInt &Int,
+                                    const llvm::APSInt &Adjustment) {
+  RangeSet New = getSymLERange(St, Sym, Int, Adjustment);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
+ProgramStateRef
+RangeConstraintManager::assumeSymbolWithinInclusiveRange(
+    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+    const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
+  RangeSet New = getSymGERange(State, Sym, From, Adjustment);
+  if (New.isEmpty())
+    return nullptr;
+  New = getSymLERange(New, To, Adjustment);
+  return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
+}
+
+ProgramStateRef
+RangeConstraintManager::assumeSymbolOutOfInclusiveRange(
+    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+    const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
+  RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
+  RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment);
+  RangeSet New(RangeLT.addRange(F, RangeGT));
+  return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
+}
+
 //===------------------------------------------------------------------------===
 // Pretty-printing.
 //===------------------------------------------------------------------------===/

lib/StaticAnalyzer/Core/SimpleConstraintManager.h

 
   ProgramStateRef assume(ProgramStateRef state, NonLoc Cond, bool Assumption);
 
+  ProgramStateRef assumeWithinInclusiveRange(ProgramStateRef State,
+                                             NonLoc Value,
+                                             const llvm::APSInt &From,
+                                             const llvm::APSInt &To,
+                                             bool InRange) override;
+
   ProgramStateRef assumeSymRel(ProgramStateRef state,
                               const SymExpr *LHS,
                               BinaryOperator::Opcode op,
                               const llvm::APSInt& Int);
 
+  ProgramStateRef assumeSymWithinInclusiveRange(ProgramStateRef State,
+                                                SymbolRef Sym,
+                                                const llvm::APSInt &From,
+                                                const llvm::APSInt &To,
+                                                bool InRange);
+
+
 protected:
 
   //===------------------------------------------------------------------===//

                                      const llvm::APSInt& V,
                                      const llvm::APSInt& Adjustment) = 0;
 
+
+  virtual ProgramStateRef assumeSymbolWithinInclusiveRange(
+      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymbolOutOfInclusiveRange(
+      ProgramStateRef state, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//

lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

   } // end switch
 }
 
+ProgramStateRef SimpleConstraintManager::assumeWithinInclusiveRange(
+    ProgramStateRef State, NonLoc Value, const llvm::APSInt &From,
+    const llvm::APSInt &To, bool InRange) {
+
+  if (!canReasonAbout(Value)) {
+    // Just add the constraint to the expression without trying to simplify.
+    SymbolRef Sym = Value.getAsSymExpr();
+    return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange);
+  }
+
+  assert(From.isUnsigned() == To.isUnsigned() &&
+         "Types of bounds should match!");
+
+  switch (Value.getSubKind()) {
+  default:
+    llvm_unreachable("'assumeWithinInclusiveRange' is not implemented"
+                     "for this NonLoc");
+
+  case nonloc::LocAsIntegerKind:
+  case nonloc::SymbolValKind: {
+    if (SymbolRef Sym = Value.getAsSymbol())
+      return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange);
+    return State;
+  } // end switch
+
+  case nonloc::ConcreteIntKind: {
+    const llvm::APSInt &IntVal = Value.castAs<nonloc::ConcreteInt>().getValue();
+    bool IsInRange = IntVal >= From && IntVal <= To;
+    bool isFeasible = (IsInRange == InRange);
+    return isFeasible ? State : nullptr;
+  }
+  } // end switch
+}
+
 static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
   // Is it a "($sym+constant1)" expression?
   if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {

   } // end switch
 }
 
+ProgramStateRef
+SimpleConstraintManager::assumeSymWithinInclusiveRange(ProgramStateRef State,
+                                                       SymbolRef Sym,
+                                                       const llvm::APSInt &From,
+                                                       const llvm::APSInt &To,
+                                                       bool InRange) {
+  // Get the type used for calculating wraparound.
+  BasicValueFactory &BVF = getBasicVals();
+  APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
+
+  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
+  SymbolRef AdjustedSym = Sym;
+  computeAdjustment(AdjustedSym, Adjustment);
+
+  // Convert the right-hand side integer as necessary.
+  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From));
+  llvm::APSInt ConvertedFrom = ComparisonType.convert(From);
+  llvm::APSInt ConvertedTo = ComparisonType.convert(To);
+
+  // Prefer unsigned comparisons.
+  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
+      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
+    Adjustment.setIsSigned(false);
+
+  if (InRange)
+    return assumeSymbolWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
+                                            ConvertedTo, Adjustment);
+  return assumeSymbolOutOfInclusiveRange(State, AdjustedSym, ConvertedFrom,
+                                         ConvertedTo, Adjustment);
+}
+
 } // end of namespace ento
 
 } // end of namespace clang

test/Analysis/switch-case.c

+// RUN: %clang_cc1 -analyze -analyzer-checker=debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+void clang_analyzer_warnIfReached();
+
+#define INT_MIN 0x80000000
+#define INT_MAX 0x7fffffff
+
+// PR16833: Analyzer consumes memory until killed by kernel OOM killer
+// while analyzing large case ranges.
+void PR16833(unsigned op) {
+  switch (op) {
+  case 0x02 << 26 ... 0x03 << 26: // Analyzer should not hang here.
+    return;
+  }
+}
+
+void testAdjustment(int t) {
+  switch (t + 1) {
+  case 2:
+    clang_analyzer_eval(t == 1); // expected-warning{{TRUE}}
+    break;
+  case 3 ... 10:
+    clang_analyzer_eval(t > 1);        // expected-warning{{TRUE}}
+    clang_analyzer_eval(t + 2 <= 11);  // expected-warning{{TRUE}}
+    clang_analyzer_eval(t + 1 == 3);   // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval(t + 1 == 10);  // expected-warning{{UNKNOWN}}
+    break;
+  default:
+    clang_analyzer_warnIfReached();    // expected-warning{{REACHABLE}}
+  }
+}
+
+void testUnknownVal(int value, int mask) {
+  // Once ConstraintManager will process '&' and this test will require some changes.
+  switch (value & mask) {
+    case 1:
+      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+      break;
+    case 3 ... 10:
+      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+      break;
+    default:
+      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  }
+}
+
+void testSwitchCond(int arg) {
+  if (arg > 10) {
+    switch (arg) {
+    case INT_MIN ... 10:
+      clang_analyzer_warnIfReached(); // no-warning
+      break;
+    case 11 ... 20:
+      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+      break;
+    default:
+      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+    }
+
+    switch (arg) {
+    case INT_MIN ... 9:
+      clang_analyzer_warnIfReached();  // no-warning
+      break;
+    case 10 ... 20:
+      clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+      clang_analyzer_eval(arg > 10);   // expected-warning{{TRUE}}
+      break;
+    default:
+      clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+    }
+  } // arg > 10
+}
+
+void testDefaultUnreachable(int arg) {
+  if (arg > 10) {
+    switch (arg) {
+    case INT_MIN ... 9:
+      clang_analyzer_warnIfReached();   // no-warning
+      break;
+    case 10 ... INT_MAX:
+      clang_analyzer_warnIfReached();   // expected-warning{{REACHABLE}}
+      clang_analyzer_eval(arg > 10);    // expected-warning{{TRUE}}
+      break;
+    default:
+      clang_analyzer_warnIfReached();   // no-warning
+    }
+  }
+}
+
+void testBranchReachability(int arg) {
+  if (arg > 10 && arg < 20) {
+    switch (arg) {
+    case INT_MIN ... 4:
+      clang_analyzer_warnIfReached(); // no-warning
+      break;
+    case 5 ... 9:
+      clang_analyzer_warnIfReached(); // no-warning
+      break;
+    case 10 ... 15:
+      clang_analyzer_warnIfReached();              // expected-warning{{REACHABLE}}
+      clang_analyzer_eval(arg > 10 && arg <= 15);  // expected-warning{{TRUE}}
+      break;
+    default:
+      clang_analyzer_warnIfReached(); // no-warning
+      break;
+    case 17 ... 25:
+      clang_analyzer_warnIfReached();              // expected-warning{{REACHABLE}}
+      clang_analyzer_eval(arg >= 17 && arg < 20);  // expected-warning{{TRUE}}
+      break;
+    case 26 ... INT_MAX:
+      clang_analyzer_warnIfReached();   // no-warning
+      break;
+    case 16:
+      clang_analyzer_warnIfReached();   // expected-warning{{REACHABLE}}
+      clang_analyzer_eval(arg == 16);   // expected-warning{{TRUE}}
+      break;
+    }
+  }
+}
+
+void testDefaultBrachRange(int arg) {
+  switch (arg) {
+  case INT_MIN ... 9:
+    clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+    break;
+  case 20 ... INT_MAX:
+    clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+    clang_analyzer_eval(arg >= 20);  // expected-warning{{TRUE}}
+    break;
+  default:
+    clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+    clang_analyzer_eval(arg == 16);  // expected-warning{{FALSE}}
+    clang_analyzer_eval(arg > 9);    // expected-warning{{TRUE}}
+    clang_analyzer_eval(arg <= 20);  // expected-warning{{TRUE}}
+
+  case 16:
+    clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  }
+}
+
+void testAllUnreachableButDefault(int arg) {
+  if (arg < 0) {
+    switch (arg) {
+    case 0 ... 9:
+      clang_analyzer_warnIfReached(); // no-warning
+      break;
+    case 20 ... INT_MAX:
+      clang_analyzer_warnIfReached(); // no-warning
+      break;
+    default:
+      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+      break;
+    case 16:
+      clang_analyzer_warnIfReached(); // no-warning
+    }
+    clang_analyzer_warnIfReached();   // expected-warning{{REACHABLE}}
+  }
+}
+
+void testAllUnreachable(int arg) {
+  if (arg < 0) {
+    switch (arg) {
+    case 0 ... 9:
+      clang_analyzer_warnIfReached(); // no-warning
+      break;
+    case 20 ... INT_MAX:
+      clang_analyzer_warnIfReached(); // no-warning
+      break;
+    case 16:
+      clang_analyzer_warnIfReached(); // no-warning
+    }
+    clang_analyzer_warnIfReached();   // expected-warning{{REACHABLE}}
+  }
+}