Ted Kremenek | 1781080 | 2008-11-12 19:24:17 +0000 | [diff] [blame] | 1 | //==- GRCoreEngine.cpp - Path-Sensitive Dataflow Engine ------------*- C++ -*-// |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 2 | // |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 3 | // The LLVM Compiler Infrastructure |
| 4 | // |
| 5 | // This file is distributed under the University of Illinois Open Source |
| 6 | // License. See LICENSE.TXT for details. |
| 7 | // |
| 8 | //===----------------------------------------------------------------------===// |
| 9 | // |
| 10 | // This file defines a generic engine for intraprocedural, path-sensitive, |
| 11 | // dataflow analysis via graph reachability engine. |
| 12 | // |
| 13 | //===----------------------------------------------------------------------===// |
| 14 | |
Ted Kremenek | f6c62f3 | 2008-02-13 17:41:41 +0000 | [diff] [blame] | 15 | #include "clang/Analysis/PathSensitive/GRCoreEngine.h" |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 16 | #include "clang/Analysis/PathSensitive/GRExprEngine.h" |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 17 | #include "clang/AST/Expr.h" |
| 18 | #include "llvm/Support/Compiler.h" |
| 19 | #include "llvm/Support/Casting.h" |
| 20 | #include "llvm/ADT/DenseMap.h" |
| 21 | #include <vector> |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 22 | #include <queue> |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 23 | |
| 24 | using llvm::cast; |
| 25 | using llvm::isa; |
| 26 | using namespace clang; |
| 27 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 28 | //===----------------------------------------------------------------------===// |
| 29 | // Worklist classes for exploration of reachable states. |
| 30 | //===----------------------------------------------------------------------===// |
| 31 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 32 | namespace { |
Zhongxing Xu | 69cc15e | 2009-07-15 09:04:01 +0000 | [diff] [blame] | 33 | class VISIBILITY_HIDDEN DFS : public GRWorkList { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 34 | llvm::SmallVector<GRWorkListUnit,20> Stack; |
| 35 | public: |
| 36 | virtual bool hasWork() const { |
| 37 | return !Stack.empty(); |
| 38 | } |
| 39 | |
| 40 | virtual void Enqueue(const GRWorkListUnit& U) { |
| 41 | Stack.push_back(U); |
| 42 | } |
| 43 | |
| 44 | virtual GRWorkListUnit Dequeue() { |
| 45 | assert (!Stack.empty()); |
| 46 | const GRWorkListUnit& U = Stack.back(); |
| 47 | Stack.pop_back(); // This technically "invalidates" U, but we are fine. |
| 48 | return U; |
| 49 | } |
| 50 | }; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 51 | |
Ted Kremenek | 2c32773 | 2009-05-01 22:18:46 +0000 | [diff] [blame] | 52 | class VISIBILITY_HIDDEN BFS : public GRWorkList { |
| 53 | std::queue<GRWorkListUnit> Queue; |
| 54 | public: |
| 55 | virtual bool hasWork() const { |
| 56 | return !Queue.empty(); |
| 57 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 58 | |
Ted Kremenek | 2c32773 | 2009-05-01 22:18:46 +0000 | [diff] [blame] | 59 | virtual void Enqueue(const GRWorkListUnit& U) { |
| 60 | Queue.push(U); |
| 61 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 62 | |
Ted Kremenek | 2c32773 | 2009-05-01 22:18:46 +0000 | [diff] [blame] | 63 | virtual GRWorkListUnit Dequeue() { |
| 64 | // Don't use const reference. The subsequent pop_back() might make it |
| 65 | // unsafe. |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 66 | GRWorkListUnit U = Queue.front(); |
Ted Kremenek | 2c32773 | 2009-05-01 22:18:46 +0000 | [diff] [blame] | 67 | Queue.pop(); |
| 68 | return U; |
| 69 | } |
| 70 | }; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 71 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 72 | } // end anonymous namespace |
| 73 | |
Ted Kremenek | 2e12c2e | 2008-01-16 18:18:48 +0000 | [diff] [blame] | 74 | // Place the dstor for GRWorkList here because it contains virtual member |
| 75 | // functions, and we the code for the dstor generated in one compilation unit. |
| 76 | GRWorkList::~GRWorkList() {} |
| 77 | |
Ted Kremenek | 2c32773 | 2009-05-01 22:18:46 +0000 | [diff] [blame] | 78 | GRWorkList *GRWorkList::MakeDFS() { return new DFS(); } |
| 79 | GRWorkList *GRWorkList::MakeBFS() { return new BFS(); } |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 80 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 81 | namespace { |
| 82 | class VISIBILITY_HIDDEN BFSBlockDFSContents : public GRWorkList { |
| 83 | std::queue<GRWorkListUnit> Queue; |
| 84 | llvm::SmallVector<GRWorkListUnit,20> Stack; |
| 85 | public: |
| 86 | virtual bool hasWork() const { |
| 87 | return !Queue.empty() || !Stack.empty(); |
| 88 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 89 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 90 | virtual void Enqueue(const GRWorkListUnit& U) { |
| 91 | if (isa<BlockEntrance>(U.getNode()->getLocation())) |
| 92 | Queue.push(U); |
| 93 | else |
| 94 | Stack.push_back(U); |
| 95 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 96 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 97 | virtual GRWorkListUnit Dequeue() { |
| 98 | // Process all basic blocks to completion. |
| 99 | if (!Stack.empty()) { |
| 100 | const GRWorkListUnit& U = Stack.back(); |
| 101 | Stack.pop_back(); // This technically "invalidates" U, but we are fine. |
| 102 | return U; |
| 103 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 104 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 105 | assert(!Queue.empty()); |
| 106 | // Don't use const reference. The subsequent pop_back() might make it |
| 107 | // unsafe. |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 108 | GRWorkListUnit U = Queue.front(); |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 109 | Queue.pop(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 110 | return U; |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 111 | } |
| 112 | }; |
| 113 | } // end anonymous namespace |
| 114 | |
| 115 | GRWorkList* GRWorkList::MakeBFSBlockDFSContents() { |
| 116 | return new BFSBlockDFSContents(); |
| 117 | } |
| 118 | |
| 119 | //===----------------------------------------------------------------------===// |
| 120 | // Core analysis engine. |
| 121 | //===----------------------------------------------------------------------===// |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 122 | void GRCoreEngine::ProcessEndPath(GREndPathNodeBuilder& Builder) { |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 123 | SubEngine.ProcessEndPath(Builder); |
| 124 | } |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 125 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 126 | void GRCoreEngine::ProcessStmt(Stmt* S, GRStmtNodeBuilder& Builder) { |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 127 | SubEngine.ProcessStmt(S, Builder); |
| 128 | } |
| 129 | |
| 130 | bool GRCoreEngine::ProcessBlockEntrance(CFGBlock* Blk, const GRState* State, |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 131 | GRBlockCounter BC) { |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 132 | return SubEngine.ProcessBlockEntrance(Blk, State, BC); |
| 133 | } |
| 134 | |
| 135 | void GRCoreEngine::ProcessBranch(Stmt* Condition, Stmt* Terminator, |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 136 | GRBranchNodeBuilder& Builder) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 137 | SubEngine.ProcessBranch(Condition, Terminator, Builder); |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 138 | } |
| 139 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 140 | void GRCoreEngine::ProcessIndirectGoto(GRIndirectGotoNodeBuilder& Builder) { |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 141 | SubEngine.ProcessIndirectGoto(Builder); |
| 142 | } |
| 143 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 144 | void GRCoreEngine::ProcessSwitch(GRSwitchNodeBuilder& Builder) { |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 145 | SubEngine.ProcessSwitch(Builder); |
| 146 | } |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 147 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 148 | /// ExecuteWorkList - Run the worklist algorithm for a maximum number of steps. |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 149 | bool GRCoreEngine::ExecuteWorkList(const LocationContext *L, unsigned Steps) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 150 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 151 | if (G->num_roots() == 0) { // Initialize the analysis by constructing |
| 152 | // the root if none exists. |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 153 | |
Zhongxing Xu | 94ec649 | 2009-08-25 03:33:41 +0000 | [diff] [blame] | 154 | CFGBlock* Entry = &(L->getCFG()->getEntry()); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 155 | |
| 156 | assert (Entry->empty() && |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 157 | "Entry block must be empty."); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 158 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 159 | assert (Entry->succ_size() == 1 && |
| 160 | "Entry block must have 1 successor."); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 161 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 162 | // Get the solitary successor. |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 163 | CFGBlock* Succ = *(Entry->succ_begin()); |
| 164 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 165 | // Construct an edge representing the |
| 166 | // starting location in the function. |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 167 | BlockEdge StartLoc(Entry, Succ, L); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 168 | |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 169 | // Set the current block counter to being empty. |
| 170 | WList->setBlockCounter(BCounterFactory.GetEmptyCounter()); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 171 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 172 | // Generate the root. |
Zhongxing Xu | 5f078cb | 2009-08-17 06:19:58 +0000 | [diff] [blame] | 173 | GenerateNode(StartLoc, getInitialState(L), 0); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 174 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 175 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 176 | while (Steps && WList->hasWork()) { |
| 177 | --Steps; |
| 178 | const GRWorkListUnit& WU = WList->Dequeue(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 179 | |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 180 | // Set the current block counter. |
| 181 | WList->setBlockCounter(WU.getBlockCounter()); |
| 182 | |
| 183 | // Retrieve the node. |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 184 | ExplodedNode* Node = WU.getNode(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 185 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 186 | // Dispatch on the location type. |
| 187 | switch (Node->getLocation().getKind()) { |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 188 | case ProgramPoint::BlockEdgeKind: |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 189 | HandleBlockEdge(cast<BlockEdge>(Node->getLocation()), Node); |
| 190 | break; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 191 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 192 | case ProgramPoint::BlockEntranceKind: |
| 193 | HandleBlockEntrance(cast<BlockEntrance>(Node->getLocation()), Node); |
| 194 | break; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 195 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 196 | case ProgramPoint::BlockExitKind: |
Ted Kremenek | e584359 | 2008-01-15 00:24:08 +0000 | [diff] [blame] | 197 | assert (false && "BlockExit location never occur in forward analysis."); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 198 | break; |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 199 | |
| 200 | default: |
| 201 | assert(isa<PostStmt>(Node->getLocation())); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 202 | HandlePostStmt(cast<PostStmt>(Node->getLocation()), WU.getBlock(), |
| 203 | WU.getIndex(), Node); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 204 | break; |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 205 | } |
| 206 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 207 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 208 | return WList->hasWork(); |
| 209 | } |
| 210 | |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 211 | |
| 212 | void GRCoreEngine::HandleBlockEdge(const BlockEdge& L, ExplodedNode* Pred) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 213 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 214 | CFGBlock* Blk = L.getDst(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 215 | |
| 216 | // Check if we are entering the EXIT block. |
Zhongxing Xu | 94ec649 | 2009-08-25 03:33:41 +0000 | [diff] [blame] | 217 | if (Blk == &(Pred->getLocationContext()->getCFG()->getExit())) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 218 | |
| 219 | assert (Pred->getLocationContext()->getCFG()->getExit().size() == 0 |
Ted Kremenek | 997d872 | 2008-01-29 00:33:40 +0000 | [diff] [blame] | 220 | && "EXIT block cannot contain Stmts."); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 221 | |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 222 | // Process the final state transition. |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 223 | GREndPathNodeBuilder Builder(Blk, Pred, this); |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 224 | ProcessEndPath(Builder); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 225 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 226 | // This path is done. Don't enqueue any more nodes. |
| 227 | return; |
| 228 | } |
Ted Kremenek | 17f4dbd | 2008-02-29 20:27:50 +0000 | [diff] [blame] | 229 | |
| 230 | // FIXME: Should we allow ProcessBlockEntrance to also manipulate state? |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 231 | |
Ted Kremenek | 17f4dbd | 2008-02-29 20:27:50 +0000 | [diff] [blame] | 232 | if (ProcessBlockEntrance(Blk, Pred->State, WList->getBlockCounter())) |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 233 | GenerateNode(BlockEntrance(Blk, Pred->getLocationContext()), Pred->State, Pred); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 234 | } |
| 235 | |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 236 | void GRCoreEngine::HandleBlockEntrance(const BlockEntrance& L, |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 237 | ExplodedNode* Pred) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 238 | |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 239 | // Increment the block counter. |
| 240 | GRBlockCounter Counter = WList->getBlockCounter(); |
| 241 | Counter = BCounterFactory.IncrementCount(Counter, L.getBlock()->getBlockID()); |
| 242 | WList->setBlockCounter(Counter); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 243 | |
| 244 | // Process the entrance of the block. |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 245 | if (Stmt* S = L.getFirstStmt()) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 246 | GRStmtNodeBuilder Builder(L.getBlock(), 0, Pred, this, |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 247 | SubEngine.getStateManager()); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 248 | ProcessStmt(S, Builder); |
| 249 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 250 | else |
Ted Kremenek | e584359 | 2008-01-15 00:24:08 +0000 | [diff] [blame] | 251 | HandleBlockExit(L.getBlock(), Pred); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 252 | } |
| 253 | |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 254 | void GRCoreEngine::HandleBlockExit(CFGBlock * B, ExplodedNode* Pred) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 255 | |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 256 | if (Stmt* Term = B->getTerminator()) { |
| 257 | switch (Term->getStmtClass()) { |
| 258 | default: |
| 259 | assert(false && "Analysis for this terminator not implemented."); |
| 260 | break; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 261 | |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 262 | case Stmt::BinaryOperatorClass: // '&&' and '||' |
| 263 | HandleBranch(cast<BinaryOperator>(Term)->getLHS(), Term, B, Pred); |
| 264 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 265 | |
Ted Kremenek | 3f2f1ad | 2008-02-05 00:26:40 +0000 | [diff] [blame] | 266 | case Stmt::ConditionalOperatorClass: |
| 267 | HandleBranch(cast<ConditionalOperator>(Term)->getCond(), Term, B, Pred); |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 268 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 269 | |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 270 | // FIXME: Use constant-folding in CFG construction to simplify this |
| 271 | // case. |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 272 | |
Ted Kremenek | 3f2f1ad | 2008-02-05 00:26:40 +0000 | [diff] [blame] | 273 | case Stmt::ChooseExprClass: |
| 274 | HandleBranch(cast<ChooseExpr>(Term)->getCond(), Term, B, Pred); |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 275 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 276 | |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 277 | case Stmt::DoStmtClass: |
| 278 | HandleBranch(cast<DoStmt>(Term)->getCond(), Term, B, Pred); |
| 279 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 280 | |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 281 | case Stmt::ForStmtClass: |
| 282 | HandleBranch(cast<ForStmt>(Term)->getCond(), Term, B, Pred); |
| 283 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 284 | |
Ted Kremenek | 632bcb8 | 2008-02-13 16:56:51 +0000 | [diff] [blame] | 285 | case Stmt::ContinueStmtClass: |
| 286 | case Stmt::BreakStmtClass: |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 287 | case Stmt::GotoStmtClass: |
Ted Kremenek | 3f2f1ad | 2008-02-05 00:26:40 +0000 | [diff] [blame] | 288 | break; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 289 | |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 290 | case Stmt::IfStmtClass: |
| 291 | HandleBranch(cast<IfStmt>(Term)->getCond(), Term, B, Pred); |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 292 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 293 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 294 | case Stmt::IndirectGotoStmtClass: { |
| 295 | // Only 1 successor: the indirect goto dispatch block. |
| 296 | assert (B->succ_size() == 1); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 297 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 298 | GRIndirectGotoNodeBuilder |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 299 | builder(Pred, B, cast<IndirectGotoStmt>(Term)->getTarget(), |
| 300 | *(B->succ_begin()), this); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 301 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 302 | ProcessIndirectGoto(builder); |
| 303 | return; |
| 304 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 305 | |
Ted Kremenek | 1781080 | 2008-11-12 19:24:17 +0000 | [diff] [blame] | 306 | case Stmt::ObjCForCollectionStmtClass: { |
| 307 | // In the case of ObjCForCollectionStmt, it appears twice in a CFG: |
| 308 | // |
| 309 | // (1) inside a basic block, which represents the binding of the |
| 310 | // 'element' variable to a value. |
| 311 | // (2) in a terminator, which represents the branch. |
| 312 | // |
| 313 | // For (1), subengines will bind a value (i.e., 0 or 1) indicating |
| 314 | // whether or not collection contains any more elements. We cannot |
| 315 | // just test to see if the element is nil because a container can |
| 316 | // contain nil elements. |
| 317 | HandleBranch(Term, Term, B, Pred); |
| 318 | return; |
| 319 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 320 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 321 | case Stmt::SwitchStmtClass: { |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 322 | GRSwitchNodeBuilder builder(Pred, B, cast<SwitchStmt>(Term)->getCond(), |
| 323 | this); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 324 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 325 | ProcessSwitch(builder); |
| 326 | return; |
| 327 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 328 | |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 329 | case Stmt::WhileStmtClass: |
| 330 | HandleBranch(cast<WhileStmt>(Term)->getCond(), Term, B, Pred); |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 331 | return; |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 332 | } |
| 333 | } |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 334 | |
| 335 | assert (B->succ_size() == 1 && |
| 336 | "Blocks with no terminator should have at most 1 successor."); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 337 | |
| 338 | GenerateNode(BlockEdge(B, *(B->succ_begin()), Pred->getLocationContext()), |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 339 | Pred->State, Pred); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 340 | } |
| 341 | |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 342 | void GRCoreEngine::HandleBranch(Stmt* Cond, Stmt* Term, CFGBlock * B, |
| 343 | ExplodedNode* Pred) { |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 344 | assert (B->succ_size() == 2); |
| 345 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 346 | GRBranchNodeBuilder Builder(B, *(B->succ_begin()), *(B->succ_begin()+1), |
| 347 | Pred, this); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 348 | |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 349 | ProcessBranch(Cond, Term, Builder); |
| 350 | } |
| 351 | |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 352 | void GRCoreEngine::HandlePostStmt(const PostStmt& L, CFGBlock* B, |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 353 | unsigned StmtIdx, ExplodedNode* Pred) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 354 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 355 | assert (!B->empty()); |
| 356 | |
Ted Kremenek | e584359 | 2008-01-15 00:24:08 +0000 | [diff] [blame] | 357 | if (StmtIdx == B->size()) |
| 358 | HandleBlockExit(B, Pred); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 359 | else { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 360 | GRStmtNodeBuilder Builder(B, StmtIdx, Pred, this, |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 361 | SubEngine.getStateManager()); |
Ted Kremenek | e914bb8 | 2008-01-16 22:13:19 +0000 | [diff] [blame] | 362 | ProcessStmt((*B)[StmtIdx], Builder); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 363 | } |
| 364 | } |
| 365 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 366 | /// GenerateNode - Utility method to generate nodes, hook up successors, |
| 367 | /// and add nodes to the worklist. |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 368 | void GRCoreEngine::GenerateNode(const ProgramPoint& Loc, |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 369 | const GRState* State, ExplodedNode* Pred) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 370 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 371 | bool IsNew; |
Zhongxing Xu | c90a0c2 | 2009-08-06 06:28:40 +0000 | [diff] [blame] | 372 | ExplodedNode* Node = G->getNode(Loc, State, &IsNew); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 373 | |
| 374 | if (Pred) |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 375 | Node->addPredecessor(Pred, *G); // Link 'Node' with its predecessor. |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 376 | else { |
| 377 | assert (IsNew); |
| 378 | G->addRoot(Node); // 'Node' has no predecessor. Make it a root. |
| 379 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 380 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 381 | // Only add 'Node' to the worklist if it was freshly generated. |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 382 | if (IsNew) WList->Enqueue(Node); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 383 | } |
| 384 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 385 | GRStmtNodeBuilder::GRStmtNodeBuilder(CFGBlock* b, unsigned idx, |
| 386 | ExplodedNode* N, GRCoreEngine* e, |
| 387 | GRStateManager &mgr) |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 388 | : Eng(*e), B(*b), Idx(idx), Pred(N), LastNode(N), Mgr(mgr), Auditor(0), |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 389 | PurgingDeadSymbols(false), BuildSinks(false), HasGeneratedNode(false), |
| 390 | PointKind(ProgramPoint::PostStmtKind), Tag(0) { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 391 | Deferred.insert(N); |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 392 | CleanedState = getLastNode()->getState(); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 393 | } |
| 394 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 395 | GRStmtNodeBuilder::~GRStmtNodeBuilder() { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 396 | for (DeferredTy::iterator I=Deferred.begin(), E=Deferred.end(); I!=E; ++I) |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 397 | if (!(*I)->isSink()) |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 398 | GenerateAutoTransition(*I); |
| 399 | } |
| 400 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 401 | void GRStmtNodeBuilder::GenerateAutoTransition(ExplodedNode* N) { |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 402 | assert (!N->isSink()); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 403 | |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 404 | PostStmt Loc(getStmt(), N->getLocationContext()); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 405 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 406 | if (Loc == N->getLocation()) { |
| 407 | // Note: 'N' should be a fresh node because otherwise it shouldn't be |
| 408 | // a member of Deferred. |
| 409 | Eng.WList->Enqueue(N, B, Idx+1); |
| 410 | return; |
| 411 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 412 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 413 | bool IsNew; |
Zhongxing Xu | c90a0c2 | 2009-08-06 06:28:40 +0000 | [diff] [blame] | 414 | ExplodedNode* Succ = Eng.G->getNode(Loc, N->State, &IsNew); |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 415 | Succ->addPredecessor(N, *Eng.G); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 416 | |
| 417 | if (IsNew) |
| 418 | Eng.WList->Enqueue(Succ, B, Idx+1); |
| 419 | } |
| 420 | |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame^] | 421 | static ProgramPoint GetProgramPoint(const Stmt *S, ProgramPoint::Kind K, |
| 422 | const LocationContext *LC, const void *tag){ |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 423 | switch (K) { |
| 424 | default: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame^] | 425 | assert(false && "Unhandled ProgramPoint kind"); |
| 426 | case ProgramPoint::PreStmtKind: |
| 427 | return PreStmt(S, LC, tag); |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 428 | case ProgramPoint::PostStmtKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame^] | 429 | return PostStmt(S, LC, tag); |
| 430 | case ProgramPoint::PreLoadKind: |
| 431 | return PreLoad(S, LC, tag); |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 432 | case ProgramPoint::PostLoadKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame^] | 433 | return PostLoad(S, LC, tag); |
| 434 | case ProgramPoint::PreStoreKind: |
| 435 | return PreStore(S, LC, tag); |
Ted Kremenek | a196618 | 2008-10-17 20:49:23 +0000 | [diff] [blame] | 436 | case ProgramPoint::PostStoreKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame^] | 437 | return PostStore(S, LC, tag); |
Ted Kremenek | a6e0832 | 2009-05-07 18:27:16 +0000 | [diff] [blame] | 438 | case ProgramPoint::PostLValueKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame^] | 439 | return PostLValue(S, LC, tag); |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 440 | case ProgramPoint::PostPurgeDeadSymbolsKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame^] | 441 | return PostPurgeDeadSymbols(S, LC, tag); |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 442 | } |
| 443 | } |
| 444 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 445 | ExplodedNode* |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame^] | 446 | GRStmtNodeBuilder::generateNodeInternal(const Stmt* S, const GRState* state, |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 447 | ExplodedNode* Pred, |
Ted Kremenek | df24000 | 2009-04-11 00:11:10 +0000 | [diff] [blame] | 448 | ProgramPoint::Kind K, |
| 449 | const void *tag) { |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame^] | 450 | |
| 451 | const ProgramPoint &L = GetProgramPoint(S, K, Pred->getLocationContext(),tag); |
| 452 | return generateNodeInternal(L, state, Pred); |
Ted Kremenek | 513f0b1 | 2009-02-19 23:45:28 +0000 | [diff] [blame] | 453 | } |
| 454 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 455 | ExplodedNode* |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 456 | GRStmtNodeBuilder::generateNodeInternal(const ProgramPoint &Loc, |
Zhongxing Xu | c90a0c2 | 2009-08-06 06:28:40 +0000 | [diff] [blame] | 457 | const GRState* State, |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 458 | ExplodedNode* Pred) { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 459 | bool IsNew; |
Zhongxing Xu | c90a0c2 | 2009-08-06 06:28:40 +0000 | [diff] [blame] | 460 | ExplodedNode* N = Eng.G->getNode(Loc, State, &IsNew); |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 461 | N->addPredecessor(Pred, *Eng.G); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 462 | Deferred.erase(Pred); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 463 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 464 | if (IsNew) { |
| 465 | Deferred.insert(N); |
| 466 | LastNode = N; |
| 467 | return N; |
| 468 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 469 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 470 | LastNode = NULL; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 471 | return NULL; |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 472 | } |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 473 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 474 | ExplodedNode* GRBranchNodeBuilder::generateNode(const GRState* State, |
| 475 | bool branch) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 476 | |
Ted Kremenek | af9f362 | 2009-07-20 18:44:36 +0000 | [diff] [blame] | 477 | // If the branch has been marked infeasible we should not generate a node. |
| 478 | if (!isFeasible(branch)) |
| 479 | return NULL; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 480 | |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 481 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 482 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 483 | ExplodedNode* Succ = |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 484 | Eng.G->getNode(BlockEdge(Src,branch ? DstT:DstF,Pred->getLocationContext()), |
| 485 | State, &IsNew); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 486 | |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 487 | Succ->addPredecessor(Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 488 | |
Ted Kremenek | af9f362 | 2009-07-20 18:44:36 +0000 | [diff] [blame] | 489 | if (branch) |
| 490 | GeneratedTrue = true; |
| 491 | else |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 492 | GeneratedFalse = true; |
| 493 | |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 494 | if (IsNew) { |
Ted Kremenek | 2531fce | 2008-01-30 23:24:39 +0000 | [diff] [blame] | 495 | Deferred.push_back(Succ); |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 496 | return Succ; |
| 497 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 498 | |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 499 | return NULL; |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 500 | } |
Ted Kremenek | 7ff1893 | 2008-01-29 23:32:35 +0000 | [diff] [blame] | 501 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 502 | GRBranchNodeBuilder::~GRBranchNodeBuilder() { |
| 503 | if (!GeneratedTrue) generateNode(Pred->State, true); |
| 504 | if (!GeneratedFalse) generateNode(Pred->State, false); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 505 | |
Ted Kremenek | 2531fce | 2008-01-30 23:24:39 +0000 | [diff] [blame] | 506 | for (DeferredTy::iterator I=Deferred.begin(), E=Deferred.end(); I!=E; ++I) |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 507 | if (!(*I)->isSink()) Eng.WList->Enqueue(*I); |
Ted Kremenek | 7ff1893 | 2008-01-29 23:32:35 +0000 | [diff] [blame] | 508 | } |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 509 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 510 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 511 | ExplodedNode* |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 512 | GRIndirectGotoNodeBuilder::generateNode(const iterator& I, const GRState* St, |
| 513 | bool isSink) { |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 514 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 515 | |
| 516 | ExplodedNode* Succ = Eng.G->getNode(BlockEdge(Src, I.getBlock(), |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 517 | Pred->getLocationContext()), St, &IsNew); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 518 | |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 519 | Succ->addPredecessor(Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 520 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 521 | if (IsNew) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 522 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 523 | if (isSink) |
| 524 | Succ->markAsSink(); |
| 525 | else |
| 526 | Eng.WList->Enqueue(Succ); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 527 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 528 | return Succ; |
| 529 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 530 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 531 | return NULL; |
| 532 | } |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 533 | |
| 534 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 535 | ExplodedNode* |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 536 | GRSwitchNodeBuilder::generateCaseStmtNode(const iterator& I, const GRState* St){ |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 537 | |
| 538 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 539 | |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 540 | ExplodedNode* Succ = Eng.G->getNode(BlockEdge(Src, I.getBlock(), |
| 541 | Pred->getLocationContext()), St, &IsNew); |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 542 | Succ->addPredecessor(Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 543 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 544 | if (IsNew) { |
| 545 | Eng.WList->Enqueue(Succ); |
| 546 | return Succ; |
| 547 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 548 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 549 | return NULL; |
| 550 | } |
| 551 | |
| 552 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 553 | ExplodedNode* |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 554 | GRSwitchNodeBuilder::generateDefaultCaseNode(const GRState* St, bool isSink) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 555 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 556 | // Get the block for the default case. |
| 557 | assert (Src->succ_rbegin() != Src->succ_rend()); |
| 558 | CFGBlock* DefaultBlock = *Src->succ_rbegin(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 559 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 560 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 561 | |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 562 | ExplodedNode* Succ = Eng.G->getNode(BlockEdge(Src, DefaultBlock, |
| 563 | Pred->getLocationContext()), St, &IsNew); |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 564 | Succ->addPredecessor(Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 565 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 566 | if (IsNew) { |
| 567 | if (isSink) |
| 568 | Succ->markAsSink(); |
| 569 | else |
| 570 | Eng.WList->Enqueue(Succ); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 571 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 572 | return Succ; |
| 573 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 574 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 575 | return NULL; |
| 576 | } |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 577 | |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 578 | GREndPathNodeBuilder::~GREndPathNodeBuilder() { |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 579 | // Auto-generate an EOP node if one has not been generated. |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 580 | if (!HasGeneratedNode) generateNode(Pred->State); |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 581 | } |
| 582 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 583 | ExplodedNode* |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 584 | GREndPathNodeBuilder::generateNode(const GRState* State, const void *tag, |
| 585 | ExplodedNode* P) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 586 | HasGeneratedNode = true; |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 587 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 588 | |
| 589 | ExplodedNode* Node = Eng.G->getNode(BlockEntrance(&B, |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 590 | Pred->getLocationContext(), tag), State, &IsNew); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 591 | |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 592 | Node->addPredecessor(P ? P : Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 593 | |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 594 | if (IsNew) { |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 595 | Eng.G->addEndOfPath(Node); |
Ted Kremenek | d004c41 | 2008-04-18 16:30:14 +0000 | [diff] [blame] | 596 | return Node; |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 597 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 598 | |
Ted Kremenek | d004c41 | 2008-04-18 16:30:14 +0000 | [diff] [blame] | 599 | return NULL; |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 600 | } |