From 6a6719a3a11087b48d9f1a4eb08b3bd43cb05a65 Mon Sep 17 00:00:00 2001 From: Ted Kremenek Date: Fri, 29 Feb 2008 20:27:50 +0000 Subject: [PATCH] "Refinement" of hack to bound loop-traversals: visit any block at a maximum of 3 times along a given path. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@47766 91177308-0d34-0410-b5e6-96231b3b80d8 --- Analysis/GRCoreEngine.cpp | 8 +-- Analysis/GRExprEngine.cpp | 60 ++++++------------- .../Analysis/PathSensitive/GRCoreEngine.h | 15 ++++- .../Analysis/PathSensitive/GRExprEngine.h | 7 ++- 4 files changed, 40 insertions(+), 50 deletions(-) diff --git a/Analysis/GRCoreEngine.cpp b/Analysis/GRCoreEngine.cpp index 0e8be29186..4eb024f036 100644 --- a/Analysis/GRCoreEngine.cpp +++ b/Analysis/GRCoreEngine.cpp @@ -136,11 +136,11 @@ void GRCoreEngineImpl::HandleBlockEdge(const BlockEdge& L, ExplodedNodeImpl* Pre // This path is done. Don't enqueue any more nodes. return; } + + // FIXME: Should we allow ProcessBlockEntrance to also manipulate state? - // FIXME: we will dispatch to a function that - // manipulates the state at the entrance to a block. - - GenerateNode(BlockEntrance(Blk), Pred->State, Pred); + if (ProcessBlockEntrance(Blk, Pred->State, WList->getBlockCounter())) + GenerateNode(BlockEntrance(Blk), Pred->State, Pred); } void GRCoreEngineImpl::HandleBlockEntrance(const BlockEntrance& L, diff --git a/Analysis/GRExprEngine.cpp b/Analysis/GRExprEngine.cpp index 74f3a9a48d..2b94b4fafa 100644 --- a/Analysis/GRExprEngine.cpp +++ b/Analysis/GRExprEngine.cpp @@ -147,6 +147,12 @@ ValueState* GRExprEngine::MarkBranch(ValueState* St, Stmt* Terminator, } } +bool GRExprEngine::ProcessBlockEntrance(CFGBlock* B, ValueState*, + GRBlockCounter BC) { + + return BC.getNumVisited(B->getBlockID()) < 3; +} + void GRExprEngine::ProcessBranch(Expr* Condition, Stmt* Term, BranchNodeBuilder& builder) { @@ -156,15 +162,6 @@ void GRExprEngine::ProcessBranch(Expr* Condition, Stmt* Term, // Check for NULL conditions; e.g. "for(;;)" if (!Condition) { builder.markInfeasible(false); - - // Get the current block counter. - GRBlockCounter BC = builder.getBlockCounter(); - unsigned BlockID = builder.getTargetBlock(true)->getBlockID(); - unsigned NumVisited = BC.getNumVisited(BlockID); - - if (NumVisited < 1) builder.generateNode(PrevState, true); - else builder.markInfeasible(true); - return; } @@ -191,46 +188,25 @@ void GRExprEngine::ProcessBranch(Expr* Condition, Stmt* Term, return; } } - - // Get the current block counter. - GRBlockCounter BC = builder.getBlockCounter(); - unsigned BlockID = builder.getTargetBlock(true)->getBlockID(); - unsigned NumVisited = BC.getNumVisited(BlockID); - - if (isa(V) || - BC.getNumVisited(builder.getTargetBlock(true)->getBlockID()) < 1) { - // Process the true branch. - bool isFeasible = true; - - ValueState* St = Assume(PrevState, V, true, isFeasible); + // Process the true branch. - if (isFeasible) - builder.generateNode(MarkBranch(St, Term, true), true); - else - builder.markInfeasible(true); - } + bool isFeasible = true; + ValueState* St = Assume(PrevState, V, true, isFeasible); + + if (isFeasible) + builder.generateNode(MarkBranch(St, Term, true), true); else builder.markInfeasible(true); + + // Process the false branch. - BlockID = builder.getTargetBlock(false)->getBlockID(); - NumVisited = BC.getNumVisited(BlockID); + isFeasible = false; + St = Assume(PrevState, V, false, isFeasible); - if (isa(V) || - BC.getNumVisited(builder.getTargetBlock(false)->getBlockID()) < 1) { - - // Process the false branch. - - bool isFeasible = false; - - ValueState* St = Assume(PrevState, V, false, isFeasible); - - if (isFeasible) - builder.generateNode(MarkBranch(St, Term, false), false); - else - builder.markInfeasible(false); - } + if (isFeasible) + builder.generateNode(MarkBranch(St, Term, false), false); else builder.markInfeasible(false); } diff --git a/include/clang/Analysis/PathSensitive/GRCoreEngine.h b/include/clang/Analysis/PathSensitive/GRCoreEngine.h index d3325b1b12..93f30c2027 100644 --- a/include/clang/Analysis/PathSensitive/GRCoreEngine.h +++ b/include/clang/Analysis/PathSensitive/GRCoreEngine.h @@ -86,11 +86,14 @@ protected: ExplodedNodeImpl* Pred); virtual void* ProcessEOP(CFGBlock* Blk, void* State) = 0; + + virtual bool ProcessBlockEntrance(CFGBlock* Blk, void* State, + GRBlockCounter BC) = 0; - virtual void ProcessStmt(Stmt* S, GRStmtNodeBuilderImpl& Builder) = 0; + virtual void ProcessStmt(Stmt* S, GRStmtNodeBuilderImpl& Builder) = 0; - virtual void ProcessBranch(Expr* Condition, Stmt* Terminator, - GRBranchNodeBuilderImpl& Builder) = 0; + virtual void ProcessBranch(Expr* Condition, Stmt* Terminator, + GRBranchNodeBuilderImpl& Builder) = 0; virtual void ProcessIndirectGoto(GRIndirectGotoNodeBuilderImpl& Builder) = 0; @@ -434,6 +437,12 @@ protected: GRStmtNodeBuilder Builder(BuilderImpl); Checker->ProcessStmt(S, Builder); } + + virtual bool ProcessBlockEntrance(CFGBlock* Blk, void* State, + GRBlockCounter BC) { + return Checker->ProcessBlockEntrance(Blk, + GRTrait::toState(State), BC); + } virtual void ProcessBranch(Expr* Condition, Stmt* Terminator, GRBranchNodeBuilderImpl& BuilderImpl) { diff --git a/include/clang/Analysis/PathSensitive/GRExprEngine.h b/include/clang/Analysis/PathSensitive/GRExprEngine.h index efccf02f6e..b4751666b2 100644 --- a/include/clang/Analysis/PathSensitive/GRExprEngine.h +++ b/include/clang/Analysis/PathSensitive/GRExprEngine.h @@ -211,9 +211,14 @@ public: undef_result_iterator undef_results_end() { return UndefResults.end(); } /// ProcessStmt - Called by GRCoreEngine. Used to generate new successor - /// nodes by processing the 'effects' of a block-level statement. + /// nodes by processing the 'effects' of a block-level statement. void ProcessStmt(Stmt* S, StmtNodeBuilder& builder); + /// ProcessBlockEntrance - Called by GRCoreEngine when start processing + /// a CFGBlock. This method returns true if the analysis should continue + /// exploring the given path, and false otherwise. + bool ProcessBlockEntrance(CFGBlock* B, ValueState* St, GRBlockCounter BC); + /// ProcessBranch - Called by GRCoreEngine. Used to generate successor /// nodes by processing the 'effects' of a branch condition. void ProcessBranch(Expr* Condition, Stmt* Term, BranchNodeBuilder& builder); -- 2.40.0