[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.

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

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
index be1b9cecca8975365404a500ad11b7b91fdb53b2..bbf0469e06e513b2e2081b1822a550c9da9ab479 100644 (file)
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
+++ b/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/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
index 0d6e18eb3cc8b0447ad8f1526d400eaee8a2789e..e4bbf6766dedd400703008016c9500f2d7c9ce9a 100644 (file)
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
+++ b/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/lib/StaticAnalyzer/Core/ExprEngineC.cpp b/lib/StaticAnalyzer/Core/ExprEngineC.cpp
index d74c48d962c785d1de081fa2e907b82efc115a4f..0f49acca936ad447dd8df75c00c3109333884688 100644 (file)
--- a/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ b/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/lib/StaticAnalyzer/Core/SVals.cpp b/lib/StaticAnalyzer/Core/SVals.cpp
index 52e52d6d59db44362252814bd39051de227b2b34..6b71f184aa8e4a7a62dbb076140d0fc3dbe4f30a 100644 (file)
--- a/lib/StaticAnalyzer/Core/SVals.cpp
+++ b/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/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index 79d8b8bf9de38a2ce6757c895fcd1626569ed435..4ae1f17eea6eea1f63a04d5a8b7a0eae52461583 100644 (file)
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/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/lib/StaticAnalyzer/Core/SimpleConstraintManager.h b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
index d4295d42d95e807e30553d3e7282aa8ebc0cd02e..000af439fdd46c201c651c6a5cbc394db610c894 100644 (file)
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
+++ b/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