[analyzer] Support generating and reasoning over more symbolic constr…

…aint types

Summary: Generate more IntSymExpr constraints, perform SVal simplification for IntSymExpr and SymbolCast constraints, and create fully symbolic SymExprs

Reviewers: zaks.anna, dcoughlin, NoQ, xazax.hun

Subscribers: mgorny, cfe-commits

Differential Revision: https://reviews.llvm.org/D28953

llvm-svn: 307833

clang/include/clang/StaticAnalyzer/Checkers/SValExplainer.h

@@ -125,17 +125,25 @@ class SValExplainer : public FullSValVisitor<SValExplainer, std::string> {
     return OS.str();
   }
 
-  // TODO: IntSymExpr doesn't appear in practice.
-  // Add the relevant code once it does.
+  std::string VisitIntSymExpr(const IntSymExpr *S) {
+    std::string Str;
+    llvm::raw_string_ostream OS(Str);
+    OS << S->getLHS()
+       << std::string(BinaryOperator::getOpcodeStr(S->getOpcode())) << " "
+       << "(" << Visit(S->getRHS()) << ") ";
+    return OS.str();
+  }
 
   std::string VisitSymSymExpr(const SymSymExpr *S) {
     return "(" + Visit(S->getLHS()) + ") " +
            std::string(BinaryOperator::getOpcodeStr(S->getOpcode())) +
            " (" + Visit(S->getRHS()) + ")";
   }
 
-  // TODO: SymbolCast doesn't appear in practice.
-  // Add the relevant code once it does.
+  std::string VisitSymbolCast(const SymbolCast *S) {
+    return "cast of type '" + S->getType().getAsString() + "' of " +
+           Visit(S->getOperand());
+  }
 
   std::string VisitSymbolicRegion(const SymbolicRegion *R) {
     // Explain 'this' object here.

clang/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,17 +354,14 @@ 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
   // instead of generating an Unknown value and propagate the taint info to it.
   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)

clang/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()) {
-      // We can only build expressions with symbols on the left,
-      // so we need a reversible operator.
+      const llvm::APSInt &lVal = lhs.castAs<loc::ConcreteInt>().getValue();
+
+      // Prefer expressions with symbols on the left
       if (!BinaryOperator::isComparisonOp(op))
-        return UnknownVal();
+        return makeNonLoc(lVal, op, rSym, resultTy);
 
-      const llvm::APSInt &lVal = lhs.castAs<loc::ConcreteInt>().getValue();
       op = BinaryOperator::reverseComparisonOp(op);
       return makeNonLoc(rSym, op, lVal, resultTy);
     }
@@ -994,7 +994,8 @@ const llvm::APSInt *SimpleSValBuilder::getKnownValue(ProgramStateRef state,
   if (SymbolRef Sym = V.getAsSymbol())
     return state->getConstraintManager().getSymVal(state, Sym);
 
-  // FIXME: Add support for SymExprs.
+  // FIXME: Add support for SymExprs in RangeConstraintManager.
+
   return nullptr;
 }
 
@@ -1019,8 +1020,11 @@ SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
       return nonloc::SymbolVal(S);
     }
 
-    // TODO: Support SymbolCast. Support IntSymExpr when/if we actually
-    // start producing them.
+    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());
+    }
 
     SVal VisitSymIntExpr(const SymIntExpr *S) {
       SVal LHS = Visit(S->getLHS());
@@ -1045,6 +1049,11 @@ 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());
@@ -1058,7 +1067,8 @@ 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.
-      if (V.getSymbol()->computeComplexity() > 100)
+      // Use a lower bound to avoid recursive blowup, e.g. on PR24184.cpp
+      if (V.getSymbol()->computeComplexity() > 10)
         return V;
       return Visit(V.getSymbol());
     }

clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

@@ -1034,31 +1034,39 @@ 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);
-
-  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);
+  QualType RTy = isBoolTy ? Ctx.BoolTy : getAPSIntType(From);
+  Z3Expr FromExp =
+      isBoolTy ? Z3Expr::fromAPSInt(From.extend(Ctx.getTypeSize(Ctx.BoolTy)))
+               : Z3Expr::fromAPSInt(From);
 
   // Construct single (in)equality
   if (From == To)
     return assumeZ3Expr(State, Sym,
                         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);
   Z3Expr RHS =
       getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
   return assumeZ3Expr(
       State, Sym,
-      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
+      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+                        RetTy->isSignedIntegerOrEnumerationType()));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
@@ -1406,6 +1414,7 @@ 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()) {
@@ -1468,10 +1477,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()) {

clang/test/Analysis/analyzer_test.py

@@ -1,3 +1,4 @@
+import copy
 import lit.formats
 import lit.TestRunner
 
@@ -8,18 +9,21 @@ def execute(self, test, litConfig):
         results = []
 
         # Parse any test requirements ('REQUIRES: ')
-        saved_test = test
+        saved_test = copy.deepcopy(test)
         lit.TestRunner.parseIntegratedTestScript(test)
 
+        # If the test does not require z3, drop it from the available features
+        # to satisfy tests that explicitly require !z3
         if 'z3' not in test.requires:
+            test.config.available_features.discard('z3')
             results.append(self.executeWithAnalyzeSubstitution(
-                saved_test, litConfig, '-analyzer-constraints=range'))
+                test, litConfig, '-analyzer-constraints=range'))
 
-            if results[-1].code == lit.Test.FAIL:
+            if results[-1].code != lit.Test.PASS:
                 return results[-1]
 
         # If z3 backend available, add an additional run line for it
-        if test.config.clang_staticanalyzer_z3 == '1':
+        if test.config.clang_staticanalyzer_z3 == '1' and '!z3' not in test.requires:
             results.append(self.executeWithAnalyzeSubstitution(
                 saved_test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3'))
 

clang/test/Analysis/bitwise-ops.c

@@ -7,10 +7,9 @@ void testPersistentConstraints(int x, int y) {
   // Sanity check
   CHECK(x); // expected-warning{{TRUE}}
   CHECK(x & 1); // expected-warning{{TRUE}}
-
-  // False positives due to SValBuilder giving up on certain kinds of exprs.
-  CHECK(1 - x); // expected-warning{{UNKNOWN}}
-  CHECK(x & y); // expected-warning{{UNKNOWN}}
+
+  CHECK(1 - x); // expected-warning{{TRUE}}
+  CHECK(x & y); // expected-warning{{TRUE}}
 }
 
 int testConstantShifts_PR18073(int which) {
@@ -29,4 +28,4 @@ int testConstantShifts_PR18073(int which) {
   default:
     return 0;
   }
-}
+}

clang/test/Analysis/bool-assignment.c

@@ -43,11 +43,7 @@ void test_BOOL_initialization(int y) {
     return;
   }
   if (y > 200 && y < 250) {
-#ifdef ANALYZER_CM_Z3
     BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
-#else
-    BOOL x = y; // no-warning
-#endif
     return;
   }
   if (y >= 127 && y < 150) {