diff options
author | Dominic Chen <d.c.ddcc@gmail.com> | 2017-07-12 19:37:57 +0000 |
---|---|---|
committer | Dominic Chen <d.c.ddcc@gmail.com> | 2017-07-12 19:37:57 +0000 |
commit | e469ff2759275e67f9072b3d67fac90f647c0fe6 (patch) | |
tree | 932028567e45b91e218e0b9e8452384b19be3096 /lib/StaticAnalyzer | |
parent | 429fe8229496f639df6b0b4734beedb1d4317aa5 (diff) |
[analyzer] Support generating and reasoning over more symbolic constraint 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
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@307833 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/StaticAnalyzer')
-rw-r--r-- | lib/StaticAnalyzer/Core/SValBuilder.cpp | 7 | ||||
-rw-r--r-- | lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp | 26 | ||||
-rw-r--r-- | lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp | 27 |
3 files changed, 38 insertions, 22 deletions
diff --git a/lib/StaticAnalyzer/Core/SValBuilder.cpp b/lib/StaticAnalyzer/Core/SValBuilder.cpp index 04452e3e7c..d3b78a055c 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,9 +354,6 @@ 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 @@ -364,7 +361,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 f09f9696f5..c1d4c03744 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()) { - // 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()); } diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp index f9f9057a89..79bc60104f 100644 --- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -1034,16 +1034,19 @@ 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) @@ -1051,6 +1054,10 @@ 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); @@ -1058,7 +1065,8 @@ 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, 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 <y, 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 <y, 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()) { |