[cfe-commits] r55412 - in /cfe/trunk: include/clang/Analysis/PathSensitive/BasicStore.h include/clang/Analysis/PathSensitive/ConstraintManager.h include/clang/Analysis/PathSensitive/GRState.h lib/Analysis/BasicConstraintManager.cpp lib/Analysis/GRExprEngine.cpp lib/Analysis/GRState.cpp
Zhongxing Xu
xuzhongxing at gmail.com
Wed Aug 27 07:03:35 PDT 2008
Author: zhongxingxu
Date: Wed Aug 27 09:03:33 2008
New Revision: 55412
URL: http://llvm.org/viewvc/llvm-project?rev=55412&view=rev
Log:
Refactor Assume logic into a separate class ConstraintManager.
Added:
cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h
cfe/trunk/lib/Analysis/BasicConstraintManager.cpp
Modified:
cfe/trunk/include/clang/Analysis/PathSensitive/BasicStore.h
cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h
cfe/trunk/lib/Analysis/GRExprEngine.cpp
cfe/trunk/lib/Analysis/GRState.cpp
Modified: cfe/trunk/include/clang/Analysis/PathSensitive/BasicStore.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/BasicStore.h?rev=55412&r1=55411&r2=55412&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/BasicStore.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/BasicStore.h Wed Aug 27 09:03:33 2008
@@ -17,7 +17,7 @@
#include "clang/Analysis/PathSensitive/Store.h"
namespace llvm {
- class llvm::BumpPtrAllocator;
+ class BumpPtrAllocator;
class ASTContext;
}
Added: cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h?rev=55412&view=auto
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h (added)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/ConstraintManager.h Wed Aug 27 09:03:33 2008
@@ -0,0 +1,20 @@
+#ifndef CONSTRAINT_MANAGER_H
+#define CONSTRAINT_MANAGER_H
+
+namespace clang {
+
+class GRState;
+class GRStateManager;
+class RVal;
+
+class ConstraintManager {
+public:
+ virtual const GRState* Assume(const GRState* St, RVal Cond, bool Assumption,
+ bool& isFeasible) = 0;
+};
+
+ConstraintManager* CreateBasicConstraintManager(GRStateManager& statemgr);
+
+} // end clang namespace
+
+#endif
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=55412&r1=55411&r2=55412&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h Wed Aug 27 09:03:33 2008
@@ -18,6 +18,7 @@
#include "clang/Analysis/PathSensitive/Environment.h"
#include "clang/Analysis/PathSensitive/Store.h"
+#include "clang/Analysis/PathSensitive/ConstraintManager.h"
#include "clang/Analysis/PathSensitive/RValues.h"
#include "clang/Analysis/PathSensitive/GRCoreEngine.h"
#include "clang/AST/Expr.h"
@@ -233,6 +234,7 @@
private:
EnvironmentManager EnvMgr;
llvm::OwningPtr<StoreManager> StMgr;
+ llvm::OwningPtr<ConstraintManager> ConstraintMgr;
GRState::IntSetTy::Factory ISetFactory;
GRState::GenericDataMap::Factory GDMFactory;
@@ -286,9 +288,12 @@
const GRState* BindVar(const GRState* St, VarDecl* D, RVal V) {
return SetRVal(St, lval::DeclVal(D), V);
}
+
+ typedef ConstraintManager* (*ConstraintManagerCreater)(GRStateManager&);
public:
GRStateManager(ASTContext& Ctx, StoreManager* stmgr,
+ ConstraintManagerCreater CreateConstraintManager,
llvm::BumpPtrAllocator& alloc, CFG& c, LiveVariables& L)
: EnvMgr(alloc),
StMgr(stmgr),
@@ -298,7 +303,9 @@
SymMgr(alloc),
Alloc(alloc),
cfg(c),
- Liveness(L) {}
+ Liveness(L) {
+ ConstraintMgr.reset((*CreateConstraintManager)(*this));
+ }
~GRStateManager();
@@ -309,6 +316,7 @@
const BasicValueFactory& getBasicVals() const { return BasicVals; }
SymbolManager& getSymbolManager() { return SymMgr; }
LiveVariables& getLiveVariables() { return Liveness; }
+ llvm::BumpPtrAllocator& getAllocator() { return Alloc; }
typedef StoreManager::DeadSymbolsTy DeadSymbolsTy;
@@ -440,52 +448,8 @@
// Assumption logic.
const GRState* Assume(const GRState* St, RVal Cond, bool Assumption,
bool& isFeasible) {
-
- if (Cond.isUnknown()) {
- isFeasible = true;
- return St;
- }
-
- if (isa<LVal>(Cond))
- return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
- else
- return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
+ return ConstraintMgr->Assume(St, Cond, Assumption, isFeasible);
}
-
- const GRState* Assume(const GRState* St, LVal Cond, bool Assumption,
- bool& isFeasible);
-
- const GRState* Assume(const GRState* St, NonLVal Cond, bool Assumption,
- bool& isFeasible);
-
-private:
- const GRState* AssumeAux(const GRState* St, LVal Cond, bool Assumption,
- bool& isFeasible);
-
-
- const GRState* AssumeAux(const GRState* St, NonLVal Cond,
- bool Assumption, bool& isFeasible);
-
- const GRState* AssumeSymInt(const GRState* St, bool Assumption,
- const SymIntConstraint& C, bool& isFeasible);
-
- const GRState* AssumeSymNE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymEQ(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymLT(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymLE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymGT(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymGE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
};
//===----------------------------------------------------------------------===//
Added: cfe/trunk/lib/Analysis/BasicConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/BasicConstraintManager.cpp?rev=55412&view=auto
==============================================================================
--- cfe/trunk/lib/Analysis/BasicConstraintManager.cpp (added)
+++ cfe/trunk/lib/Analysis/BasicConstraintManager.cpp Wed Aug 27 09:03:33 2008
@@ -0,0 +1,298 @@
+#include "clang/Analysis/PathSensitive/ConstraintManager.h"
+#include "clang/Analysis/PathSensitive/GRState.h"
+#include "llvm/Support/Compiler.h"
+
+using namespace clang;
+
+namespace {
+
+// BasicConstraintManager only tracks equality and inequality constraints of
+// constants and integer variables.
+class VISIBILITY_HIDDEN BasicConstraintManager : public ConstraintManager {
+ typedef llvm::ImmutableMap<SymbolID, GRState::IntSetTy> ConstNotEqTy;
+ typedef llvm::ImmutableMap<SymbolID, const llvm::APSInt*> ConstEqTy;
+
+ GRStateManager& StateMgr;
+
+public:
+ BasicConstraintManager(GRStateManager& statemgr) : StateMgr(statemgr) {}
+
+ virtual const GRState* Assume(const GRState* St, RVal Cond,
+ bool Assumption, bool& isFeasible);
+
+ const GRState* Assume(const GRState* St, LVal Cond, bool Assumption,
+ bool& isFeasible);
+
+ const GRState* AssumeAux(const GRState* St, LVal Cond,bool Assumption,
+ bool& isFeasible);
+
+ const GRState* Assume(const GRState* St, NonLVal Cond, bool Assumption,
+ bool& isFeasible);
+
+ const GRState* AssumeAux(const GRState* St, NonLVal Cond, bool Assumption,
+ bool& isFeasible);
+
+ const GRState* AssumeSymInt(const GRState* St, bool Assumption,
+ const SymIntConstraint& C, bool& isFeasible);
+
+ const GRState* AssumeSymNE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymEQ(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymLT(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymGT(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymGE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymLE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+ };
+
+} // end anonymous namespace
+
+ConstraintManager* clang::CreateBasicConstraintManager(GRStateManager& StateMgr)
+{
+ return new BasicConstraintManager(StateMgr);
+}
+
+const GRState* BasicConstraintManager::Assume(const GRState* St, RVal Cond,
+ bool Assumption, bool& isFeasible) {
+ if (Cond.isUnknown()) {
+ isFeasible = true;
+ return St;
+ }
+
+ if (isa<NonLVal>(Cond))
+ return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
+ else
+ return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
+}
+
+const GRState* BasicConstraintManager::Assume(const GRState* St, LVal Cond,
+ bool Assumption, bool& isFeasible) {
+ St = AssumeAux(St, Cond, Assumption, isFeasible);
+ // TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
+ return St;
+}
+
+const GRState* BasicConstraintManager::AssumeAux(const GRState* St, LVal Cond,
+ bool Assumption, bool& isFeasible) {
+ BasicValueFactory& BasicVals = StateMgr.getBasicVals();
+
+ switch (Cond.getSubKind()) {
+ default:
+ assert (false && "'Assume' not implemented for this LVal.");
+ return St;
+
+ case lval::SymbolValKind:
+ if (Assumption)
+ return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+ BasicVals.getZeroWithPtrWidth(), isFeasible);
+ else
+ return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+ BasicVals.getZeroWithPtrWidth(), isFeasible);
+
+ case lval::DeclValKind:
+ case lval::FuncValKind:
+ case lval::GotoLabelKind:
+ case lval::StringLiteralValKind:
+ isFeasible = Assumption;
+ return St;
+
+ case lval::FieldOffsetKind:
+ return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
+ Assumption, isFeasible);
+
+ case lval::ArrayOffsetKind:
+ return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
+ Assumption, isFeasible);
+
+ case lval::ConcreteIntKind: {
+ bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
+ isFeasible = b ? Assumption : !Assumption;
+ return St;
+ }
+ } // end switch
+}
+
+const GRState*
+BasicConstraintManager::Assume(const GRState* St, NonLVal Cond, bool Assumption,
+ bool& isFeasible) {
+ St = AssumeAux(St, Cond, Assumption, isFeasible);
+ // TF->EvalAssume() does nothing now.
+ return St;
+}
+
+const GRState*
+BasicConstraintManager::AssumeAux(const GRState* St,NonLVal Cond,
+ bool Assumption, bool& isFeasible) {
+ BasicValueFactory& BasicVals = StateMgr.getBasicVals();
+ SymbolManager& SymMgr = StateMgr.getSymbolManager();
+
+ switch (Cond.getSubKind()) {
+ default:
+ assert(false && "'Assume' not implemented for this NonLVal");
+
+ case nonlval::SymbolValKind: {
+ nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
+ SymbolID sym = SV.getSymbol();
+
+ if (Assumption)
+ return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
+ isFeasible);
+ else
+ return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
+ isFeasible);
+ }
+
+ case nonlval::SymIntConstraintValKind:
+ return
+ AssumeSymInt(St, Assumption,
+ cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
+ isFeasible);
+
+ case nonlval::ConcreteIntKind: {
+ bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
+ isFeasible = b ? Assumption : !Assumption;
+ return St;
+ }
+
+ case nonlval::LValAsIntegerKind:
+ return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
+ Assumption, isFeasible);
+ } // end switch
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymInt(const GRState* St, bool Assumption,
+ const SymIntConstraint& C, bool& isFeasible) {
+
+ switch (C.getOpcode()) {
+ default:
+ // No logic yet for other operators.
+ isFeasible = true;
+ return St;
+
+ case BinaryOperator::EQ:
+ if (Assumption)
+ return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
+ else
+ return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
+
+ case BinaryOperator::NE:
+ if (Assumption)
+ return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
+ else
+ return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
+
+ case BinaryOperator::GE:
+ if (Assumption)
+ return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
+ else
+ return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
+
+ case BinaryOperator::LE:
+ if (Assumption)
+ return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
+ else
+ return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
+ } // end switch
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymNE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+ // First, determine if sym == X, where X != V.
+ if (const llvm::APSInt* X = St->getSymVal(sym)) {
+ isFeasible = (*X != V);
+ return St;
+ }
+
+ // Second, determine if sym != V.
+ if (St->isNotEqual(sym, V)) {
+ isFeasible = true;
+ return St;
+ }
+
+ // If we reach here, sym is not a constant and we don't know if it is != V.
+ // Make that assumption.
+ isFeasible = true;
+ return StateMgr.AddNE(St, sym, V);
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymEQ(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+ // First, determine if sym == X, where X != V.
+ if (const llvm::APSInt* X = St->getSymVal(sym)) {
+ isFeasible = *X == V;
+ return St;
+ }
+
+ // Second, determine if sym != V.
+ if (St->isNotEqual(sym, V)) {
+ isFeasible = false;
+ return St;
+ }
+
+ // If we reach here, sym is not a constant and we don't know if it is == V.
+ // Make that assumption.
+
+ isFeasible = true;
+ return StateMgr.AddEQ(St, sym, V);
+}
+
+// These logic will be handled in another ConstraintManager.
+const GRState*
+BasicConstraintManager::AssumeSymLT(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+
+ // FIXME: For now have assuming x < y be the same as assuming sym != V;
+ return AssumeSymNE(St, sym, V, isFeasible);
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymGT(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+
+ // FIXME: For now have assuming x > y be the same as assuming sym != V;
+ return AssumeSymNE(St, sym, V, isFeasible);
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+
+ // FIXME: Primitive logic for now. Only reject a path if the value of
+ // sym is a constant X and !(X >= V).
+
+ if (const llvm::APSInt* X = St->getSymVal(sym)) {
+ isFeasible = *X >= V;
+ return St;
+ }
+
+ isFeasible = true;
+ return St;
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+
+ // FIXME: Primitive logic for now. Only reject a path if the value of
+ // sym is a constant X and !(X <= V).
+
+ if (const llvm::APSInt* X = St->getSymVal(sym)) {
+ isFeasible = *X <= V;
+ return St;
+ }
+
+ isFeasible = true;
+ return St;
+}
Modified: cfe/trunk/lib/Analysis/GRExprEngine.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/GRExprEngine.cpp?rev=55412&r1=55411&r2=55412&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/GRExprEngine.cpp (original)
+++ cfe/trunk/lib/Analysis/GRExprEngine.cpp Wed Aug 27 09:03:33 2008
@@ -121,7 +121,7 @@
Liveness(L),
Builder(NULL),
StateMgr(G.getContext(), CreateBasicStoreManager(G.getAllocator(), Ctx),
- G.getAllocator(), G.getCFG(), L),
+ CreateBasicConstraintManager, G.getAllocator(), G.getCFG(), L),
SymMgr(StateMgr.getSymbolManager()),
CurrentStmt(NULL),
NSExceptionII(NULL), NSExceptionInstanceRaiseSelectors(NULL),
Modified: cfe/trunk/lib/Analysis/GRState.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/GRState.cpp?rev=55412&r1=55411&r2=55412&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/GRState.cpp (original)
+++ cfe/trunk/lib/Analysis/GRState.cpp Wed Aug 27 09:03:33 2008
@@ -383,241 +383,3 @@
bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
}
-
-//===----------------------------------------------------------------------===//
-// "Assume" logic.
-//===----------------------------------------------------------------------===//
-
-const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
- bool Assumption, bool& isFeasible) {
-
- St = AssumeAux(St, Cond, Assumption, isFeasible);
-
- return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
- : St;
-}
-
-const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
- bool Assumption, bool& isFeasible) {
-
- switch (Cond.getSubKind()) {
- default:
- assert (false && "'Assume' not implemented for this LVal.");
- return St;
-
- case lval::SymbolValKind:
- if (Assumption)
- return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
- BasicVals.getZeroWithPtrWidth(), isFeasible);
- else
- return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
- BasicVals.getZeroWithPtrWidth(), isFeasible);
-
- case lval::DeclValKind:
- case lval::FuncValKind:
- case lval::GotoLabelKind:
- case lval::StringLiteralValKind:
- isFeasible = Assumption;
- return St;
-
- case lval::FieldOffsetKind:
- return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
- Assumption, isFeasible);
-
- case lval::ArrayOffsetKind:
- return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
- Assumption, isFeasible);
-
- case lval::ConcreteIntKind: {
- bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
- isFeasible = b ? Assumption : !Assumption;
- return St;
- }
- }
-}
-
-const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
- bool Assumption, bool& isFeasible) {
-
- St = AssumeAux(St, Cond, Assumption, isFeasible);
-
- return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
- : St;
-}
-
-const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
- bool Assumption, bool& isFeasible) {
- switch (Cond.getSubKind()) {
- default:
- assert (false && "'Assume' not implemented for this NonLVal.");
- return St;
-
-
- case nonlval::SymbolValKind: {
- nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
- SymbolID sym = SV.getSymbol();
-
- if (Assumption)
- return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
- isFeasible);
- else
- return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
- isFeasible);
- }
-
- case nonlval::SymIntConstraintValKind:
- return
- AssumeSymInt(St, Assumption,
- cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
- isFeasible);
-
- case nonlval::ConcreteIntKind: {
- bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
- isFeasible = b ? Assumption : !Assumption;
- return St;
- }
-
- case nonlval::LValAsIntegerKind: {
- return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
- Assumption, isFeasible);
- }
- }
-}
-
-
-
-const GRState* GRStateManager::AssumeSymInt(const GRState* St,
- bool Assumption,
- const SymIntConstraint& C,
- bool& isFeasible) {
-
- switch (C.getOpcode()) {
- default:
- // No logic yet for other operators.
- isFeasible = true;
- return St;
-
- case BinaryOperator::EQ:
- if (Assumption)
- return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
- else
- return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
-
- case BinaryOperator::NE:
- if (Assumption)
- return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
- else
- return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
-
- case BinaryOperator::GE:
- if (Assumption)
- return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
- else
- return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
-
- case BinaryOperator::LE:
- if (Assumption)
- return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
- else
- return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
- }
-}
-
-//===----------------------------------------------------------------------===//
-// FIXME: This should go into a plug-in constraint engine.
-//===----------------------------------------------------------------------===//
-
-const GRState*
-GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // First, determine if sym == X, where X != V.
- if (const llvm::APSInt* X = St->getSymVal(sym)) {
- isFeasible = *X != V;
- return St;
- }
-
- // Second, determine if sym != V.
- if (St->isNotEqual(sym, V)) {
- isFeasible = true;
- return St;
- }
-
- // 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);
-}
-
-const GRState*
-GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // First, determine if sym == X, where X != V.
- if (const llvm::APSInt* X = St->getSymVal(sym)) {
- isFeasible = *X == V;
- return St;
- }
-
- // Second, determine if sym != V.
- if (St->isNotEqual(sym, V)) {
- isFeasible = false;
- return St;
- }
-
- // 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);
-}
-
-const GRState*
-GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // FIXME: For now have assuming x < y be the same as assuming sym != V;
- return AssumeSymNE(St, sym, V, isFeasible);
-}
-
-const GRState*
-GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // FIXME: For now have assuming x > y be the same as assuming sym != V;
- return AssumeSymNE(St, sym, V, isFeasible);
-}
-
-const GRState*
-GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // FIXME: Primitive logic for now. Only reject a path if the value of
- // sym is a constant X and !(X >= V).
-
- if (const llvm::APSInt* X = St->getSymVal(sym)) {
- isFeasible = *X >= V;
- return St;
- }
-
- isFeasible = true;
- return St;
-}
-
-const GRState*
-GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // FIXME: Primitive logic for now. Only reject a path if the value of
- // sym is a constant X and !(X <= V).
-
- if (const llvm::APSInt* X = St->getSymVal(sym)) {
- isFeasible = *X <= V;
- return St;
- }
-
- isFeasible = true;
- return St;
-}
-
More information about the cfe-commits
mailing list