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