From a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9 Mon Sep 17 00:00:00 2001 From: Ted Kremenek Date: Thu, 18 Jun 2009 22:57:13 +0000 Subject: [PATCH] libAnalysis: - Remove the 'isFeasible' flag from all uses of 'Assume'. - Remove the 'Assume' methods from GRStateManager. Now the only way to create a new GRState with an assumption is to use the new 'assume' methods in GRState. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@73731 91177308-0d34-0410-b5e6-96231b3b80d8 --- .../PathSensitive/ConstraintManager.h | 21 +- .../Analysis/PathSensitive/GRExprEngine.h | 19 +- .../clang/Analysis/PathSensitive/GRState.h | 121 ++++++----- .../Analysis/PathSensitive/GRTransferFuncs.h | 8 +- lib/Analysis/BasicConstraintManager.cpp | 160 +++++++-------- lib/Analysis/CFRefCount.cpp | 13 +- lib/Analysis/GRExprEngine.cpp | 194 +++++++----------- lib/Analysis/GRExprEngineInternalChecks.cpp | 13 +- lib/Analysis/RangeConstraintManager.cpp | 17 +- lib/Analysis/SimpleConstraintManager.cpp | 183 ++++++++--------- lib/Analysis/SimpleConstraintManager.h | 78 +++---- 11 files changed, 368 insertions(+), 459 deletions(-) diff --git a/include/clang/Analysis/PathSensitive/ConstraintManager.h b/include/clang/Analysis/PathSensitive/ConstraintManager.h index c8e5e85c8a..eb519e0e74 100644 --- a/include/clang/Analysis/PathSensitive/ConstraintManager.h +++ b/include/clang/Analysis/PathSensitive/ConstraintManager.h @@ -30,26 +30,25 @@ class SVal; class ConstraintManager { public: virtual ~ConstraintManager(); - virtual const GRState* Assume(const GRState* St, SVal Cond, - bool Assumption, bool& isFeasible) = 0; + virtual const GRState *Assume(const GRState *state, SVal Cond, + bool Assumption) = 0; - virtual const GRState* AssumeInBound(const GRState* St, SVal Idx, - SVal UpperBound, bool Assumption, - bool& isFeasible) = 0; + virtual const GRState *AssumeInBound(const GRState *state, SVal Idx, + SVal UpperBound, bool Assumption) = 0; - virtual const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) - const = 0; + virtual const llvm::APSInt* getSymVal(const GRState *state, + SymbolRef sym) const = 0; - virtual bool isEqual(const GRState* St, SymbolRef sym, + virtual bool isEqual(const GRState *state, SymbolRef sym, const llvm::APSInt& V) const = 0; - virtual const GRState* RemoveDeadBindings(const GRState* St, + virtual const GRState *RemoveDeadBindings(const GRState *state, SymbolReaper& SymReaper) = 0; - virtual void print(const GRState* St, std::ostream& Out, + virtual void print(const GRState *state, std::ostream& Out, const char* nl, const char *sep) = 0; - virtual void EndPath(const GRState* St) {} + virtual void EndPath(const GRState *state) {} /// canReasonAbout - Not all ConstraintManagers can accurately reason about /// all SVal values. This method returns true if the ConstraintManager can diff --git a/include/clang/Analysis/PathSensitive/GRExprEngine.h b/include/clang/Analysis/PathSensitive/GRExprEngine.h index 2068b1beaa..6cf49d0db1 100644 --- a/include/clang/Analysis/PathSensitive/GRExprEngine.h +++ b/include/clang/Analysis/PathSensitive/GRExprEngine.h @@ -520,24 +520,7 @@ protected: inline NonLoc MakeConstantVal(uint64_t X, Expr* Ex) { return NonLoc::MakeVal(getBasicVals(), X, Ex->getType()); - } - - /// Assume - Create new state by assuming that a given expression - /// is true or false. - const GRState* Assume(const GRState* St, SVal Cond, bool Assumption, - bool& isFeasible) { - return StateMgr.Assume(St, Cond, Assumption, isFeasible); - } - - const GRState* Assume(const GRState* St, Loc Cond, bool Assumption, - bool& isFeasible) { - return StateMgr.Assume(St, Cond, Assumption, isFeasible); - } - - const GRState* AssumeInBound(const GRState* St, SVal Idx, SVal UpperBound, - bool Assumption, bool& isFeasible) { - return StateMgr.AssumeInBound(St, Idx, UpperBound, Assumption, isFeasible); - } + } public: NodeTy* MakeNode(NodeSet& Dst, Stmt* S, NodeTy* Pred, const GRState* St, diff --git a/include/clang/Analysis/PathSensitive/GRState.h b/include/clang/Analysis/PathSensitive/GRState.h index 25863ffd4a..5c151efc34 100644 --- a/include/clang/Analysis/PathSensitive/GRState.h +++ b/include/clang/Analysis/PathSensitive/GRState.h @@ -158,6 +158,49 @@ public: BasicValueFactory &getBasicVals() const; SymbolManager &getSymbolManager() const; + GRTransferFuncs &getTransferFuncs() const; + + //==---------------------------------------------------------------------==// + // Constraints on values. + //==---------------------------------------------------------------------==// + // + // Each GRState records constraints on symbolic values. These constraints + // are managed using the ConstraintManager associated with a GRStateManager. + // As constraints gradually accrue on symbolic values, added constraints + // may conflict and indicate that a state is infeasible (as no real values + // could satisfy all the constraints). This is the principal mechanism + // for modeling path-sensitivity in GRExprEngine/GRState. + // + // Various "Assume" methods form the interface for adding constraints to + // symbolic values. A call to "Assume" indicates an assumption being placed + // on one or symbolic values. Assume methods take the following inputs: + // + // (1) A GRState object representing the current state. + // + // (2) The assumed constraint (which is specific to a given "Assume" method). + // + // (3) A binary value "Assumption" that indicates whether the constraint is + // assumed to be true or false. + // + // The output of "Assume" are two values: + // + // (a) "isFeasible" is set to true or false to indicate whether or not + // the assumption is feasible. + // + // (b) A new GRState object with the added constraints. + // + // FIXME: (a) should probably disappear since it is redundant with (b). + // (i.e., (b) could just be set to NULL). + // + + const GRState *assume(SVal condition, bool assumption) const; + + const GRState *assumeInBound(SVal idx, SVal upperBound, + bool assumption) const; + + //==---------------------------------------------------------------------==// + // Binding and retrieving values to/from the environment and symbolic store. + //==---------------------------------------------------------------------==// const GRState *bindExpr(Stmt* Ex, SVal V, bool isBlkExpr, bool Invalidate) const; @@ -171,6 +214,8 @@ public: const GRState *unbindLoc(Loc LV) const; SVal getLValue(const VarDecl* VD) const; + + const llvm::APSInt *getSymVal(SymbolRef sym) const; SVal getSVal(Expr* Ex) const; @@ -188,7 +233,10 @@ public: template CB scanReachableSymbols(SVal val) const; - // Trait based GDM dispatch. + //==---------------------------------------------------------------------==// + // Accessing the Generic Data Map (GDM). + //==---------------------------------------------------------------------==// + void* const* FindGDM(void* K) const; template @@ -671,56 +719,6 @@ public: return GRStateTrait::MakeContext(p); } - - //==---------------------------------------------------------------------==// - // Constraints on values. - //==---------------------------------------------------------------------==// - // - // Each GRState records constraints on symbolic values. These constraints - // are managed using the ConstraintManager associated with a GRStateManager. - // As constraints gradually accrue on symbolic values, added constraints - // may conflict and indicate that a state is infeasible (as no real values - // could satisfy all the constraints). This is the principal mechanism - // for modeling path-sensitivity in GRExprEngine/GRState. - // - // Various "Assume" methods form the interface for adding constraints to - // symbolic values. A call to "Assume" indicates an assumption being placed - // on one or symbolic values. Assume methods take the following inputs: - // - // (1) A GRState object representing the current state. - // - // (2) The assumed constraint (which is specific to a given "Assume" method). - // - // (3) A binary value "Assumption" that indicates whether the constraint is - // assumed to be true or false. - // - // The output of "Assume" are two values: - // - // (a) "isFeasible" is set to true or false to indicate whether or not - // the assumption is feasible. - // - // (b) A new GRState object with the added constraints. - // - // FIXME: (a) should probably disappear since it is redundant with (b). - // (i.e., (b) could just be set to NULL). - // - - const GRState* Assume(const GRState* St, SVal Cond, bool Assumption, - bool& isFeasible) { - const GRState *state = - ConstraintMgr->Assume(St, Cond, Assumption, isFeasible); - assert(!isFeasible || state); - return isFeasible ? state : NULL; - } - - const GRState* AssumeInBound(const GRState* St, SVal Idx, SVal UpperBound, - bool Assumption, bool& isFeasible) { - const GRState *state = - ConstraintMgr->AssumeInBound(St, Idx, UpperBound, Assumption, - isFeasible); - assert(!isFeasible || state); - return isFeasible ? state : NULL; - } const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) { return ConstraintMgr->getSymVal(St, sym); @@ -736,6 +734,15 @@ public: // Out-of-line method definitions for GRState. //===----------------------------------------------------------------------===// +inline const GRState *GRState::assume(SVal Cond, bool Assumption) const { + return Mgr->ConstraintMgr->Assume(this, Cond, Assumption); +} + +inline const GRState *GRState::assumeInBound(SVal Idx, SVal UpperBound, + bool Assumption) const { + return Mgr->ConstraintMgr->AssumeInBound(this, Idx, UpperBound, Assumption); +} + inline const GRState *GRState::bindExpr(Stmt* Ex, SVal V, bool isBlkExpr, bool Invalidate) const { return Mgr->BindExpr(this, Ex, V, isBlkExpr, Invalidate); @@ -758,6 +765,10 @@ inline SVal GRState::getLValue(const VarDecl* VD) const { return Mgr->GetLValue(this, VD); } +inline const llvm::APSInt *GRState::getSymVal(SymbolRef sym) const { + return Mgr->getSymVal(this, sym); +} + inline SVal GRState::getSVal(Expr* Ex) const { return Mgr->GetSVal(this, Ex); } @@ -782,13 +793,17 @@ inline SVal GRState::getSValAsScalarOrLoc(const MemRegion *R) const { return Mgr->GetSValAsScalarOrLoc(this, R); } -inline BasicValueFactory& GRState::getBasicVals() const { +inline BasicValueFactory &GRState::getBasicVals() const { return Mgr->getBasicVals(); } -inline SymbolManager& GRState::getSymbolManager() const { +inline SymbolManager &GRState::getSymbolManager() const { return Mgr->getSymbolManager(); } + +inline GRTransferFuncs &GRState::getTransferFuncs() const { + return Mgr->getTransferFuncs(); +} template const GRState *GRState::add(typename GRStateTrait::key_type K) const { diff --git a/include/clang/Analysis/PathSensitive/GRTransferFuncs.h b/include/clang/Analysis/PathSensitive/GRTransferFuncs.h index 0f353d0700..c2f8f5aae0 100644 --- a/include/clang/Analysis/PathSensitive/GRTransferFuncs.h +++ b/include/clang/Analysis/PathSensitive/GRTransferFuncs.h @@ -110,11 +110,9 @@ public: // Assumptions. - virtual const GRState* EvalAssume(GRStateManager& VMgr, - const GRState* St, - SVal Cond, bool Assumption, - bool& isFeasible) { - return St; + virtual const GRState* EvalAssume(const GRState *state, + SVal Cond, bool Assumption) { + return state; } }; diff --git a/lib/Analysis/BasicConstraintManager.cpp b/lib/Analysis/BasicConstraintManager.cpp index 1f907baa24..7bd22fd313 100644 --- a/lib/Analysis/BasicConstraintManager.cpp +++ b/lib/Analysis/BasicConstraintManager.cpp @@ -53,37 +53,37 @@ public: BasicConstraintManager(GRStateManager& statemgr) : SimpleConstraintManager(statemgr), ISetFactory(statemgr.getAllocator()) {} - const GRState* AssumeSymNE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const GRState* AssumeSymNE(const GRState* state, SymbolRef sym, + const llvm::APSInt& V); - const GRState* AssumeSymEQ(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const GRState* AssumeSymEQ(const GRState* state, SymbolRef sym, + const llvm::APSInt& V); - const GRState* AssumeSymLT(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const GRState* AssumeSymLT(const GRState* state, SymbolRef sym, + const llvm::APSInt& V); - const GRState* AssumeSymGT(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const GRState* AssumeSymGT(const GRState* state, SymbolRef sym, + const llvm::APSInt& V); - const GRState* AssumeSymGE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const GRState* AssumeSymGE(const GRState* state, SymbolRef sym, + const llvm::APSInt& V); - const GRState* AssumeSymLE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const GRState* AssumeSymLE(const GRState* state, SymbolRef sym, + const llvm::APSInt& V); - const GRState* AddEQ(const GRState* St, SymbolRef sym, const llvm::APSInt& V); + const GRState* AddEQ(const GRState* state, SymbolRef sym, const llvm::APSInt& V); - const GRState* AddNE(const GRState* St, SymbolRef sym, const llvm::APSInt& V); + const GRState* AddNE(const GRState* state, SymbolRef sym, const llvm::APSInt& V); - const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) const; - bool isNotEqual(const GRState* St, SymbolRef sym, const llvm::APSInt& V) + const llvm::APSInt* getSymVal(const GRState* state, SymbolRef sym) const; + bool isNotEqual(const GRState* state, SymbolRef sym, const llvm::APSInt& V) const; - bool isEqual(const GRState* St, SymbolRef sym, const llvm::APSInt& V) + bool isEqual(const GRState* state, SymbolRef sym, const llvm::APSInt& V) const; - const GRState* RemoveDeadBindings(const GRState* St, SymbolReaper& SymReaper); + const GRState* RemoveDeadBindings(const GRState* state, SymbolReaper& SymReaper); - void print(const GRState* St, std::ostream& Out, + void print(const GRState* state, std::ostream& Out, const char* nl, const char *sep); }; @@ -95,87 +95,77 @@ ConstraintManager* clang::CreateBasicConstraintManager(GRStateManager& StateMgr) } const GRState* -BasicConstraintManager::AssumeSymNE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible) { +BasicConstraintManager::AssumeSymNE(const GRState *state, SymbolRef sym, + const llvm::APSInt& V) { // First, determine if sym == X, where X != V. - if (const llvm::APSInt* X = getSymVal(St, sym)) { - isFeasible = (*X != V); - return St; + if (const llvm::APSInt* X = getSymVal(state, sym)) { + bool isFeasible = (*X != V); + return isFeasible ? state : NULL; } // Second, determine if sym != V. - if (isNotEqual(St, sym, V)) { - isFeasible = true; - return St; - } + if (isNotEqual(state, sym, V)) + return state; // If we reach here, sym is not a constant and we don't know if it is != V. // Make that assumption. - isFeasible = true; - return AddNE(St, sym, V); + return AddNE(state, sym, V); } -const GRState* -BasicConstraintManager::AssumeSymEQ(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible) { +const GRState *BasicConstraintManager::AssumeSymEQ(const GRState *state, + SymbolRef sym, + const llvm::APSInt &V) { // First, determine if sym == X, where X != V. - if (const llvm::APSInt* X = getSymVal(St, sym)) { - isFeasible = *X == V; - return St; + if (const llvm::APSInt* X = getSymVal(state, sym)) { + bool isFeasible = *X == V; + return isFeasible ? state : NULL; } // Second, determine if sym != V. - if (isNotEqual(St, sym, V)) { - isFeasible = false; - return St; - } + if (isNotEqual(state, sym, V)) + return NULL; // If we reach here, sym is not a constant and we don't know if it is == V. // Make that assumption. - - isFeasible = true; - return AddEQ(St, sym, V); + return AddEQ(state, sym, V); } // These logic will be handled in another ConstraintManager. -const GRState* -BasicConstraintManager::AssumeSymLT(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible) { - +const GRState *BasicConstraintManager::AssumeSymLT(const GRState *state, + SymbolRef sym, + const llvm::APSInt& V) { // Is 'V' the smallest possible value? if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) { // sym cannot be any value less than 'V'. This path is infeasible. - isFeasible = false; - return St; + return NULL; } // FIXME: For now have assuming x < y be the same as assuming sym != V; - return AssumeSymNE(St, sym, V, isFeasible); + return AssumeSymNE(state, sym, V); } -const GRState* -BasicConstraintManager::AssumeSymGT(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible) { +const GRState *BasicConstraintManager::AssumeSymGT(const GRState *state, + SymbolRef sym, + const llvm::APSInt& V) { // Is 'V' the largest possible value? if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) { // sym cannot be any value greater than 'V'. This path is infeasible. - isFeasible = false; - return St; + return NULL; } // FIXME: For now have assuming x > y be the same as assuming sym != V; - return AssumeSymNE(St, sym, V, isFeasible); + return AssumeSymNE(state, sym, V); } -const GRState* -BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible) { +const GRState *BasicConstraintManager::AssumeSymGE(const GRState *state, + SymbolRef sym, + const llvm::APSInt &V) { // Reject a path if the value of sym is a constant X and !(X >= V). - if (const llvm::APSInt* X = getSymVal(St, sym)) { - isFeasible = *X >= V; - return St; + if (const llvm::APSInt *X = getSymVal(state, sym)) { + bool isFeasible = *X >= V; + return isFeasible ? state : NULL; } // Sym is not a constant, but it is worth looking to see if V is the @@ -183,28 +173,25 @@ BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolRef sym, if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) { // If we know that sym != V, then this condition is infeasible since // there is no other value greater than V. - isFeasible = !isNotEqual(St, sym, V); + bool isFeasible = !isNotEqual(state, sym, V); // If the path is still feasible then as a consequence we know that // 'sym == V' because we cannot have 'sym > V' (no larger values). // Add this constraint. - if (isFeasible) - return AddEQ(St, sym, V); + return isFeasible ? AddEQ(state, sym, V) : NULL; } - else - isFeasible = true; - return St; + return state; } const GRState* -BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible) { +BasicConstraintManager::AssumeSymLE(const GRState* state, SymbolRef sym, + const llvm::APSInt& V) { // Reject a path if the value of sym is a constant X and !(X <= V). - if (const llvm::APSInt* X = getSymVal(St, sym)) { - isFeasible = *X <= V; - return St; + if (const llvm::APSInt* X = getSymVal(state, sym)) { + bool isFeasible = *X <= V; + return isFeasible ? state : NULL; } // Sym is not a constant, but it is worth looking to see if V is the @@ -212,18 +199,15 @@ BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolRef sym, if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) { // If we know that sym != V, then this condition is infeasible since // there is no other value less than V. - isFeasible = !isNotEqual(St, sym, V); + bool isFeasible = !isNotEqual(state, sym, V); // If the path is still feasible then as a consequence we know that // 'sym == V' because we cannot have 'sym < V' (no smaller values). // Add this constraint. - if (isFeasible) - return AddEQ(St, sym, V); + return isFeasible ? AddEQ(state, sym, V) : NULL; } - else - isFeasible = true; - return St; + return state; } const GRState* BasicConstraintManager::AddEQ(const GRState* state, SymbolRef sym, @@ -246,26 +230,26 @@ const GRState* BasicConstraintManager::AddNE(const GRState* state, SymbolRef sym return state->set(sym, S); } -const llvm::APSInt* BasicConstraintManager::getSymVal(const GRState* St, +const llvm::APSInt* BasicConstraintManager::getSymVal(const GRState* state, SymbolRef sym) const { - const ConstEqTy::data_type* T = St->get(sym); + const ConstEqTy::data_type* T = state->get(sym); return T ? *T : NULL; } -bool BasicConstraintManager::isNotEqual(const GRState* St, SymbolRef sym, +bool BasicConstraintManager::isNotEqual(const GRState* state, SymbolRef sym, const llvm::APSInt& V) const { // Retrieve the NE-set associated with the given symbol. - const ConstNotEqTy::data_type* T = St->get(sym); + const ConstNotEqTy::data_type* T = state->get(sym); // See if V is present in the NE-set. return T ? T->contains(&V) : false; } -bool BasicConstraintManager::isEqual(const GRState* St, SymbolRef sym, +bool BasicConstraintManager::isEqual(const GRState* state, SymbolRef sym, const llvm::APSInt& V) const { // Retrieve the EQ-set associated with the given symbol. - const ConstEqTy::data_type* T = St->get(sym); + const ConstEqTy::data_type* T = state->get(sym); // See if V is present in the EQ-set. return T ? **T == V : false; } @@ -296,11 +280,11 @@ BasicConstraintManager::RemoveDeadBindings(const GRState* state, return state->set(CNE); } -void BasicConstraintManager::print(const GRState* St, std::ostream& Out, +void BasicConstraintManager::print(const GRState* state, std::ostream& Out, const char* nl, const char *sep) { // Print equality constraints. - ConstEqTy CE = St->get(); + ConstEqTy CE = state->get(); if (!CE.isEmpty()) { Out << nl << sep << "'==' constraints:"; @@ -314,7 +298,7 @@ void BasicConstraintManager::print(const GRState* St, std::ostream& Out, // Print != constraints. - ConstNotEqTy CNE = St->get(); + ConstNotEqTy CNE = state->get(); if (!CNE.isEmpty()) { Out << nl << sep << "'!=' constraints:"; diff --git a/lib/Analysis/CFRefCount.cpp b/lib/Analysis/CFRefCount.cpp index 6603ba72b7..9cdc769431 100644 --- a/lib/Analysis/CFRefCount.cpp +++ b/lib/Analysis/CFRefCount.cpp @@ -1953,9 +1953,8 @@ public: // Assumptions. - virtual const GRState* EvalAssume(GRStateManager& VMgr, - const GRState* St, SVal Cond, - bool Assumption, bool& isFeasible); + virtual const GRState *EvalAssume(const GRState* state, SVal condition, + bool assumption); }; } // end anonymous namespace @@ -3307,10 +3306,8 @@ void CFRefCount::EvalReturn(ExplodedNodeSet& Dst, // Assumptions. -const GRState* CFRefCount::EvalAssume(GRStateManager& VMgr, - const GRState* state, - SVal Cond, bool Assumption, - bool& isFeasible) { +const GRState* CFRefCount::EvalAssume(const GRState *state, + SVal Cond, bool Assumption) { // FIXME: We may add to the interface of EvalAssume the list of symbols // whose assumptions have changed. For now we just iterate through the @@ -3329,7 +3326,7 @@ const GRState* CFRefCount::EvalAssume(GRStateManager& VMgr, for (RefBindings::iterator I=B.begin(), E=B.end(); I!=E; ++I) { // Check if the symbol is null (or equal to any constant). // If this is the case, stop tracking the symbol. - if (VMgr.getSymVal(state, I.getKey())) { + if (state->getSymVal(I.getKey())) { changed = true; B = RefBFactory.Remove(B, I.getKey()); } diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp index e392de6aab..c43c83b259 100644 --- a/lib/Analysis/GRExprEngine.cpp +++ b/lib/Analysis/GRExprEngine.cpp @@ -181,10 +181,9 @@ const GRState* GRExprEngine::getInitialState() { SVal Constraint = EvalBinOp(state, BinaryOperator::GT, V, ValMgr.makeZeroVal(T), getContext().IntTy); - bool isFeasible = false; - const GRState *newState = Assume(state, Constraint, true, - isFeasible); - if (newState) state = newState; + + if (const GRState *newState = state->assume(Constraint, true)) + state = newState; } } @@ -708,21 +707,13 @@ void GRExprEngine::ProcessBranch(Stmt* Condition, Stmt* Term, } // Process the true branch. - - bool isFeasible = false; - const GRState* state = Assume(PrevState, V, true, isFeasible); - - if (isFeasible) + if (const GRState *state = PrevState->assume(V, true)) builder.generateNode(MarkBranch(state, Term, true), true); else builder.markInfeasible(true); // Process the false branch. - - isFeasible = false; - state = Assume(PrevState, V, false, isFeasible); - - if (isFeasible) + if (const GRState *state = PrevState->assume(V, false)) builder.generateNode(MarkBranch(state, Term, false), false); else builder.markInfeasible(false); @@ -808,7 +799,7 @@ void GRExprEngine::ProcessSwitch(SwitchNodeBuilder& builder) { } const GRState* DefaultSt = state; - bool DefaultFeasible = false; + bool defaultIsFeasible = false; for (iterator I = builder.begin(), EI = builder.end(); I != EI; ++I) { CaseStmt* Case = cast(I.getCase()); @@ -846,11 +837,8 @@ void GRExprEngine::ProcessSwitch(SwitchNodeBuilder& builder) { getContext().IntTy); // Now "assume" that the case matches. - bool isFeasible = false; - const GRState* StNew = Assume(state, Res, true, isFeasible); - - if (isFeasible) { - builder.generateCaseStmtNode(I, StNew); + if (const GRState* stateNew = state->assume(Res, true)) { + builder.generateCaseStmtNode(I, stateNew); // If CondV evaluates to a constant, then we know that this // is the *only* case that we can take, so stop evaluating the @@ -861,13 +849,9 @@ void GRExprEngine::ProcessSwitch(SwitchNodeBuilder& builder) { // Now "assume" that the case doesn't match. Add this state // to the default state (if it is feasible). - - isFeasible = false; - StNew = Assume(DefaultSt, Res, false, isFeasible); - - if (isFeasible) { - DefaultFeasible = true; - DefaultSt = StNew; + if (const GRState *stateNew = DefaultSt->assume(Res, false)) { + defaultIsFeasible = true; + DefaultSt = stateNew; } // Concretize the next value in the range. @@ -882,7 +866,7 @@ void GRExprEngine::ProcessSwitch(SwitchNodeBuilder& builder) { // If we reach here, than we know that the default branch is // possible. - if (DefaultFeasible) builder.generateDefaultCaseNode(DefaultSt); + if (defaultIsFeasible) builder.generateDefaultCaseNode(DefaultSt); } //===----------------------------------------------------------------------===// @@ -922,27 +906,17 @@ void GRExprEngine::VisitLogicalExpr(BinaryOperator* B, NodeTy* Pred, // or 1. Alternatively, we could take a lazy approach, and calculate this // value later when necessary. We don't have the machinery in place for // this right now, and since most logical expressions are used for branches, - // the payoff is not likely to be large. Instead, we do eager evaluation. - - bool isFeasible = false; - const GRState* NewState = Assume(state, X, true, isFeasible); - - if (isFeasible) - MakeNode(Dst, B, Pred, - BindBlkExpr(NewState, B, MakeConstantVal(1U, B))); + // the payoff is not likely to be large. Instead, we do eager evaluation. + if (const GRState *newState = state->assume(X, true)) + MakeNode(Dst, B, Pred, BindBlkExpr(newState, B, MakeConstantVal(1U, B))); - isFeasible = false; - NewState = Assume(state, X, false, isFeasible); - - if (isFeasible) - MakeNode(Dst, B, Pred, - BindBlkExpr(NewState, B, MakeConstantVal(0U, B))); + if (const GRState *newState = state->assume(X, false)) + MakeNode(Dst, B, Pred, BindBlkExpr(newState, B, MakeConstantVal(0U, B))); } else { // We took the LHS expression. Depending on whether we are '&&' or // '||' we know what the value of the expression is via properties of // the short-circuiting. - X = MakeConstantVal( B->getOpcode() == BinaryOperator::LAnd ? 0U : 1U, B); MakeNode(Dst, B, Pred, BindBlkExpr(state, B, X)); } @@ -1189,15 +1163,12 @@ GRExprEngine::NodeTy* GRExprEngine::EvalLocation(Stmt* Ex, NodeTy* Pred, Loc LV = cast(location); // "Assume" that the pointer is not NULL. - bool isFeasibleNotNull = false; - const GRState* StNotNull = Assume(state, LV, true, isFeasibleNotNull); + const GRState *StNotNull = state->assume(LV, true); // "Assume" that the pointer is NULL. - bool isFeasibleNull = false; - const GRState *StNull = Assume(state, LV, false, isFeasibleNull); + const GRState *StNull = state->assume(LV, false); - if (isFeasibleNull) { - + if (StNull) { // Use the Generic Data Map to mark in the state what lval was null. const SVal* PersistentLV = getBasicVals().getPersistentSVal(LV); StNull = StNull->set(PersistentLV); @@ -1208,17 +1179,15 @@ GRExprEngine::NodeTy* GRExprEngine::EvalLocation(Stmt* Ex, NodeTy* Pred, Builder->generateNode(Ex, StNull, Pred, ProgramPoint::PostNullCheckFailedKind); - if (NullNode) { - - NullNode->markAsSink(); - - if (isFeasibleNotNull) ImplicitNullDeref.insert(NullNode); + if (NullNode) { + NullNode->markAsSink(); + if (StNotNull) ImplicitNullDeref.insert(NullNode); else ExplicitNullDeref.insert(NullNode); } } - if (!isFeasibleNotNull) - return 0; + if (!StNotNull) + return NULL; // Check for out-of-bound array access. if (isa(LV)) { @@ -1230,15 +1199,12 @@ GRExprEngine::NodeTy* GRExprEngine::EvalLocation(Stmt* Ex, NodeTy* Pred, SVal NumElements = getStoreManager().getSizeInElements(StNotNull, ER->getSuperRegion()); - bool isFeasibleInBound = false; - const GRState* StInBound = AssumeInBound(StNotNull, Idx, NumElements, - true, isFeasibleInBound); + const GRState * StInBound = StNotNull->assumeInBound(Idx, NumElements, + true); + const GRState* StOutBound = StNotNull->assumeInBound(Idx, NumElements, + false); - bool isFeasibleOutBound = false; - const GRState* StOutBound = AssumeInBound(StNotNull, Idx, NumElements, - false, isFeasibleOutBound); - - if (isFeasibleOutBound) { + if (StOutBound) { // Report warning. Make sink node manually. NodeTy* OOBNode = Builder->generateNode(Ex, StOutBound, Pred, @@ -1247,16 +1213,16 @@ GRExprEngine::NodeTy* GRExprEngine::EvalLocation(Stmt* Ex, NodeTy* Pred, if (OOBNode) { OOBNode->markAsSink(); - if (isFeasibleInBound) + if (StInBound) ImplicitOOBMemAccesses.insert(OOBNode); else ExplicitOOBMemAccesses.insert(OOBNode); } } - if (!isFeasibleInBound) - return 0; - + if (!StInBound) + return NULL; + StNotNull = StInBound; } } @@ -1329,19 +1295,18 @@ static bool EvalOSAtomicCompareAndSwap(ExplodedNodeSet& Dst, ExplodedNode *N = *I; const GRState *stateLoad = N->getState(); - SVal theValueVal = StateMgr.GetSVal(stateLoad, theValueExpr); - SVal oldValueVal = StateMgr.GetSVal(stateLoad, oldValueExpr); + SVal theValueVal = stateLoad->getSVal(theValueExpr); + SVal oldValueVal = stateLoad->getSVal(oldValueExpr); // Perform the comparison. SVal Cmp = Engine.EvalBinOp(stateLoad, BinaryOperator::EQ, theValueVal, oldValueVal, Engine.getContext().IntTy); - bool isFeasible = false; - const GRState *stateEqual = StateMgr.Assume(stateLoad, Cmp, true, - isFeasible); + + const GRState *stateEqual = stateLoad->assume(Cmp, true); // Were they equal? - if (isFeasible) { + if (stateEqual) { // Perform the store. ExplodedNodeSet TmpStore; Engine.EvalStore(TmpStore, theValueExpr, N, stateEqual, location, @@ -1359,11 +1324,7 @@ static bool EvalOSAtomicCompareAndSwap(ExplodedNodeSet& Dst, } // Were they not equal? - isFeasible = false; - const GRState *stateNotEqual = StateMgr.Assume(stateLoad, Cmp, false, - isFeasible); - - if (isFeasible) { + if (const GRState *stateNotEqual = stateLoad->assume(Cmp, false)) { SVal Res = Engine.getValueManager().makeTruthVal(false, CE->getType()); Engine.MakeNode(Dst, CE, N, Engine.BindExpr(stateNotEqual, CE, Res)); } @@ -1659,19 +1620,15 @@ void GRExprEngine::EvalEagerlyAssume(NodeSet &Dst, NodeSet &Src, Expr *Ex) { SVal V = GetSVal(state, Ex); if (isa(V)) { // First assume that the condition is true. - bool isFeasible = false; - const GRState *stateTrue = Assume(state, V, true, isFeasible); - if (isFeasible) { - stateTrue = BindExpr(stateTrue, Ex, MakeConstantVal(1U, Ex)); + if (const GRState *stateTrue = state->assume(V, true)) { + stateTrue = stateTrue->bindExpr(Ex, MakeConstantVal(1U, Ex)); Dst.Add(Builder->generateNode(PostStmtCustom(Ex, &EagerlyAssumeTag), stateTrue, Pred)); } // Next, assume that the condition is false. - isFeasible = false; - const GRState *stateFalse = Assume(state, V, false, isFeasible); - if (isFeasible) { - stateFalse = BindExpr(stateFalse, Ex, MakeConstantVal(0U, Ex)); + if (const GRState *stateFalse = state->assume(V, false)) { + stateFalse = stateFalse->bindExpr(Ex, MakeConstantVal(0U, Ex)); Dst.Add(Builder->generateNode(PostStmtCustom(Ex, &EagerlyAssumeTag), stateFalse, Pred)); } @@ -1873,14 +1830,12 @@ void GRExprEngine::VisitObjCMessageExprDispatchHelper(ObjCMessageExpr* ME, } // "Assume" that the receiver is not NULL. - bool isFeasibleNotNull = false; - const GRState *StNotNull = Assume(state, L, true, isFeasibleNotNull); + const GRState *StNotNull = state->assume(L, true); // "Assume" that the receiver is NULL. - bool isFeasibleNull = false; - const GRState *StNull = Assume(state, L, false, isFeasibleNull); + const GRState *StNull = state->assume(L, false); - if (isFeasibleNull) { + if (StNull) { QualType RetTy = ME->getType(); // Check if the receiver was nil and the return value a struct. @@ -1894,7 +1849,7 @@ void GRExprEngine::VisitObjCMessageExprDispatchHelper(ObjCMessageExpr* ME, // garbage. if (NodeTy* N = Builder->generateNode(ME, StNull, Pred)) { N->markAsSink(); - if (isFeasibleNotNull) + if (StNotNull) NilReceiverStructRetImplicit.insert(N); else NilReceiverStructRetExplicit.insert(N); @@ -1913,13 +1868,13 @@ void GRExprEngine::VisitObjCMessageExprDispatchHelper(ObjCMessageExpr* ME, if(voidPtrSize < returnTypeSize) { if (NodeTy* N = Builder->generateNode(ME, StNull, Pred)) { N->markAsSink(); - if(isFeasibleNotNull) + if(StNotNull) NilReceiverLargerThanVoidPtrRetImplicit.insert(N); else NilReceiverLargerThanVoidPtrRetExplicit.insert(N); } } - else if (!isFeasibleNotNull) { + else if (!StNotNull) { // Handle the safe cases where the return value is 0 if the // receiver is nil. // @@ -2266,21 +2221,20 @@ void GRExprEngine::VisitDeclStmt(DeclStmt* DS, NodeTy* Pred, NodeSet& Dst) { continue; } - bool isFeasibleZero = false; - const GRState* ZeroSt = Assume(state, Size, false, isFeasibleZero); + const GRState* zeroState = state->assume(Size, false); + state = state->assume(Size, true); - bool isFeasibleNotZero = false; - state = Assume(state, Size, true, isFeasibleNotZero); - - if (isFeasibleZero) { - if (NodeTy* N = Builder->generateNode(DS, ZeroSt, Pred)) { + if (zeroState) { + if (NodeTy* N = Builder->generateNode(DS, zeroState, Pred)) { N->markAsSink(); - if (isFeasibleNotZero) ImplicitBadSizedVLA.insert(N); - else ExplicitBadSizedVLA.insert(N); + if (state) + ImplicitBadSizedVLA.insert(N); + else + ExplicitBadSizedVLA.insert(N); } } - if (!isFeasibleNotZero) + if (!state) continue; } @@ -2697,23 +2651,20 @@ void GRExprEngine::VisitUnaryOperator(UnaryOperator* U, NodeTy* Pred, ValMgr.makeZeroVal(U->getType()), getContext().IntTy); - bool isFeasible = false; - Assume(state, Constraint, true, isFeasible); - if (!isFeasible) { + if (!state->assume(Constraint, true)) { // It isn't feasible for the original value to be null. // Propagate this constraint. Constraint = EvalBinOp(state, BinaryOperator::EQ, Result, ValMgr.makeZeroVal(U->getType()), getContext().IntTy); - bool isFeasible = false; - state = Assume(state, Constraint, false, isFeasible); - assert(isFeasible && state); + state = state->assume(Constraint, false); + assert(state); } } } - state = BindExpr(state, U, U->isPostfix() ? V2 : Result); + state = state->bindExpr(U, U->isPostfix() ? V2 : Result); // Perform the store. EvalStore(Dst, U, *I2, state, V1, Result); @@ -2861,29 +2812,24 @@ const GRState* GRExprEngine::CheckDivideZero(Expr* Ex, const GRState* state, // Check for divide/remainder-by-zero. // First, "assume" that the denominator is 0 or undefined. - - bool isFeasibleZero = false; - const GRState* ZeroSt = Assume(state, Denom, false, isFeasibleZero); + const GRState* zeroState = state->assume(Denom, false); // Second, "assume" that the denominator cannot be 0. + state = state->assume(Denom, true); - bool isFeasibleNotZero = false; - state = Assume(state, Denom, true, isFeasibleNotZero); - - // Create the node for the divide-by-zero (if it occurred). - - if (isFeasibleZero) - if (NodeTy* DivZeroNode = Builder->generateNode(Ex, ZeroSt, Pred)) { + // Create the node for the divide-by-zero (if it occurred). + if (zeroState) + if (NodeTy* DivZeroNode = Builder->generateNode(Ex, zeroState, Pred)) { DivZeroNode->markAsSink(); - if (isFeasibleNotZero) + if (state) ImplicitBadDivides.insert(DivZeroNode); else ExplicitBadDivides.insert(DivZeroNode); } - return isFeasibleNotZero ? state : 0; + return state; } void GRExprEngine::VisitBinaryOperator(BinaryOperator* B, diff --git a/lib/Analysis/GRExprEngineInternalChecks.cpp b/lib/Analysis/GRExprEngineInternalChecks.cpp index a0de13f702..838cb9867b 100644 --- a/lib/Analysis/GRExprEngineInternalChecks.cpp +++ b/lib/Analysis/GRExprEngineInternalChecks.cpp @@ -819,24 +819,15 @@ public: // Check if in the previous state it was feasible for this constraint // to *not* be true. - - GRStateManager &StateMgr = BRC.getStateManager(); - bool isFeasible = false; - if (StateMgr.Assume(PrevN->getState(), Constraint, !Assumption, - isFeasible)) { - assert(isFeasible); // Eventually we don't need 'isFeasible'. + if (PrevN->getState()->assume(Constraint, !Assumption)) { isSatisfied = true; // As a sanity check, make sure that the negation of the constraint // was infeasible in the current state. If it is feasible, we somehow // missed the transition point. - isFeasible = false; - if (StateMgr.Assume(N->getState(), Constraint, !Assumption, - isFeasible)) { - assert(isFeasible); + if (N->getState()->assume(Constraint, !Assumption)) return NULL; - } // We found the transition point for the constraint. We now need to // pretty-print the constraint. (work-in-progress) diff --git a/lib/Analysis/RangeConstraintManager.cpp b/lib/Analysis/RangeConstraintManager.cpp index 89f3a716d2..3b4d0c4122 100644 --- a/lib/Analysis/RangeConstraintManager.cpp +++ b/lib/Analysis/RangeConstraintManager.cpp @@ -239,22 +239,22 @@ public: : SimpleConstraintManager(statemgr) {} const GRState* AssumeSymNE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const llvm::APSInt& V); const GRState* AssumeSymEQ(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const llvm::APSInt& V); const GRState* AssumeSymLT(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const llvm::APSInt& V); const GRState* AssumeSymGT(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const llvm::APSInt& V); const GRState* AssumeSymGE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const llvm::APSInt& V); const GRState* AssumeSymLE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, bool& isFeasible); + const llvm::APSInt& V); const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) const; @@ -327,10 +327,9 @@ RangeConstraintManager::GetRange(const GRState *state, SymbolRef sym) { #define AssumeX(OP)\ const GRState*\ RangeConstraintManager::AssumeSym ## OP(const GRState* state, SymbolRef sym,\ - const llvm::APSInt& V, bool& isFeasible){\ + const llvm::APSInt& V){\ const RangeSet& R = GetRange(state, sym).Add##OP(state->getBasicVals(), F, V);\ - isFeasible = !R.isEmpty();\ - return isFeasible ? state->set(sym, R) : 0;\ + return !R.isEmpty() ? state->set(sym, R) : NULL;\ } AssumeX(EQ) diff --git a/lib/Analysis/SimpleConstraintManager.cpp b/lib/Analysis/SimpleConstraintManager.cpp index f79dba0cc5..6e858891fa 100644 --- a/lib/Analysis/SimpleConstraintManager.cpp +++ b/lib/Analysis/SimpleConstraintManager.cpp @@ -55,60 +55,55 @@ bool SimpleConstraintManager::canReasonAbout(SVal X) const { return true; } -const GRState* -SimpleConstraintManager::Assume(const GRState* St, SVal Cond, bool Assumption, - bool& isFeasible) { +const GRState *SimpleConstraintManager::Assume(const GRState *state, + SVal Cond, bool Assumption) { if (Cond.isUnknown()) { - isFeasible = true; - return St; + return state; } if (isa(Cond)) - return Assume(St, cast(Cond), Assumption, isFeasible); + return Assume(state, cast(Cond), Assumption); else - return Assume(St, cast(Cond), Assumption, isFeasible); + return Assume(state, cast(Cond), Assumption); } -const GRState* -SimpleConstraintManager::Assume(const GRState* St, Loc Cond, bool Assumption, - bool& isFeasible) { - St = AssumeAux(St, Cond, Assumption, isFeasible); - - if (!isFeasible) - return St; - +const GRState *SimpleConstraintManager::Assume(const GRState *state, Loc Cond, + bool Assumption) { + + state = AssumeAux(state, Cond, Assumption); + // EvalAssume is used to call into the GRTransferFunction object to perform // any checker-specific update of the state based on this assumption being - // true or false. - return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption, - isFeasible); + // true or false. + return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption) + : NULL; } -const GRState* -SimpleConstraintManager::AssumeAux(const GRState* St, Loc Cond, bool Assumption, - bool& isFeasible) { - BasicValueFactory& BasicVals = StateMgr.getBasicVals(); +const GRState *SimpleConstraintManager::AssumeAux(const GRState *state, + Loc Cond, bool Assumption) { + + BasicValueFactory &BasicVals = state->getBasicVals(); switch (Cond.getSubKind()) { default: assert (false && "'Assume' not implemented for this Loc."); - return St; + return state; case loc::MemRegionKind: { // FIXME: Should this go into the storemanager? - const MemRegion* R = cast(Cond).getRegion(); - const SubRegion* SubR = dyn_cast(R); + const MemRegion *R = cast(Cond).getRegion(); + const SubRegion *SubR = dyn_cast(R); while (SubR) { // FIXME: now we only find the first symbolic region. - if (const SymbolicRegion* SymR = dyn_cast(SubR)) { + if (const SymbolicRegion *SymR = dyn_cast(SubR)) { if (Assumption) - return AssumeSymNE(St, SymR->getSymbol(), - BasicVals.getZeroWithPtrWidth(), isFeasible); + return AssumeSymNE(state, SymR->getSymbol(), + BasicVals.getZeroWithPtrWidth()); else - return AssumeSymEQ(St, SymR->getSymbol(), - BasicVals.getZeroWithPtrWidth(), isFeasible); + return AssumeSymEQ(state, SymR->getSymbol(), + BasicVals.getZeroWithPtrWidth()); } SubR = dyn_cast(SubR->getSuperRegion()); } @@ -117,43 +112,42 @@ SimpleConstraintManager::AssumeAux(const GRState* St, Loc Cond, bool Assumption, } case loc::GotoLabelKind: - isFeasible = Assumption; - return St; + return Assumption ? state : NULL; case loc::ConcreteIntKind: { - bool b = cast(Cond).getValue() != 0; - isFeasible = b ? Assumption : !Assumption; - return St; + bool b = cast(Cond).getValue() != 0; + bool isFeasible = b ? Assumption : !Assumption; + return isFeasible ? state : NULL; } } // end switch } -const GRState* -SimpleConstraintManager::Assume(const GRState* St, NonLoc Cond, bool Assumption, - bool& isFeasible) { - St = AssumeAux(St, Cond, Assumption, isFeasible); - - if (!isFeasible) - return St; - +const GRState *SimpleConstraintManager::Assume(const GRState *state, + NonLoc Cond, + bool Assumption) { + + state = AssumeAux(state, Cond, Assumption); + // EvalAssume is used to call into the GRTransferFunction object to perform // any checker-specific update of the state based on this assumption being - // true or false. - return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption, - isFeasible); + // true or false. + return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption) + : NULL; } -const GRState* -SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond, - bool Assumption, bool& isFeasible) { +const GRState *SimpleConstraintManager::AssumeAux(const GRState *state, + NonLoc Cond, + bool Assumption) { + // We cannot reason about SymIntExpr and SymSymExpr. if (!canReasonAbout(Cond)) { - isFeasible = true; - return St; + // Just return the current state indicating that the path is feasible. + // This may be an over-approximation of what is possible. + return state; } - BasicValueFactory& BasicVals = StateMgr.getBasicVals(); - SymbolManager& SymMgr = StateMgr.getSymbolManager(); + BasicValueFactory &BasicVals = state->getBasicVals(); + SymbolManager &SymMgr = state->getSymbolManager(); switch (Cond.getSubKind()) { default: @@ -162,38 +156,38 @@ SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond, case nonloc::SymbolValKind: { nonloc::SymbolVal& SV = cast(Cond); SymbolRef sym = SV.getSymbol(); - QualType T = SymMgr.getType(sym); - - if (Assumption) - return AssumeSymNE(St, sym, BasicVals.getValue(0, T), isFeasible); - else - return AssumeSymEQ(St, sym, BasicVals.getValue(0, T), isFeasible); + QualType T = SymMgr.getType(sym); + const llvm::APSInt &zero = BasicVals.getValue(0, T); + + return Assumption ? AssumeSymNE(state, sym, zero) + : AssumeSymEQ(state, sym, zero); } case nonloc::SymExprValKind: { nonloc::SymExprVal V = cast(Cond); if (const SymIntExpr *SE = dyn_cast(V.getSymbolicExpression())) - return AssumeSymInt(St, Assumption, SE, isFeasible); + return AssumeSymInt(state, Assumption, SE); - isFeasible = true; - return St; + // For all other symbolic expressions, over-approximate and consider + // the constraint feasible. + return state; } case nonloc::ConcreteIntKind: { bool b = cast(Cond).getValue() != 0; - isFeasible = b ? Assumption : !Assumption; - return St; + bool isFeasible = b ? Assumption : !Assumption; + return isFeasible ? state : NULL; } case nonloc::LocAsIntegerKind: - return AssumeAux(St, cast(Cond).getLoc(), - Assumption, isFeasible); + return AssumeAux(state, cast(Cond).getLoc(), + Assumption); } // end switch } -const GRState* -SimpleConstraintManager::AssumeSymInt(const GRState* St, bool Assumption, - const SymIntExpr *SE, bool& isFeasible) { +const GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state, + bool Assumption, + const SymIntExpr *SE) { // Here we assume that LHS is a symbol. This is consistent with the @@ -203,45 +197,42 @@ SimpleConstraintManager::AssumeSymInt(const GRState* St, bool Assumption, switch (SE->getOpcode()) { default: - // No logic yet for other operators. - isFeasible = true; - return St; + // No logic yet for other operators. Assume the constraint is feasible. + return state; case BinaryOperator::EQ: - return Assumption ? AssumeSymEQ(St, Sym, Int, isFeasible) - : AssumeSymNE(St, Sym, Int, isFeasible); + return Assumption ? AssumeSymEQ(state, Sym, Int) + : AssumeSymNE(state, Sym, Int); case BinaryOperator::NE: - return Assumption ? AssumeSymNE(St, Sym, Int, isFeasible) - : AssumeSymEQ(St, Sym, Int, isFeasible); - + return Assumption ? AssumeSymNE(state, Sym, Int) + : AssumeSymEQ(state, Sym, Int); case BinaryOperator::GT: - return Assumption ? AssumeSymGT(St, Sym, Int, isFeasible) - : AssumeSymLE(St, Sym, Int, isFeasible); + return Assumption ? AssumeSymGT(state, Sym, Int) + : AssumeSymLE(state, Sym, Int); case BinaryOperator::GE: - return Assumption ? AssumeSymGE(St, Sym, Int, isFeasible) - : AssumeSymLT(St, Sym, Int, isFeasible); + return Assumption ? AssumeSymGE(state, Sym, Int) + : AssumeSymLT(state, Sym, Int); case BinaryOperator::LT: - return Assumption ? AssumeSymLT(St, Sym, Int, isFeasible) - : AssumeSymGE(St, Sym, Int, isFeasible); + return Assumption ? AssumeSymLT(state, Sym, Int) + : AssumeSymGE(state, Sym, Int); case BinaryOperator::LE: - return Assumption ? AssumeSymLE(St, Sym, Int, isFeasible) - : AssumeSymGT(St, Sym, Int, isFeasible); + return Assumption ? AssumeSymLE(state, Sym, Int) + : AssumeSymGT(state, Sym, Int); } // end switch } -const GRState* -SimpleConstraintManager::AssumeInBound(const GRState* St, SVal Idx, - SVal UpperBound, bool Assumption, - bool& isFeasible) { +const GRState *SimpleConstraintManager::AssumeInBound(const GRState *state, + SVal Idx, + SVal UpperBound, + bool Assumption) { + // Only support ConcreteInt for now. - if (!(isa(Idx) && isa(UpperBound))){ - isFeasible = true; - return St; - } + if (!(isa(Idx) && isa(UpperBound))) + return state; const llvm::APSInt& Zero = getBasicVals().getZeroWithPtrWidth(false); llvm::APSInt IdxV = cast(Idx).getValue(); @@ -254,10 +245,8 @@ SimpleConstraintManager::AssumeInBound(const GRState* St, SVal Idx, UBV.extend(Zero.getBitWidth()); bool InBound = (Zero <= IdxV) && (IdxV < UBV); - - isFeasible = Assumption ? InBound : !InBound; - - return St; + bool isFeasible = Assumption ? InBound : !InBound; + return isFeasible ? state : NULL; } } // end of namespace clang diff --git a/lib/Analysis/SimpleConstraintManager.h b/lib/Analysis/SimpleConstraintManager.h index fb41e2f1da..bd18b6af93 100644 --- a/lib/Analysis/SimpleConstraintManager.h +++ b/lib/Analysis/SimpleConstraintManager.h @@ -29,50 +29,58 @@ public: bool canReasonAbout(SVal X) const; - virtual const GRState* Assume(const GRState* St, SVal Cond, bool Assumption, - bool& isFeasible); + virtual const GRState *Assume(const GRState *state, SVal Cond, + bool Assumption); - const GRState* Assume(const GRState* St, Loc Cond, bool Assumption, - bool& isFeasible); - - const GRState* AssumeAux(const GRState* St, Loc Cond,bool Assumption, - bool& isFeasible); - - const GRState* Assume(const GRState* St, NonLoc Cond, bool Assumption, - bool& isFeasible); - - const GRState* AssumeAux(const GRState* St, NonLoc Cond, bool Assumption, - bool& isFeasible); + //===------------------------------------------------------------------===// + // Common implementation for the interface provided by ConstraintManager. + //===------------------------------------------------------------------===// + + const GRState *Assume(const GRState *state, Loc Cond, bool Assumption); - const GRState* AssumeSymInt(const GRState* St, bool Assumption, - const SymIntExpr *SE, bool& isFeasible); + const GRState *Assume(const GRState *state, NonLoc Cond, bool Assumption); - virtual const GRState* AssumeSymNE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, - bool& isFeasible) = 0; + const GRState *AssumeSymInt(const GRState *state, bool Assumption, + const SymIntExpr *SE); + + const GRState *AssumeInBound(const GRState *state, SVal Idx, SVal UpperBound, + bool Assumption); + +protected: + + //===------------------------------------------------------------------===// + // Interface that subclasses must implement. + //===------------------------------------------------------------------===// + + virtual const GRState *AssumeSymNE(const GRState *state, SymbolRef sym, + const llvm::APSInt& V) = 0; - virtual const GRState* AssumeSymEQ(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, - bool& isFeasible) = 0; + virtual const GRState *AssumeSymEQ(const GRState *state, SymbolRef sym, + const llvm::APSInt& V) = 0; - virtual const GRState* AssumeSymLT(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, - bool& isFeasible) = 0; + virtual const GRState *AssumeSymLT(const GRState *state, SymbolRef sym, + const llvm::APSInt& V) = 0; - virtual const GRState* AssumeSymGT(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, - bool& isFeasible) = 0; + virtual const GRState *AssumeSymGT(const GRState *state, SymbolRef sym, + const llvm::APSInt& V) = 0; - virtual const GRState* AssumeSymLE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, - bool& isFeasible) = 0; + virtual const GRState *AssumeSymLE(const GRState *state, SymbolRef sym, + const llvm::APSInt& V) = 0; - virtual const GRState* AssumeSymGE(const GRState* St, SymbolRef sym, - const llvm::APSInt& V, - bool& isFeasible) = 0; + virtual const GRState *AssumeSymGE(const GRState *state, SymbolRef sym, + const llvm::APSInt& V) = 0; + + //===------------------------------------------------------------------===// + // Internal implementation. + //===------------------------------------------------------------------===// + + const GRState *AssumeAux(const GRState *state, Loc Cond,bool Assumption); + + const GRState *AssumeAux(const GRState *state, NonLoc Cond, bool Assumption); - const GRState* AssumeInBound(const GRState* St, SVal Idx, SVal UpperBound, - bool Assumption, bool& isFeasible); + //===------------------------------------------------------------------===// + // FIXME: These can probably be removed now. + //===------------------------------------------------------------------===// private: BasicValueFactory& getBasicVals() { return StateMgr.getBasicVals(); } -- 2.40.0