Refactor Assume logic into a separate class ConstraintManager.

llvm-svn: 55412

clang/include/clang/Analysis/PathSensitive/BasicStore.h

@@ -17,7 +17,7 @@
 #include "clang/Analysis/PathSensitive/Store.h"
 
 namespace llvm {
-  class llvm::BumpPtrAllocator; 
+  class BumpPtrAllocator; 
   class ASTContext;
 }
   

clang/include/clang/Analysis/PathSensitive/ConstraintManager.h

@@ -0,0 +1,20 @@
+#ifndef CONSTRAINT_MANAGER_H
+#define CONSTRAINT_MANAGER_H
+
+namespace clang {
+
+class GRState;
+class GRStateManager;
+class RVal;
+
+class ConstraintManager {
+public:
+  virtual const GRState* Assume(const GRState* St, RVal Cond, bool Assumption,
+                                bool& isFeasible) = 0;
+};
+
+ConstraintManager* CreateBasicConstraintManager(GRStateManager& statemgr);
+
+} // end clang namespace
+
+#endif

clang/include/clang/Analysis/PathSensitive/GRState.h

@@ -18,6 +18,7 @@
 
 #include "clang/Analysis/PathSensitive/Environment.h"
 #include "clang/Analysis/PathSensitive/Store.h"
+#include "clang/Analysis/PathSensitive/ConstraintManager.h"
 #include "clang/Analysis/PathSensitive/RValues.h"
 #include "clang/Analysis/PathSensitive/GRCoreEngine.h"
 #include "clang/AST/Expr.h"
@@ -233,6 +234,7 @@ class GRStateManager {
 private:
   EnvironmentManager                   EnvMgr;
   llvm::OwningPtr<StoreManager>        StMgr;
+  llvm::OwningPtr<ConstraintManager>   ConstraintMgr;
   GRState::IntSetTy::Factory           ISetFactory;
   
   GRState::GenericDataMap::Factory     GDMFactory;
@@ -287,8 +289,11 @@ private:
     return SetRVal(St, lval::DeclVal(D), V);
   }
 
+  typedef ConstraintManager* (*ConstraintManagerCreater)(GRStateManager&);
+    
 public:  
   GRStateManager(ASTContext& Ctx, StoreManager* stmgr,
+                 ConstraintManagerCreater CreateConstraintManager,
                  llvm::BumpPtrAllocator& alloc, CFG& c, LiveVariables& L) 
   : EnvMgr(alloc),
     StMgr(stmgr),
@@ -298,7 +303,9 @@ public:
     SymMgr(alloc),
     Alloc(alloc),
     cfg(c),
-    Liveness(L) {}
+    Liveness(L) {
+    ConstraintMgr.reset((*CreateConstraintManager)(*this));
+  }
   
   ~GRStateManager();
 
@@ -309,6 +316,7 @@ public:
   const BasicValueFactory& getBasicVals() const { return BasicVals; }
   SymbolManager& getSymbolManager() { return SymMgr; }
   LiveVariables& getLiveVariables() { return Liveness; }
+  llvm::BumpPtrAllocator& getAllocator() { return Alloc; }
 
   typedef StoreManager::DeadSymbolsTy DeadSymbolsTy;
 
@@ -440,52 +448,8 @@ public:
   // Assumption logic.
   const GRState* Assume(const GRState* St, RVal Cond, bool Assumption,
                            bool& isFeasible) {
-    
+    return ConstraintMgr->Assume(St, Cond, Assumption, isFeasible);
-    if (Cond.isUnknown()) {
-      isFeasible = true;
-      return St;
   }
-    
-    if (isa<LVal>(Cond))
-      return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
-    else
-      return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
-  }
-  
-  const GRState* Assume(const GRState* St, LVal Cond, bool Assumption,
-                           bool& isFeasible);
-
-  const GRState* Assume(const GRState* St, NonLVal Cond, bool Assumption,
-                           bool& isFeasible);
-
-private:  
-  const GRState* AssumeAux(const GRState* St, LVal Cond, bool Assumption,
-                              bool& isFeasible);
-  
-  
-  const GRState* AssumeAux(const GRState* St, NonLVal Cond,
-                              bool Assumption, bool& isFeasible);
-    
-  const GRState* AssumeSymInt(const GRState* St, bool Assumption,                                 
-                                 const SymIntConstraint& C, bool& isFeasible);
-  
-  const GRState* AssumeSymNE(const GRState* St, SymbolID sym,
-                                const llvm::APSInt& V, bool& isFeasible);
-  
-  const GRState* AssumeSymEQ(const GRState* St, SymbolID sym,
-                                const llvm::APSInt& V, bool& isFeasible);
-  
-  const GRState* AssumeSymLT(const GRState* St, SymbolID sym,
-                                const llvm::APSInt& V, bool& isFeasible);
-  
-  const GRState* AssumeSymLE(const GRState* St, SymbolID sym,
-                                const llvm::APSInt& V, bool& isFeasible);
-  
-  const GRState* AssumeSymGT(const GRState* St, SymbolID sym,
-                                const llvm::APSInt& V, bool& isFeasible);
-  
-  const GRState* AssumeSymGE(const GRState* St, SymbolID sym,
-                                const llvm::APSInt& V, bool& isFeasible);
 };
   
 //===----------------------------------------------------------------------===//

clang/lib/Analysis/BasicConstraintManager.cpp

@@ -0,0 +1,298 @@
+#include "clang/Analysis/PathSensitive/ConstraintManager.h"
+#include "clang/Analysis/PathSensitive/GRState.h"
+#include "llvm/Support/Compiler.h"
+
+using namespace clang;
+
+namespace {
+
+// BasicConstraintManager only tracks equality and inequality constraints of
+// constants and integer variables.
+class VISIBILITY_HIDDEN BasicConstraintManager : public ConstraintManager {
+  typedef llvm::ImmutableMap<SymbolID, GRState::IntSetTy> ConstNotEqTy;
+  typedef llvm::ImmutableMap<SymbolID, const llvm::APSInt*> ConstEqTy;
+
+  GRStateManager& StateMgr;
+
+public:
+  BasicConstraintManager(GRStateManager& statemgr) : StateMgr(statemgr) {}
+
+  virtual const GRState* Assume(const GRState* St, RVal Cond,
+                                bool Assumption, bool& isFeasible);
+
+  const GRState* Assume(const GRState* St, LVal Cond, bool Assumption,
+                        bool& isFeasible);
+
+  const GRState* AssumeAux(const GRState* St, LVal Cond,bool Assumption,
+                           bool& isFeasible);
+
+  const GRState* Assume(const GRState* St, NonLVal Cond, bool Assumption,
+                        bool& isFeasible);
+
+  const GRState* AssumeAux(const GRState* St, NonLVal Cond, bool Assumption,
+                           bool& isFeasible);
+
+  const GRState* AssumeSymInt(const GRState* St, bool Assumption,
+                              const SymIntConstraint& C, bool& isFeasible);
+
+  const GRState* AssumeSymNE(const GRState* St, SymbolID sym,
+                                const llvm::APSInt& V, bool& isFeasible);
+
+  const GRState* AssumeSymEQ(const GRState* St, SymbolID sym,
+                                const llvm::APSInt& V, bool& isFeasible);
+
+  const GRState* AssumeSymLT(const GRState* St, SymbolID sym,
+                                    const llvm::APSInt& V, bool& isFeasible);
+
+  const GRState* AssumeSymGT(const GRState* St, SymbolID sym,
+                             const llvm::APSInt& V, bool& isFeasible);
+
+  const GRState* AssumeSymGE(const GRState* St, SymbolID sym,
+                             const llvm::APSInt& V, bool& isFeasible);
+
+  const GRState* AssumeSymLE(const GRState* St, SymbolID sym,
+                             const llvm::APSInt& V, bool& isFeasible);
+  };
+
+} // end anonymous namespace
+
+ConstraintManager* clang::CreateBasicConstraintManager(GRStateManager& StateMgr)
+{
+  return new BasicConstraintManager(StateMgr);
+}
+
+const GRState* BasicConstraintManager::Assume(const GRState* St, RVal Cond,
+                                            bool Assumption, bool& isFeasible) {
+  if (Cond.isUnknown()) {
+    isFeasible = true;
+    return St;
+  }
+
+  if (isa<NonLVal>(Cond))
+    return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
+  else
+    return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
+}
+
+const GRState* BasicConstraintManager::Assume(const GRState* St, LVal Cond,
+                                            bool Assumption, bool& isFeasible) {
+  St = AssumeAux(St, Cond, Assumption, isFeasible);
+  // TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
+  return St;
+}
+
+const GRState* BasicConstraintManager::AssumeAux(const GRState* St, LVal Cond,
+                                            bool Assumption, bool& isFeasible) {
+  BasicValueFactory& BasicVals = StateMgr.getBasicVals();
+
+  switch (Cond.getSubKind()) {
+  default:
+    assert (false && "'Assume' not implemented for this LVal.");
+    return St;
+
+  case lval::SymbolValKind:
+    if (Assumption)
+      return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+                         BasicVals.getZeroWithPtrWidth(), isFeasible);
+    else
+      return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+                         BasicVals.getZeroWithPtrWidth(), isFeasible);
+
+  case lval::DeclValKind:
+  case lval::FuncValKind:
+  case lval::GotoLabelKind:
+  case lval::StringLiteralValKind:
+    isFeasible = Assumption;
+    return St;
+
+  case lval::FieldOffsetKind:
+    return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
+                     Assumption, isFeasible);
+
+  case lval::ArrayOffsetKind:
+    return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
+                     Assumption, isFeasible);
+
+  case lval::ConcreteIntKind: {
+    bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
+    isFeasible = b ? Assumption : !Assumption;
+    return St;
+  }
+  } // end switch
+}
+
+const GRState*
+BasicConstraintManager::Assume(const GRState* St, NonLVal Cond, bool Assumption,
+                               bool& isFeasible) {
+  St = AssumeAux(St, Cond, Assumption, isFeasible);
+  // TF->EvalAssume() does nothing now.
+  return St;
+}
+
+const GRState*
+BasicConstraintManager::AssumeAux(const GRState* St,NonLVal Cond,
+                                  bool Assumption, bool& isFeasible) {
+  BasicValueFactory& BasicVals = StateMgr.getBasicVals();
+  SymbolManager& SymMgr = StateMgr.getSymbolManager();
+
+  switch (Cond.getSubKind()) {
+  default:
+    assert(false && "'Assume' not implemented for this NonLVal");
+
+  case nonlval::SymbolValKind: {
+    nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
+    SymbolID sym = SV.getSymbol();
+
+    if (Assumption)
+      return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
+                         isFeasible);
+    else
+      return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
+                         isFeasible);
+  }
+
+  case nonlval::SymIntConstraintValKind:
+    return
+      AssumeSymInt(St, Assumption,
+                   cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
+                   isFeasible);
+
+  case nonlval::ConcreteIntKind: {
+    bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
+    isFeasible = b ? Assumption : !Assumption;
+    return St;
+  }
+
+  case nonlval::LValAsIntegerKind:
+    return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
+                     Assumption, isFeasible);
+  } // end switch
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymInt(const GRState* St, bool Assumption,
+                                  const SymIntConstraint& C, bool& isFeasible) {
+
+  switch (C.getOpcode()) {
+  default:
+    // No logic yet for other operators.
+    isFeasible = true;
+    return St;
+
+  case BinaryOperator::EQ:
+    if (Assumption)
+      return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
+    else
+      return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
+
+  case BinaryOperator::NE:
+    if (Assumption)
+      return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
+    else
+      return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
+
+  case BinaryOperator::GE:
+    if (Assumption)
+      return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
+    else
+      return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
+
+  case BinaryOperator::LE:
+    if (Assumption)
+      return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
+    else
+      return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
+  } // end switch
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymNE(const GRState* St, SymbolID sym,
+                                    const llvm::APSInt& V, bool& isFeasible) {
+  // First, determine if sym == X, where X != V.
+  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+    isFeasible = (*X != V);
+    return St;
+  }
+
+  // Second, determine if sym != V.
+  if (St->isNotEqual(sym, V)) {
+    isFeasible = true;
+    return St;
+  }
+
+  // If we reach here, sym is not a constant and we don't know if it is != V.
+  // Make that assumption.
+  isFeasible = true;
+  return StateMgr.AddNE(St, sym, V);
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymEQ(const GRState* St, SymbolID sym,
+                                    const llvm::APSInt& V, bool& isFeasible) {
+  // First, determine if sym == X, where X != V.
+  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+    isFeasible = *X == V;
+    return St;
+  }
+
+  // Second, determine if sym != V.
+  if (St->isNotEqual(sym, V)) {
+    isFeasible = false;
+    return St;
+  }
+
+  // If we reach here, sym is not a constant and we don't know if it is == V.
+  // Make that assumption.
+
+  isFeasible = true;
+  return StateMgr.AddEQ(St, sym, V);
+}
+
+// These logic will be handled in another ConstraintManager.
+const GRState*
+BasicConstraintManager::AssumeSymLT(const GRState* St, SymbolID sym,
+                                    const llvm::APSInt& V, bool& isFeasible) {
+
+  // FIXME: For now have assuming x < y be the same as assuming sym != V;
+  return AssumeSymNE(St, sym, V, isFeasible);
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymGT(const GRState* St, SymbolID sym,
+                                    const llvm::APSInt& V, bool& isFeasible) {
+
+  // FIXME: For now have assuming x > y be the same as assuming sym != V;
+  return AssumeSymNE(St, sym, V, isFeasible);
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolID sym,
+                                    const llvm::APSInt& V, bool& isFeasible) {
+
+  // FIXME: Primitive logic for now.  Only reject a path if the value of
+  //  sym is a constant X and !(X >= V).
+
+  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+    isFeasible = *X >= V;
+    return St;
+  }
+
+  isFeasible = true;
+  return St;
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolID sym,
+                                    const llvm::APSInt& V, bool& isFeasible) {
+
+  // FIXME: Primitive logic for now.  Only reject a path if the value of
+  //  sym is a constant X and !(X <= V).
+
+  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+    isFeasible = *X <= V;
+    return St;
+  }
+
+  isFeasible = true;
+  return St;
+}

clang/lib/Analysis/GRExprEngine.cpp

@@ -121,7 +121,7 @@ GRExprEngine::GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx,
     Liveness(L),
     Builder(NULL),
     StateMgr(G.getContext(), CreateBasicStoreManager(G.getAllocator(), Ctx),
-             G.getAllocator(), G.getCFG(), L),
+             CreateBasicConstraintManager, G.getAllocator(), G.getCFG(), L),
     SymMgr(StateMgr.getSymbolManager()),
     CurrentStmt(NULL),
   NSExceptionII(NULL), NSExceptionInstanceRaiseSelectors(NULL),

clang/lib/Analysis/GRState.cpp

@@ -383,241 +383,3 @@ bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
 bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
   return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
 }
-
-//===----------------------------------------------------------------------===//
-// "Assume" logic.
-//===----------------------------------------------------------------------===//
-
-const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
-                                            bool Assumption, bool& isFeasible) {
-  
-  St = AssumeAux(St, Cond, Assumption, isFeasible);
-  
-  return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
-                    : St;
-}
-
-const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
-                                          bool Assumption, bool& isFeasible) {
-  
-  switch (Cond.getSubKind()) {
-    default:
-      assert (false && "'Assume' not implemented for this LVal.");
-      return St;
-      
-    case lval::SymbolValKind:
-      if (Assumption)
-        return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
-                           BasicVals.getZeroWithPtrWidth(), isFeasible);
-      else
-        return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
-                           BasicVals.getZeroWithPtrWidth(), isFeasible);
-      
-    case lval::DeclValKind:
-    case lval::FuncValKind:
-    case lval::GotoLabelKind:
-    case lval::StringLiteralValKind:
-      isFeasible = Assumption;
-      return St;
-      
-    case lval::FieldOffsetKind:
-      return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
-                       Assumption, isFeasible);
-      
-    case lval::ArrayOffsetKind:
-      return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
-                       Assumption, isFeasible);
-      
-    case lval::ConcreteIntKind: {
-      bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
-      isFeasible = b ? Assumption : !Assumption;      
-      return St;
-    }
-  }
-}
-
-const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
-                                       bool Assumption, bool& isFeasible) {
-  
-  St = AssumeAux(St, Cond, Assumption, isFeasible);
-  
-  return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
-  : St;
-}
-
-const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
-                                          bool Assumption, bool& isFeasible) {  
-  switch (Cond.getSubKind()) {
-    default:
-      assert (false && "'Assume' not implemented for this NonLVal.");
-      return St;
-      
-      
-    case nonlval::SymbolValKind: {
-      nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
-      SymbolID sym = SV.getSymbol();
-      
-      if (Assumption)
-        return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
-                           isFeasible);
-      else
-        return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
-                           isFeasible);
-    }
-      
-    case nonlval::SymIntConstraintValKind:
-      return
-      AssumeSymInt(St, Assumption,
-                   cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
-                   isFeasible);
-      
-    case nonlval::ConcreteIntKind: {
-      bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
-      isFeasible = b ? Assumption : !Assumption;      
-      return St;
-    }
-      
-    case nonlval::LValAsIntegerKind: {
-      return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
-                       Assumption, isFeasible);
-    }
-  }
-}
-
-
-
-const GRState* GRStateManager::AssumeSymInt(const GRState* St,
-                                             bool Assumption,
-                                             const SymIntConstraint& C,
-                                             bool& isFeasible) {
-  
-  switch (C.getOpcode()) {
-    default:
-      // No logic yet for other operators.
-      isFeasible = true;
-      return St;
-      
-    case BinaryOperator::EQ:
-      if (Assumption)
-        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
-      else
-        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
-      
-    case BinaryOperator::NE:
-      if (Assumption)
-        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
-      else
-        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
-      
-    case BinaryOperator::GE:
-      if (Assumption)
-        return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
-      else
-        return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
-      
-    case BinaryOperator::LE:
-      if (Assumption)
-        return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
-      else
-        return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);    
-  }
-}
-
-//===----------------------------------------------------------------------===//
-// FIXME: This should go into a plug-in constraint engine.
-//===----------------------------------------------------------------------===//
-
-const GRState*
-GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
-                               const llvm::APSInt& V, bool& isFeasible) {
-  
-  // First, determine if sym == X, where X != V.
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
-    isFeasible = *X != V;
-    return St;
-  }
-  
-  // Second, determine if sym != V.
-  if (St->isNotEqual(sym, V)) {
-    isFeasible = true;
-    return St;
-  }
-  
-  // If we reach here, sym is not a constant and we don't know if it is != V.
-  // Make that assumption.
-  
-  isFeasible = true;
-  return AddNE(St, sym, V);
-}
-
-const GRState*
-GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
-                               const llvm::APSInt& V, bool& isFeasible) {
-  
-  // First, determine if sym == X, where X != V.
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
-    isFeasible = *X == V;
-    return St;
-  }
-  
-  // Second, determine if sym != V.
-  if (St->isNotEqual(sym, V)) {
-    isFeasible = false;
-    return St;
-  }
-  
-  // If we reach here, sym is not a constant and we don't know if it is == V.
-  // Make that assumption.
-  
-  isFeasible = true;
-  return AddEQ(St, sym, V);
-}
-
-const GRState*
-GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
-                               const llvm::APSInt& V, bool& isFeasible) {
-  
-  // FIXME: For now have assuming x < y be the same as assuming sym != V;
-  return AssumeSymNE(St, sym, V, isFeasible);
-}
-
-const GRState*
-GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
-                               const llvm::APSInt& V, bool& isFeasible) {
-  
-  // FIXME: For now have assuming x > y be the same as assuming sym != V;
-  return AssumeSymNE(St, sym, V, isFeasible);
-}
-
-const GRState*
-GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
-                               const llvm::APSInt& V, bool& isFeasible) {
-  
-  // FIXME: Primitive logic for now.  Only reject a path if the value of
-  //  sym is a constant X and !(X >= V).
-  
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
-    isFeasible = *X >= V;
-    return St;
-  }
-  
-  isFeasible = true;
-  return St;
-}
-
-const GRState*
-GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
-                               const llvm::APSInt& V, bool& isFeasible) {
-  
-  // FIXME: Primitive logic for now.  Only reject a path if the value of
-  //  sym is a constant X and !(X <= V).
-    
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
-    isFeasible = *X <= V;
-    return St;
-  }
-  
-  isFeasible = true;
-  return St;
-}
-