r296242 - [analyzer] Refactor and simplify SimpleConstraintManager

Dominic Chen via cfe-commits cfe-commits at lists.llvm.org
Fri Feb 24 20:51:31 PST 2017


Author: ddcc
Date: Fri Feb 24 22:51:31 2017
New Revision: 296242

URL: http://llvm.org/viewvc/llvm-project?rev=296242&view=rev
Log:
[analyzer] Refactor and simplify SimpleConstraintManager

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.

Reviewers: zaks.anna, dcoughlin

Subscribers: mgorny, xazax.hun, NoQ, rgov, cfe-commits

Differential Revision: https://reviews.llvm.org/D26061

Added:
    cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
    cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
    cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h
      - copied, changed from r296241, cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
Removed:
    cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
Modified:
    cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
    cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
    cfe/trunk/lib/StaticAnalyzer/Core/ConstraintManager.cpp
    cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
    cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h?rev=296242&r1=296241&r2=296242&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h Fri Feb 24 22:51:31 2017
@@ -139,6 +139,8 @@ public:
     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;
 

Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h?rev=296242&view=auto
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h (added)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h Fri Feb 24 22:51:31 2017
@@ -0,0 +1,92 @@
+//== 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

Modified: cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt?rev=296242&r1=296241&r2=296242&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt Fri Feb 24 22:51:31 2017
@@ -34,6 +34,7 @@ add_clang_library(clangStaticAnalyzerCor
   PlistDiagnostics.cpp
   ProgramState.cpp
   RangeConstraintManager.cpp
+  RangedConstraintManager.cpp
   RegionStore.cpp
   SValBuilder.cpp
   SVals.cpp

Modified: cfe/trunk/lib/StaticAnalyzer/Core/ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/ConstraintManager.cpp?rev=296242&r1=296241&r2=296242&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/ConstraintManager.cpp Fri Feb 24 22:51:31 2017
@@ -20,8 +20,8 @@ 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);
 }
 

Modified: cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp?rev=296242&r1=296241&r2=296242&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Fri Feb 24 22:51:31 2017
@@ -12,7 +12,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#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"
@@ -282,12 +282,31 @@ REGISTER_TRAIT_WITH_PROGRAMSTATE(Constra
                                                              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,
@@ -313,26 +332,19 @@ public:
                               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);
@@ -356,10 +368,46 @@ ento::CreateRangeConstraintManager(Progr
   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,
@@ -386,6 +434,12 @@ ConditionTruthVal RangeConstraintManager
   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
@@ -429,7 +483,7 @@ RangeSet RangeConstraintManager::getRang
 }
 
 //===------------------------------------------------------------------------===
-// 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
@@ -646,7 +700,7 @@ RangeConstraintManager::assumeSymLE(Prog
   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);
@@ -656,7 +710,7 @@ ProgramStateRef RangeConstraintManager::
   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);

Added: cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp?rev=296242&view=auto
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp (added)
+++ cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp Fri Feb 24 22:51:31 2017
@@ -0,0 +1,204 @@
+//== 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

Copied: cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h (from r296241, cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h)
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h?p2=cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h&p1=cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h&r1=296241&r2=296242&rev=296242&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/RangedConstraintManager.h Fri Feb 24 22:51:31 2017
@@ -1,4 +1,4 @@
-//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
+//== RangedConstraintManager.h ----------------------------------*- C++ -*--==//
 //
 //                     The LLVM Compiler Infrastructure
 //
@@ -7,59 +7,55 @@
 //
 //===----------------------------------------------------------------------===//
 //
-//  Code shared between BasicConstraintManager and RangeConstraintManager.
+//  Ranged constraint manager, built on SimpleConstraintManager.
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
-#define LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
 
-#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
 
 namespace clang {
 
 namespace ento {
 
-class SimpleConstraintManager : public ConstraintManager {
-  SubEngine *SU;
-  SValBuilder &SVB;
-
+class RangedConstraintManager : public SimpleConstraintManager {
 public:
-  SimpleConstraintManager(SubEngine *SE, SValBuilder &SB) : SU(SE), SVB(SB) {}
-  ~SimpleConstraintManager() override;
+  RangedConstraintManager(SubEngine *SE, SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB) {}
+
+  ~RangedConstraintManager() override;
 
   //===------------------------------------------------------------------===//
-  // Common implementation for the interface provided by ConstraintManager.
+  // Implementation for interface from SimpleConstraintManager.
   //===------------------------------------------------------------------===//
 
-  ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond,
-                         bool Assumption) override;
+  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
+                            bool Assumption) override;
 
-  ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
+  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &From,
+                                          const llvm::APSInt &To,
+                                          bool InRange) override;
 
-  ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
-                                       const llvm::APSInt &From,
-                                       const llvm::APSInt &To,
-                                       bool InRange) override;
+  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
+                                       bool Assumption) override;
 
-  ProgramStateRef assumeSymRel(ProgramStateRef State, const SymExpr *LHS,
-                               BinaryOperator::Opcode Op,
+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);
 
-  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;
@@ -84,28 +80,19 @@ protected:
                                       const llvm::APSInt &V,
                                       const llvm::APSInt &Adjustment) = 0;
 
-  virtual ProgramStateRef assumeSymbolWithinInclusiveRange(
+  virtual ProgramStateRef assumeSymWithinInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
 
-  virtual ProgramStateRef assumeSymbolOutOfInclusiveRange(
+  virtual ProgramStateRef assumeSymOutsideInclusiveRange(
       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);
+private:
+  static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
 };
 
 } // end GR namespace

Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp?rev=296242&r1=296241&r2=296242&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp Fri Feb 24 22:51:31 2017
@@ -7,12 +7,12 @@
 //
 //===----------------------------------------------------------------------===//
 //
-//  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"
@@ -23,48 +23,6 @@ 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) {
@@ -92,23 +50,6 @@ ProgramStateRef SimpleConstraintManager:
   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) {
@@ -118,7 +59,8 @@ ProgramStateRef SimpleConstraintManager:
   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()) {
@@ -129,51 +71,7 @@ ProgramStateRef SimpleConstraintManager:
     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: {
@@ -206,7 +104,7 @@ ProgramStateRef SimpleConstraintManager:
     // 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()) {
@@ -217,7 +115,7 @@ ProgramStateRef SimpleConstraintManager:
   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
 
@@ -230,118 +128,6 @@ ProgramStateRef SimpleConstraintManager:
   } // 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

Removed: cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h?rev=296241&view=auto
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h (removed)
@@ -1,115 +0,0 @@
-//== 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




More information about the cfe-commits mailing list