Revert "[analyzer] Support generating and reasoning over more symbolic constraint types"

Assertion `Loc::isLocType(SSE->getLHS()->getType())' failed in Analysis/PR3991.m

This reverts commit e469ff2759275e67f9072b3d67fac90f647c0fe6.

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

3 files changed, 22 insertions, 38 deletions

diff --git a/lib/StaticAnalyzer/Core/SValBuilder.cpp b/lib/StaticAnalyzer/Core/SValBuilder.cpp
index d3b78a055c..04452e3e7c 100644
--- a/lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ b/lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -100,7 +100,7 @@ SValBuilder::getRegionValueSymbolVal(const TypedValueRegion* region) {
 
   if (T->isNullPtrType())
     return makeZeroVal(T);
-
+  
   if (!SymbolManager::canSymbolicate(T))
     return UnknownVal();
 
@@ -354,6 +354,9 @@ SVal SValBuilder::makeSymExprValNN(ProgramStateRef State,
                                    BinaryOperator::Opcode Op,
                                    NonLoc LHS, NonLoc RHS,
                                    QualType ResultTy) {
+  if (!State->isTainted(RHS) && !State->isTainted(LHS))
+    return UnknownVal();
+
   const SymExpr *symLHS = LHS.getAsSymExpr();
   const SymExpr *symRHS = RHS.getAsSymExpr();
   // TODO: When the Max Complexity is reached, we should conjure a symbol
@@ -361,7 +364,7 @@ SVal SValBuilder::makeSymExprValNN(ProgramStateRef State,
   const unsigned MaxComp = 10000; // 100000 28X
 
   if (symLHS && symRHS &&
-      (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
+      (symLHS->computeComplexity() + symRHS->computeComplexity()) <  MaxComp)
     return makeNonLoc(symLHS, Op, symRHS, ResultTy);
 
   if (symLHS && symLHS->computeComplexity() < MaxComp)
diff --git a/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp b/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
index c1d4c03744..f09f9696f5 100644
--- a/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -669,12 +669,12 @@ SVal SimpleSValBuilder::evalBinOpLL(ProgramStateRef state,
     // If one of the operands is a symbol and the other is a constant,
     // build an expression for use by the constraint manager.
     if (SymbolRef rSym = rhs.getAsLocSymbol()) {
-      const llvm::APSInt &lVal = lhs.castAs<loc::ConcreteInt>().getValue();
-
-      // Prefer expressions with symbols on the left
+      // We can only build expressions with symbols on the left,
+      // so we need a reversible operator.
       if (!BinaryOperator::isComparisonOp(op))
-        return makeNonLoc(lVal, op, rSym, resultTy);
+        return UnknownVal();
 
+      const llvm::APSInt &lVal = lhs.castAs<loc::ConcreteInt>().getValue();
       op = BinaryOperator::reverseComparisonOp(op);
       return makeNonLoc(rSym, op, lVal, resultTy);
     }
@@ -994,8 +994,7 @@ const llvm::APSInt *SimpleSValBuilder::getKnownValue(ProgramStateRef state,
   if (SymbolRef Sym = V.getAsSymbol())
     return state->getConstraintManager().getSymVal(state, Sym);
 
-  // FIXME: Add support for SymExprs in RangeConstraintManager.
-
+  // FIXME: Add support for SymExprs.
   return nullptr;
 }
 
@@ -1020,11 +1019,8 @@ SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
       return nonloc::SymbolVal(S);
     }
 
-    SVal VisitIntSymExpr(const IntSymExpr *S) {
-      SVal RHS = Visit(S->getRHS());
-      SVal LHS = SVB.makeIntVal(S->getLHS());
-      return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
-    }
+    // TODO: Support SymbolCast. Support IntSymExpr when/if we actually
+    // start producing them.
 
     SVal VisitSymIntExpr(const SymIntExpr *S) {
       SVal LHS = Visit(S->getLHS());
@@ -1049,11 +1045,6 @@ SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
       return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
     }
 
-    SVal VisitSymbolCast(const SymbolCast *S) {
-      SVal V = Visit(S->getOperand());
-      return SVB.evalCast(V, S->getType(), S->getOperand()->getType());
-    }
-
     SVal VisitSymSymExpr(const SymSymExpr *S) {
       SVal LHS = Visit(S->getLHS());
       SVal RHS = Visit(S->getRHS());
@@ -1067,8 +1058,7 @@ SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
     SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
       // Simplification is much more costly than computing complexity.
       // For high complexity, it may be not worth it.
-      // Use a lower bound to avoid recursive blowup, e.g. on PR24184.cpp
-      if (V.getSymbol()->computeComplexity() > 10)
+      if (V.getSymbol()->computeComplexity() > 100)
         return V;
       return Visit(V.getSymbol());
     }
diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
index 79bc60104f..f9f9057a89 100644
--- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -1034,19 +1034,16 @@ ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
-  ASTContext &Ctx = getBasicVals().getContext();
-  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
-  // but the former is not available in Clang. Instead, extend the APSInt
-  // directly.
-  bool isBoolTy = From.getBitWidth() == 1 && getAPSIntType(From).isNull();
-
   QualType RetTy;
   // The expression may be casted, so we cannot call getZ3DataExpr() directly
   Z3Expr Exp = getZ3Expr(Sym, &RetTy);
-  QualType RTy = isBoolTy ? Ctx.BoolTy : getAPSIntType(From);
-  Z3Expr FromExp =
-      isBoolTy ? Z3Expr::fromAPSInt(From.extend(Ctx.getTypeSize(Ctx.BoolTy)))
-               : Z3Expr::fromAPSInt(From);
+
+  assert((getAPSIntType(From) == getAPSIntType(To)) &&
+         "Range values have different types!");
+  QualType RTy = getAPSIntType(From);
+  bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
+  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
+  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
 
   // Construct single (in)equality
   if (From == To)
@@ -1054,10 +1051,6 @@ ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
                         getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
                                      FromExp, RTy, nullptr));
 
-  assert((getAPSIntType(From) == getAPSIntType(To)) &&
-         "Range values have different types!");
-
-  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
   // Construct two (in)equalities, and a logical and/or
   Z3Expr LHS =
       getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
@@ -1065,8 +1058,7 @@ ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
       getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
   return assumeZ3Expr(
       State, Sym,
-      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
-                        RetTy->isSignedIntegerOrEnumerationType()));
+      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
@@ -1414,7 +1406,6 @@ void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
                                            QualType &LTy, QualType &RTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
 
-  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Perform type conversion
   if (LTy->isIntegralOrEnumerationType() &&
       RTy->isIntegralOrEnumerationType()) {
@@ -1477,10 +1468,10 @@ template <typename T,
 void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T &RHS,
                                               QualType &RTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
+
   uint64_t LBitWidth = Ctx.getTypeSize(LTy);
   uint64_t RBitWidth = Ctx.getTypeSize(RTy);
 
-  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Always perform integer promotion before checking type equality.
   // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
   if (LTy->isPromotableIntegerType()) {