Move GRTransferFunc* into ValueStateManager, and move the assumption logic there as well.

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

1 files changed, 172 insertions, 0 deletions

diff --git a/lib/Analysis/ValueState.cpp b/lib/Analysis/ValueState.cpp
index ca78faf349..2c3e6dabc6 100644
--- a/lib/Analysis/ValueState.cpp
+++ b/lib/Analysis/ValueState.cpp
@@ -13,6 +13,7 @@
 
 #include "clang/Analysis/PathSensitive/ValueState.h"
 #include "llvm/ADT/SmallSet.h"
+#include "clang/Analysis/PathSensitive/GRTransferFuncs.h"
 
 using namespace clang;
 
@@ -294,3 +295,174 @@ void ValueState::print(std::ostream& Out, CheckerStatePrinter* P,
   if (P && CheckerState)
     P->PrintCheckerState(Out, CheckerState, nl, sep);
 }
+
+//===----------------------------------------------------------------------===//
+// "Assume" logic.
+//===----------------------------------------------------------------------===//
+
+const ValueState* ValueStateManager::Assume(const ValueState* St, LVal Cond,
+                                            bool Assumption, bool& isFeasible) {
+  
+  St = AssumeAux(St, Cond, Assumption, isFeasible);
+  
+  return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
+                    : St;
+}
+
+const ValueState* ValueStateManager::AssumeAux(const ValueState* 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 ValueState* ValueStateManager::Assume(const ValueState* St, NonLVal Cond,
+                                       bool Assumption, bool& isFeasible) {
+  
+  St = AssumeAux(St, Cond, Assumption, isFeasible);
+  
+  return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
+  : St;
+}
+
+const ValueState* ValueStateManager::AssumeAux(const ValueState* 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 ValueState* ValueStateManager::AssumeSymNE(const ValueState* 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 ValueState* ValueStateManager::AssumeSymEQ(const ValueState* 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 ValueState* ValueStateManager::AssumeSymInt(const ValueState* 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);
+  }
+}