Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 1 | //==- CoreEngine.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 | d99bd55 | 2010-12-23 19:38:26 +0000 | [diff] [blame] | 15 | #include "clang/StaticAnalyzer/PathSensitive/AnalysisManager.h" |
| 16 | #include "clang/StaticAnalyzer/PathSensitive/CoreEngine.h" |
| 17 | #include "clang/StaticAnalyzer/PathSensitive/ExprEngine.h" |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 18 | #include "clang/Index/TranslationUnit.h" |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 19 | #include "clang/AST/Expr.h" |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 20 | #include "llvm/Support/Casting.h" |
| 21 | #include "llvm/ADT/DenseMap.h" |
| 22 | #include <vector> |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 23 | #include <queue> |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 24 | |
| 25 | using llvm::cast; |
| 26 | using llvm::isa; |
| 27 | using namespace clang; |
Ted Kremenek | 98857c9 | 2010-12-23 07:20:52 +0000 | [diff] [blame] | 28 | using namespace ento; |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 29 | |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 30 | // This should be removed in the future. |
| 31 | namespace clang { |
Ted Kremenek | 98857c9 | 2010-12-23 07:20:52 +0000 | [diff] [blame] | 32 | namespace ento { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 33 | TransferFuncs* MakeCFRefCountTF(ASTContext& Ctx, bool GCEnabled, |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 34 | const LangOptions& lopts); |
| 35 | } |
Argyrios Kyrtzidis | ca08fba | 2010-12-22 18:53:20 +0000 | [diff] [blame] | 36 | } |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 37 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 38 | //===----------------------------------------------------------------------===// |
| 39 | // Worklist classes for exploration of reachable states. |
| 40 | //===----------------------------------------------------------------------===// |
| 41 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 42 | WorkList::Visitor::~Visitor() {} |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 43 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 44 | namespace { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 45 | class DFS : public WorkList { |
| 46 | llvm::SmallVector<WorkListUnit,20> Stack; |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 47 | public: |
| 48 | virtual bool hasWork() const { |
| 49 | return !Stack.empty(); |
| 50 | } |
| 51 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 52 | virtual void Enqueue(const WorkListUnit& U) { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 53 | Stack.push_back(U); |
| 54 | } |
| 55 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 56 | virtual WorkListUnit Dequeue() { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 57 | assert (!Stack.empty()); |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 58 | const WorkListUnit& U = Stack.back(); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 59 | Stack.pop_back(); // This technically "invalidates" U, but we are fine. |
| 60 | return U; |
| 61 | } |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 62 | |
| 63 | virtual bool VisitItemsInWorkList(Visitor &V) { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 64 | for (llvm::SmallVectorImpl<WorkListUnit>::iterator |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 65 | I = Stack.begin(), E = Stack.end(); I != E; ++I) { |
| 66 | if (V.Visit(*I)) |
| 67 | return true; |
| 68 | } |
| 69 | return false; |
| 70 | } |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 71 | }; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 72 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 73 | class BFS : public WorkList { |
| 74 | std::deque<WorkListUnit> Queue; |
Ted Kremenek | 2c32773 | 2009-05-01 22:18:46 +0000 | [diff] [blame] | 75 | public: |
| 76 | virtual bool hasWork() const { |
| 77 | return !Queue.empty(); |
| 78 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 79 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 80 | virtual void Enqueue(const WorkListUnit& U) { |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 81 | Queue.push_front(U); |
Ted Kremenek | 2c32773 | 2009-05-01 22:18:46 +0000 | [diff] [blame] | 82 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 83 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 84 | virtual WorkListUnit Dequeue() { |
| 85 | WorkListUnit U = Queue.front(); |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 86 | Queue.pop_front(); |
Ted Kremenek | 2c32773 | 2009-05-01 22:18:46 +0000 | [diff] [blame] | 87 | return U; |
| 88 | } |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 89 | |
| 90 | virtual bool VisitItemsInWorkList(Visitor &V) { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 91 | for (std::deque<WorkListUnit>::iterator |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 92 | I = Queue.begin(), E = Queue.end(); I != E; ++I) { |
| 93 | if (V.Visit(*I)) |
| 94 | return true; |
| 95 | } |
| 96 | return false; |
| 97 | } |
Ted Kremenek | 2c32773 | 2009-05-01 22:18:46 +0000 | [diff] [blame] | 98 | }; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 99 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 100 | } // end anonymous namespace |
| 101 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 102 | // Place the dstor for WorkList here because it contains virtual member |
Ted Kremenek | 2e12c2e | 2008-01-16 18:18:48 +0000 | [diff] [blame] | 103 | // functions, and we the code for the dstor generated in one compilation unit. |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 104 | WorkList::~WorkList() {} |
Ted Kremenek | 2e12c2e | 2008-01-16 18:18:48 +0000 | [diff] [blame] | 105 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 106 | WorkList *WorkList::MakeDFS() { return new DFS(); } |
| 107 | WorkList *WorkList::MakeBFS() { return new BFS(); } |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 108 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 109 | namespace { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 110 | class BFSBlockDFSContents : public WorkList { |
| 111 | std::deque<WorkListUnit> Queue; |
| 112 | llvm::SmallVector<WorkListUnit,20> Stack; |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 113 | public: |
| 114 | virtual bool hasWork() const { |
| 115 | return !Queue.empty() || !Stack.empty(); |
| 116 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 117 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 118 | virtual void Enqueue(const WorkListUnit& U) { |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 119 | if (isa<BlockEntrance>(U.getNode()->getLocation())) |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 120 | Queue.push_front(U); |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 121 | else |
| 122 | Stack.push_back(U); |
| 123 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 124 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 125 | virtual WorkListUnit Dequeue() { |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 126 | // Process all basic blocks to completion. |
| 127 | if (!Stack.empty()) { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 128 | const WorkListUnit& U = Stack.back(); |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 129 | Stack.pop_back(); // This technically "invalidates" U, but we are fine. |
| 130 | return U; |
| 131 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 132 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 133 | assert(!Queue.empty()); |
| 134 | // Don't use const reference. The subsequent pop_back() might make it |
| 135 | // unsafe. |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 136 | WorkListUnit U = Queue.front(); |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 137 | Queue.pop_front(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 138 | return U; |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 139 | } |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 140 | virtual bool VisitItemsInWorkList(Visitor &V) { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 141 | for (llvm::SmallVectorImpl<WorkListUnit>::iterator |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 142 | I = Stack.begin(), E = Stack.end(); I != E; ++I) { |
| 143 | if (V.Visit(*I)) |
| 144 | return true; |
| 145 | } |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 146 | for (std::deque<WorkListUnit>::iterator |
Ted Kremenek | b02788d | 2010-11-13 05:04:49 +0000 | [diff] [blame] | 147 | I = Queue.begin(), E = Queue.end(); I != E; ++I) { |
| 148 | if (V.Visit(*I)) |
| 149 | return true; |
| 150 | } |
| 151 | return false; |
| 152 | } |
| 153 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 154 | }; |
| 155 | } // end anonymous namespace |
| 156 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 157 | WorkList* WorkList::MakeBFSBlockDFSContents() { |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 158 | return new BFSBlockDFSContents(); |
| 159 | } |
| 160 | |
| 161 | //===----------------------------------------------------------------------===// |
| 162 | // Core analysis engine. |
| 163 | //===----------------------------------------------------------------------===// |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 164 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 165 | /// ExecuteWorkList - Run the worklist algorithm for a maximum number of steps. |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 166 | bool CoreEngine::ExecuteWorkList(const LocationContext *L, unsigned Steps, |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 167 | const GRState *InitState) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 168 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 169 | if (G->num_roots() == 0) { // Initialize the analysis by constructing |
| 170 | // the root if none exists. |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 171 | |
Zhongxing Xu | edb77fe | 2010-07-20 06:22:24 +0000 | [diff] [blame] | 172 | const CFGBlock* Entry = &(L->getCFG()->getEntry()); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 173 | |
| 174 | assert (Entry->empty() && |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 175 | "Entry block must be empty."); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 176 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 177 | assert (Entry->succ_size() == 1 && |
| 178 | "Entry block must have 1 successor."); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 179 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 180 | // Get the solitary successor. |
Zhongxing Xu | edb77fe | 2010-07-20 06:22:24 +0000 | [diff] [blame] | 181 | const CFGBlock* Succ = *(Entry->succ_begin()); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 182 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 183 | // Construct an edge representing the |
| 184 | // starting location in the function. |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 185 | BlockEdge StartLoc(Entry, Succ, L); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 186 | |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 187 | // Set the current block counter to being empty. |
| 188 | WList->setBlockCounter(BCounterFactory.GetEmptyCounter()); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 189 | |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 190 | if (!InitState) |
| 191 | // Generate the root. |
Ted Kremenek | 750b7ac | 2010-12-20 21:19:09 +0000 | [diff] [blame] | 192 | generateNode(StartLoc, getInitialState(L), 0); |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 193 | else |
Ted Kremenek | 750b7ac | 2010-12-20 21:19:09 +0000 | [diff] [blame] | 194 | generateNode(StartLoc, InitState, 0); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 195 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 196 | |
Tom Care | 472205b | 2010-09-29 23:48:13 +0000 | [diff] [blame] | 197 | // Check if we have a steps limit |
| 198 | bool UnlimitedSteps = Steps == 0; |
| 199 | |
| 200 | while (WList->hasWork()) { |
| 201 | if (!UnlimitedSteps) { |
| 202 | if (Steps == 0) |
| 203 | break; |
| 204 | --Steps; |
| 205 | } |
| 206 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 207 | const WorkListUnit& WU = WList->Dequeue(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 208 | |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 209 | // Set the current block counter. |
| 210 | WList->setBlockCounter(WU.getBlockCounter()); |
| 211 | |
| 212 | // Retrieve the node. |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 213 | ExplodedNode* Node = WU.getNode(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 214 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 215 | // Dispatch on the location type. |
| 216 | switch (Node->getLocation().getKind()) { |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 217 | case ProgramPoint::BlockEdgeKind: |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 218 | HandleBlockEdge(cast<BlockEdge>(Node->getLocation()), Node); |
| 219 | break; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 220 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 221 | case ProgramPoint::BlockEntranceKind: |
| 222 | HandleBlockEntrance(cast<BlockEntrance>(Node->getLocation()), Node); |
| 223 | break; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 224 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 225 | case ProgramPoint::BlockExitKind: |
Ted Kremenek | e584359 | 2008-01-15 00:24:08 +0000 | [diff] [blame] | 226 | assert (false && "BlockExit location never occur in forward analysis."); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 227 | break; |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 228 | |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 229 | case ProgramPoint::CallEnterKind: |
| 230 | HandleCallEnter(cast<CallEnter>(Node->getLocation()), WU.getBlock(), |
| 231 | WU.getIndex(), Node); |
| 232 | break; |
| 233 | |
| 234 | case ProgramPoint::CallExitKind: |
| 235 | HandleCallExit(cast<CallExit>(Node->getLocation()), Node); |
| 236 | break; |
| 237 | |
Ted Kremenek | d9de9f1 | 2008-12-16 22:13:33 +0000 | [diff] [blame] | 238 | default: |
Zhongxing Xu | 1ade326 | 2010-11-16 07:52:17 +0000 | [diff] [blame] | 239 | assert(isa<PostStmt>(Node->getLocation()) || |
| 240 | isa<PostInitializer>(Node->getLocation())); |
| 241 | HandlePostStmt(WU.getBlock(), WU.getIndex(), Node); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 242 | break; |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 243 | } |
| 244 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 245 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 246 | SubEng.ProcessEndWorklist(hasWorkRemaining()); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 247 | return WList->hasWork(); |
| 248 | } |
| 249 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 250 | void CoreEngine::ExecuteWorkListWithInitialState(const LocationContext *L, |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 251 | unsigned Steps, |
| 252 | const GRState *InitState, |
| 253 | ExplodedNodeSet &Dst) { |
| 254 | ExecuteWorkList(L, Steps, InitState); |
| 255 | for (llvm::SmallVectorImpl<ExplodedNode*>::iterator I = G->EndNodes.begin(), |
| 256 | E = G->EndNodes.end(); I != E; ++I) { |
| 257 | Dst.Add(*I); |
| 258 | } |
| 259 | } |
| 260 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 261 | void CoreEngine::HandleCallEnter(const CallEnter &L, const CFGBlock *Block, |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 262 | unsigned Index, ExplodedNode *Pred) { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 263 | CallEnterNodeBuilder Builder(*this, Pred, L.getCallExpr(), |
Zhongxing Xu | 84f65e0 | 2010-07-19 01:31:21 +0000 | [diff] [blame] | 264 | L.getCalleeContext(), Block, Index); |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 265 | ProcessCallEnter(Builder); |
| 266 | } |
| 267 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 268 | void CoreEngine::HandleCallExit(const CallExit &L, ExplodedNode *Pred) { |
| 269 | CallExitNodeBuilder Builder(*this, Pred); |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 270 | ProcessCallExit(Builder); |
| 271 | } |
Zhongxing Xu | 82003da | 2009-08-06 10:00:15 +0000 | [diff] [blame] | 272 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 273 | void CoreEngine::HandleBlockEdge(const BlockEdge& L, ExplodedNode* Pred) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 274 | |
Zhongxing Xu | edb77fe | 2010-07-20 06:22:24 +0000 | [diff] [blame] | 275 | const CFGBlock* Blk = L.getDst(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 276 | |
| 277 | // Check if we are entering the EXIT block. |
Zhongxing Xu | d2ab38e | 2009-12-23 08:54:57 +0000 | [diff] [blame] | 278 | if (Blk == &(L.getLocationContext()->getCFG()->getExit())) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 279 | |
Zhongxing Xu | d2ab38e | 2009-12-23 08:54:57 +0000 | [diff] [blame] | 280 | assert (L.getLocationContext()->getCFG()->getExit().size() == 0 |
Ted Kremenek | 997d872 | 2008-01-29 00:33:40 +0000 | [diff] [blame] | 281 | && "EXIT block cannot contain Stmts."); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 282 | |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 283 | // Process the final state transition. |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 284 | EndPathNodeBuilder Builder(Blk, Pred, this); |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 285 | ProcessEndPath(Builder); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 286 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 287 | // This path is done. Don't enqueue any more nodes. |
| 288 | return; |
| 289 | } |
Ted Kremenek | 17f4dbd | 2008-02-29 20:27:50 +0000 | [diff] [blame] | 290 | |
| 291 | // FIXME: Should we allow ProcessBlockEntrance to also manipulate state? |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 292 | |
Zhongxing Xu | 3c0c81a | 2010-03-23 05:05:02 +0000 | [diff] [blame] | 293 | if (ProcessBlockEntrance(Blk, Pred, WList->getBlockCounter())) |
Ted Kremenek | 750b7ac | 2010-12-20 21:19:09 +0000 | [diff] [blame] | 294 | generateNode(BlockEntrance(Blk, Pred->getLocationContext()), |
Ted Kremenek | 090d62e | 2010-06-29 21:58:54 +0000 | [diff] [blame] | 295 | Pred->State, Pred); |
Ted Kremenek | 2b4adff | 2010-08-11 00:03:02 +0000 | [diff] [blame] | 296 | else { |
| 297 | blocksAborted.push_back(std::make_pair(L, Pred)); |
| 298 | } |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 299 | } |
| 300 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 301 | void CoreEngine::HandleBlockEntrance(const BlockEntrance& L, |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 302 | ExplodedNode* Pred) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 303 | |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 304 | // Increment the block counter. |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 305 | BlockCounter Counter = WList->getBlockCounter(); |
Zhongxing Xu | 3c0c81a | 2010-03-23 05:05:02 +0000 | [diff] [blame] | 306 | Counter = BCounterFactory.IncrementCount(Counter, |
| 307 | Pred->getLocationContext()->getCurrentStackFrame(), |
| 308 | L.getBlock()->getBlockID()); |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 309 | WList->setBlockCounter(Counter); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 310 | |
| 311 | // Process the entrance of the block. |
Ted Kremenek | 4cad5fc | 2009-12-16 03:18:58 +0000 | [diff] [blame] | 312 | if (CFGElement E = L.getFirstElement()) { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 313 | StmtNodeBuilder Builder(L.getBlock(), 0, Pred, this, |
| 314 | SubEng.getStateManager()); |
Zhongxing Xu | 5d30c69 | 2010-11-15 08:48:43 +0000 | [diff] [blame] | 315 | ProcessElement(E, Builder); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 316 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 317 | else |
Ted Kremenek | e584359 | 2008-01-15 00:24:08 +0000 | [diff] [blame] | 318 | HandleBlockExit(L.getBlock(), Pred); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 319 | } |
| 320 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 321 | void CoreEngine::HandleBlockExit(const CFGBlock * B, ExplodedNode* Pred) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 322 | |
Zhongxing Xu | edb77fe | 2010-07-20 06:22:24 +0000 | [diff] [blame] | 323 | if (const Stmt* Term = B->getTerminator()) { |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 324 | switch (Term->getStmtClass()) { |
| 325 | default: |
| 326 | assert(false && "Analysis for this terminator not implemented."); |
| 327 | break; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 328 | |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 329 | case Stmt::BinaryOperatorClass: // '&&' and '||' |
| 330 | HandleBranch(cast<BinaryOperator>(Term)->getLHS(), Term, B, Pred); |
| 331 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 332 | |
Ted Kremenek | 3f2f1ad | 2008-02-05 00:26:40 +0000 | [diff] [blame] | 333 | case Stmt::ConditionalOperatorClass: |
| 334 | HandleBranch(cast<ConditionalOperator>(Term)->getCond(), Term, B, Pred); |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 335 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 336 | |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 337 | // FIXME: Use constant-folding in CFG construction to simplify this |
| 338 | // case. |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 339 | |
Ted Kremenek | 3f2f1ad | 2008-02-05 00:26:40 +0000 | [diff] [blame] | 340 | case Stmt::ChooseExprClass: |
| 341 | HandleBranch(cast<ChooseExpr>(Term)->getCond(), Term, B, Pred); |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 342 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 343 | |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 344 | case Stmt::DoStmtClass: |
| 345 | HandleBranch(cast<DoStmt>(Term)->getCond(), Term, B, Pred); |
| 346 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 347 | |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 348 | case Stmt::ForStmtClass: |
| 349 | HandleBranch(cast<ForStmt>(Term)->getCond(), Term, B, Pred); |
| 350 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 351 | |
Ted Kremenek | 632bcb8 | 2008-02-13 16:56:51 +0000 | [diff] [blame] | 352 | case Stmt::ContinueStmtClass: |
| 353 | case Stmt::BreakStmtClass: |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 354 | case Stmt::GotoStmtClass: |
Ted Kremenek | 3f2f1ad | 2008-02-05 00:26:40 +0000 | [diff] [blame] | 355 | break; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 356 | |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 357 | case Stmt::IfStmtClass: |
| 358 | HandleBranch(cast<IfStmt>(Term)->getCond(), Term, B, Pred); |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 359 | return; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 360 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 361 | case Stmt::IndirectGotoStmtClass: { |
| 362 | // Only 1 successor: the indirect goto dispatch block. |
| 363 | assert (B->succ_size() == 1); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 364 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 365 | IndirectGotoNodeBuilder |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 366 | builder(Pred, B, cast<IndirectGotoStmt>(Term)->getTarget(), |
| 367 | *(B->succ_begin()), this); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 368 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 369 | ProcessIndirectGoto(builder); |
| 370 | return; |
| 371 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 372 | |
Ted Kremenek | 1781080 | 2008-11-12 19:24:17 +0000 | [diff] [blame] | 373 | case Stmt::ObjCForCollectionStmtClass: { |
| 374 | // In the case of ObjCForCollectionStmt, it appears twice in a CFG: |
| 375 | // |
| 376 | // (1) inside a basic block, which represents the binding of the |
| 377 | // 'element' variable to a value. |
| 378 | // (2) in a terminator, which represents the branch. |
| 379 | // |
| 380 | // For (1), subengines will bind a value (i.e., 0 or 1) indicating |
| 381 | // whether or not collection contains any more elements. We cannot |
| 382 | // just test to see if the element is nil because a container can |
| 383 | // contain nil elements. |
| 384 | HandleBranch(Term, Term, B, Pred); |
| 385 | return; |
| 386 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 387 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 388 | case Stmt::SwitchStmtClass: { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 389 | SwitchNodeBuilder builder(Pred, B, cast<SwitchStmt>(Term)->getCond(), |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 390 | this); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 391 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 392 | ProcessSwitch(builder); |
| 393 | return; |
| 394 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 395 | |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 396 | case Stmt::WhileStmtClass: |
| 397 | HandleBranch(cast<WhileStmt>(Term)->getCond(), Term, B, Pred); |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 398 | return; |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 399 | } |
| 400 | } |
Ted Kremenek | 822f737 | 2008-02-12 21:51:20 +0000 | [diff] [blame] | 401 | |
| 402 | assert (B->succ_size() == 1 && |
| 403 | "Blocks with no terminator should have at most 1 successor."); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 404 | |
Ted Kremenek | 750b7ac | 2010-12-20 21:19:09 +0000 | [diff] [blame] | 405 | generateNode(BlockEdge(B, *(B->succ_begin()), Pred->getLocationContext()), |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 406 | Pred->State, Pred); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 407 | } |
| 408 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 409 | void CoreEngine::HandleBranch(const Stmt* Cond, const Stmt* Term, |
Zhongxing Xu | edb77fe | 2010-07-20 06:22:24 +0000 | [diff] [blame] | 410 | const CFGBlock * B, ExplodedNode* Pred) { |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 411 | assert (B->succ_size() == 2); |
| 412 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 413 | BranchNodeBuilder Builder(B, *(B->succ_begin()), *(B->succ_begin()+1), |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 414 | Pred, this); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 415 | |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 416 | ProcessBranch(Cond, Term, Builder); |
| 417 | } |
| 418 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 419 | void CoreEngine::HandlePostStmt(const CFGBlock* B, unsigned StmtIdx, |
Zhongxing Xu | 1ade326 | 2010-11-16 07:52:17 +0000 | [diff] [blame] | 420 | ExplodedNode* Pred) { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 421 | assert (!B->empty()); |
| 422 | |
Ted Kremenek | e584359 | 2008-01-15 00:24:08 +0000 | [diff] [blame] | 423 | if (StmtIdx == B->size()) |
| 424 | HandleBlockExit(B, Pred); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 425 | else { |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 426 | StmtNodeBuilder Builder(B, StmtIdx, Pred, this, |
| 427 | SubEng.getStateManager()); |
Zhongxing Xu | 5d30c69 | 2010-11-15 08:48:43 +0000 | [diff] [blame] | 428 | ProcessElement((*B)[StmtIdx], Builder); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 429 | } |
| 430 | } |
| 431 | |
Ted Kremenek | 750b7ac | 2010-12-20 21:19:09 +0000 | [diff] [blame] | 432 | /// generateNode - Utility method to generate nodes, hook up successors, |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 433 | /// and add nodes to the worklist. |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 434 | void CoreEngine::generateNode(const ProgramPoint& Loc, |
| 435 | const GRState* State, ExplodedNode* Pred) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 436 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 437 | bool IsNew; |
Zhongxing Xu | c90a0c2 | 2009-08-06 06:28:40 +0000 | [diff] [blame] | 438 | ExplodedNode* Node = G->getNode(Loc, State, &IsNew); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 439 | |
| 440 | if (Pred) |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 441 | Node->addPredecessor(Pred, *G); // Link 'Node' with its predecessor. |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 442 | else { |
| 443 | assert (IsNew); |
| 444 | G->addRoot(Node); // 'Node' has no predecessor. Make it a root. |
| 445 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 446 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 447 | // Only add 'Node' to the worklist if it was freshly generated. |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 448 | if (IsNew) WList->Enqueue(Node); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 449 | } |
| 450 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 451 | StmtNodeBuilder::StmtNodeBuilder(const CFGBlock* b, unsigned idx, |
| 452 | ExplodedNode* N, CoreEngine* e, |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 453 | GRStateManager &mgr) |
Ted Kremenek | 982b32b | 2010-10-20 23:48:34 +0000 | [diff] [blame] | 454 | : Eng(*e), B(*b), Idx(idx), Pred(N), Mgr(mgr), |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 455 | PurgingDeadSymbols(false), BuildSinks(false), HasGeneratedNode(false), |
| 456 | PointKind(ProgramPoint::PostStmtKind), Tag(0) { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 457 | Deferred.insert(N); |
Zhongxing Xu | d041bc6 | 2010-02-26 02:38:09 +0000 | [diff] [blame] | 458 | CleanedState = Pred->getState(); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 459 | } |
| 460 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 461 | StmtNodeBuilder::~StmtNodeBuilder() { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 462 | for (DeferredTy::iterator I=Deferred.begin(), E=Deferred.end(); I!=E; ++I) |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 463 | if (!(*I)->isSink()) |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 464 | GenerateAutoTransition(*I); |
| 465 | } |
| 466 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 467 | void StmtNodeBuilder::GenerateAutoTransition(ExplodedNode* N) { |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 468 | assert (!N->isSink()); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 469 | |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 470 | // Check if this node entered a callee. |
| 471 | if (isa<CallEnter>(N->getLocation())) { |
| 472 | // Still use the index of the CallExpr. It's needed to create the callee |
| 473 | // StackFrameContext. |
Zhongxing Xu | edb77fe | 2010-07-20 06:22:24 +0000 | [diff] [blame] | 474 | Eng.WList->Enqueue(N, &B, Idx); |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 475 | return; |
| 476 | } |
| 477 | |
Zhongxing Xu | 1ade326 | 2010-11-16 07:52:17 +0000 | [diff] [blame] | 478 | // Do not create extra nodes. Move to the next CFG element. |
| 479 | if (isa<PostInitializer>(N->getLocation())) { |
| 480 | Eng.WList->Enqueue(N, &B, Idx+1); |
| 481 | return; |
| 482 | } |
| 483 | |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 484 | PostStmt Loc(getStmt(), N->getLocationContext()); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 485 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 486 | if (Loc == N->getLocation()) { |
| 487 | // Note: 'N' should be a fresh node because otherwise it shouldn't be |
| 488 | // a member of Deferred. |
Zhongxing Xu | edb77fe | 2010-07-20 06:22:24 +0000 | [diff] [blame] | 489 | Eng.WList->Enqueue(N, &B, Idx+1); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 490 | return; |
| 491 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 492 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 493 | bool IsNew; |
Zhongxing Xu | c90a0c2 | 2009-08-06 06:28:40 +0000 | [diff] [blame] | 494 | ExplodedNode* Succ = Eng.G->getNode(Loc, N->State, &IsNew); |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 495 | Succ->addPredecessor(N, *Eng.G); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 496 | |
| 497 | if (IsNew) |
Zhongxing Xu | edb77fe | 2010-07-20 06:22:24 +0000 | [diff] [blame] | 498 | Eng.WList->Enqueue(Succ, &B, Idx+1); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 499 | } |
| 500 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 501 | ExplodedNode* StmtNodeBuilder::MakeNode(ExplodedNodeSet& Dst, const Stmt* S, |
Zhongxing Xu | 5eb08f7 | 2010-04-14 06:35:09 +0000 | [diff] [blame] | 502 | ExplodedNode* Pred, const GRState* St, |
| 503 | ProgramPoint::Kind K) { |
Ted Kremenek | bd2c800 | 2010-10-20 23:38:56 +0000 | [diff] [blame] | 504 | |
Zhongxing Xu | 5eb08f7 | 2010-04-14 06:35:09 +0000 | [diff] [blame] | 505 | ExplodedNode* N = generateNode(S, St, Pred, K); |
| 506 | |
| 507 | if (N) { |
| 508 | if (BuildSinks) |
| 509 | N->markAsSink(); |
Ted Kremenek | 982b32b | 2010-10-20 23:48:34 +0000 | [diff] [blame] | 510 | else |
Zhongxing Xu | 5eb08f7 | 2010-04-14 06:35:09 +0000 | [diff] [blame] | 511 | Dst.Add(N); |
Zhongxing Xu | 5eb08f7 | 2010-04-14 06:35:09 +0000 | [diff] [blame] | 512 | } |
| 513 | |
| 514 | return N; |
| 515 | } |
| 516 | |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame] | 517 | static ProgramPoint GetProgramPoint(const Stmt *S, ProgramPoint::Kind K, |
| 518 | const LocationContext *LC, const void *tag){ |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 519 | switch (K) { |
| 520 | default: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame] | 521 | assert(false && "Unhandled ProgramPoint kind"); |
| 522 | case ProgramPoint::PreStmtKind: |
| 523 | return PreStmt(S, LC, tag); |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 524 | case ProgramPoint::PostStmtKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame] | 525 | return PostStmt(S, LC, tag); |
| 526 | case ProgramPoint::PreLoadKind: |
| 527 | return PreLoad(S, LC, tag); |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 528 | case ProgramPoint::PostLoadKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame] | 529 | return PostLoad(S, LC, tag); |
| 530 | case ProgramPoint::PreStoreKind: |
| 531 | return PreStore(S, LC, tag); |
Ted Kremenek | a196618 | 2008-10-17 20:49:23 +0000 | [diff] [blame] | 532 | case ProgramPoint::PostStoreKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame] | 533 | return PostStore(S, LC, tag); |
Ted Kremenek | a6e0832 | 2009-05-07 18:27:16 +0000 | [diff] [blame] | 534 | case ProgramPoint::PostLValueKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame] | 535 | return PostLValue(S, LC, tag); |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 536 | case ProgramPoint::PostPurgeDeadSymbolsKind: |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame] | 537 | return PostPurgeDeadSymbols(S, LC, tag); |
Ted Kremenek | 9a935fb | 2008-06-18 05:34:07 +0000 | [diff] [blame] | 538 | } |
| 539 | } |
| 540 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 541 | ExplodedNode* |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 542 | StmtNodeBuilder::generateNodeInternal(const Stmt* S, const GRState* state, |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 543 | ExplodedNode* Pred, |
Ted Kremenek | df24000 | 2009-04-11 00:11:10 +0000 | [diff] [blame] | 544 | ProgramPoint::Kind K, |
| 545 | const void *tag) { |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame] | 546 | |
Zhongxing Xu | d2ab38e | 2009-12-23 08:54:57 +0000 | [diff] [blame] | 547 | const ProgramPoint &L = GetProgramPoint(S, K, Pred->getLocationContext(),tag); |
Ted Kremenek | 5e1f78a | 2009-11-11 03:26:34 +0000 | [diff] [blame] | 548 | return generateNodeInternal(L, state, Pred); |
Ted Kremenek | 513f0b1 | 2009-02-19 23:45:28 +0000 | [diff] [blame] | 549 | } |
| 550 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 551 | ExplodedNode* |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 552 | StmtNodeBuilder::generateNodeInternal(const ProgramPoint &Loc, |
Zhongxing Xu | c90a0c2 | 2009-08-06 06:28:40 +0000 | [diff] [blame] | 553 | const GRState* State, |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 554 | ExplodedNode* Pred) { |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 555 | bool IsNew; |
Zhongxing Xu | c90a0c2 | 2009-08-06 06:28:40 +0000 | [diff] [blame] | 556 | ExplodedNode* N = Eng.G->getNode(Loc, State, &IsNew); |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 557 | N->addPredecessor(Pred, *Eng.G); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 558 | Deferred.erase(Pred); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 559 | |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 560 | if (IsNew) { |
| 561 | Deferred.insert(N); |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 562 | return N; |
| 563 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 564 | |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 565 | return NULL; |
Ted Kremenek | 3e74366 | 2008-01-14 23:24:37 +0000 | [diff] [blame] | 566 | } |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 567 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 568 | ExplodedNode* BranchNodeBuilder::generateNode(const GRState* State, |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 569 | bool branch) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 570 | |
Ted Kremenek | af9f362 | 2009-07-20 18:44:36 +0000 | [diff] [blame] | 571 | // If the branch has been marked infeasible we should not generate a node. |
| 572 | if (!isFeasible(branch)) |
| 573 | return NULL; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 574 | |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 575 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 576 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 577 | ExplodedNode* Succ = |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 578 | Eng.G->getNode(BlockEdge(Src,branch ? DstT:DstF,Pred->getLocationContext()), |
| 579 | State, &IsNew); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 580 | |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 581 | Succ->addPredecessor(Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 582 | |
Ted Kremenek | af9f362 | 2009-07-20 18:44:36 +0000 | [diff] [blame] | 583 | if (branch) |
| 584 | GeneratedTrue = true; |
| 585 | else |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 586 | GeneratedFalse = true; |
| 587 | |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 588 | if (IsNew) { |
Ted Kremenek | 2531fce | 2008-01-30 23:24:39 +0000 | [diff] [blame] | 589 | Deferred.push_back(Succ); |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 590 | return Succ; |
| 591 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 592 | |
Ted Kremenek | a50d985 | 2008-01-30 23:03:39 +0000 | [diff] [blame] | 593 | return NULL; |
Ted Kremenek | 9b4211d | 2008-01-29 22:56:11 +0000 | [diff] [blame] | 594 | } |
Ted Kremenek | 7ff1893 | 2008-01-29 23:32:35 +0000 | [diff] [blame] | 595 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 596 | BranchNodeBuilder::~BranchNodeBuilder() { |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 597 | if (!GeneratedTrue) generateNode(Pred->State, true); |
| 598 | if (!GeneratedFalse) generateNode(Pred->State, false); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 599 | |
Ted Kremenek | 2531fce | 2008-01-30 23:24:39 +0000 | [diff] [blame] | 600 | for (DeferredTy::iterator I=Deferred.begin(), E=Deferred.end(); I!=E; ++I) |
Ted Kremenek | 90ae68f | 2008-02-12 18:08:17 +0000 | [diff] [blame] | 601 | if (!(*I)->isSink()) Eng.WList->Enqueue(*I); |
Ted Kremenek | 7ff1893 | 2008-01-29 23:32:35 +0000 | [diff] [blame] | 602 | } |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 603 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 604 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 605 | ExplodedNode* |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 606 | IndirectGotoNodeBuilder::generateNode(const iterator& I, const GRState* St, |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 607 | bool isSink) { |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 608 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 609 | |
| 610 | ExplodedNode* Succ = Eng.G->getNode(BlockEdge(Src, I.getBlock(), |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 611 | Pred->getLocationContext()), St, &IsNew); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 612 | |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 613 | Succ->addPredecessor(Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 614 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 615 | if (IsNew) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 616 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 617 | if (isSink) |
| 618 | Succ->markAsSink(); |
| 619 | else |
| 620 | Eng.WList->Enqueue(Succ); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 621 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 622 | return Succ; |
| 623 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 624 | |
Ted Kremenek | 7022efb | 2008-02-13 00:24:44 +0000 | [diff] [blame] | 625 | return NULL; |
| 626 | } |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 627 | |
| 628 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 629 | ExplodedNode* |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 630 | SwitchNodeBuilder::generateCaseStmtNode(const iterator& I, const GRState* St){ |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 631 | |
| 632 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 633 | |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 634 | ExplodedNode* Succ = Eng.G->getNode(BlockEdge(Src, I.getBlock(), |
| 635 | Pred->getLocationContext()), St, &IsNew); |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 636 | Succ->addPredecessor(Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 637 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 638 | if (IsNew) { |
| 639 | Eng.WList->Enqueue(Succ); |
| 640 | return Succ; |
| 641 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 642 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 643 | return NULL; |
| 644 | } |
| 645 | |
| 646 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 647 | ExplodedNode* |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 648 | SwitchNodeBuilder::generateDefaultCaseNode(const GRState* St, bool isSink) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 649 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 650 | // Get the block for the default case. |
| 651 | assert (Src->succ_rbegin() != Src->succ_rend()); |
| 652 | CFGBlock* DefaultBlock = *Src->succ_rbegin(); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 653 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 654 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 655 | |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 656 | ExplodedNode* Succ = Eng.G->getNode(BlockEdge(Src, DefaultBlock, |
| 657 | Pred->getLocationContext()), St, &IsNew); |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 658 | Succ->addPredecessor(Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 659 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 660 | if (IsNew) { |
| 661 | if (isSink) |
| 662 | Succ->markAsSink(); |
| 663 | else |
| 664 | Eng.WList->Enqueue(Succ); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 665 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 666 | return Succ; |
| 667 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 668 | |
Ted Kremenek | 80ebc1d | 2008-02-13 23:08:21 +0000 | [diff] [blame] | 669 | return NULL; |
| 670 | } |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 671 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 672 | EndPathNodeBuilder::~EndPathNodeBuilder() { |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 673 | // Auto-generate an EOP node if one has not been generated. |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 674 | if (!HasGeneratedNode) { |
| 675 | // If we are in an inlined call, generate CallExit node. |
| 676 | if (Pred->getLocationContext()->getParent()) |
| 677 | GenerateCallExitNode(Pred->State); |
| 678 | else |
| 679 | generateNode(Pred->State); |
| 680 | } |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 681 | } |
| 682 | |
Zhongxing Xu | 20227f7 | 2009-08-06 01:32:16 +0000 | [diff] [blame] | 683 | ExplodedNode* |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 684 | EndPathNodeBuilder::generateNode(const GRState* State, const void *tag, |
Zhongxing Xu | 107f759 | 2009-08-06 12:48:26 +0000 | [diff] [blame] | 685 | ExplodedNode* P) { |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 686 | HasGeneratedNode = true; |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 687 | bool IsNew; |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 688 | |
| 689 | ExplodedNode* Node = Eng.G->getNode(BlockEntrance(&B, |
Zhongxing Xu | e1190f7 | 2009-08-15 03:17:38 +0000 | [diff] [blame] | 690 | Pred->getLocationContext(), tag), State, &IsNew); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 691 | |
Ted Kremenek | c3661de | 2009-10-07 00:42:52 +0000 | [diff] [blame] | 692 | Node->addPredecessor(P ? P : Pred, *Eng.G); |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 693 | |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 694 | if (IsNew) { |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 695 | Eng.G->addEndOfPath(Node); |
Ted Kremenek | d004c41 | 2008-04-18 16:30:14 +0000 | [diff] [blame] | 696 | return Node; |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 697 | } |
Mike Stump | 11289f4 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 698 | |
Ted Kremenek | d004c41 | 2008-04-18 16:30:14 +0000 | [diff] [blame] | 699 | return NULL; |
Ted Kremenek | 811c2b4 | 2008-04-11 22:03:04 +0000 | [diff] [blame] | 700 | } |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 701 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 702 | void EndPathNodeBuilder::GenerateCallExitNode(const GRState *state) { |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 703 | HasGeneratedNode = true; |
| 704 | // Create a CallExit node and enqueue it. |
| 705 | const StackFrameContext *LocCtx |
| 706 | = cast<StackFrameContext>(Pred->getLocationContext()); |
| 707 | const Stmt *CE = LocCtx->getCallSite(); |
| 708 | |
| 709 | // Use the the callee location context. |
| 710 | CallExit Loc(CE, LocCtx); |
| 711 | |
| 712 | bool isNew; |
| 713 | ExplodedNode *Node = Eng.G->getNode(Loc, state, &isNew); |
| 714 | Node->addPredecessor(Pred, *Eng.G); |
| 715 | |
| 716 | if (isNew) |
| 717 | Eng.WList->Enqueue(Node); |
| 718 | } |
| 719 | |
| 720 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 721 | void CallEnterNodeBuilder::generateNode(const GRState *state) { |
Zhongxing Xu | 84f65e0 | 2010-07-19 01:31:21 +0000 | [diff] [blame] | 722 | // Check if the callee is in the same translation unit. |
| 723 | if (CalleeCtx->getTranslationUnit() != |
| 724 | Pred->getLocationContext()->getTranslationUnit()) { |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 725 | // Create a new engine. We must be careful that the new engine should not |
| 726 | // reference data structures owned by the old engine. |
| 727 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 728 | AnalysisManager &OldMgr = Eng.SubEng.getAnalysisManager(); |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 729 | |
| 730 | // Get the callee's translation unit. |
| 731 | idx::TranslationUnit *TU = CalleeCtx->getTranslationUnit(); |
| 732 | |
| 733 | // Create a new AnalysisManager with components of the callee's |
| 734 | // TranslationUnit. |
Sebastian Redl | d44cd6a | 2010-08-18 23:57:06 +0000 | [diff] [blame] | 735 | // The Diagnostic is actually shared when we create ASTUnits from AST files. |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 736 | AnalysisManager AMgr(TU->getASTContext(), TU->getDiagnostic(), |
| 737 | OldMgr.getLangOptions(), |
| 738 | OldMgr.getPathDiagnosticClient(), |
| 739 | OldMgr.getStoreManagerCreator(), |
| 740 | OldMgr.getConstraintManagerCreator(), |
| 741 | OldMgr.getIndexer(), |
Tom Care | c88ed95 | 2010-09-14 21:35:27 +0000 | [diff] [blame] | 742 | OldMgr.getMaxNodes(), OldMgr.getMaxVisit(), |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 743 | OldMgr.shouldVisualizeGraphviz(), |
| 744 | OldMgr.shouldVisualizeUbigraph(), |
| 745 | OldMgr.shouldPurgeDead(), |
| 746 | OldMgr.shouldEagerlyAssume(), |
| 747 | OldMgr.shouldTrimGraph(), |
Ted Kremenek | 4a2b237 | 2010-08-03 00:09:51 +0000 | [diff] [blame] | 748 | OldMgr.shouldInlineCall(), |
Marcin Swiderski | 99a9040 | 2010-09-30 07:41:24 +0000 | [diff] [blame] | 749 | OldMgr.getAnalysisContextManager().getUseUnoptimizedCFG(), |
| 750 | OldMgr.getAnalysisContextManager().getAddImplicitDtors(), |
| 751 | OldMgr.getAnalysisContextManager().getAddInitializers()); |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 752 | llvm::OwningPtr<TransferFuncs> TF(MakeCFRefCountTF(AMgr.getASTContext(), |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 753 | /* GCEnabled */ false, |
| 754 | AMgr.getLangOptions())); |
| 755 | // Create the new engine. |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 756 | ExprEngine NewEng(AMgr, TF.take()); |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 757 | |
| 758 | // Create the new LocationContext. |
| 759 | AnalysisContext *NewAnaCtx = AMgr.getAnalysisContext(CalleeCtx->getDecl(), |
| 760 | CalleeCtx->getTranslationUnit()); |
Zhongxing Xu | cb29802 | 2010-11-24 08:53:20 +0000 | [diff] [blame] | 761 | const StackFrameContext *OldLocCtx = CalleeCtx; |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 762 | const StackFrameContext *NewLocCtx = AMgr.getStackFrame(NewAnaCtx, |
| 763 | OldLocCtx->getParent(), |
Ted Kremenek | 8219b82 | 2010-12-16 07:46:53 +0000 | [diff] [blame] | 764 | OldLocCtx->getCallSite(), |
Zhongxing Xu | adf644d | 2010-07-22 13:52:13 +0000 | [diff] [blame] | 765 | OldLocCtx->getCallSiteBlock(), |
| 766 | OldLocCtx->getIndex()); |
| 767 | |
| 768 | // Now create an initial state for the new engine. |
| 769 | const GRState *NewState = NewEng.getStateManager().MarshalState(state, |
| 770 | NewLocCtx); |
| 771 | ExplodedNodeSet ReturnNodes; |
| 772 | NewEng.ExecuteWorkListWithInitialState(NewLocCtx, AMgr.getMaxNodes(), |
| 773 | NewState, ReturnNodes); |
| 774 | return; |
Zhongxing Xu | 84f65e0 | 2010-07-19 01:31:21 +0000 | [diff] [blame] | 775 | } |
| 776 | |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 777 | // Get the callee entry block. |
Zhongxing Xu | cb29802 | 2010-11-24 08:53:20 +0000 | [diff] [blame] | 778 | const CFGBlock *Entry = &(CalleeCtx->getCFG()->getEntry()); |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 779 | assert(Entry->empty()); |
| 780 | assert(Entry->succ_size() == 1); |
| 781 | |
| 782 | // Get the solitary successor. |
| 783 | const CFGBlock *SuccB = *(Entry->succ_begin()); |
| 784 | |
| 785 | // Construct an edge representing the starting location in the callee. |
Zhongxing Xu | cb29802 | 2010-11-24 08:53:20 +0000 | [diff] [blame] | 786 | BlockEdge Loc(Entry, SuccB, CalleeCtx); |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 787 | |
| 788 | bool isNew; |
| 789 | ExplodedNode *Node = Eng.G->getNode(Loc, state, &isNew); |
| 790 | Node->addPredecessor(const_cast<ExplodedNode*>(Pred), *Eng.G); |
| 791 | |
| 792 | if (isNew) |
| 793 | Eng.WList->Enqueue(Node); |
| 794 | } |
| 795 | |
Argyrios Kyrtzidis | 1696f50 | 2010-12-22 18:53:44 +0000 | [diff] [blame] | 796 | void CallExitNodeBuilder::generateNode(const GRState *state) { |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 797 | // Get the callee's location context. |
| 798 | const StackFrameContext *LocCtx |
| 799 | = cast<StackFrameContext>(Pred->getLocationContext()); |
Zhongxing Xu | 2cf9b13 | 2010-11-20 08:17:16 +0000 | [diff] [blame] | 800 | // When exiting an implicit automatic obj dtor call, the callsite is the Stmt |
| 801 | // that triggers the dtor. |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 802 | PostStmt Loc(LocCtx->getCallSite(), LocCtx->getParent()); |
| 803 | bool isNew; |
| 804 | ExplodedNode *Node = Eng.G->getNode(Loc, state, &isNew); |
| 805 | Node->addPredecessor(const_cast<ExplodedNode*>(Pred), *Eng.G); |
| 806 | if (isNew) |
Zhongxing Xu | edb77fe | 2010-07-20 06:22:24 +0000 | [diff] [blame] | 807 | Eng.WList->Enqueue(Node, LocCtx->getCallSiteBlock(), |
Douglas Gregor | a2fbc94 | 2010-02-25 19:01:53 +0000 | [diff] [blame] | 808 | LocCtx->getIndex() + 1); |
| 809 | } |