Refactor Assume logic into a separate class ConstraintManager.

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@55412 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 0 insertions, 238 deletions

diff --git a/lib/Analysis/GRState.cpp b/lib/Analysis/GRState.cpp
index dd9bf69715..4ad0a449bb 100644
--- a/lib/Analysis/GRState.cpp
+++ b/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;
-}
-