diff options
author | Ted Kremenek <kremenek@apple.com> | 2009-02-25 22:32:02 +0000 |
---|---|---|
committer | Ted Kremenek <kremenek@apple.com> | 2009-02-25 22:32:02 +0000 |
commit | 48af2a9c1ed3259512f2d1431720add1fbe8fb5f (patch) | |
tree | f6c7032eb6348c37542f1f81e534a2f43a37096c /lib/Analysis/GRExprEngine.cpp | |
parent | 6bc9f7e286913fb1df95fa3fdcac7aab2628eaeb (diff) |
Add experimental logic in GRExprEngine::EvalEagerlyAssume() to handle
expressions of the form: 'short x = (y != 10);' While we handle 'int x = (y !=
10)' lazily, the cast to another integer type currently loses the symbolic
constraint. Eager evaluation of the constraint causes the paths to bifurcate and
eagerly evaluate 'y != 10' to a constant of 1 or 0. This should address
<rdar://problem/6619921> until we have a better (more lazy approach) for
handling promotions/truncations of symbolic integer values.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@65480 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Analysis/GRExprEngine.cpp')
-rw-r--r-- | lib/Analysis/GRExprEngine.cpp | 52 |
1 files changed, 49 insertions, 3 deletions
diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp index d34e8a3ed3..08c8d9bf01 100644 --- a/lib/Analysis/GRExprEngine.cpp +++ b/lib/Analysis/GRExprEngine.cpp @@ -103,7 +103,7 @@ static inline Selector GetNullarySelector(const char* name, ASTContext& Ctx) { GRExprEngine::GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx, LiveVariables& L, BugReporterData& BRD, - bool purgeDead, + bool purgeDead, bool eagerlyAssume, StoreManagerCreator SMC, ConstraintManagerCreator CMC) : CoreEngine(cfg, CD, Ctx, *this), @@ -116,7 +116,8 @@ GRExprEngine::GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx, NSExceptionII(NULL), NSExceptionInstanceRaiseSelectors(NULL), RaiseSel(GetNullarySelector("raise", G.getContext())), PurgeDead(purgeDead), - BR(BRD, *this) {} + BR(BRD, *this), + EagerlyAssume(eagerlyAssume) {} GRExprEngine::~GRExprEngine() { BR.FlushReports(); @@ -262,7 +263,14 @@ void GRExprEngine::Visit(Stmt* S, NodeTy* Pred, NodeSet& Dst) { break; } - VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Dst); + if (EagerlyAssume && (B->isRelationalOp() || B->isEqualityOp())) { + NodeSet Tmp; + VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Tmp); + EvalEagerlyAssume(Dst, Tmp); + } + else + VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Dst); + break; } @@ -1349,6 +1357,44 @@ void GRExprEngine::VisitCallRec(CallExpr* CE, NodeTy* Pred, // Transfer function: Objective-C ivar references. //===----------------------------------------------------------------------===// +static std::pair<const void*,const void*> EagerlyAssumeTag(&EagerlyAssumeTag,0); + +void GRExprEngine::EvalEagerlyAssume(NodeSet &Dst, NodeSet &Src) { + for (NodeSet::iterator I=Src.begin(), E=Src.end(); I!=E; ++I) { + NodeTy *Pred = *I; + Stmt *S = cast<PostStmt>(Pred->getLocation()).getStmt(); + const GRState* state = Pred->getState(); + SVal V = GetSVal(state, S); + if (isa<nonloc::SymIntConstraintVal>(V)) { + // First assume that the condition is true. + bool isFeasible = false; + const GRState *stateTrue = Assume(state, V, true, isFeasible); + if (isFeasible) { + stateTrue = BindExpr(stateTrue, cast<Expr>(S), + MakeConstantVal(1U, cast<Expr>(S))); + Dst.Add(Builder->generateNode(PostStmtCustom(S, &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, cast<Expr>(S), + MakeConstantVal(0U, cast<Expr>(S))); + Dst.Add(Builder->generateNode(PostStmtCustom(S, &EagerlyAssumeTag), + stateFalse, Pred)); + } + } + else + Dst.Add(Pred); + } +} + +//===----------------------------------------------------------------------===// +// Transfer function: Objective-C ivar references. +//===----------------------------------------------------------------------===// + void GRExprEngine::VisitObjCIvarRefExpr(ObjCIvarRefExpr* Ex, NodeTy* Pred, NodeSet& Dst, bool asLValue) { |