1d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis//==- CoreEngine.cpp - Path-Sensitive Dataflow Engine ------------*- C++ -*-//
21eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump//
3f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//                     The LLVM Compiler Infrastructure
4f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//
5f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek// This file is distributed under the University of Illinois Open Source
6f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek// License. See LICENSE.TXT for details.
7f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//
8f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//===----------------------------------------------------------------------===//
9f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//
10f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//  This file defines a generic engine for intraprocedural, path-sensitive,
11f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//  dataflow analysis via graph reachability engine.
12f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//
13f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//===----------------------------------------------------------------------===//
14f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
15131579f198f9cc9e6405adbe6159110c283ec5a4Anna Zaks#define DEBUG_TYPE "CoreEngine"
16131579f198f9cc9e6405adbe6159110c283ec5a4Anna Zaks
179b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
189b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h"
199b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
20f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#include "clang/AST/Expr.h"
2146eaf7789a1059a7b42b7dbd183150c72df5738fTed Kremenek#include "clang/AST/StmtCXX.h"
22f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#include "llvm/Support/Casting.h"
23f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#include "llvm/ADT/DenseMap.h"
24131579f198f9cc9e6405adbe6159110c283ec5a4Anna Zaks#include "llvm/ADT/Statistic.h"
25131579f198f9cc9e6405adbe6159110c283ec5a4Anna Zaks
26f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenekusing namespace clang;
279ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenekusing namespace ento;
28f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
29df19fe7cafcb02859efeb6963cddeafef4350ddfAnna ZaksSTATISTIC(NumSteps,
30df19fe7cafcb02859efeb6963cddeafef4350ddfAnna Zaks            "The # of steps executed.");
31131579f198f9cc9e6405adbe6159110c283ec5a4Anna ZaksSTATISTIC(NumReachedMaxSteps,
32131579f198f9cc9e6405adbe6159110c283ec5a4Anna Zaks            "The # of times we reached the max number of steps.");
33638e2d31fceed041e7e16aada4188c94cb5797bbAnna ZaksSTATISTIC(NumPathsExplored,
34638e2d31fceed041e7e16aada4188c94cb5797bbAnna Zaks            "The # of paths explored by the analyzer.");
35131579f198f9cc9e6405adbe6159110c283ec5a4Anna Zaks
36e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek//===----------------------------------------------------------------------===//
37e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek// Worklist classes for exploration of reachable states.
38e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek//===----------------------------------------------------------------------===//
39e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek
40d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios KyrtzidisWorkList::Visitor::~Visitor() {}
413e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek
42f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremeneknamespace {
43d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass DFS : public WorkList {
445f9e272e632e951b1efe824cd16acb4d96077930Chris Lattner  SmallVector<WorkListUnit,20> Stack;
45f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenekpublic:
46f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  virtual bool hasWork() const {
47f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    return !Stack.empty();
48f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  }
49f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
5055825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek  virtual void enqueue(const WorkListUnit& U) {
51f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    Stack.push_back(U);
52f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  }
53f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
5455825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek  virtual WorkListUnit dequeue() {
55f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    assert (!Stack.empty());
56d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    const WorkListUnit& U = Stack.back();
57f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    Stack.pop_back(); // This technically "invalidates" U, but we are fine.
58f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    return U;
59f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  }
603e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek
6155825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek  virtual bool visitItemsInWorkList(Visitor &V) {
625f9e272e632e951b1efe824cd16acb4d96077930Chris Lattner    for (SmallVectorImpl<WorkListUnit>::iterator
633e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek         I = Stack.begin(), E = Stack.end(); I != E; ++I) {
6455825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek      if (V.visit(*I))
653e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek        return true;
663e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek    }
673e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek    return false;
683e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek  }
69f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek};
701eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
71d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass BFS : public WorkList {
72d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  std::deque<WorkListUnit> Queue;
738ff59e832591eaa5f3be9885857e71bbcb3da77cTed Kremenekpublic:
748ff59e832591eaa5f3be9885857e71bbcb3da77cTed Kremenek  virtual bool hasWork() const {
758ff59e832591eaa5f3be9885857e71bbcb3da77cTed Kremenek    return !Queue.empty();
768ff59e832591eaa5f3be9885857e71bbcb3da77cTed Kremenek  }
771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
7855825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek  virtual void enqueue(const WorkListUnit& U) {
798d0f528afd9fcb9ebb8ccb4b8a529a05375b628eJordan Rose    Queue.push_back(U);
808ff59e832591eaa5f3be9885857e71bbcb3da77cTed Kremenek  }
811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
8255825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek  virtual WorkListUnit dequeue() {
83d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    WorkListUnit U = Queue.front();
843e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek    Queue.pop_front();
858ff59e832591eaa5f3be9885857e71bbcb3da77cTed Kremenek    return U;
868ff59e832591eaa5f3be9885857e71bbcb3da77cTed Kremenek  }
873e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek
8855825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek  virtual bool visitItemsInWorkList(Visitor &V) {
89d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    for (std::deque<WorkListUnit>::iterator
903e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek         I = Queue.begin(), E = Queue.end(); I != E; ++I) {
9155825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek      if (V.visit(*I))
923e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek        return true;
933e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek    }
943e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek    return false;
953e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek  }
968ff59e832591eaa5f3be9885857e71bbcb3da77cTed Kremenek};
971eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
98f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek} // end anonymous namespace
99f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
100d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis// Place the dstor for WorkList here because it contains virtual member
101ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek// functions, and we the code for the dstor generated in one compilation unit.
102d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios KyrtzidisWorkList::~WorkList() {}
103ee98546b0d5f3439c4a590b0d7d1545af794a0ecTed Kremenek
10455825aa2d88fe82bf3622f195046ae48532d3106Ted KremenekWorkList *WorkList::makeDFS() { return new DFS(); }
10555825aa2d88fe82bf3622f195046ae48532d3106Ted KremenekWorkList *WorkList::makeBFS() { return new BFS(); }
106f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
107e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremeneknamespace {
108d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  class BFSBlockDFSContents : public WorkList {
109d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    std::deque<WorkListUnit> Queue;
1105f9e272e632e951b1efe824cd16acb4d96077930Chris Lattner    SmallVector<WorkListUnit,20> Stack;
111e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek  public:
112e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek    virtual bool hasWork() const {
113e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek      return !Queue.empty() || !Stack.empty();
114e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek    }
1151eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
11655825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek    virtual void enqueue(const WorkListUnit& U) {
117e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek      if (isa<BlockEntrance>(U.getNode()->getLocation()))
1183e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek        Queue.push_front(U);
119e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek      else
120e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek        Stack.push_back(U);
121e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek    }
1221eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
12355825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek    virtual WorkListUnit dequeue() {
124e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek      // Process all basic blocks to completion.
125e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek      if (!Stack.empty()) {
126d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis        const WorkListUnit& U = Stack.back();
127e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek        Stack.pop_back(); // This technically "invalidates" U, but we are fine.
128e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek        return U;
129e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek      }
1301eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
131e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek      assert(!Queue.empty());
132e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek      // Don't use const reference.  The subsequent pop_back() might make it
133e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek      // unsafe.
134d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis      WorkListUnit U = Queue.front();
1353e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek      Queue.pop_front();
1361eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump      return U;
137e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek    }
13855825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek    virtual bool visitItemsInWorkList(Visitor &V) {
1395f9e272e632e951b1efe824cd16acb4d96077930Chris Lattner      for (SmallVectorImpl<WorkListUnit>::iterator
1403e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek           I = Stack.begin(), E = Stack.end(); I != E; ++I) {
14155825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek        if (V.visit(*I))
1423e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek          return true;
1433e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek      }
144d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis      for (std::deque<WorkListUnit>::iterator
1453e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek           I = Queue.begin(), E = Queue.end(); I != E; ++I) {
14655825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek        if (V.visit(*I))
1473e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek          return true;
1483e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek      }
1493e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek      return false;
1503e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek    }
1513e47b486f200d2b4cfb069c6f0d20fe5cf189fcdTed Kremenek
152e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek  };
153e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek} // end anonymous namespace
154e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek
15555825aa2d88fe82bf3622f195046ae48532d3106Ted KremenekWorkList* WorkList::makeBFSBlockDFSContents() {
156e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek  return new BFSBlockDFSContents();
157e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek}
158e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek
159e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek//===----------------------------------------------------------------------===//
160e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek// Core analysis engine.
161e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek//===----------------------------------------------------------------------===//
162102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor
163f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek/// ExecuteWorkList - Run the worklist algorithm for a maximum number of steps.
164d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisbool CoreEngine::ExecuteWorkList(const LocationContext *L, unsigned Steps,
1658bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                   ProgramStateRef InitState) {
1661eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
167f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  if (G->num_roots() == 0) { // Initialize the analysis by constructing
168f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    // the root if none exists.
1691eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1709c378f705405d37f49795d5e915989de774fe11fTed Kremenek    const CFGBlock *Entry = &(L->getCFG()->getEntry());
1711eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1721eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    assert (Entry->empty() &&
173f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek            "Entry block must be empty.");
1741eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
175f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    assert (Entry->succ_size() == 1 &&
176f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek            "Entry block must have 1 successor.");
1771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
178e62f048960645b79363408fdead53fec2a063c52Anna Zaks    // Mark the entry block as visited.
179e62f048960645b79363408fdead53fec2a063c52Anna Zaks    FunctionSummaries->markVisitedBasicBlock(Entry->getBlockID(),
180e62f048960645b79363408fdead53fec2a063c52Anna Zaks                                             L->getDecl(),
181e62f048960645b79363408fdead53fec2a063c52Anna Zaks                                             L->getCFG()->getNumBlockIDs());
182e62f048960645b79363408fdead53fec2a063c52Anna Zaks
183f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    // Get the solitary successor.
1849c378f705405d37f49795d5e915989de774fe11fTed Kremenek    const CFGBlock *Succ = *(Entry->succ_begin());
1851eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
186f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    // Construct an edge representing the
187f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    // starting location in the function.
18825e695b2d574d919cc1bbddf3a2efe073d449b1cZhongxing Xu    BlockEdge StartLoc(Entry, Succ, L);
1891eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1908e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek    // Set the current block counter to being empty.
1918e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek    WList->setBlockCounter(BCounterFactory.GetEmptyCounter());
1921eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1932ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu    if (!InitState)
1942ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu      // Generate the root.
1957771406ac3c58d77468d9d176262ad7ae7ff5050Ted Kremenek      generateNode(StartLoc, SubEng.getInitialState(L), 0);
1962ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu    else
197d048c6ef5b6cfaa0cecb8cc1d4bdace32ed21d07Ted Kremenek      generateNode(StartLoc, InitState, 0);
198f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  }
1991eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
200cf9ce13774dad86f780d84cd41e6bd64c039324aTom Care  // Check if we have a steps limit
201cf9ce13774dad86f780d84cd41e6bd64c039324aTom Care  bool UnlimitedSteps = Steps == 0;
202cf9ce13774dad86f780d84cd41e6bd64c039324aTom Care
203cf9ce13774dad86f780d84cd41e6bd64c039324aTom Care  while (WList->hasWork()) {
204cf9ce13774dad86f780d84cd41e6bd64c039324aTom Care    if (!UnlimitedSteps) {
205131579f198f9cc9e6405adbe6159110c283ec5a4Anna Zaks      if (Steps == 0) {
206131579f198f9cc9e6405adbe6159110c283ec5a4Anna Zaks        NumReachedMaxSteps++;
207cf9ce13774dad86f780d84cd41e6bd64c039324aTom Care        break;
208131579f198f9cc9e6405adbe6159110c283ec5a4Anna Zaks      }
209cf9ce13774dad86f780d84cd41e6bd64c039324aTom Care      --Steps;
210cf9ce13774dad86f780d84cd41e6bd64c039324aTom Care    }
211cf9ce13774dad86f780d84cd41e6bd64c039324aTom Care
212df19fe7cafcb02859efeb6963cddeafef4350ddfAnna Zaks    NumSteps++;
213df19fe7cafcb02859efeb6963cddeafef4350ddfAnna Zaks
21455825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek    const WorkListUnit& WU = WList->dequeue();
2151eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2168e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek    // Set the current block counter.
2178e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek    WList->setBlockCounter(WU.getBlockCounter());
2188e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek
2198e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek    // Retrieve the node.
2209c378f705405d37f49795d5e915989de774fe11fTed Kremenek    ExplodedNode *Node = WU.getNode();
2211eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2225903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    dispatchWorkItem(Node, Node->getLocation(), WU);
2235903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  }
2245903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  SubEng.processEndWorklist(hasWorkRemaining());
2255903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  return WList->hasWork();
2265903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks}
227e1efd4de8685e0785daf9cab227f7a21cfc9c80bTed Kremenek
2285903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaksvoid CoreEngine::dispatchWorkItem(ExplodedNode* Pred, ProgramPoint Loc,
2295903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks                                  const WorkListUnit& WU) {
2305903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  // Dispatch on the location type.
2315903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  switch (Loc.getKind()) {
2325903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    case ProgramPoint::BlockEdgeKind:
2335903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      HandleBlockEdge(cast<BlockEdge>(Loc), Pred);
2345903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      break;
2355903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks
2365903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    case ProgramPoint::BlockEntranceKind:
2375903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      HandleBlockEntrance(cast<BlockEntrance>(Loc), Pred);
2385903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      break;
2395903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks
2405903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    case ProgramPoint::BlockExitKind:
2415903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      assert (false && "BlockExit location never occur in forward analysis.");
2425903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      break;
2435903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks
2445903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    case ProgramPoint::CallEnterKind: {
2455903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      CallEnter CEnter = cast<CallEnter>(Loc);
2465903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      SubEng.processCallEnter(CEnter, Pred);
2475903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      break;
2485903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    }
249102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor
2500b3ade86a1c60cf0c7b56aa238aff458eb7f5974Anna Zaks    case ProgramPoint::CallExitBeginKind:
2515903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      SubEng.processCallExit(Pred);
2525903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      break;
253102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor
2545903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    case ProgramPoint::EpsilonKind: {
2555903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      assert(Pred->hasSinglePred() &&
2565903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks             "Assume epsilon has exactly one predecessor by construction");
2575903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      ExplodedNode *PNode = Pred->getFirstPred();
2585903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      dispatchWorkItem(Pred, PNode->getLocation(), WU);
2595903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      break;
260f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    }
2615903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    default:
2625903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      assert(isa<PostStmt>(Loc) ||
263852aa0d2c5d2d1faf2d77b5aa3c0848068a342c5Jordan Rose             isa<PostInitializer>(Loc) ||
264df51fb91c5c2a265019c3f24bf2993149abc79f8Jordan Rose             isa<PostImplicitCall>(Loc) ||
265852aa0d2c5d2d1faf2d77b5aa3c0848068a342c5Jordan Rose             isa<CallExitEnd>(Loc));
2665903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      HandlePostStmt(WU.getBlock(), WU.getIndex(), Pred);
2675903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks      break;
268f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  }
269f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek}
270f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
271253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaksbool CoreEngine::ExecuteWorkListWithInitialState(const LocationContext *L,
27218c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek                                                 unsigned Steps,
2738bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                                 ProgramStateRef InitState,
27418c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek                                                 ExplodedNodeSet &Dst) {
275253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks  bool DidNotFinish = ExecuteWorkList(L, Steps, InitState);
276626719bd2c09e27fe7c182724a812d27f59e3819Ted Kremenek  for (ExplodedGraph::eop_iterator I = G->eop_begin(),
277626719bd2c09e27fe7c182724a812d27f59e3819Ted Kremenek                                   E = G->eop_end(); I != E; ++I) {
2782ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu    Dst.Add(*I);
2792ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu  }
280253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks  return DidNotFinish;
2812ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu}
2822ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu
2839c378f705405d37f49795d5e915989de774fe11fTed Kremenekvoid CoreEngine::HandleBlockEdge(const BlockEdge &L, ExplodedNode *Pred) {
2841eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2859c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *Blk = L.getDst();
286c03a39e16762627b421247b12a2658be630a3300Anna Zaks  NodeBuilderContext BuilderCtx(*this, Blk, Pred);
2871eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
288e62f048960645b79363408fdead53fec2a063c52Anna Zaks  // Mark this block as visited.
289e62f048960645b79363408fdead53fec2a063c52Anna Zaks  const LocationContext *LC = Pred->getLocationContext();
290e62f048960645b79363408fdead53fec2a063c52Anna Zaks  FunctionSummaries->markVisitedBasicBlock(Blk->getBlockID(),
291e62f048960645b79363408fdead53fec2a063c52Anna Zaks                                           LC->getDecl(),
292e62f048960645b79363408fdead53fec2a063c52Anna Zaks                                           LC->getCFG()->getNumBlockIDs());
293e62f048960645b79363408fdead53fec2a063c52Anna Zaks
2941eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  // Check if we are entering the EXIT block.
295cb74d720b89b68bb2ecf2827d0e2eb66d236ab85Zhongxing Xu  if (Blk == &(L.getLocationContext()->getCFG()->getExit())) {
2961eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
297cb74d720b89b68bb2ecf2827d0e2eb66d236ab85Zhongxing Xu    assert (L.getLocationContext()->getCFG()->getExit().size() == 0
298cb48b9c9c3c95f2650b74530264c288d1f58c73cTed Kremenek            && "EXIT block cannot contain Stmts.");
299f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
30011062b118476368fa5b294954713e5df97d8599fTed Kremenek    // Process the final state transition.
301af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks    SubEng.processEndOfFunction(BuilderCtx);
302f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
303f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    // This path is done. Don't enqueue any more nodes.
304f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    return;
305f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  }
3066a6719a3a11087b48d9f1a4eb08b3bd43cb05a65Ted Kremenek
307c03a39e16762627b421247b12a2658be630a3300Anna Zaks  // Call into the SubEngine to process entering the CFGBlock.
30827c54e57c4a012dcdf2b40cf985b70d0b9caa69eTed Kremenek  ExplodedNodeSet dstNodes;
30927c54e57c4a012dcdf2b40cf985b70d0b9caa69eTed Kremenek  BlockEntrance BE(Blk, Pred->getLocationContext());
310c03a39e16762627b421247b12a2658be630a3300Anna Zaks  NodeBuilderWithSinks nodeBuilder(Pred, dstNodes, BuilderCtx, BE);
311253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks  SubEng.processCFGBlockEntrance(L, nodeBuilder);
31227c54e57c4a012dcdf2b40cf985b70d0b9caa69eTed Kremenek
313c03a39e16762627b421247b12a2658be630a3300Anna Zaks  // Auto-generate a node.
314c03a39e16762627b421247b12a2658be630a3300Anna Zaks  if (!nodeBuilder.hasGeneratedNodes()) {
315c03a39e16762627b421247b12a2658be630a3300Anna Zaks    nodeBuilder.generateNode(Pred->State, Pred);
31627c54e57c4a012dcdf2b40cf985b70d0b9caa69eTed Kremenek  }
31727c54e57c4a012dcdf2b40cf985b70d0b9caa69eTed Kremenek
318c03a39e16762627b421247b12a2658be630a3300Anna Zaks  // Enqueue nodes onto the worklist.
319c03a39e16762627b421247b12a2658be630a3300Anna Zaks  enqueue(dstNodes);
320f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek}
321f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
3229c378f705405d37f49795d5e915989de774fe11fTed Kremenekvoid CoreEngine::HandleBlockEntrance(const BlockEntrance &L,
3239c378f705405d37f49795d5e915989de774fe11fTed Kremenek                                       ExplodedNode *Pred) {
3241eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
3258e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek  // Increment the block counter.
326e62f048960645b79363408fdead53fec2a063c52Anna Zaks  const LocationContext *LC = Pred->getLocationContext();
327e62f048960645b79363408fdead53fec2a063c52Anna Zaks  unsigned BlockId = L.getBlock()->getBlockID();
328d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  BlockCounter Counter = WList->getBlockCounter();
329e62f048960645b79363408fdead53fec2a063c52Anna Zaks  Counter = BCounterFactory.IncrementCount(Counter, LC->getCurrentStackFrame(),
330e62f048960645b79363408fdead53fec2a063c52Anna Zaks                                           BlockId);
3318e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek  WList->setBlockCounter(Counter);
3321eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
3331eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  // Process the entrance of the block.
334852274d4257134906995cb252fb3dfd2d71deae8Ted Kremenek  if (CFGElement E = L.getFirstElement()) {
335c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks    NodeBuilderContext Ctx(*this, L.getBlock(), Pred);
336ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    SubEng.processCFGElement(E, Pred, 0, &Ctx);
337f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  }
3381eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  else
339425c08c53ccbfb84e52129406b259ec59da22e64Ted Kremenek    HandleBlockExit(L.getBlock(), Pred);
340f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek}
341f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
3429c378f705405d37f49795d5e915989de774fe11fTed Kremenekvoid CoreEngine::HandleBlockExit(const CFGBlock * B, ExplodedNode *Pred) {
3431eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
3449c378f705405d37f49795d5e915989de774fe11fTed Kremenek  if (const Stmt *Term = B->getTerminator()) {
3457d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek    switch (Term->getStmtClass()) {
3467d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek      default:
347b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie        llvm_unreachable("Analysis for this terminator not implemented.");
3481eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
349f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek      case Stmt::BinaryOperatorClass: // '&&' and '||'
350f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        HandleBranch(cast<BinaryOperator>(Term)->getLHS(), Term, B, Pred);
351f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        return;
3521eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
35356ca35d396d8692c384c785f9aeebcf22563fe1eJohn McCall      case Stmt::BinaryConditionalOperatorClass:
354f233d48cfc513b045e2c2cfca5c175220fbd0a82Ted Kremenek      case Stmt::ConditionalOperatorClass:
35556ca35d396d8692c384c785f9aeebcf22563fe1eJohn McCall        HandleBranch(cast<AbstractConditionalOperator>(Term)->getCond(),
35656ca35d396d8692c384c785f9aeebcf22563fe1eJohn McCall                     Term, B, Pred);
357f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        return;
3581eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
359f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        // FIXME: Use constant-folding in CFG construction to simplify this
360f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        // case.
3611eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
362f233d48cfc513b045e2c2cfca5c175220fbd0a82Ted Kremenek      case Stmt::ChooseExprClass:
363f233d48cfc513b045e2c2cfca5c175220fbd0a82Ted Kremenek        HandleBranch(cast<ChooseExpr>(Term)->getCond(), Term, B, Pred);
364f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        return;
3651eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
366337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek      case Stmt::CXXTryStmtClass: {
367337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek        // Generate a node for each of the successors.
368337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek        // Our logic for EH analysis can certainly be improved.
369337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek        for (CFGBlock::const_succ_iterator it = B->succ_begin(),
370337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek             et = B->succ_end(); it != et; ++it) {
371337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek          if (const CFGBlock *succ = *it) {
372337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek            generateNode(BlockEdge(B, succ, Pred->getLocationContext()),
373337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek                         Pred->State, Pred);
374337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek          }
375337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek        }
376337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek        return;
377337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek      }
378337e4dbc6859589b8878146a88bebf754e916702Ted Kremenek
379f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek      case Stmt::DoStmtClass:
380f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        HandleBranch(cast<DoStmt>(Term)->getCond(), Term, B, Pred);
381f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        return;
3821eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
38346eaf7789a1059a7b42b7dbd183150c72df5738fTed Kremenek      case Stmt::CXXForRangeStmtClass:
38446eaf7789a1059a7b42b7dbd183150c72df5738fTed Kremenek        HandleBranch(cast<CXXForRangeStmt>(Term)->getCond(), Term, B, Pred);
38546eaf7789a1059a7b42b7dbd183150c72df5738fTed Kremenek        return;
38646eaf7789a1059a7b42b7dbd183150c72df5738fTed Kremenek
3877d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek      case Stmt::ForStmtClass:
3887d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek        HandleBranch(cast<ForStmt>(Term)->getCond(), Term, B, Pred);
389f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        return;
3901eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
391a58e833c81a95e76c3a96fc982810d148537531bTed Kremenek      case Stmt::ContinueStmtClass:
392a58e833c81a95e76c3a96fc982810d148537531bTed Kremenek      case Stmt::BreakStmtClass:
3931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump      case Stmt::GotoStmtClass:
3947d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek        break;
3951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
396f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek      case Stmt::IfStmtClass:
397f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        HandleBranch(cast<IfStmt>(Term)->getCond(), Term, B, Pred);
398f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        return;
3991eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
400754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek      case Stmt::IndirectGotoStmtClass: {
401754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek        // Only 1 successor: the indirect goto dispatch block.
402754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek        assert (B->succ_size() == 1);
4031eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
404d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis        IndirectGotoNodeBuilder
405754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek           builder(Pred, B, cast<IndirectGotoStmt>(Term)->getTarget(),
406754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek                   *(B->succ_begin()), this);
4071eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4087771406ac3c58d77468d9d176262ad7ae7ff5050Ted Kremenek        SubEng.processIndirectGoto(builder);
409754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek        return;
410754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek      }
4111eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
412af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek      case Stmt::ObjCForCollectionStmtClass: {
413af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        // In the case of ObjCForCollectionStmt, it appears twice in a CFG:
414af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        //
415af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        //  (1) inside a basic block, which represents the binding of the
416af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        //      'element' variable to a value.
417af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        //  (2) in a terminator, which represents the branch.
418af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        //
419af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        // For (1), subengines will bind a value (i.e., 0 or 1) indicating
420af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        // whether or not collection contains any more elements.  We cannot
421af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        // just test to see if the element is nil because a container can
422af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        // contain nil elements.
423af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        HandleBranch(Term, Term, B, Pred);
424af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek        return;
425af3374187c47acea45706eab6744be6b1c66a856Ted Kremenek      }
4261eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
427daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek      case Stmt::SwitchStmtClass: {
428d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis        SwitchNodeBuilder builder(Pred, B, cast<SwitchStmt>(Term)->getCond(),
429031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu                                    this);
4301eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4317771406ac3c58d77468d9d176262ad7ae7ff5050Ted Kremenek        SubEng.processSwitch(builder);
432daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek        return;
433daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek      }
4341eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4357d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek      case Stmt::WhileStmtClass:
4367d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek        HandleBranch(cast<WhileStmt>(Term)->getCond(), Term, B, Pred);
437f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek        return;
4387d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek    }
4397d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek  }
440f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek
441f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek  assert (B->succ_size() == 1 &&
442f81086940024c8fd1c6497800386e88fd313a3d3Ted Kremenek          "Blocks with no terminator should have at most 1 successor.");
4431eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
444d048c6ef5b6cfaa0cecb8cc1d4bdace32ed21d07Ted Kremenek  generateNode(BlockEdge(B, *(B->succ_begin()), Pred->getLocationContext()),
44525e695b2d574d919cc1bbddf3a2efe073d449b1cZhongxing Xu               Pred->State, Pred);
446f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek}
447f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
4489c378f705405d37f49795d5e915989de774fe11fTed Kremenekvoid CoreEngine::HandleBranch(const Stmt *Cond, const Stmt *Term,
4499c378f705405d37f49795d5e915989de774fe11fTed Kremenek                                const CFGBlock * B, ExplodedNode *Pred) {
4507771406ac3c58d77468d9d176262ad7ae7ff5050Ted Kremenek  assert(B->succ_size() == 2);
451c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks  NodeBuilderContext Ctx(*this, B, Pred);
4521aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  ExplodedNodeSet Dst;
4531aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  SubEng.processBranch(Cond, Term, Ctx, Pred, Dst,
454a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks                       *(B->succ_begin()), *(B->succ_begin()+1));
4551aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  // Enqueue the new frontier onto the worklist.
4561aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  enqueue(Dst);
4577d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek}
4587d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek
4599c378f705405d37f49795d5e915989de774fe11fTed Kremenekvoid CoreEngine::HandlePostStmt(const CFGBlock *B, unsigned StmtIdx,
4609c378f705405d37f49795d5e915989de774fe11fTed Kremenek                                  ExplodedNode *Pred) {
461a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  assert(B);
462a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  assert(!B->empty());
463f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
464425c08c53ccbfb84e52129406b259ec59da22e64Ted Kremenek  if (StmtIdx == B->size())
465425c08c53ccbfb84e52129406b259ec59da22e64Ted Kremenek    HandleBlockExit(B, Pred);
466f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  else {
467c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks    NodeBuilderContext Ctx(*this, B, Pred);
468ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    SubEng.processCFGElement((*B)[StmtIdx], Pred, StmtIdx, &Ctx);
469f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  }
470f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek}
471f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
472d048c6ef5b6cfaa0cecb8cc1d4bdace32ed21d07Ted Kremenek/// generateNode - Utility method to generate nodes, hook up successors,
473f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek///  and add nodes to the worklist.
4749c378f705405d37f49795d5e915989de774fe11fTed Kremenekvoid CoreEngine::generateNode(const ProgramPoint &Loc,
4758bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                              ProgramStateRef State,
47618c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek                              ExplodedNode *Pred) {
4771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
478f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  bool IsNew;
4796800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  ExplodedNode *Node = G->getNode(Loc, State, false, &IsNew);
4801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  if (Pred)
4825fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek    Node->addPredecessor(Pred, *G);  // Link 'Node' with its predecessor.
483f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  else {
484f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    assert (IsNew);
485f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek    G->addRoot(Node);  // 'Node' has no predecessor.  Make it a root.
486f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  }
4871eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
488f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  // Only add 'Node' to the worklist if it was freshly generated.
48955825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek  if (IsNew) WList->enqueue(Node);
490f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek}
491f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
492dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaksvoid CoreEngine::enqueueStmtNode(ExplodedNode *N,
493dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks                                 const CFGBlock *Block, unsigned Idx) {
494cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks  assert(Block);
495dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  assert (!N->isSink());
496dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
497dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  // Check if this node entered a callee.
498dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  if (isa<CallEnter>(N->getLocation())) {
499dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    // Still use the index of the CallExpr. It's needed to create the callee
500dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    // StackFrameContext.
501dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    WList->enqueue(N, Block, Idx);
502dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    return;
503dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  }
504dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
505dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  // Do not create extra nodes. Move to the next CFG element.
506df51fb91c5c2a265019c3f24bf2993149abc79f8Jordan Rose  if (isa<PostInitializer>(N->getLocation()) ||
507df51fb91c5c2a265019c3f24bf2993149abc79f8Jordan Rose      isa<PostImplicitCall>(N->getLocation())) {
508dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    WList->enqueue(N, Block, Idx+1);
509dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    return;
510dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  }
511dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
5125903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  if (isa<EpsilonPoint>(N->getLocation())) {
5135903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    WList->enqueue(N, Block, Idx);
5145903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks    return;
5155903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  }
5165903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks
5179198c71a626e2f0d29d92152832f3e80f4af59b3Jordan Rose  // At this point, we know we're processing a normal statement.
5189198c71a626e2f0d29d92152832f3e80f4af59b3Jordan Rose  CFGStmt CS = cast<CFGStmt>((*Block)[Idx]);
5199198c71a626e2f0d29d92152832f3e80f4af59b3Jordan Rose  PostStmt Loc(CS.getStmt(), N->getLocationContext());
520dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
521dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  if (Loc == N->getLocation()) {
522dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    // Note: 'N' should be a fresh node because otherwise it shouldn't be
523dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    // a member of Deferred.
524dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    WList->enqueue(N, Block, Idx+1);
525dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    return;
526dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  }
527dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
528dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  bool IsNew;
5296800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  ExplodedNode *Succ = G->getNode(Loc, N->getState(), false, &IsNew);
530dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  Succ->addPredecessor(N, *G);
531dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
532dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  if (IsNew)
533dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    WList->enqueue(Succ, Block, Idx+1);
534dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks}
535dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
5360b3ade86a1c60cf0c7b56aa238aff458eb7f5974Anna ZaksExplodedNode *CoreEngine::generateCallExitBeginNode(ExplodedNode *N) {
5370b3ade86a1c60cf0c7b56aa238aff458eb7f5974Anna Zaks  // Create a CallExitBegin node and enqueue it.
5384d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  const StackFrameContext *LocCtx
5394d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks                         = cast<StackFrameContext>(N->getLocationContext());
5404d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks
541bed28ac1d1463adca3ecf24fca5c30646fa9dbb2Sylvestre Ledru  // Use the callee location context.
542852aa0d2c5d2d1faf2d77b5aa3c0848068a342c5Jordan Rose  CallExitBegin Loc(LocCtx);
5434d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks
5444d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  bool isNew;
5456800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  ExplodedNode *Node = G->getNode(Loc, N->getState(), false, &isNew);
5464d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  Node->addPredecessor(N, *G);
5474d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  return isNew ? Node : 0;
5484d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks}
5494d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks
5504d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks
551dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaksvoid CoreEngine::enqueue(ExplodedNodeSet &Set) {
552dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  for (ExplodedNodeSet::iterator I = Set.begin(),
553dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks                                 E = Set.end(); I != E; ++I) {
554a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    WList->enqueue(*I);
555a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  }
556a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks}
557a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks
558dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaksvoid CoreEngine::enqueue(ExplodedNodeSet &Set,
559dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks                         const CFGBlock *Block, unsigned Idx) {
560dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  for (ExplodedNodeSet::iterator I = Set.begin(),
561dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks                                 E = Set.end(); I != E; ++I) {
562dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks    enqueueStmtNode(*I, Block, Idx);
563dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  }
564dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks}
565dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
5664d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaksvoid CoreEngine::enqueueEndOfFunction(ExplodedNodeSet &Set) {
5674d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  for (ExplodedNodeSet::iterator I = Set.begin(), E = Set.end(); I != E; ++I) {
5684d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks    ExplodedNode *N = *I;
5690b3ade86a1c60cf0c7b56aa238aff458eb7f5974Anna Zaks    // If we are in an inlined call, generate CallExitBegin node.
5704d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks    if (N->getLocationContext()->getParent()) {
5710b3ade86a1c60cf0c7b56aa238aff458eb7f5974Anna Zaks      N = generateCallExitBeginNode(N);
5724d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks      if (N)
5734d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks        WList->enqueue(N);
574638e2d31fceed041e7e16aada4188c94cb5797bbAnna Zaks    } else {
5750b3ade86a1c60cf0c7b56aa238aff458eb7f5974Anna Zaks      // TODO: We should run remove dead bindings here.
5764d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks      G->addEndOfPath(N);
577638e2d31fceed041e7e16aada4188c94cb5797bbAnna Zaks      NumPathsExplored++;
578638e2d31fceed041e7e16aada4188c94cb5797bbAnna Zaks    }
5794d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  }
5804d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks}
5814d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks
582dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
58399ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikievoid NodeBuilder::anchor() { }
58499ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie
585f05aac8472d8ed081a361a218fd14d59ddc91b85Anna ZaksExplodedNode* NodeBuilder::generateNodeImpl(const ProgramPoint &Loc,
5868bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                            ProgramStateRef State,
587319a9184d5ca9f77622b45ae15c08f6b9ce01621Anna Zaks                                            ExplodedNode *FromN,
588319a9184d5ca9f77622b45ae15c08f6b9ce01621Anna Zaks                                            bool MarkAsSink) {
5894e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks  HasGeneratedNodes = true;
590f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  bool IsNew;
5916800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  ExplodedNode *N = C.Eng.G->getNode(Loc, State, MarkAsSink, &IsNew);
592a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  N->addPredecessor(FromN, *C.Eng.G);
5931aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  Frontier.erase(FromN);
5942d950b15b2b2b650b102ecf0c6b50b45e0cb6a8aAnna Zaks
5952d950b15b2b2b650b102ecf0c6b50b45e0cb6a8aAnna Zaks  if (!IsNew)
5962d950b15b2b2b650b102ecf0c6b50b45e0cb6a8aAnna Zaks    return 0;
597f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
5986800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  if (!MarkAsSink)
5991aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    Frontier.Add(N);
600f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
6012d950b15b2b2b650b102ecf0c6b50b45e0cb6a8aAnna Zaks  return N;
602f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks}
603f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
60499ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikievoid NodeBuilderWithSinks::anchor() { }
60599ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie
606aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna ZaksStmtNodeBuilder::~StmtNodeBuilder() {
607cca79db2ea94f71fb088f4b0f104cef8bedf8ff2Anna Zaks  if (EnclosingBldr)
608cca79db2ea94f71fb088f4b0f104cef8bedf8ff2Anna Zaks    for (ExplodedNodeSet::iterator I = Frontier.begin(),
609cca79db2ea94f71fb088f4b0f104cef8bedf8ff2Anna Zaks                                   E = Frontier.end(); I != E; ++I )
610cca79db2ea94f71fb088f4b0f104cef8bedf8ff2Anna Zaks      EnclosingBldr->addNodes(*I);
611868e78d59d2dfaf9cda511925e5a58f3a712db96Zhongxing Xu}
612868e78d59d2dfaf9cda511925e5a58f3a712db96Zhongxing Xu
61399ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikievoid BranchNodeBuilder::anchor() { }
61499ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie
6158bef8238181a30e52dea380789a7e2d760eac532Ted KremenekExplodedNode *BranchNodeBuilder::generateNode(ProgramStateRef State,
616a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks                                              bool branch,
617a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks                                              ExplodedNode *NodePred) {
618520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  // If the branch has been marked infeasible we should not generate a node.
619520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  if (!isFeasible(branch))
620520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    return NULL;
6211eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
622a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  ProgramPoint Loc = BlockEdge(C.Block, branch ? DstT:DstF,
623a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks                               NodePred->getLocationContext());
624a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  ExplodedNode *Succ = generateNodeImpl(Loc, State, NodePred);
625a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  return Succ;
6267d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek}
62771c29bdc931bc49644c581ec7d698f0dbf01a0aaTed Kremenek
628c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing XuExplodedNode*
62918c66fdc3c4008d335885695fe36fb5353c5f672Ted KremenekIndirectGotoNodeBuilder::generateNode(const iterator &I,
6308bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                      ProgramStateRef St,
6316800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks                                      bool IsSink) {
632754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek  bool IsNew;
6339c378f705405d37f49795d5e915989de774fe11fTed Kremenek  ExplodedNode *Succ = Eng.G->getNode(BlockEdge(Src, I.getBlock(),
6346800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks                                      Pred->getLocationContext()), St,
6356800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks                                      IsSink, &IsNew);
6365fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek  Succ->addPredecessor(Pred, *Eng.G);
6371eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
6386800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  if (!IsNew)
6396800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks    return 0;
6401eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
6416800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  if (!IsSink)
6426800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks    Eng.WList->enqueue(Succ);
6431eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
6446800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  return Succ;
645754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek}
646daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek
647daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek
648c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing XuExplodedNode*
64918c66fdc3c4008d335885695fe36fb5353c5f672Ted KremenekSwitchNodeBuilder::generateCaseStmtNode(const iterator &I,
6508bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                        ProgramStateRef St) {
651daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek
652daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  bool IsNew;
6539c378f705405d37f49795d5e915989de774fe11fTed Kremenek  ExplodedNode *Succ = Eng.G->getNode(BlockEdge(Src, I.getBlock(),
6546800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks                                      Pred->getLocationContext()), St,
6556800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks                                      false, &IsNew);
6565fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek  Succ->addPredecessor(Pred, *Eng.G);
6576800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  if (!IsNew)
6586800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks    return 0;
6596800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks
6606800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  Eng.WList->enqueue(Succ);
6616800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  return Succ;
662daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek}
663daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek
664daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek
665c5619d901a68dc27a9e310a6a831f03efebcd950Zhongxing XuExplodedNode*
6668bef8238181a30e52dea380789a7e2d760eac532Ted KremenekSwitchNodeBuilder::generateDefaultCaseNode(ProgramStateRef St,
6676800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks                                           bool IsSink) {
668daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  // Get the block for the default case.
669e4c6675cccbaac991843def43072687bca50d989Ted Kremenek  assert(Src->succ_rbegin() != Src->succ_rend());
6709c378f705405d37f49795d5e915989de774fe11fTed Kremenek  CFGBlock *DefaultBlock = *Src->succ_rbegin();
6711eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
672e4c6675cccbaac991843def43072687bca50d989Ted Kremenek  // Sanity check for default blocks that are unreachable and not caught
673e4c6675cccbaac991843def43072687bca50d989Ted Kremenek  // by earlier stages.
674e4c6675cccbaac991843def43072687bca50d989Ted Kremenek  if (!DefaultBlock)
675e4c6675cccbaac991843def43072687bca50d989Ted Kremenek    return NULL;
676e4c6675cccbaac991843def43072687bca50d989Ted Kremenek
677daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  bool IsNew;
6789c378f705405d37f49795d5e915989de774fe11fTed Kremenek  ExplodedNode *Succ = Eng.G->getNode(BlockEdge(Src, DefaultBlock,
6796800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks                                      Pred->getLocationContext()), St,
6806800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks                                      IsSink, &IsNew);
6815fe4d9deb543a19f557e3d85c5f33867af97cd96Ted Kremenek  Succ->addPredecessor(Pred, *Eng.G);
6821eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
6836800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  if (!IsNew)
6846800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks    return 0;
6851eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
6866800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  if (!IsSink)
6876800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks    Eng.WList->enqueue(Succ);
6881eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
6896800ba622e4edf287801ac69c42c61e7e294b06bAnna Zaks  return Succ;
690daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek}
691