From: Anna Zaks Date: Mon, 5 Dec 2011 18:58:19 +0000 (+0000) Subject: [analyzer] First step toward removing X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=3cdf584e068056540769dab56cad333e95a89750;p=clang [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 --- diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h index be1b9cecca..bbf0469e06 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h @@ -281,7 +281,7 @@ public: SymbolVal(SymbolRef sym) : NonLoc(SymbolValKind, sym) {} SymbolRef getSymbol() const { - return (const SymbolData*) Data; + return (const SymExpr*) Data; } static inline bool classof(const SVal* V) { diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h index 0d6e18eb3c..e4bbf6766d 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h @@ -40,6 +40,8 @@ namespace ento { class TypedValueRegion; class VarRegion; +/// \brief Symbolic value. These values used to capture symbolic execution of +/// the program. class SymExpr : public llvm::FoldingSetNode { public: enum Kind { RegionValueKind, ConjuredKind, DerivedKind, ExtentKind, @@ -69,8 +71,12 @@ public: static inline bool classof(const SymExpr*) { return true; } }; -typedef unsigned SymbolID; +typedef const SymExpr* SymbolRef; +typedef llvm::SmallVector SymbolRefSmallVectorTy; +typedef unsigned SymbolID; +/// \brief A symbol representing data which can be stored in a memory location +/// (region). class SymbolData : public SymExpr { private: const SymbolID Sym; @@ -90,9 +96,6 @@ public: } }; -typedef const SymbolData* SymbolRef; -typedef llvm::SmallVector SymbolRefSmallVectorTy; - /// A symbol representing the value of a MemRegion. class SymbolRegionValue : public SymbolData { const TypedValueRegion *R; @@ -122,7 +125,8 @@ public: } }; -/// A symbol representing the result of an expression. +/// A symbol representing the result of an expression in the case when we do +/// not know anything about what the expression is. class SymbolConjured : public SymbolData { const Stmt *S; QualType T; diff --git a/lib/StaticAnalyzer/Core/ExprEngineC.cpp b/lib/StaticAnalyzer/Core/ExprEngineC.cpp index d74c48d962..0f49acca93 100644 --- a/lib/StaticAnalyzer/Core/ExprEngineC.cpp +++ b/lib/StaticAnalyzer/Core/ExprEngineC.cpp @@ -43,8 +43,7 @@ void ExprEngine::VisitBinaryOperator(const BinaryOperator* B, if (Op == BO_Assign) { // EXPERIMENTAL: "Conjured" symbols. // FIXME: Handle structs. - if (RightV.isUnknown() || - !getConstraintManager().canReasonAbout(RightV)) { + if (RightV.isUnknown()) { unsigned Count = currentBuilderContext->getCurrentBlockCount(); RightV = svalBuilder.getConjuredSymbolVal(NULL, B->getRHS(), Count); } diff --git a/lib/StaticAnalyzer/Core/SVals.cpp b/lib/StaticAnalyzer/Core/SVals.cpp index 52e52d6d59..6b71f184aa 100644 --- a/lib/StaticAnalyzer/Core/SVals.cpp +++ b/lib/StaticAnalyzer/Core/SVals.cpp @@ -99,7 +99,7 @@ SymbolRef SVal::getAsSymbol() const { return X->getSymbol(); if (const nonloc::SymExprVal *X = dyn_cast(this)) - if (SymbolRef Y = dyn_cast(X->getSymbolicExpression())) + if (SymbolRef Y = X->getSymbolicExpression()) return Y; return getAsLocSymbol(); 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(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(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(V.getSymbolicExpression()); + SymbolRef sym = V.getSymbolicExpression(); + assert(sym); + + // We can only simplify expressions whose RHS is an integer. + const SymIntExpr *SE = dyn_cast(sym); if (!SE) - return state; + return assumeAuxForSymbol(state, sym, Assumption); BinaryOperator::Opcode op = SE->getOpcode(); // Implicitly compare non-comparison expressions to 0. diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h index d4295d42d9..000af439fd 100644 --- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h +++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h @@ -81,9 +81,17 @@ protected: // Internal implementation. //===------------------------------------------------------------------===// - const ProgramState *assumeAux(const ProgramState *state, Loc Cond,bool Assumption); + const ProgramState *assumeAux(const ProgramState *state, + Loc Cond, + bool Assumption); - const ProgramState *assumeAux(const ProgramState *state, NonLoc Cond, bool Assumption); + const ProgramState *assumeAux(const ProgramState *state, + NonLoc Cond, + bool Assumption); + + const ProgramState *assumeAuxForSymbol(const ProgramState *State, + SymbolRef Sym, + bool Assumption); }; } // end GR namespace