[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

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

#endif
   ///
   /// 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 {
     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;
 
   virtual void print(ProgramStateRef state,
                      raw_ostream &Out,
                      const char* nl,
                      const char *sep) = 0;
 

cfe/trunk/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:
+  //===------------------------------------------------------------------===//
+  // 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;
+
+  /// 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;
+
+  /// 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) = 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

cfe/trunk/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
   )

cfe/trunk/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();
 }

cfe/trunk/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;

 };
 } // 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 *SE, SValBuilder &SVB)
-      : SimpleConstraintManager(SE, SVB) {}
+      : RangedConstraintManager(SE, SVB) {}
+
+  //===------------------------------------------------------------------===//
+  // 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 &V,
                               const llvm::APSInt &Adjustment) override;
public:
   ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
                               const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
                               const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymbolWithinInclusiveRange(
+  ProgramStateRef assumeSymWithinInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymbolOutOfInclusiveRange(
+  ProgramStateRef assumeSymOutsideInclusiveRange(
       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;
-
-  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) {
   bool Changed = false;
   ConstraintRangeTy CR = State->get<ConstraintRange>();
   ConstraintRangeTy::Factory &CRFactory = State->get_context<ConstraintRange>();
if (T->isReferenceType()) {
     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,

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

cfe/trunk/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 assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &From,
+                                          const llvm::APSInt &To,
+                                          bool InRange) override;
+
+  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
+                                       bool Assumption) override;
+
+protected:
+  /// Assume a constraint between a symbolic expression and a concrete integer.
+  virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
+                               BinaryOperator::Opcode op,
+                               const llvm::APSInt &Int);
+
+  //===------------------------------------------------------------------===//
+  // 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

cfe/trunk/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::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);
+}
+
+ProgramStateRef
+RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
+                                              SymbolRef Sym, bool Assumption) {
+  BasicValueFactory &BVF = getBasicVals();
+  QualType T = Sym->getType();
+
+  // Non-integer types are not supported.
+  if (!T->isIntegralOrEnumerationType())
+    return State;
+
+  // Reverse the operation and add directly to state.
+  const llvm::APSInt &Zero = BVF.getValue(0, T);
+  if (Assumption)
+    return assumeSymNE(State, Sym, Zero, Zero);
+  else
+    return assumeSymEQ(State, Sym, Zero, Zero);
+}
+
+ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
+                                                      SymbolRef Sym,
+                                                      BinaryOperator::Opcode Op,
+                                                      const llvm::APSInt &Int) {
+  assert(BinaryOperator::isComparisonOp(Op) &&
+         "Non-comparison ops should be rewritten as comparisons to zero.");
+
+  // Simplification: translate an assume of a constraint of the form
+  // "(exp comparison_op expr) != 0" to true into an assume of
+  // "exp comparison_op expr" to true. (And similarly, an assume of the form
+  // "(exp comparison_op expr) == 0" to true into an assume of
+  // "exp comparison_op expr" to false.)
+  if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
+    if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym))
+      if (BinaryOperator::isComparisonOp(SE->getOpcode()))
+        return assumeSym(State, Sym, (Op == BO_NE ? true : false));
+  }
+
+  // Get the type used for calculating wraparound.
+  BasicValueFactory &BVF = getBasicVals();
+  APSIntType WraparoundType = BVF.getAPSIntType(Sym->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.
+  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
+}
+
+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

cfe/trunk/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 *SE, SValBuilder &SB) : SU(SE), 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 assumeInclusiveRange(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

cfe/trunk/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,
                                                 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();
     QualType T;
     const MemRegion *MR = LV->getAsRegion();

 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);
-}
-
 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);
+    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);
-
-    // 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;
   }
 
ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
   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("'assumeInclusiveRange' 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.");
-
-  SymbolRef Sym = LHS;
-
-  // Simplification: translate an assume of a constraint of the form
-  // "(exp comparison_op expr) != 0" to true into an assume of 
-  // "exp comparison_op expr" to true. (And similarly, an assume of the form
-  // "(exp comparison_op expr) == 0" to true into an assume of
-  // "exp comparison_op expr" to false.)
-  if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
-    if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym))
-      if (BinaryOperator::isComparisonOp(SE->getOpcode()))
-        return assume(State, nonloc::SymbolVal(Sym), (Op == BO_NE ? true : false));
-  }
-
-  // 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.
-  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