[analyzer] Refactor and simplify SimpleConstraintManager

[ddcc]

Summary

SimpleConstraintManager is difficult to use, and makes assumptions about capabilities of the constraint manager. This patch refactors out those portions into a new RangedConstraintManager, and also fixes some issues with camel case, formatting, and confusing naming.

[ddcc]

To summarize, here is a list of changes:

• General
  • Fixed some issues with formatting (clang-format)
  • Fixed inconsistent capitalization following camel case style guidelines

• ConstraintManager.h
  • Renamed assumeWithinInclusiveRange*() to assumeInclusiveRange*(), since the range is not necessarily contained within unless Assumption is true, to match assume()

• RangedConstraintManager.h (inherits SimpleConstraintManager)
  • Moved assumeSym* and canReasonAbout() from SimpleConstraintManager to here
  • Renamed assumeSymbolWithinInclusiveRange/assumeSymbolOutOfInclusiveRange to assumeSymWithinInclusiveRange/assumeSymOutsideInclusiveRange to match the above, and moved to here
  • This is now inherited by RangeConstraintManager, and essentially provides the current interface in SimpleConstraintManager

• SimpleConstraintManager.h (inherits ConstraintManager)
  • Implemented a new interface that internally converts the DefinedSVal in assume(...) from ConstraintManager.h to NonLoc to SymbolRef. Subclasses only need to override ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption)
  • For inclusive ranges, implemented a new interface that internally converts from NonLoc to SymbolRef. Subclasses only need to override ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
  • Implemented a new interface that internally handles expressions that fail canReasonAbout() by adding them directly to the constraint manager state. Subclasses only need to expose ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym, BinaryOperator::Opcode op, const llvm::APSInt &Int)

• RangeConstraintManager.cpp
  • Minor optimization to avoid updating the state if nothing is pruned in removeDeadBindings()

[dcoughlin]

Thanks for the patch!

Would it be possible to split this up into several patches? I think it is important to separate the interface layering changes from the formatting changes, renaming changes, and minor optimization changes. This will make the patches easier to review.

Also: is this motivated by a different implementation of range constraints? Is this something you plan on upstreaming?

In D26061#581778, @ddcc wrote:

To summarize, here is a list of changes:

• General
  • Fixed some issues with formatting (clang-format)
  • Fixed inconsistent capitalization following camel case style guidelines

• ConstraintManager.h
  • Renamed assumeWithinInclusiveRange*() to assumeInclusiveRange*(), since the range is not necessarily contained within unless Assumption is true, to match assume()

• RangedConstraintManager.h (inherits SimpleConstraintManager)
  • Moved assumeSym* and canReasonAbout() from SimpleConstraintManager to here
  • Renamed assumeSymbolWithinInclusiveRange/assumeSymbolOutOfInclusiveRange to assumeSymWithinInclusiveRange/assumeSymOutsideInclusiveRange to match the above, and moved to here
  • This is now inherited by RangeConstraintManager, and essentially provides the current interface in SimpleConstraintManager

What do you view as the distinction between RangeConstraintMananger and RangedConstraintManager? In other words, if I'm a developer adding new functionality how would you suggest I decide which to add it to? It would be good to document this in the code! Also: the closeness in the names of these classes could be potentially confusing. Are there other, more distinctive, names that still communicate the difference you intend?

• SimpleConstraintManager.h (inherits ConstraintManager)
  • Implemented a new interface that internally converts the DefinedSVal in assume(...) from ConstraintManager.h to NonLoc to SymbolRef. Subclasses only need to override ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption)
  • For inclusive ranges, implemented a new interface that internally converts from NonLoc to SymbolRef. Subclasses only need to override ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
  • Implemented a new interface that internally handles expressions that fail canReasonAbout() by adding them directly to the constraint manager state. Subclasses only need to expose ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym, BinaryOperator::Opcode op, const llvm::APSInt &Int)

• RangeConstraintManager.cpp
  • Minor optimization to avoid updating the state if nothing is pruned in removeDeadBindings()

[ddcc]

Yes, I've been writing a Z3 solver interface, which motivated this patch. However, this patch has snowballed into something that it's a little too convoluted, so I'll split it up.

I'm not sure whether the RangedConstraintManager interface is useful or not; I preserved it because it's currently in the code, but since RangeConstraintManager is the only user, it is possible to merge the two together and eliminate the interface. In the past, BasicConstraintManager was the other class that used this interface, but that was deleted quite a while back, and I'm not sure if there are plans for anything else?

[ddcc]

Rebase on recent changes

[ddcc]

Rebase, move assumeSymRel() to RangedConstraintManager, make assumeSymUnsupported pure virtual in SimpleConstraintManager.

[ddcc]

How does this look now?

[ddcc]

Rebase

[ddcc]

Rebase, incorporate D22862

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

 
 namespace clang {
 namespace ento {
 
 class SubEngine;
 
 class ConditionTruthVal {
   Optional<bool> Val;
+
 public:
   /// Construct a ConditionTruthVal indicating the constraint is constrained
   /// to either true or false, depending on the boolean value provided.
   ConditionTruthVal(bool constraint) : Val(constraint) {}
 
   /// Construct a ConstraintVal indicating the constraint is underconstrained.
   ConditionTruthVal() {}
-  
   /// Return true if the constraint is perfectly constrained to 'true'.
-  bool isConstrainedTrue() const {
-    return Val.hasValue() && Val.getValue();
-  }
+  bool isConstrainedTrue() const { return Val.hasValue() && Val.getValue(); }
 
   /// Return true if the constraint is perfectly constrained to 'false'.
-  bool isConstrainedFalse() const {
-    return Val.hasValue() && !Val.getValue();
-  }
+  bool isConstrainedFalse() const { return Val.hasValue() && !Val.getValue(); }
 
   /// Return true if the constrained is perfectly constrained.
-  bool isConstrained() const {
-    return Val.hasValue();
-  }
+  bool isConstrained() const { return Val.hasValue(); }
 
   /// Return true if the constrained is underconstrained and we do not know
   /// if the constraint is true of value.
-  bool isUnderconstrained() const {
-    return !Val.hasValue();
-  }
+  bool isUnderconstrained() const { return !Val.hasValue(); }
 };
-  
 class ConstraintManager {
 public:
   ConstraintManager() : NotifyAssumeClients(true) {}
-  
   virtual ~ConstraintManager();
-  virtual ProgramStateRef assume(ProgramStateRef state,
-                                 DefinedSVal Cond,
-                                 bool Assumption) = 0;
 
   typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair;
 
+  virtual ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond,
+                                 bool Assumption) = 0;
+
   /// Returns a pair of states (StTrue, StFalse) where the given condition is
   /// assumed to be true or false, respectively.
   ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) {
     ProgramStateRef StTrue = assume(State, Cond, true);
 
     // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
     // because the existing constraints already establish this.
     if (!StTrue) {
 #ifndef __OPTIMIZE__
       // This check is expensive and should be disabled even in Release+Asserts
       // builds.
       // FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC
       // does not. Is there a good equivalent there?
       assert(assume(State, Cond, false) && "System is over constrained.");
 #endif
-      return ProgramStatePair((ProgramStateRef)nullptr, State);
+      return ProgramStatePair((ProgramStateRef) nullptr, State);
     }
 
     ProgramStateRef StFalse = assume(State, Cond, false);
     if (!StFalse) {
       // 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(State, (ProgramStateRef) nullptr);
     }
 
     return ProgramStatePair(StTrue, StFalse);
   }
 
-  virtual ProgramStateRef assumeWithinInclusiveRange(ProgramStateRef State,
-                                                     NonLoc Value,
-                                                     const llvm::APSInt &From,
-                                                     const llvm::APSInt &To,
-                                                     bool InBound) = 0;
+  virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
 
-  virtual ProgramStatePair assumeWithinInclusiveRangeDual(
-      ProgramStateRef State, NonLoc Value, const llvm::APSInt &From,
+  virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State,
+                                                    NonLoc Value,
+                                                    const llvm::APSInt &From,
                                                     const llvm::APSInt &To) {
-    ProgramStateRef StInRange = assumeWithinInclusiveRange(State, Value, From,
-                                                           To, true);
+    ProgramStateRef StInRange =
+        assumeInclusiveRange(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);
+      return ProgramStatePair((ProgramStateRef) nullptr, State);
 
-    ProgramStateRef StOutOfRange = assumeWithinInclusiveRange(State, Value,
-                                                              From, To, false);
+    ProgramStateRef StOutOfRange =
+        assumeInclusiveRange(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(State, (ProgramStateRef) nullptr);
     }
 
     return ProgramStatePair(StInRange, StOutOfRange);
   }
 
   /// \brief If a symbol is perfectly constrained to a constant, attempt
   /// to return the concrete value.
   ///
   /// Note that a ConstraintManager is not obligated to return a concretized
   /// value for a symbol, even if it is perfectly constrained.
-  virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
-                                        SymbolRef sym) const {
+  virtual const llvm::APSInt *getSymVal(ProgramStateRef State,
+                                        SymbolRef Sym) const {
     return nullptr;
   }
 
+  /// Scan all symbols referenced by the constraints. If the symbol is not
+  /// alive, remove it.
   virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
-                                                 SymbolReaper& SymReaper) = 0;
+                                             SymbolReaper &SymReaper) = 0;
 
-  virtual void print(ProgramStateRef state,
-                     raw_ostream &Out,
-                     const char* nl,
+  virtual void print(ProgramStateRef state, raw_ostream &Out, const char *nl,
                      const char *sep) = 0;
 
   virtual void EndPath(ProgramStateRef state) {}
-  
   /// Convenience method to query the state to see if a symbol is null or
   /// not null, or if neither assumption can be made.
   ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
     SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
 
     return checkNull(State, Sym);
   }
 
protected:
   /// canReasonAbout - Not all ConstraintManagers can accurately reason about
   ///  all SVal values.  This method returns true if the ConstraintManager can
   ///  reasonably handle a given SVal value.  This is typically queried by
   ///  ExprEngine to determine if the value should be replaced with a
   ///  conjured symbolic value in order to recover some precision.
   virtual bool canReasonAbout(SVal X) const = 0;
 
   /// Returns whether or not a symbol is known to be null ("true"), known to be
-  /// non-null ("false"), or may be either ("underconstrained"). 
+  /// non-null ("false"), or may be either ("underconstrained").
   virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
 };
 
 std::unique_ptr<ConstraintManager>
 CreateRangeConstraintManager(ProgramStateManager &statemgr,
                              SubEngine *subengine);
 
 } // end GR namespace
 
 } // end clang namespace
 
 #endif

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

ProgramStateRef assumeInBound(DefinedOrUnknownSVal idx,
                                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;
+  ProgramStateRef assumeInclusiveRange(DefinedOrUnknownSVal Val,
 
   /// 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;
+  assumeInclusiveRange(DefinedOrUnknownSVal Val, const llvm::APSInt &From,
 
   
   /// \brief Check if the given SVal is constrained to zero or is a zero
   ///        constant.
   ConditionTruthVal isNull(SVal V) const;
   
   /// Utility method for getting regions.
   const VarRegion* getRegion(const VarDecl *D, const LocationContext *LC) const;
ProgramState::assume(DefinedOrUnknownSVal Cond) const {
   if (Cond.isUnknown())
     return std::make_pair(this, this);
 
   return getStateManager().ConstraintMgr
       ->assumeDual(this, Cond.castAs<DefinedSVal>());
 }
 
 inline ProgramStateRef
-ProgramState::assumeWithinInclusiveRange(DefinedOrUnknownSVal Val,
-                                         const llvm::APSInt &From,
-                                         const llvm::APSInt &To,
-                                         bool Assumption) const {
+ProgramState::assumeInclusiveRange(DefinedOrUnknownSVal Val,
   if (Val.isUnknown())
     return this;
 
   assert(Val.getAs<NonLoc>() && "Only NonLocs are supported!");
 
-  return getStateManager().ConstraintMgr->assumeWithinInclusiveRange(
+  return getStateManager().ConstraintMgr->assumeInclusiveRange(
         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 {
+ProgramState::assumeInclusiveRange(DefinedOrUnknownSVal Val,
   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);
+      ->assumeInclusiveRangeDual(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);
   return this;
 }
 

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

+//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  Simplified constraint manager backend.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+
+namespace clang {
+
+namespace ento {
+
+class SimpleConstraintManager : public ConstraintManager {
+  SubEngine *SU;
+  SValBuilder &SVB;
+
+public:
+  SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
+      : SU(subengine), SVB(SB) {}
+
+  ~SimpleConstraintManager() override;
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from ConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  /// Ensures that the DefinedSVal conditional is expressed as a NonLoc by
+  /// creating boolean casts to handle Loc's.
+  ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond,
+                         bool Assumption) override;
+
+  ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
+                                       const llvm::APSInt &From,
+                                       const llvm::APSInt &To,
+                                       bool InRange) override;
+
+protected:
+  /// Given a symbolic expression that cannot be reasoned about, assume that
+  /// it is zero/nonzero and add it directly to the solver state.
+  virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State,
+                                               SymbolRef Sym, bool Assumption);
+
+  //===------------------------------------------------------------------===//
+  // Interface that subclasses must implement.
+  //===------------------------------------------------------------------===//
+
+  /// Given a symbolic expression that can be reasoned about, assume that it is
+  /// true/false and generate the new program state.
+  virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
+                                    bool Assumption) = 0;
+
+  /// Assume a constraint between a symbolic expression and a concrete integer.
+  /// Used to directly add unsupported constraints to the solver state.
+  virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
+                                       BinaryOperator::Opcode op,
+                                       const llvm::APSInt &Int) = 0;
+
+  /// Given a symbolic expression within the range [From, To], assume that it is
+  /// true/false and generate the new program state.
+  /// This function is used to handle case ranges produced by a language
+  /// extension
+  /// for switch case statements.
+  virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State,
+                                                  SymbolRef Sym,
+                                                  const llvm::APSInt &From,
+                                                  const llvm::APSInt &To,
+                                                  bool InRange) = 0;
+
+  //===------------------------------------------------------------------===//
+  // Internal implementation.
+  //===------------------------------------------------------------------===//
+
+  BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
+  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
+
+private:
+  ProgramStateRef assume(ProgramStateRef State, NonLoc Cond,
+                         bool Assumption);
+
+  ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
+                            bool Assumption);
+
+};
+
+} // end GR namespace
+
+} // end clang namespace
+
+#endif

lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

ProgramStateRef StdLibraryFunctionsChecker::ValueRange::applyAsOutOfRange(
 
   if (auto N = V.getAs<NonLoc>()) {
     const IntRangeVectorTy &R = getRanges();
     size_t E = R.size();
     for (size_t I = 0; I != E; ++I) {
       const llvm::APSInt &Min = BVF.getValue(R[I].first, T);
       const llvm::APSInt &Max = BVF.getValue(R[I].second, T);
       assert(Min <= Max);
-      State = CM.assumeWithinInclusiveRange(State, *N, Min, Max, false);
+      State = CM.assumeInclusiveRange(State, *N, Min, Max, false);
       if (!State)
         break;
     }
   }
 
   return State;
 }
 
if (auto N = V.getAs<NonLoc>()) {
     size_t E = R.size();
 
     const llvm::APSInt &MinusInf = BVF.getMinValue(T);
     const llvm::APSInt &PlusInf = BVF.getMaxValue(T);
 
     const llvm::APSInt &Left = BVF.getValue(R[0].first - 1ULL, T);
     if (Left != PlusInf) {
       assert(MinusInf <= Left);
-      State = CM.assumeWithinInclusiveRange(State, *N, MinusInf, Left, false);
+      State = CM.assumeInclusiveRange(State, *N, MinusInf, Left, false);
       if (!State)
         return nullptr;
     }
 
     const llvm::APSInt &Right = BVF.getValue(R[E - 1].second + 1ULL, T);
     if (Right != MinusInf) {
       assert(Right <= PlusInf);
-      State = CM.assumeWithinInclusiveRange(State, *N, Right, PlusInf, false);
+      State = CM.assumeInclusiveRange(State, *N, Right, PlusInf, false);
       if (!State)
         return nullptr;
     }
 
     for (size_t I = 1; I != E; ++I) {
       const llvm::APSInt &Min = BVF.getValue(R[I - 1].second + 1ULL, T);
       const llvm::APSInt &Max = BVF.getValue(R[I].first - 1ULL, T);
       assert(Min <= Max);
-      State = CM.assumeWithinInclusiveRange(State, *N, Min, Max, false);
+      State = CM.assumeInclusiveRange(State, *N, Min, Max, false);
       if (!State)
         return nullptr;
     }
   }
 
   return State;
 }
 

lib/StaticAnalyzer/Core/CMakeLists.txt

add_clang_library(clangStaticAnalyzerCore
   FunctionSummary.cpp
   HTMLDiagnostics.cpp
   LoopWidening.cpp
   MemRegion.cpp
   PathDiagnostic.cpp
   PlistDiagnostics.cpp
   ProgramState.cpp
   RangeConstraintManager.cpp
+  RangedConstraintManager.cpp
   RegionStore.cpp
   SValBuilder.cpp
   SVals.cpp
   SimpleConstraintManager.cpp
   SimpleSValBuilder.cpp
   Store.cpp
   SubEngine.cpp
   SymbolManager.cpp
 
   LINK_LIBS
   clangAST
   clangAnalysis
   clangBasic
   clangLex
   clangRewrite
   )

lib/StaticAnalyzer/Core/ConstraintManager.cpp

 
 using namespace clang;
 using namespace ento;
 
 ConstraintManager::~ConstraintManager() {}
 
 static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
                                     SymbolRef Sym) {
-  const MemRegion *R = State->getStateManager().getRegionManager()
-                                               .getSymbolicRegion(Sym);
+  const MemRegion *R =
+      State->getStateManager().getRegionManager().getSymbolicRegion(Sym);
   return loc::MemRegionVal(R);
 }
 
 ConditionTruthVal ConstraintManager::checkNull(ProgramStateRef State,
                                                SymbolRef Sym) {
   QualType Ty = Sym->getType();
   DefinedSVal V = Loc::isLocType(Ty) ? getLocFromSymbol(State, Sym)
                                      : nonloc::SymbolVal(Sym);
   const ProgramStatePair &P = assumeDual(State, V);
   if (P.first && !P.second)
     return ConditionTruthVal(false);
   if (!P.first && P.second)
     return ConditionTruthVal(true);
   return ConditionTruthVal();
 }

lib/StaticAnalyzer/Core/ExprEngine.cpp

for ( ; I != EI; ++I) {
     if (const Expr *E = Case->getRHS())
       V2 = E->EvaluateKnownConstInt(getContext());
     else
       V2 = V1;
 
     ProgramStateRef StateCase;
     if (Optional<NonLoc> NL = CondV.getAs<NonLoc>())
       std::tie(StateCase, DefaultSt) =
-          DefaultSt->assumeWithinInclusiveRange(*NL, V1, V2);
+          DefaultSt->assumeInclusiveRange(*NL, V1, V2);
     else // UnknownVal
       StateCase = DefaultSt;
 
     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).

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 //== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==//
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines RangeConstraintManager, a class that tracks simple
 //  equality and inequality constraints on symbolic values of ProgramState.
 //
 //===----------------------------------------------------------------------===//
 
-#include "SimpleConstraintManager.h"
+#include "RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/ImmutableSet.h"
 #include "llvm/Support/raw_ostream.h"
 
 using namespace clang;
 using namespace ento;
 
 /// A Range represents the closed range [from, to].  The caller must
 /// guarantee that from <= to.  Note that Range is immutable, so as not
 /// to subvert RangeSet's immutability.
 namespace {
-class Range : public std::pair<const llvm::APSInt*,
-                                                const llvm::APSInt*> {
+class Range : public std::pair<const llvm::APSInt *, const llvm::APSInt *> {
 public:
   Range(const llvm::APSInt &from, const llvm::APSInt &to)
-    : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) {
+      : std::pair<const llvm::APSInt *, const llvm::APSInt *>(&from, &to) {
     assert(from <= to);
   }
   bool Includes(const llvm::APSInt &v) const {
     return *first <= v && v <= *second;
   }
-  const llvm::APSInt &From() const {
-    return *first;
-  }
-  const llvm::APSInt &To() const {
-    return *second;
-  }
+  const llvm::APSInt &From() const { return *first; }
+  const llvm::APSInt &To() const { return *second; }
   const llvm::APSInt *getConcreteValue() const {
     return &From() == &To() ? &From() : nullptr;
   }
 
   void Profile(llvm::FoldingSetNodeID &ID) const {
     ID.AddPointer(&From());
     ID.AddPointer(&To());
   }
 };
 
-
 class RangeTrait : public llvm::ImutContainerInfo<Range> {
 public:
   // When comparing if one Range is less than another, we should compare
   // the actual APSInt values instead of their pointers.  This keeps the order
   // consistent (instead of comparing by pointer values) and can potentially
   // be used to speed up some of the operations in RangeSet.
   static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
-    return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) &&
-                                       *lhs.second < *rhs.second);
+    return *lhs.first < *rhs.first ||
+           (!(*rhs.first < *lhs.first) && *lhs.second < *rhs.second);
   }
 };
 
 /// RangeSet contains a set of ranges. If the set is empty, then
 ///  there the value of a symbol is overly constrained and there are no
 ///  possible values for that symbol.
 class RangeSet {
   typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
public:
 
   iterator begin() const { return ranges.begin(); }
   iterator end() const { return ranges.end(); }
 
   bool isEmpty() const { return ranges.isEmpty(); }
 
   /// Construct a new RangeSet representing '{ [from, to] }'.
   RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
       : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
 
   /// Profile - Generates a hash profile of this RangeSet for use
   ///  by FoldingSet.
   void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
 
   /// getConcreteValue - If a symbol is contrained to equal a specific integer
   ///  constant then this method returns that value.  Otherwise, it returns
   ///  NULL.
-  const llvm::APSInt* getConcreteValue() const {
+  const llvm::APSInt *getConcreteValue() const {
     return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
   }
 
 private:
   void IntersectInRange(BasicValueFactory &BV, Factory &F,
-                        const llvm::APSInt &Lower,
-                        const llvm::APSInt &Upper,
-                        PrimRangeSet &newRanges,
-                        PrimRangeSet::iterator &i,
+                        const llvm::APSInt &Lower, const llvm::APSInt &Upper,
+                        PrimRangeSet &newRanges, PrimRangeSet::iterator &i,
                         PrimRangeSet::iterator &e) const {
     // There are six cases for each range R in the set:
     //   1. R is entirely before the intersection range.
     //   2. R is entirely after the intersection range.
     //   3. R contains the entire intersection range.
     //   4. R starts before the intersection range and ends in the middle.
     //   5. R starts in the middle of the intersection range and ends after it.
     //   6. R is entirely contained in the intersection range.
     // These correspond to each of the conditions below.
     for (/* i = begin(), e = end() */; i != e; ++i) {
       if (i->To() < Lower) {
         continue;
       }
       if (i->From() > Upper) {
         break;
       }
 
       if (i->Includes(Lower)) {
         if (i->Includes(Upper)) {
-          newRanges = F.add(newRanges, Range(BV.getValue(Lower),
-                                             BV.getValue(Upper)));
+          newRanges =
+              F.add(newRanges, Range(BV.getValue(Lower), BV.getValue(Upper)));
           break;
         } else
           newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
       } else {
         if (i->Includes(Upper)) {
           newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
           break;
         } else

 public:
   // Returns a set containing the values in the receiving set, intersected with
   // the closed range [Lower, Upper]. Unlike the Range type, this range uses
   // modular arithmetic, corresponding to the common treatment of C integer
   // overflow. Thus, if the Lower bound is greater than the Upper bound, the
   // range is taken to wrap around. This is equivalent to taking the
   // intersection with the two ranges [Min, Upper] and [Lower, Max],
   // or, alternatively, /removing/ all integers between Upper and Lower.
-  RangeSet Intersect(BasicValueFactory &BV, Factory &F,
-                     llvm::APSInt Lower, llvm::APSInt Upper) const {
+  RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower,
+                     llvm::APSInt Upper) const {
     if (!pin(Lower, Upper))
       return F.getEmptySet();
 
     PrimRangeSet newRanges = F.getEmptySet();
 
     PrimRangeSet::iterator i = begin(), e = end();
     if (Lower <= Upper)
       IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);

 };
 } // end anonymous namespace
 
 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintRange,
                                  CLANG_ENTO_PROGRAMSTATE_MAP(SymbolRef,
                                                              RangeSet))
 
 namespace {
-class RangeConstraintManager : public SimpleConstraintManager{
-  RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
+class RangeConstraintManager : public RangedConstraintManager {
 public:
-  RangeConstraintManager(SubEngine *subengine, SValBuilder &SVB)
-    : SimpleConstraintManager(subengine, SVB) {}
+  RangeConstraintManager(SubEngine *SE, SValBuilder &SVB)
+      : RangedConstraintManager(SE, SVB) {}
 
-  ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from ConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  bool canReasonAbout(SVal X) const override;
+
+  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
+
+  const llvm::APSInt *getSymVal(ProgramStateRef State,
+                                SymbolRef Sym) const override;
+
+  ProgramStateRef removeDeadBindings(ProgramStateRef State,
+                                     SymbolReaper &SymReaper) override;
+
+  void print(ProgramStateRef State, raw_ostream &Out, const char *nl,
+             const char *sep) override;
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from RangedConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              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 assumeSymWithinInclusiveRange(
 
-  ProgramStateRef assumeSymbolOutOfInclusiveRange(
-        ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-        const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+  ProgramStateRef assumeSymOutsideInclusiveRange(
 
-  const llvm::APSInt* getSymVal(ProgramStateRef St,
-                                SymbolRef sym) const override;
-  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
-
-  ProgramStateRef removeDeadBindings(ProgramStateRef St,
-                                     SymbolReaper& SymReaper) override;
-
-  void print(ProgramStateRef St, raw_ostream &Out,
-             const char* nl, const char *sep) override;
-
 private:
   RangeSet::Factory F;
+
+  RangeSet getRange(ProgramStateRef state, SymbolRef sym);
+
   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
 
 std::unique_ptr<ConstraintManager>
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
   return llvm::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
 }
 
-const llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
-                                                      SymbolRef sym) const {
-  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
-  return T ? T->getConcreteValue() : nullptr;
+bool RangeConstraintManager::canReasonAbout(SVal X) const {
+  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
+  if (SymVal && SymVal->isExpression()) {
+    const SymExpr *SE = SymVal->getSymbol();
+
+    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
+      switch (SIE->getOpcode()) {
+      // We don't reason yet about bitwise-constraints on symbolic values.
+      case BO_And:
+      case BO_Or:
+      case BO_Xor:
+        return false;
+      // We don't reason yet about these arithmetic constraints on
+      // symbolic values.
+      case BO_Mul:
+      case BO_Div:
+      case BO_Rem:
+      case BO_Shl:
+      case BO_Shr:
+        return false;
+      // All other cases.
+      default:
+        return true;
+      }
+    }
+
+    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
+      if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
+        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
+        if (Loc::isLocType(SSE->getLHS()->getType())) {
+          assert(Loc::isLocType(SSE->getRHS()->getType()));
+          return true;
+        }
+      }
+    }
+
+    return false;
+  }
+
+  return true;
 }
 
 ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
                                                     SymbolRef Sym) {
   const RangeSet *Ranges = State->get<ConstraintRange>(Sym);
 
   // If we don't have any information about this symbol, it's underconstrained.
   if (!Ranges)
ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
   // Check if zero is in the set of possible values.
   if (Ranges->Intersect(BV, F, Zero, Zero).isEmpty())
     return false;
 
   // Zero is a possible value, but it is not the /only/ possible value.
   return ConditionTruthVal();
 }
 
+const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
+                                                      SymbolRef Sym) const {
+  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(Sym);
+  return T ? T->getConcreteValue() : nullptr;
+}
+
 /// Scan all symbols referenced by the constraints. If the symbol is not alive
 /// as marked in LSymbols, mark it as dead in DSymbols.
 ProgramStateRef
 RangeConstraintManager::removeDeadBindings(ProgramStateRef state,
-                                           SymbolReaper& SymReaper) {
-
+                                           SymbolReaper &SymReaper) {
+  bool Changed = false;
   ConstraintRangeTy CR = state->get<ConstraintRange>();
-  ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
+  ConstraintRangeTy::Factory &CRFactory = state->get_context<ConstraintRange>();
 
   for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
     SymbolRef sym = I.getKey();
-    if (SymReaper.maybeDead(sym))
+    if (SymReaper.maybeDead(sym)) {
+      Changed = true;
       CR = CRFactory.remove(CR, sym);
     }
+  }
 
-  return state->set<ConstraintRange>(CR);
+  return Changed ? state->set<ConstraintRange>(CR) : state;
 }
 
-RangeSet
-RangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
-  if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
+RangeSet RangeConstraintManager::getRange(ProgramStateRef state,
+                                          SymbolRef sym) {
+  if (ConstraintRangeTy::data_type *V = state->get<ConstraintRange>(sym))
     return *V;
 
   // Lazily generate a new RangeSet representing all possible values for the
   // given symbol type.
   BasicValueFactory &BV = getBasicVals();
   QualType T = sym->getType();
 
   RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T));
 
   // Special case: references are known to be non-zero.
   if (T->isReferenceType()) {
     APSIntType IntType = BV.getAPSIntType(T);
     Result = Result.Intersect(BV, F, ++IntType.getZeroValue(),
-                                     --IntType.getZeroValue());
   }
 
   return Result;
 }
 
 //===------------------------------------------------------------------------===
-// assumeSymX methods: public interface for RangeConstraintManager.
+// assumeSymX methods: protected interface for RangeConstraintManager.
 //===------------------------------------------------------------------------===/
 
 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
 // and (x, y) for open ranges. These ranges are modular, corresponding with
 // a common treatment of C integer overflow. This means that these methods
 // do not have to worry about overflow; RangeSet::Intersect can handle such a
 // "wraparound" range.
 // As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
 
   llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment;
   llvm::APSInt Upper = Lower;
   --Lower;
   ++Upper;
 
   // [Int-Adjustment+1, Int-Adjustment-1]
   // Notice that the lower bound is greater than the upper bound.
-  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
+  RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymEQ(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);
   if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
     return nullptr;
 
   // [Int-Adjustment, Int-Adjustment]
   llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
-  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
+  RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
 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 F.getEmptySet();
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
-    return GetRange(St, Sym);
+    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 F.getEmptySet();
 
   llvm::APSInt Lower = Min - Adjustment;
   llvm::APSInt Upper = ComparisonVal - Adjustment;
   --Upper;
 
-  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 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,
+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 GetRange(St, Sym);
+    return getRange(St, Sym);
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
     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 F.getEmptySet();
 
   llvm::APSInt Lower = ComparisonVal - Adjustment;
   llvm::APSInt Upper = Max - Adjustment;
   ++Lower;
 
-  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 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,
+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 GetRange(St, Sym);
+    return getRange(St, Sym);
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
     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 GetRange(St, Sym);
+    return getRange(St, Sym);
 
   llvm::APSInt Max = AdjustmentType.getMaxValue();
   llvm::APSInt Lower = ComparisonVal - Adjustment;
   llvm::APSInt Upper = Max - Adjustment;
 
-  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 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,
+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 F.getEmptySet();
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
     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 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,
+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);
+    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);
+    return getRange(St, Sym);
 
   llvm::APSInt Min = AdjustmentType.getMinValue();
   llvm::APSInt Lower = Min - Adjustment;
   llvm::APSInt Upper = ComparisonVal - Adjustment;
 
-  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return 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 RangeConstraintManager::assumeSymWithinInclusiveRange(
     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 RangeConstraintManager::assumeSymOutsideInclusiveRange(
     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.
 //===------------------------------------------------------------------------===/
 
 void RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
-                                   const char* nl, const char *sep) {
+                                   const char *nl, const char *sep) {
 
   ConstraintRangeTy Ranges = St->get<ConstraintRange>();
 
   if (Ranges.isEmpty()) {
     Out << nl << sep << "Ranges are empty." << nl;
     return;
   }
 
   Out << nl << sep << "Ranges of symbol values:";
-  for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
+  for (ConstraintRangeTy::iterator I = Ranges.begin(), E = Ranges.end(); I != E;
+       ++I) {
     Out << nl << ' ' << I.getKey() << " : ";
     I.getData().print(Out);
   }
   Out << nl;
 }

lib/StaticAnalyzer/Core/RangedConstraintManager.h

+//== RangedConstraintManager.h ----------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  Ranged constraint manager, built on SimpleConstraintManager.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
+
+namespace clang {
+
+namespace ento {
+
+class RangedConstraintManager : public SimpleConstraintManager {
+public:
+  RangedConstraintManager(SubEngine *SE, SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB) {}
+
+  ~RangedConstraintManager() override;
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from SimpleConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
+                            bool Assumption) override;
+
+  ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
+                               BinaryOperator::Opcode op,
+                               const llvm::APSInt &Int) override;
+
+  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &From,
+                                          const llvm::APSInt &To,
+                                          bool InRange) override;
+
+protected:
+  //===------------------------------------------------------------------===//
+  // Interface that subclasses must implement.
+  //===------------------------------------------------------------------===//
+
+  // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison
+  // operation for the method being invoked.
+
+  virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymWithinInclusiveRange(
+      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymOutsideInclusiveRange(
+      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+
+  //===------------------------------------------------------------------===//
+  // Internal implementation.
+  //===------------------------------------------------------------------===//
+private:
+  static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
+};
+
+} // end GR namespace
+
+} // end clang namespace
+
+#endif

lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

+//== RangedConstraintManager.cpp --------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines RangedConstraintManager, a class that provides a
+//  range-based constraint manager interface.
+//
+//===----------------------------------------------------------------------===//
+
+#include "RangedConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+
+namespace clang {
+
+namespace ento {
+
+RangedConstraintManager::~RangedConstraintManager() {}
+
+ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
+                                                   SymbolRef Sym,
+                                                   bool Assumption) {
+  // Handle SymbolData.
+  if (isa<SymbolData>(Sym)) {
+    return assumeSymUnsupported(State, Sym, Assumption);
+
+    // Handle symbolic expression.
+  } else if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
+    // We can only simplify expressions whose RHS is an integer.
+
+    BinaryOperator::Opcode op = SIE->getOpcode();
+    if (BinaryOperator::isComparisonOp(op)) {
+      if (!Assumption)
+        op = BinaryOperator::negateComparisonOp(op);
+
+      return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
+    }
+
+  } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
+    // Translate "a != b" to "(b - a) != 0".
+    // We invert the order of the operands as a heuristic for how loop
+    // conditions are usually written ("begin != end") as compared to length
+    // calculations ("end - begin"). The more correct thing to do would be to
+    // canonicalize "a - b" and "b - a", which would allow us to treat
+    // "a != b" and "b != a" the same.
+    SymbolManager &SymMgr = getSymbolManager();
+    BinaryOperator::Opcode Op = SSE->getOpcode();
+    assert(BinaryOperator::isComparisonOp(Op));
+
+    // For now, we only support comparing pointers.
+    assert(Loc::isLocType(SSE->getLHS()->getType()));
+    assert(Loc::isLocType(SSE->getRHS()->getType()));
+    QualType DiffTy = SymMgr.getContext().getPointerDiffType();
+    SymbolRef Subtraction =
+        SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
+
+    const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
+    Op = BinaryOperator::reverseComparisonOp(Op);
+    if (!Assumption)
+      Op = BinaryOperator::negateComparisonOp(Op);
+    return assumeSymRel(State, Subtraction, Op, Zero);
+  }
+
+  // If we get here, there's nothing else we can do but treat the symbol as
+  // opaque.
+  return assumeSymUnsupported(State, Sym, Assumption);
+}
+
+ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
+                                                      SymbolRef LHS,
+                                                      BinaryOperator::Opcode op,
+                                                      const llvm::APSInt &Int) {
+  assert(BinaryOperator::isComparisonOp(op) &&
+         "Non-comparison ops should be rewritten as comparisons to zero.");
+
+  // Get the type used for calculating wraparound.
+  BasicValueFactory &BVF = getBasicVals();
+  APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
+
+  // We only handle simple comparisons of the form "$sym == constant"
+  // or "($sym+constant1) == constant2".
+  // The adjustment is "constant1" in the above expression. It's used to
+  // "slide" the solution range around for modular arithmetic. For example,
+  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
+  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
+  // the subclasses of SimpleConstraintManager to handle the adjustment.
+  SymbolRef Sym = LHS;
+  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
+  computeAdjustment(Sym, Adjustment);
+
+  // Convert the right-hand side integer as necessary.
+  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
+  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
+
+  // Prefer unsigned comparisons.
+  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
+      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
+    Adjustment.setIsSigned(false);
+
+  switch (op) {
+  default:
+    llvm_unreachable("invalid operation not caught by assertion above");
+
+  case BO_EQ:
+    return assumeSymEQ(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_NE:
+    return assumeSymNE(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_GT:
+    return assumeSymGT(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_GE:
+    return assumeSymGE(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_LT:
+    return assumeSymLT(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_LE:
+    return assumeSymLE(State, Sym, ConvertedInt, Adjustment);
+  } // end switch
+}
+
+ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
+    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 assumeSymWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
+                                         ConvertedTo, Adjustment);
+  return assumeSymOutsideInclusiveRange(State, AdjustedSym, ConvertedFrom,
+                                        ConvertedTo, Adjustment);
+}
+
+void RangedConstraintManager::computeAdjustment(SymbolRef &Sym,
+                                                llvm::APSInt &Adjustment) {
+  // Is it a "($sym+constant1)" expression?
+  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
+    BinaryOperator::Opcode Op = SE->getOpcode();
+    if (Op == BO_Add || Op == BO_Sub) {
+      Sym = SE->getLHS();
+      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
+
+      // Don't forget to negate the adjustment if it's being subtracted.
+      // This should happen /after/ promotion, in case the value being
+      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
+      if (Op == BO_Sub)
+        Adjustment = -Adjustment;
+    }
+  }
+}
+
+} // end of namespace ento
+
+} // end of namespace clang

lib/StaticAnalyzer/Core/SimpleConstraintManager.h

-//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
-//
-//                     The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-//  Code shared between BasicConstraintManager and RangeConstraintManager.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
-#define LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
-
-#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-
-namespace clang {
-
-namespace ento {
-
-class SimpleConstraintManager : public ConstraintManager {
-  SubEngine *SU;
-  SValBuilder &SVB;
-public:
-  SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
-    : SU(subengine), SVB(SB) {}
-  ~SimpleConstraintManager() override;
-
-  //===------------------------------------------------------------------===//
-  // Common implementation for the interface provided by ConstraintManager.
-  //===------------------------------------------------------------------===//
-
-  ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond,
-                        bool Assumption) override;
-
-  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:
-
-  //===------------------------------------------------------------------===//
-  // Interface that subclasses must implement.
-  //===------------------------------------------------------------------===//
-
-  // Each of these is of the form "$sym+Adj <> V", where "<>" is the comparison
-  // operation for the method being invoked.
-  virtual ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
-                                     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.
-  //===------------------------------------------------------------------===//
-
-  BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
-  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
-
-  bool canReasonAbout(SVal X) const override;
-
-  ProgramStateRef assumeAux(ProgramStateRef state,
-                                NonLoc Cond,
-                                bool Assumption);
-
-  ProgramStateRef assumeAuxForSymbol(ProgramStateRef State,
-                                         SymbolRef Sym,
-                                         bool Assumption);
-};
-
-} // end GR namespace
-
-} // end clang namespace
-
-#endif

lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

 //== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==//
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
 //
-//  This file defines SimpleConstraintManager, a class that holds code shared
-//  between BasicConstraintManager and RangeConstraintManager.
+//  This file defines SimpleConstraintManager, a class that provides a
+//  simplified constraint manager interface, compared to ConstraintManager.
 //
 //===----------------------------------------------------------------------===//
 
-#include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 
 namespace clang {
 
 namespace ento {
 
 SimpleConstraintManager::~SimpleConstraintManager() {}
 
-bool SimpleConstraintManager::canReasonAbout(SVal X) const {
-  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
-  if (SymVal && SymVal->isExpression()) {
-    const SymExpr *SE = SymVal->getSymbol();
-
-    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
-      switch (SIE->getOpcode()) {
-          // We don't reason yet about bitwise-constraints on symbolic values.
-        case BO_And:
-        case BO_Or:
-        case BO_Xor:
-          return false;
-        // We don't reason yet about these arithmetic constraints on
-        // symbolic values.
-        case BO_Mul:
-        case BO_Div:
-        case BO_Rem:
-        case BO_Shl:
-        case BO_Shr:
-          return false;
-        // All other cases.
-        default:
-          return true;
-      }
-    }
-
-    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
-      if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
-        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
-        if (Loc::isLocType(SSE->getLHS()->getType())) {
-          assert(Loc::isLocType(SSE->getRHS()->getType()));
-          return true;
-        }
-      }
-    }
-
-    return false;
-  }
-
-  return true;
-}
-
-ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
+ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
                                                 DefinedSVal Cond,
                                                 bool Assumption) {
   // If we have a Loc value, cast it to a bool NonLoc first.
   if (Optional<Loc> LV = Cond.getAs<Loc>()) {
-    SValBuilder &SVB = state->getStateManager().getSValBuilder();
+    SValBuilder &SVB = State->getStateManager().getSValBuilder();
     QualType T;
     const MemRegion *MR = LV->getAsRegion();
     if (const TypedRegion *TR = dyn_cast_or_null<TypedRegion>(MR))
       T = TR->getLocationType();
     else
       T = SVB.getContext().VoidPtrTy;
 
     Cond = SVB.evalCast(*LV, SVB.getContext().BoolTy, T).castAs<DefinedSVal>();
   }
 
-  return assume(state, Cond.castAs<NonLoc>(), Assumption);
+  return assume(State, Cond.castAs<NonLoc>(), Assumption);
 }
 
-ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
-                                               NonLoc cond,
-                                               bool assumption) {
-  state = assumeAux(state, cond, assumption);
+ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
+                                                NonLoc Cond, bool Assumption) {
+  State = assumeAux(State, Cond, Assumption);
   if (NotifyAssumeClients && SU)
-    return SU->processAssume(state, cond, assumption);
-  return state;
-}
-
-
-ProgramStateRef
-SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
-                                            SymbolRef Sym, bool Assumption) {
-  BasicValueFactory &BVF = getBasicVals();
-  QualType T = Sym->getType();
-
-  // None of the constraint solvers currently support non-integer types.
-  if (!T->isIntegralOrEnumerationType())
-    return State;
-
-  const llvm::APSInt &zero = BVF.getValue(0, T);
-  if (Assumption)
-    return assumeSymNE(State, Sym, zero, zero);
-  else
-    return assumeSymEQ(State, Sym, zero, zero);
+    return SU->processAssume(State, Cond, Assumption);
 }
 
-ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
+ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
                                                    NonLoc Cond,
                                                    bool Assumption) {
 
   // We cannot reason about SymSymExprs, and can only reason about some
   // SymIntExprs.
   if (!canReasonAbout(Cond)) {
     // Just add the constraint to the expression without trying to simplify.
-    SymbolRef sym = Cond.getAsSymExpr();
-    return assumeAuxForSymbol(state, sym, Assumption);
+    SymbolRef Sym = Cond.getAsSymExpr();
+    assert(Sym);
+    return assumeSymUnsupported(State, Sym, Assumption);
   }
 
   switch (Cond.getSubKind()) {
   default:
     llvm_unreachable("'Assume' not implemented for this NonLoc");
 
   case nonloc::SymbolValKind: {
     nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>();
-    SymbolRef sym = SV.getSymbol();
-    assert(sym);
+    SymbolRef Sym = SV.getSymbol();
+    assert(Sym);
 
-    // Handle SymbolData.
-    if (!SV.isExpression()) {
-      return assumeAuxForSymbol(state, sym, Assumption);
-
-    // Handle symbolic expression.
-    } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) {
-      // We can only simplify expressions whose RHS is an integer.
-
-      BinaryOperator::Opcode op = SE->getOpcode();
-      if (BinaryOperator::isComparisonOp(op)) {
-        if (!Assumption)
-          op = BinaryOperator::negateComparisonOp(op);
-
-        return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
-      }
-
-    } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) {
-      // Translate "a != b" to "(b - a) != 0".
-      // We invert the order of the operands as a heuristic for how loop
-      // conditions are usually written ("begin != end") as compared to length
-      // calculations ("end - begin"). The more correct thing to do would be to
-      // canonicalize "a - b" and "b - a", which would allow us to treat
-      // "a != b" and "b != a" the same.
-      SymbolManager &SymMgr = getSymbolManager();
-      BinaryOperator::Opcode Op = SSE->getOpcode();
-      assert(BinaryOperator::isComparisonOp(Op));
-
-      // For now, we only support comparing pointers.
-      assert(Loc::isLocType(SSE->getLHS()->getType()));
-      assert(Loc::isLocType(SSE->getRHS()->getType()));
-      QualType DiffTy = SymMgr.getContext().getPointerDiffType();
-      SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
-                                                   SSE->getLHS(), DiffTy);
-
-      const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
-      Op = BinaryOperator::reverseComparisonOp(Op);
-      if (!Assumption)
-        Op = BinaryOperator::negateComparisonOp(Op);
-      return assumeSymRel(state, Subtraction, Op, Zero);
-    }
-
-    // If we get here, there's nothing else we can do but treat the symbol as
-    // opaque.
-    return assumeAuxForSymbol(state, sym, Assumption);
+    return assumeSym(State, Sym, Assumption);
   }
 
   case nonloc::ConcreteIntKind: {
     bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0;
     bool isFeasible = b ? Assumption : !Assumption;
-    return isFeasible ? state : nullptr;
+    return isFeasible ? State : nullptr;
   }
 
   case nonloc::LocAsIntegerKind:
-    return assume(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
+    return assume(State, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
                   Assumption);
   } // end switch
 }
 
-ProgramStateRef SimpleConstraintManager::assumeWithinInclusiveRange(
+ProgramStateRef
+SimpleConstraintManager::assumeSymUnsupported(ProgramStateRef State,
+                                              SymbolRef Sym, bool Assumption) {
+  BasicValueFactory &BVF = getBasicVals();
+  QualType T = Sym->getType();
+
+  // None of the constraint solvers currently support non-integer types.
+  if (!T->isIntegralOrEnumerationType())
+    return State;
+
+  // Reverse the operation.
+  const llvm::APSInt &Zero = BVF.getValue(0, T);
+  return assumeSymRel(State, Sym, Assumption ? BO_NE : BO_EQ, Zero);
+}
+
+ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
     ProgramStateRef State, NonLoc Value, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
 
   assert(From.isUnsigned() == To.isUnsigned() &&
          From.getBitWidth() == To.getBitWidth() &&
          "Values should have same types!");
 
   if (!canReasonAbout(Value)) {
     // Just add the constraint to the expression without trying to simplify.
     SymbolRef Sym = Value.getAsSymExpr();
     assert(Sym);
-    return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange);
+    return assumeSymInclusiveRange(State, Sym, From, To, InRange);
   }
 
   switch (Value.getSubKind()) {
   default:
-    llvm_unreachable("'assumeWithinInclusiveRange' is not implemented"
+    llvm_unreachable("'assumeWithInclusiveRange' 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 assumeSymInclusiveRange(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)) {
-    BinaryOperator::Opcode Op = SE->getOpcode();
-    if (Op == BO_Add || Op == BO_Sub) {
-      Sym = SE->getLHS();
-      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
-
-      // Don't forget to negate the adjustment if it's being subtracted.
-      // This should happen /after/ promotion, in case the value being
-      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
-      if (Op == BO_Sub)
-        Adjustment = -Adjustment;
-    }
-  }
-}
-
-ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
-                                                     const SymExpr *LHS,
-                                                     BinaryOperator::Opcode op,
-                                                     const llvm::APSInt& Int) {
-  assert(BinaryOperator::isComparisonOp(op) &&
-         "Non-comparison ops should be rewritten as comparisons to zero.");
-
-  // Get the type used for calculating wraparound.
-  BasicValueFactory &BVF = getBasicVals();
-  APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
-
-  // We only handle simple comparisons of the form "$sym == constant"
-  // or "($sym+constant1) == constant2".
-  // The adjustment is "constant1" in the above expression. It's used to
-  // "slide" the solution range around for modular arithmetic. For example,
-  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
-  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
-  // the subclasses of SimpleConstraintManager to handle the adjustment.
-  SymbolRef Sym = LHS;
-  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
-  computeAdjustment(Sym, Adjustment);
-
-  // Convert the right-hand side integer as necessary.
-  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
-  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
-
-  // Prefer unsigned comparisons.
-  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
-      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
-    Adjustment.setIsSigned(false);
-
-  switch (op) {
-  default:
-    llvm_unreachable("invalid operation not caught by assertion above");
-
-  case BO_EQ:
-    return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_NE:
-    return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_GT:
-    return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_GE:
-    return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_LT:
-    return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_LE:
-    return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
-  } // 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