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
diff --git a/lib/Analysis/BasicConstraintManager.cpp b/lib/Analysis/BasicConstraintManager.cpp
index 1f907ba..7bd22fd 100644
--- a/lib/Analysis/BasicConstraintManager.cpp
+++ b/lib/Analysis/BasicConstraintManager.cpp
@@ -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:";