[analyzer] First step toward removing

ConstraintManager::canReasonAbout() from the ExprEngine.

ExprEngine should not care if the constraint solver can reason about
something or not. The solver should be able to handle all the SymExprs.

To do this, the solver should be able to keep track of not only the
SymbolData but of all SymExprs. This is why we change SymbolRef to be an
alias of SymExpr*. When encountering an expression it cannot simplify,
the solver should just add the constraints to it.

llvm-svn: 145831

6 files changed, 47 insertions, 26 deletions

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
index be1b9cecca8..bbf0469e06e 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
@@ -281,7 +281,7 @@ public:
   SymbolVal(SymbolRef sym) : NonLoc(SymbolValKind, sym) {}
 
   SymbolRef getSymbol() const {
-    return (const SymbolData*) Data;
+    return (const SymExpr*) Data;
   }
 
   static inline bool classof(const SVal* V) {
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
index 0d6e18eb3cc..e4bbf6766de 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
@@ -40,6 +40,8 @@ namespace ento {
   class TypedValueRegion;
   class VarRegion;
 
+/// \brief Symbolic value. These values used to capture symbolic execution of
+/// the program.
 class SymExpr : public llvm::FoldingSetNode {
 public:
   enum Kind { RegionValueKind, ConjuredKind, DerivedKind, ExtentKind,
@@ -69,8 +71,12 @@ public:
   static inline bool classof(const SymExpr*) { return true; }
 };
 
-typedef unsigned SymbolID;
+typedef const SymExpr* SymbolRef;
+typedef llvm::SmallVector<SymbolRef, 2> SymbolRefSmallVectorTy;
 
+typedef unsigned SymbolID;
+/// \brief A symbol representing data which can be stored in a memory location
+/// (region).
 class SymbolData : public SymExpr {
 private:
   const SymbolID Sym;
@@ -90,9 +96,6 @@ public:
   }
 };
 
-typedef const SymbolData* SymbolRef;
-typedef llvm::SmallVector<SymbolRef, 2> SymbolRefSmallVectorTy;
-
 /// A symbol representing the value of a MemRegion.
 class SymbolRegionValue : public SymbolData {
   const TypedValueRegion *R;
@@ -122,7 +125,8 @@ public:
   }
 };
 
-/// A symbol representing the result of an expression.
+/// A symbol representing the result of an expression in the case when we do
+/// not know anything about what the expression is.
 class SymbolConjured : public SymbolData {
   const Stmt *S;
   QualType T;
diff --git a/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp b/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
index d74c48d962c..0f49acca936 100644
--- a/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -43,8 +43,7 @@ void ExprEngine::VisitBinaryOperator(const BinaryOperator* B,
     if (Op == BO_Assign) {
       // EXPERIMENTAL: "Conjured" symbols.
       // FIXME: Handle structs.
-      if (RightV.isUnknown() ||
-          !getConstraintManager().canReasonAbout(RightV)) {
+      if (RightV.isUnknown()) {
         unsigned Count = currentBuilderContext->getCurrentBlockCount();
         RightV = svalBuilder.getConjuredSymbolVal(NULL, B->getRHS(), Count);
       }
diff --git a/clang/lib/StaticAnalyzer/Core/SVals.cpp b/clang/lib/StaticAnalyzer/Core/SVals.cpp
index 52e52d6d59d..6b71f184aa8 100644
--- a/clang/lib/StaticAnalyzer/Core/SVals.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SVals.cpp
@@ -99,7 +99,7 @@ SymbolRef SVal::getAsSymbol() const {
     return X->getSymbol();
 
   if (const nonloc::SymExprVal *X = dyn_cast<nonloc::SymExprVal>(this))
-    if (SymbolRef Y = dyn_cast<SymbolData>(X->getSymbolicExpression()))
+    if (SymbolRef Y = X->getSymbolicExpression())
       return Y;
 
   return getAsLocSymbol();
diff --git a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index 79d8b8bf9de..4ae1f17eea6 100644
--- a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -135,16 +135,29 @@ static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
   }
 }
 
+
+const ProgramState *SimpleConstraintManager::assumeAuxForSymbol(
+                                              const ProgramState *State,
+                                              SymbolRef Sym,
+                                              bool Assumption) {
+  QualType T =  State->getSymbolManager().getType(Sym);
+  const llvm::APSInt &zero = State->getBasicVals().getValue(0, T);
+  if (Assumption)
+    return assumeSymNE(State, Sym, zero, zero);
+  else
+    return assumeSymEQ(State, Sym, zero, zero);
+}
+
 const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state,
                                                   NonLoc Cond,
                                                   bool Assumption) {
 
-  // We cannot reason about SymSymExprs,
-  // and can only reason about some SymIntExprs.
+  // We cannot reason about SymSymExprs, and can only reason about some
+  // SymIntExprs.
   if (!canReasonAbout(Cond)) {
-    // Just return the current state indicating that the path is feasible.
-    // This may be an over-approximation of what is possible.
-    return state;
+    // Just add the constraint to the expression without trying to simplify.
+    SymbolRef sym = Cond.getAsSymExpr();
+    return assumeAuxForSymbol(state, sym, Assumption);
   }
 
   BasicValueFactory &BasicVals = state->getBasicVals();
@@ -157,22 +170,19 @@ const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state
   case nonloc::SymbolValKind: {
     nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
     SymbolRef sym = SV.getSymbol();
-    QualType T =  SymMgr.getType(sym);
-    const llvm::APSInt &zero = BasicVals.getValue(0, T);
-    if (Assumption)
-      return assumeSymNE(state, sym, zero, zero);
-    else
-      return assumeSymEQ(state, sym, zero, zero);
+    return assumeAuxForSymbol(state, sym, Assumption);
   }
 
   case nonloc::SymExprValKind: {
     nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
 
-    // For now, we only handle expressions whose RHS is an integer.
-    // All other expressions are assumed to be feasible.
-    const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression());
+    SymbolRef sym = V.getSymbolicExpression();
+    assert(sym);
+
+    // We can only simplify expressions whose RHS is an integer.
+    const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
     if (!SE)
-      return state;
+      return assumeAuxForSymbol(state, sym, Assumption);
 
     BinaryOperator::Opcode op = SE->getOpcode();
     // Implicitly compare non-comparison expressions to 0.
diff --git a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.h b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
index d4295d42d95..000af439fdd 100644
--- a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
+++ b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
@@ -81,9 +81,17 @@ protected:
   // Internal implementation.
   //===------------------------------------------------------------------===//
 
-  const ProgramState *assumeAux(const ProgramState *state, Loc Cond,bool Assumption);
+  const ProgramState *assumeAux(const ProgramState *state,
+                                Loc Cond,
+                                bool Assumption);
 
-  const ProgramState *assumeAux(const ProgramState *state, NonLoc Cond, bool Assumption);
+  const ProgramState *assumeAux(const ProgramState *state,
+                                NonLoc Cond,
+                                bool Assumption);
+
+  const ProgramState *assumeAuxForSymbol(const ProgramState *State,
+                                         SymbolRef Sym,
+                                         bool Assumption);
 };
 
 } // end GR namespace