[cfe-commits] r73731 - in /cfe/trunk: include/clang/Analysis/PathSensitive/ConstraintManager.h include/clang/Analysis/PathSensitive/GRExprEngine.h include/clang/Analysis/PathSensitive/GRState.h include/clang/Analysis/PathSensitive/GRTransferFuncs.h lib/Analysis/BasicConstraintManager.cpp lib/Analysis/CFRefCount.cpp lib/Analysis/GRExprEngine.cpp lib/Analysis/GRExprEngineInternalChecks.cpp lib/Analysis/RangeConstraintManager.cpp lib/Analysis/SimpleConstraintManager.cpp lib/Analysis/SimpleConstraintManager.h
Ted Kremenek
kremenek at apple.com
Thu Jun 18 15:57:15 PDT 2009
Author: kremenek
Date: Thu Jun 18 17:57:13 2009
New Revision: 73731
URL: http://llvm.org/viewvc/llvm-project?rev=73731&view=rev
Log:
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.
Modified:
cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h
cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h
cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h
cfe/trunk/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
cfe/trunk/lib/Analysis/BasicConstraintManager.cpp
cfe/trunk/lib/Analysis/CFRefCount.cpp
cfe/trunk/lib/Analysis/GRExprEngine.cpp
cfe/trunk/lib/Analysis/GRExprEngineInternalChecks.cpp
cfe/trunk/lib/Analysis/RangeConstraintManager.cpp
cfe/trunk/lib/Analysis/SimpleConstraintManager.cpp
cfe/trunk/lib/Analysis/SimpleConstraintManager.h
Modified: cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h Thu Jun 18 17:57:13 2009
@@ -30,26 +30,25 @@
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
Modified: cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h Thu Jun 18 17:57:13 2009
@@ -520,24 +520,7 @@
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,
Modified: cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h Thu Jun 18 17:57:13 2009
@@ -158,6 +158,49 @@
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 @@
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 @@
template <typename CB> CB scanReachableSymbols(SVal val) const;
- // Trait based GDM dispatch.
+ //==---------------------------------------------------------------------==//
+ // Accessing the Generic Data Map (GDM).
+ //==---------------------------------------------------------------------==//
+
void* const* FindGDM(void* K) const;
template<typename T>
@@ -671,56 +719,6 @@
return GRStateTrait<T>::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 @@
// 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 @@
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 @@
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<typename T>
const GRState *GRState::add(typename GRStateTrait<T>::key_type K) const {
Modified: cfe/trunk/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/GRTransferFuncs.h?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/GRTransferFuncs.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/GRTransferFuncs.h Thu Jun 18 17:57:13 2009
@@ -110,11 +110,9 @@
// 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;
}
};
Modified: cfe/trunk/lib/Analysis/BasicConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/BasicConstraintManager.cpp?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/BasicConstraintManager.cpp (original)
+++ cfe/trunk/lib/Analysis/BasicConstraintManager.cpp Thu Jun 18 17:57:13 2009
@@ -53,37 +53,37 @@
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 @@
}
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 @@
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 @@
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 @@
return state->set<ConstNotEq>(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<ConstEq>(sym);
+ const ConstEqTy::data_type* T = state->get<ConstEq>(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<ConstNotEq>(sym);
+ const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(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<ConstEq>(sym);
+ const ConstEqTy::data_type* T = state->get<ConstEq>(sym);
// See if V is present in the EQ-set.
return T ? **T == V : false;
}
@@ -296,11 +280,11 @@
return state->set<ConstNotEq>(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<ConstEq>();
+ ConstEqTy CE = state->get<ConstEq>();
if (!CE.isEmpty()) {
Out << nl << sep << "'==' constraints:";
@@ -314,7 +298,7 @@
// Print != constraints.
- ConstNotEqTy CNE = St->get<ConstNotEq>();
+ ConstNotEqTy CNE = state->get<ConstNotEq>();
if (!CNE.isEmpty()) {
Out << nl << sep << "'!=' constraints:";
Modified: cfe/trunk/lib/Analysis/CFRefCount.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/CFRefCount.cpp?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/CFRefCount.cpp (original)
+++ cfe/trunk/lib/Analysis/CFRefCount.cpp Thu Jun 18 17:57:13 2009
@@ -1953,9 +1953,8 @@
// 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 @@
// 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 @@
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());
}
Modified: cfe/trunk/lib/Analysis/GRExprEngine.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/GRExprEngine.cpp?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/GRExprEngine.cpp (original)
+++ cfe/trunk/lib/Analysis/GRExprEngine.cpp Thu Jun 18 17:57:13 2009
@@ -181,10 +181,9 @@
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 @@
}
// 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 @@
}
const GRState* DefaultSt = state;
- bool DefaultFeasible = false;
+ bool defaultIsFeasible = false;
for (iterator I = builder.begin(), EI = builder.end(); I != EI; ++I) {
CaseStmt* Case = cast<CaseStmt>(I.getCase());
@@ -846,11 +837,8 @@
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 @@
// 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 @@
// 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 @@
// 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 @@
Loc LV = cast<Loc>(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<GRState::NullDerefTag>(PersistentLV);
@@ -1208,17 +1179,15 @@
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<loc::MemRegionVal>(LV)) {
@@ -1230,15 +1199,12 @@
SVal NumElements = getStoreManager().getSizeInElements(StNotNull,
ER->getSuperRegion());
- bool isFeasibleInBound = false;
- const GRState* StInBound = AssumeInBound(StNotNull, Idx, NumElements,
- true, isFeasibleInBound);
-
- bool isFeasibleOutBound = false;
- const GRState* StOutBound = AssumeInBound(StNotNull, Idx, NumElements,
- false, isFeasibleOutBound);
+ const GRState * StInBound = StNotNull->assumeInBound(Idx, NumElements,
+ true);
+ const GRState* StOutBound = StNotNull->assumeInBound(Idx, NumElements,
+ false);
- if (isFeasibleOutBound) {
+ if (StOutBound) {
// Report warning. Make sink node manually.
NodeTy* OOBNode =
Builder->generateNode(Ex, StOutBound, Pred,
@@ -1247,16 +1213,16 @@
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 @@
ExplodedNode<GRState> *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<GRState> TmpStore;
Engine.EvalStore(TmpStore, theValueExpr, N, stateEqual, location,
@@ -1359,11 +1324,7 @@
}
// 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 @@
SVal V = GetSVal(state, Ex);
if (isa<nonloc::SymExprVal>(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 @@
}
// "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 @@
// 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 @@
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 @@
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 @@
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 @@
// 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,
Modified: cfe/trunk/lib/Analysis/GRExprEngineInternalChecks.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/GRExprEngineInternalChecks.cpp?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/GRExprEngineInternalChecks.cpp (original)
+++ cfe/trunk/lib/Analysis/GRExprEngineInternalChecks.cpp Thu Jun 18 17:57:13 2009
@@ -819,24 +819,15 @@
// 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)
Modified: cfe/trunk/lib/Analysis/RangeConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/RangeConstraintManager.cpp?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/RangeConstraintManager.cpp (original)
+++ cfe/trunk/lib/Analysis/RangeConstraintManager.cpp Thu Jun 18 17:57:13 2009
@@ -239,22 +239,22 @@
: 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 @@
#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<ConstraintRange>(sym, R) : 0;\
+ return !R.isEmpty() ? state->set<ConstraintRange>(sym, R) : NULL;\
}
AssumeX(EQ)
Modified: cfe/trunk/lib/Analysis/SimpleConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/SimpleConstraintManager.cpp?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/SimpleConstraintManager.cpp (original)
+++ cfe/trunk/lib/Analysis/SimpleConstraintManager.cpp Thu Jun 18 17:57:13 2009
@@ -55,60 +55,55 @@
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<NonLoc>(Cond))
- return Assume(St, cast<NonLoc>(Cond), Assumption, isFeasible);
+ return Assume(state, cast<NonLoc>(Cond), Assumption);
else
- return Assume(St, cast<Loc>(Cond), Assumption, isFeasible);
+ return Assume(state, cast<Loc>(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<loc::MemRegionVal>(Cond).getRegion();
- const SubRegion* SubR = dyn_cast<SubRegion>(R);
+ const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
+ const SubRegion *SubR = dyn_cast<SubRegion>(R);
while (SubR) {
// FIXME: now we only find the first symbolic region.
- if (const SymbolicRegion* SymR = dyn_cast<SymbolicRegion>(SubR)) {
+ if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(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<SubRegion>(SubR->getSuperRegion());
}
@@ -117,43 +112,42 @@
}
case loc::GotoLabelKind:
- isFeasible = Assumption;
- return St;
+ return Assumption ? state : NULL;
case loc::ConcreteIntKind: {
- bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
- isFeasible = b ? Assumption : !Assumption;
- return St;
+ bool b = cast<loc::ConcreteInt>(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 @@
case nonloc::SymbolValKind: {
nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(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<nonloc::SymExprVal>(Cond);
if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(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<nonloc::ConcreteInt>(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<nonloc::LocAsInteger>(Cond).getLoc(),
- Assumption, isFeasible);
+ return AssumeAux(state, cast<nonloc::LocAsInteger>(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 @@
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<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))){
- isFeasible = true;
- return St;
- }
+ if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound)))
+ return state;
const llvm::APSInt& Zero = getBasicVals().getZeroWithPtrWidth(false);
llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue();
@@ -254,10 +245,8 @@
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
Modified: cfe/trunk/lib/Analysis/SimpleConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/SimpleConstraintManager.h?rev=73731&r1=73730&r2=73731&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/SimpleConstraintManager.h (original)
+++ cfe/trunk/lib/Analysis/SimpleConstraintManager.h Thu Jun 18 17:57:13 2009
@@ -29,50 +29,58 @@
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(); }
More information about the cfe-commits
mailing list