[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

1 files changed, 25 insertions, 15 deletions

diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index 79d8b8bf9d..4ae1f17eea 100644
--- 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.