From: Ted Kremenek Date: Wed, 25 Feb 2009 22:32:02 +0000 (+0000) Subject: Add experimental logic in GRExprEngine::EvalEagerlyAssume() to handle X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=48af2a9c1ed3259512f2d1431720add1fbe8fb5f;p=clang 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 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 --- diff --git a/Driver/AnalysisConsumer.cpp b/Driver/AnalysisConsumer.cpp index fd74f7dcd1..860cf156b5 100644 --- a/Driver/AnalysisConsumer.cpp +++ b/Driver/AnalysisConsumer.cpp @@ -152,6 +152,12 @@ PurgeDead("analyzer-purge-dead", llvm::cl::desc("Remove dead symbols, bindings, and constraints before" " processing a statement.")); +static llvm::cl::opt +EagerlyAssume("analyzer-eagerly-assume", + llvm::cl::init(false), + llvm::cl::desc("Eagerly assume the truth/falseness of some " + "symbolic constraints.")); + static llvm::cl::opt AnalyzeSpecificFunction("analyze-function", llvm::cl::desc("Run analysis on specific function")); @@ -516,7 +522,7 @@ static void ActionGRExprEngine(AnalysisManager& mgr, GRTransferFuncs* tf, if (!L) return; GRExprEngine Eng(*mgr.getCFG(), *mgr.getCodeDecl(), mgr.getContext(), *L, mgr, - PurgeDead, + PurgeDead, EagerlyAssume, mgr.getStoreManagerCreator(), mgr.getConstraintManagerCreator()); diff --git a/include/clang/Analysis/PathSensitive/GRExprEngine.h b/include/clang/Analysis/PathSensitive/GRExprEngine.h index 7f2b5f595b..797b0ae0cd 100644 --- a/include/clang/Analysis/PathSensitive/GRExprEngine.h +++ b/include/clang/Analysis/PathSensitive/GRExprEngine.h @@ -90,6 +90,15 @@ protected: // destructor is called before the rest of the GRExprEngine is destroyed. GRBugReporter BR; + /// EargerlyAssume - A flag indicating how the engine should handle + // expressions such as: 'x = (y != 0)'. When this flag is true then + // the subexpression 'y != 0' will be eagerly assumed to be true or false, + // thus evaluating it to the integers 0 or 1 respectively. The upside + // is that this can increase analysis precision until we have a better way + // to lazily evaluate such logic. The downside is that it eagerly + // bifurcates paths. + const bool EagerlyAssume; + public: typedef llvm::SmallPtrSet ErrorNodes; typedef llvm::DenseMap UndefArgsTy; @@ -186,7 +195,7 @@ public: public: GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx, LiveVariables& L, BugReporterData& BRD, - bool purgeDead, + bool purgeDead, bool eagerlyAssume = true, StoreManagerCreator SMC = CreateBasicStoreManager, ConstraintManagerCreator CMC = CreateBasicConstraintManager); @@ -606,6 +615,11 @@ protected: const GRState* CheckDivideZero(Expr* Ex, const GRState* St, NodeTy* Pred, SVal Denom); + /// EvalEagerlyAssume - Given the nodes in 'Src', eagerly assume symbolic + /// expressions of the form 'x != 0' and generate new nodes (stored in Dst) + /// with those assumptions. + void EvalEagerlyAssume(NodeSet& Dst, NodeSet& Src); + SVal EvalCast(SVal X, QualType CastT) { if (X.isUnknownOrUndef()) return X; 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(S), Pred, Dst); + if (EagerlyAssume && (B->isRelationalOp() || B->isEqualityOp())) { + NodeSet Tmp; + VisitBinaryOperator(cast(S), Pred, Tmp); + EvalEagerlyAssume(Dst, Tmp); + } + else + VisitBinaryOperator(cast(S), Pred, Dst); + break; } @@ -1349,6 +1357,44 @@ void GRExprEngine::VisitCallRec(CallExpr* CE, NodeTy* Pred, // Transfer function: Objective-C ivar references. //===----------------------------------------------------------------------===// +static std::pair 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(Pred->getLocation()).getStmt(); + const GRState* state = Pred->getState(); + SVal V = GetSVal(state, S); + if (isa(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(S), + MakeConstantVal(1U, cast(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(S), + MakeConstantVal(0U, cast(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) { diff --git a/test/Analysis/misc-ps-eager-assume.m b/test/Analysis/misc-ps-eager-assume.m new file mode 100644 index 0000000000..48d5b8f9d2 --- /dev/null +++ b/test/Analysis/misc-ps-eager-assume.m @@ -0,0 +1,14 @@ +// RUN: clang -analyze -checker-cfref --analyzer-store=region -analyzer-constraints=range --verify -fblocks %s -analyzer-eagerly-assume + +void handle_assign_of_condition(int x) { + // The cast to 'short' causes us to lose symbolic constraint. + short y = (x != 0); + char *p = 0; + if (y) { + // This should be infeasible. + if (!(x != 0)) { + *p = 1; // no-warning + } + } +} +