From: Anna Zaks Date: Mon, 5 Dec 2011 18:58:25 +0000 (+0000) Subject: [analyzer] Remove all uses of ConstraintManager::canResonAbout() from X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=76462f00854171d2aa3ebc34f9aac1c60021b0ea;p=clang [analyzer] Remove all uses of ConstraintManager::canResonAbout() from ExprEngine. Teach SimpleConstraintManager::assumeSymRel() to propagate constraints to symbolic expressions. + One extra warning (real bug) is now generated due to enhanced assumeSymRel(). git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@145832 91177308-0d34-0410-b5e6-96231b3b80d8 --- diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h index bbf0469e06..ca9315d2ce 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h @@ -276,6 +276,7 @@ namespace nonloc { enum Kind { ConcreteIntKind, SymbolValKind, SymExprValKind, LocAsIntegerKind, CompoundValKind, LazyCompoundValKind }; +// TODO: Change to contain symbol data. class SymbolVal : public NonLoc { public: SymbolVal(SymbolRef sym) : NonLoc(SymbolValKind, sym) {} diff --git a/lib/StaticAnalyzer/Core/ExprEngineC.cpp b/lib/StaticAnalyzer/Core/ExprEngineC.cpp index 0f49acca93..12b658eb2d 100644 --- a/lib/StaticAnalyzer/Core/ExprEngineC.cpp +++ b/lib/StaticAnalyzer/Core/ExprEngineC.cpp @@ -121,8 +121,7 @@ void ExprEngine::VisitBinaryOperator(const BinaryOperator* B, SVal LHSVal; - if (Result.isUnknown() || - !getConstraintManager().canReasonAbout(Result)) { + if (Result.isUnknown()) { unsigned Count = currentBuilderContext->getCurrentBlockCount(); @@ -358,8 +357,7 @@ void ExprEngine::VisitDeclStmt(const DeclStmt *DS, ExplodedNode *Pred, // Recover some path-sensitivity if a scalar value evaluated to // UnknownVal. - if ((InitVal.isUnknown() || - !getConstraintManager().canReasonAbout(InitVal)) && + if ((InitVal.isUnknown()) && !VD->getType()->isReferenceType() && !Pred->getState()->isTainted(InitVal)) { InitVal = svalBuilder.getConjuredSymbolVal(NULL, InitEx, @@ -726,7 +724,7 @@ void ExprEngine::VisitIncrementDecrementOperator(const UnaryOperator* U, SVal Result = evalBinOp(state, Op, V2, RHS, U->getType()); // Conjure a new symbol if necessary to recover precision. - if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result)){ + if (Result.isUnknown()){ DefinedOrUnknownSVal SymVal = svalBuilder.getConjuredSymbolVal(NULL, Ex, currentBuilderContext->getCurrentBlockCount()); diff --git a/lib/StaticAnalyzer/Core/ProgramState.cpp b/lib/StaticAnalyzer/Core/ProgramState.cpp index a93b5bfd64..79f4348b7c 100644 --- a/lib/StaticAnalyzer/Core/ProgramState.cpp +++ b/lib/StaticAnalyzer/Core/ProgramState.cpp @@ -550,9 +550,8 @@ bool ScanReachableSymbols::scan(const SymExpr *sym) { return true; isVisited = 1; - if (const SymbolData *sData = dyn_cast(sym)) - if (!visitor.VisitSymbol(sData)) - return false; + if (!visitor.VisitSymbol(sym)) + return false; switch (sym->getKind()) { case SymExpr::RegionValueKind: diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp index 4ae1f17eea..8b7c2c1398 100644 --- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp @@ -212,6 +212,40 @@ const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state } // end switch } +static llvm::APSInt computeAdjustment(const SymExpr *LHS, + SymbolRef &Sym) { + llvm::APSInt DefaultAdjustment; + DefaultAdjustment = 0; + + // First check if the LHS is a simple symbol reference. + if (isa(LHS)) + return DefaultAdjustment; + + // Next, see if it's a "($sym+constant1)" expression. + const SymIntExpr *SE = dyn_cast(LHS); + + // We cannot simplify "($sym1+$sym2)". + if (!SE) + return DefaultAdjustment; + + // Get the constant out of the expression "($sym+constant1)" or + // "+constant1". + Sym = SE->getLHS(); + switch (SE->getOpcode()) { + case BO_Add: + return SE->getRHS(); + break; + case BO_Sub: + return -SE->getRHS(); + break; + default: + // We cannot simplify non-additive operators. + return DefaultAdjustment; + } + + return DefaultAdjustment; +} + const ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *state, const SymExpr *LHS, BinaryOperator::Opcode op, @@ -219,48 +253,15 @@ const ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *st assert(BinaryOperator::isComparisonOp(op) && "Non-comparison ops should be rewritten as comparisons to zero."); - // We only handle simple comparisons of the form "$sym == constant" - // or "($sym+constant1) == constant2". - // The adjustment is "constant1" in the above expression. It's used to - // "slide" the solution range around for modular arithmetic. For example, - // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which - // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to - // the subclasses of SimpleConstraintManager to handle the adjustment. - llvm::APSInt Adjustment; - - // First check if the LHS is a simple symbol reference. - SymbolRef Sym = dyn_cast(LHS); - if (Sym) { - Adjustment = 0; - } else { - // Next, see if it's a "($sym+constant1)" expression. - const SymIntExpr *SE = dyn_cast(LHS); - - // We don't handle "($sym1+$sym2)". - // Give up and assume the constraint is feasible. - if (!SE) - return state; - - // We don't handle "(+constant1)". - // Give up and assume the constraint is feasible. - Sym = dyn_cast(SE->getLHS()); - if (!Sym) - return state; - - // Get the constant out of the expression "($sym+constant1)". - switch (SE->getOpcode()) { - case BO_Add: - Adjustment = SE->getRHS(); - break; - case BO_Sub: - Adjustment = -SE->getRHS(); - break; - default: - // We don't handle non-additive operators. - // Give up and assume the constraint is feasible. - return state; - } - } + // We only handle simple comparisons of the form "$sym == constant" + // or "($sym+constant1) == constant2". + // The adjustment is "constant1" in the above expression. It's used to + // "slide" the solution range around for modular arithmetic. For example, + // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which + // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to + // the subclasses of SimpleConstraintManager to handle the adjustment. + SymbolRef Sym = LHS; + llvm::APSInt Adjustment = computeAdjustment(LHS, Sym); // FIXME: This next section is a hack. It silently converts the integers to // be of the same type as the symbol, which is not always correct. Really the diff --git a/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp b/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp index f7924319e5..2e6f33353e 100644 --- a/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp +++ b/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp @@ -260,9 +260,10 @@ SVal SimpleSValBuilder::MakeSymIntVal(const SymExpr *LHS, // Wrap the LHS up in a NonLoc again and let evalCastFromNonLoc do the // dirty work. if (isIdempotent) { - if (SymbolRef LHSSym = dyn_cast(LHS)) - return evalCastFromNonLoc(nonloc::SymbolVal(LHSSym), resultTy); - return evalCastFromNonLoc(nonloc::SymExprVal(LHS), resultTy); + if (isa(LHS)) + return evalCastFromNonLoc(nonloc::SymbolVal(LHS), resultTy); + else + return evalCastFromNonLoc(nonloc::SymExprVal(LHS), resultTy); } // If we reach this point, the expression cannot be simplified. diff --git a/test/Analysis/out-of-bounds.c b/test/Analysis/out-of-bounds.c index ac2cdc8259..a97bba5bb3 100644 --- a/test/Analysis/out-of-bounds.c +++ b/test/Analysis/out-of-bounds.c @@ -128,13 +128,11 @@ void test2_multi_ok(int x) { buf[0][0] = 1; // no-warning } -// *** FIXME *** -// We don't get a warning here yet because our symbolic constraint solving -// doesn't handle: (symbol * constant) < constant +// Testing if solver handles (symbol * constant) < constant void test3(int x) { int buf[100]; if (x < 0) - buf[x] = 1; + buf[x] = 1; // expected-warning {{Out of bound memory access (accessed memory precedes memory block)}} } // *** FIXME ***