From dc3f50fbd95317f96d9ce0084b19bd331e3f8560 Mon Sep 17 00:00:00 2001 From: Ted Kremenek Date: Wed, 25 Feb 2009 22:32:02 +0000 Subject: [PATCH] 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. llvm-svn: 65480 --- clang/Driver/AnalysisConsumer.cpp | 8 ++- .../Analysis/PathSensitive/GRExprEngine.h | 16 +++++- clang/lib/Analysis/GRExprEngine.cpp | 52 +++++++++++++++++-- clang/test/Analysis/misc-ps-eager-assume.m | 14 +++++ 4 files changed, 85 insertions(+), 5 deletions(-) create mode 100644 clang/test/Analysis/misc-ps-eager-assume.m diff --git a/clang/Driver/AnalysisConsumer.cpp b/clang/Driver/AnalysisConsumer.cpp index fd74f7dcd179..860cf156b5a5 100644 --- a/clang/Driver/AnalysisConsumer.cpp +++ b/clang/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/clang/include/clang/Analysis/PathSensitive/GRExprEngine.h b/clang/include/clang/Analysis/PathSensitive/GRExprEngine.h index 7f2b5f595b8c..797b0ae0cd80 100644 --- a/clang/include/clang/Analysis/PathSensitive/GRExprEngine.h +++ b/clang/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/clang/lib/Analysis/GRExprEngine.cpp b/clang/lib/Analysis/GRExprEngine.cpp index d34e8a3ed3a1..08c8d9bf01d0 100644 --- a/clang/lib/Analysis/GRExprEngine.cpp +++ b/clang/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/clang/test/Analysis/misc-ps-eager-assume.m b/clang/test/Analysis/misc-ps-eager-assume.m new file mode 100644 index 000000000000..48d5b8f9d225 --- /dev/null +++ b/clang/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 + } + } +} +