[cfe-commits] r53743 - in /cfe/trunk: include/clang/Analysis/PathSensitive/GRExprEngine.h include/clang/Analysis/PathSensitive/GRTransferFuncs.h include/clang/Analysis/PathSensitive/ValueState.h lib/Analysis/GRExprEngine.cpp lib/Analysis/ValueState.cpp
Ted Kremenek
kremenek at apple.com
Thu Jul 17 16:15:45 PDT 2008
Author: kremenek
Date: Thu Jul 17 18:15:45 2008
New Revision: 53743
URL: http://llvm.org/viewvc/llvm-project?rev=53743&view=rev
Log:
Move GRTransferFunc* into ValueStateManager, and move the assumption logic there as well.
Modified:
cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h
cfe/trunk/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h
cfe/trunk/lib/Analysis/GRExprEngine.cpp
cfe/trunk/lib/Analysis/ValueState.cpp
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=53743&r1=53742&r2=53743&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h Thu Jul 17 18:15:45 2008
@@ -70,10 +70,6 @@
/// ValueMgr - Object that manages the data for all created RVals.
BasicValueFactory& BasicVals;
- /// TF - Object that represents a bundle of transfer functions
- /// for manipulating and creating RVals.
- GRTransferFuncs* TF;
-
/// BugTypes - Objects used for reporting bugs.
typedef std::vector<BugType*> BugTypeSet;
BugTypeSet BugTypes;
@@ -187,6 +183,8 @@
/// getCFG - Returns the CFG associated with this analysis.
CFG& getCFG() { return G.getCFG(); }
+ GRTransferFuncs& getTF() { return *StateMgr.TF; }
+
/// setTransferFunctions
void setTransferFunctions(GRTransferFuncs* tf);
@@ -371,7 +369,7 @@
/// ProcessEndPath - Called by GRCoreEngine. Used to generate end-of-path
/// nodes when the control reaches the end of a function.
void ProcessEndPath(EndPathNodeBuilder& builder) {
- TF->EvalEndPath(*this, builder);
+ getTF().EvalEndPath(*this, builder);
}
ValueStateManager& getStateManager() { return StateMgr; }
@@ -433,39 +431,14 @@
/// is true or false.
const ValueState* Assume(const ValueState* 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 StateMgr.Assume(St, Cond, Assumption, isFeasible);
}
const ValueState* Assume(const ValueState* St, LVal Cond, bool Assumption,
- bool& isFeasible);
-
- const ValueState* AssumeAux(const ValueState* St, LVal Cond, bool Assumption,
- bool& isFeasible);
+ bool& isFeasible) {
+ return StateMgr.Assume(St, Cond, Assumption, isFeasible);
+ }
- const ValueState* Assume(const ValueState* St, NonLVal Cond, bool Assumption,
- bool& isFeasible);
-
- const ValueState* AssumeAux(const ValueState* St, NonLVal Cond,
- bool Assumption, bool& isFeasible);
-
- const ValueState* AssumeSymNE(const ValueState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const ValueState* AssumeSymEQ(const ValueState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,
- const SymIntConstraint& C, bool& isFeasible);
-
NodeTy* MakeNode(NodeSet& Dst, Stmt* S, NodeTy* Pred, const ValueState* St) {
assert (Builder && "GRStmtNodeBuilder not present.");
return Builder->MakeNode(Dst, S, Pred, St);
@@ -560,25 +533,25 @@
return X;
if (isa<LVal>(X))
- return TF->EvalCast(*this, cast<LVal>(X), CastT);
+ return getTF().EvalCast(*this, cast<LVal>(X), CastT);
else
- return TF->EvalCast(*this, cast<NonLVal>(X), CastT);
+ return getTF().EvalCast(*this, cast<NonLVal>(X), CastT);
}
RVal EvalMinus(UnaryOperator* U, RVal X) {
- return X.isValid() ? TF->EvalMinus(*this, U, cast<NonLVal>(X)) : X;
+ return X.isValid() ? getTF().EvalMinus(*this, U, cast<NonLVal>(X)) : X;
}
RVal EvalComplement(RVal X) {
- return X.isValid() ? TF->EvalComplement(*this, cast<NonLVal>(X)) : X;
+ return X.isValid() ? getTF().EvalComplement(*this, cast<NonLVal>(X)) : X;
}
RVal EvalBinOp(BinaryOperator::Opcode Op, NonLVal L, RVal R) {
- return R.isValid() ? TF->EvalBinOp(*this, Op, L, cast<NonLVal>(R)) : R;
+ return R.isValid() ? getTF().EvalBinOp(*this, Op, L, cast<NonLVal>(R)) : R;
}
RVal EvalBinOp(BinaryOperator::Opcode Op, NonLVal L, NonLVal R) {
- return R.isValid() ? TF->EvalBinOp(*this, Op, L, R) : R;
+ return R.isValid() ? getTF().EvalBinOp(*this, Op, L, R) : R;
}
RVal EvalBinOp(BinaryOperator::Opcode Op, RVal L, RVal R) {
@@ -591,9 +564,9 @@
if (isa<LVal>(L)) {
if (isa<LVal>(R))
- return TF->EvalBinOp(*this, Op, cast<LVal>(L), cast<LVal>(R));
+ return getTF().EvalBinOp(*this, Op, cast<LVal>(L), cast<LVal>(R));
else
- return TF->EvalBinOp(*this, Op, cast<LVal>(L), cast<NonLVal>(R));
+ return getTF().EvalBinOp(*this, Op, cast<LVal>(L), cast<NonLVal>(R));
}
if (isa<LVal>(R)) {
@@ -603,10 +576,10 @@
assert (Op == BinaryOperator::Add || Op == BinaryOperator::Sub);
// Commute the operands.
- return TF->EvalBinOp(*this, Op, cast<LVal>(R), cast<NonLVal>(L));
+ return getTF().EvalBinOp(*this, Op, cast<LVal>(R), cast<NonLVal>(L));
}
else
- return TF->EvalBinOp(*this, Op, cast<NonLVal>(L), cast<NonLVal>(R));
+ return getTF().EvalBinOp(*this, Op, cast<NonLVal>(L), cast<NonLVal>(R));
}
void EvalBinOp(ExplodedNodeSet<ValueState>& Dst, Expr* E,
@@ -615,12 +588,12 @@
void EvalCall(NodeSet& Dst, CallExpr* CE, RVal L, NodeTy* Pred) {
assert (Builder && "GRStmtNodeBuilder must be defined.");
- TF->EvalCall(Dst, *this, *Builder, CE, L, Pred);
+ getTF().EvalCall(Dst, *this, *Builder, CE, L, Pred);
}
void EvalObjCMessageExpr(NodeSet& Dst, ObjCMessageExpr* ME, NodeTy* Pred) {
assert (Builder && "GRStmtNodeBuilder must be defined.");
- TF->EvalObjCMessageExpr(Dst, *this, *Builder, ME, Pred);
+ getTF().EvalObjCMessageExpr(Dst, *this, *Builder, ME, Pred);
}
void EvalStore(NodeSet& Dst, Expr* E, NodeTy* Pred, const ValueState* St,
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=53743&r1=53742&r2=53743&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/GRTransferFuncs.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/GRTransferFuncs.h Thu Jul 17 18:15:45 2008
@@ -108,8 +108,7 @@
const ValueState* St,
const ValueStateManager::DeadSymbolsTy& Dead) {}
- // Return statements.
-
+ // Return statements.
virtual void EvalReturn(ExplodedNodeSet<ValueState>& Dst,
GRExprEngine& Engine,
GRStmtNodeBuilder<ValueState>& Builder,
@@ -118,7 +117,7 @@
// Assumptions.
- virtual const ValueState* EvalAssume(GRExprEngine& Engine,
+ virtual const ValueState* EvalAssume(ValueStateManager& VMgr,
const ValueState* St,
RVal Cond, bool Assumption,
bool& isFeasible) {
Modified: cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h?rev=53743&r1=53742&r2=53743&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h Thu Jul 17 18:15:45 2008
@@ -41,6 +41,7 @@
namespace clang {
class ValueStateManager;
+class GRTransferFuncs;
//===----------------------------------------------------------------------===//
// ValueState- An ImmutableMap type Stmt*/Decl*/Symbols to RVals.
@@ -217,6 +218,10 @@
/// cfg - The CFG for the analyzed function/method.
CFG& cfg;
+
+ /// TF - Object that represents a bundle of transfer functions
+ /// for manipulating and creating RVals.
+ GRTransferFuncs* TF;
private:
@@ -322,6 +327,44 @@
const ValueState* AddNE(const ValueState* St, SymbolID sym,
const llvm::APSInt& V);
+
+ // Assumption logic.
+ const ValueState* Assume(const ValueState* 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);
+ }
+
+ const ValueState* Assume(const ValueState* St, LVal Cond, bool Assumption,
+ bool& isFeasible);
+
+ const ValueState* Assume(const ValueState* St, NonLVal Cond, bool Assumption,
+ bool& isFeasible);
+
+private:
+ const ValueState* AssumeAux(const ValueState* St, LVal Cond, bool Assumption,
+ bool& isFeasible);
+
+
+ const ValueState* AssumeAux(const ValueState* St, NonLVal Cond,
+ bool Assumption, bool& isFeasible);
+
+ const ValueState* AssumeSymNE(const ValueState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const ValueState* AssumeSymEQ(const ValueState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,
+ const SymIntConstraint& C, bool& isFeasible);
};
} // end clang namespace
Modified: cfe/trunk/lib/Analysis/GRExprEngine.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/GRExprEngine.cpp?rev=53743&r1=53742&r2=53743&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/GRExprEngine.cpp (original)
+++ cfe/trunk/lib/Analysis/GRExprEngine.cpp Thu Jul 17 18:15:45 2008
@@ -123,7 +123,6 @@
StateMgr(G.getContext(), CreateBasicStoreManager(G.getAllocator()),
G.getAllocator(), G.getCFG()),
BasicVals(StateMgr.getBasicValueFactory()),
- TF(NULL), // FIXME
SymMgr(StateMgr.getSymbolManager()),
CurrentStmt(NULL),
NSExceptionII(NULL), NSExceptionInstanceRaiseSelectors(NULL),
@@ -178,8 +177,8 @@
}
void GRExprEngine::setTransferFunctions(GRTransferFuncs* tf) {
- TF = tf;
- TF->RegisterChecks(*this);
+ StateMgr.TF = tf;
+ getTF().RegisterChecks(*this);
}
void GRExprEngine::AddCheck(GRSimpleAPICheck* A, Stmt::StmtClass C) {
@@ -252,7 +251,7 @@
SaveAndRestore<bool> OldPurgeDeadSymbols(Builder->PurgingDeadSymbols);
Builder->PurgingDeadSymbols = true;
- TF->EvalDeadSymbols(Tmp, *this, *Builder, EntryNode, S,
+ getTF().EvalDeadSymbols(Tmp, *this, *Builder, EntryNode, S,
CleanedState, DeadSymbols);
if (!Builder->BuildSinks && !Builder->HasGeneratedNode)
@@ -964,13 +963,13 @@
assert (!location.isUndef());
- TF->EvalStore(Dst, *this, *Builder, Ex, Pred, St, location, Val);
+ getTF().EvalStore(Dst, *this, *Builder, Ex, Pred, St, location, Val);
// Handle the case where no nodes where generated. Auto-generate that
// contains the updated state if we aren't generating sinks.
if (!Builder->BuildSinks && Dst.size() == size && !Builder->HasGeneratedNode)
- TF->GRTransferFuncs::EvalStore(Dst, *this, *Builder, Ex, Pred, St,
+ getTF().GRTransferFuncs::EvalStore(Dst, *this, *Builder, Ex, Pred, St,
location, Val);
}
@@ -1939,7 +1938,7 @@
SaveAndRestore<bool> OldSink(Builder->BuildSinks);
SaveOr OldHasGen(Builder->HasGeneratedNode);
- TF->EvalReturn(Dst, *this, *Builder, S, Pred);
+ getTF().EvalReturn(Dst, *this, *Builder, S, Pred);
// Handle the case where no nodes where generated.
@@ -2240,7 +2239,7 @@
unsigned size = Dst.size();
SaveOr OldHasGen(Builder->HasGeneratedNode);
- TF->EvalBinOpNN(Dst, *this, *Builder, Op, Ex, L, R, Pred);
+ getTF().EvalBinOpNN(Dst, *this, *Builder, Op, Ex, L, R, Pred);
if (!Builder->BuildSinks && Dst.size() == size &&
!Builder->HasGeneratedNode)
@@ -2248,177 +2247,6 @@
}
//===----------------------------------------------------------------------===//
-// "Assume" logic.
-//===----------------------------------------------------------------------===//
-
-const ValueState* GRExprEngine::Assume(const ValueState* St, LVal Cond,
- bool Assumption, bool& isFeasible) {
-
- St = AssumeAux(St, Cond, Assumption, isFeasible);
-
- return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
- : St;
-}
-
-const ValueState* GRExprEngine::AssumeAux(const ValueState* 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 ValueState* GRExprEngine::Assume(const ValueState* St, NonLVal Cond,
- bool Assumption, bool& isFeasible) {
-
- St = AssumeAux(St, Cond, Assumption, isFeasible);
-
- return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
- : St;
-}
-
-const ValueState* GRExprEngine::AssumeAux(const ValueState* 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 ValueState* GRExprEngine::AssumeSymNE(const ValueState* 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 ValueState* GRExprEngine::AssumeSymEQ(const ValueState* 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);
-}
-
-const ValueState* GRExprEngine::AssumeSymInt(const ValueState* 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);
- }
-}
-
-//===----------------------------------------------------------------------===//
// Visualization.
//===----------------------------------------------------------------------===//
@@ -2733,7 +2561,7 @@
else {
GraphPrintCheckerState = this;
GraphPrintSourceManager = &getContext().getSourceManager();
- GraphCheckerStatePrinter = TF->getCheckerStatePrinter();
+ GraphCheckerStatePrinter = getTF().getCheckerStatePrinter();
llvm::ViewGraph(*G.roots_begin(), "GRExprEngine");
@@ -2748,7 +2576,7 @@
#ifndef NDEBUG
GraphPrintCheckerState = this;
GraphPrintSourceManager = &getContext().getSourceManager();
- GraphCheckerStatePrinter = TF->getCheckerStatePrinter();
+ GraphCheckerStatePrinter = getTF().getCheckerStatePrinter();
GRExprEngine::GraphTy* TrimmedG = G.Trim(Beg, End);
Modified: cfe/trunk/lib/Analysis/ValueState.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/ValueState.cpp?rev=53743&r1=53742&r2=53743&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/ValueState.cpp (original)
+++ cfe/trunk/lib/Analysis/ValueState.cpp Thu Jul 17 18:15:45 2008
@@ -13,6 +13,7 @@
#include "clang/Analysis/PathSensitive/ValueState.h"
#include "llvm/ADT/SmallSet.h"
+#include "clang/Analysis/PathSensitive/GRTransferFuncs.h"
using namespace clang;
@@ -294,3 +295,174 @@
if (P && CheckerState)
P->PrintCheckerState(Out, CheckerState, nl, sep);
}
+
+//===----------------------------------------------------------------------===//
+// "Assume" logic.
+//===----------------------------------------------------------------------===//
+
+const ValueState* ValueStateManager::Assume(const ValueState* St, LVal Cond,
+ bool Assumption, bool& isFeasible) {
+
+ St = AssumeAux(St, Cond, Assumption, isFeasible);
+
+ return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
+ : St;
+}
+
+const ValueState* ValueStateManager::AssumeAux(const ValueState* 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 ValueState* ValueStateManager::Assume(const ValueState* St, NonLVal Cond,
+ bool Assumption, bool& isFeasible) {
+
+ St = AssumeAux(St, Cond, Assumption, isFeasible);
+
+ return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
+ : St;
+}
+
+const ValueState* ValueStateManager::AssumeAux(const ValueState* 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 ValueState* ValueStateManager::AssumeSymNE(const ValueState* 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 ValueState* ValueStateManager::AssumeSymEQ(const ValueState* 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 ValueState* ValueStateManager::AssumeSymInt(const ValueState* 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);
+ }
+}
More information about the cfe-commits
mailing list