CoreEngine.h revision 8d0f528afd9fcb9ebb8ccb4b8a529a05375b628e
1d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis//==- CoreEngine.h - 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,
118e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek//  dataflow analysis via graph reachability.
12f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//
13f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek//===----------------------------------------------------------------------===//
14f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
15d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis#ifndef LLVM_CLANG_GR_COREENGINE
16d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis#define LLVM_CLANG_GR_COREENGINE
17f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
1899c6ad3f22b865d0f4cce52bc36904403c9ed4c4Ted Kremenek#include "clang/AST/Expr.h"
195eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek#include "clang/Analysis/AnalysisContext.h"
209b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h"
21e62f048960645b79363408fdead53fec2a063c52Anna Zaks#include "clang/StaticAnalyzer/Core/PathSensitive/FunctionSummary.h"
229b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/WorkList.h"
239b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/BlockCounter.h"
24f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#include "llvm/ADT/OwningPtr.h"
25f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
26f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremeneknamespace clang {
270111f575b968e423dccae439e501225b8314b257Zhongxing Xu
28ca804539d908d3a0e8c72a0df5f1f571d29490bbTed Kremenekclass ProgramPointTag;
29ca804539d908d3a0e8c72a0df5f1f571d29490bbTed Kremenek
309ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento {
315a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis
32a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksclass NodeBuilder;
33a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks
3424f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek//===----------------------------------------------------------------------===//
35d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis/// CoreEngine - Implements the core logic of the graph-reachability
36922059dec59c7bed235da01aff75ae522a369811Ted Kremenek///   analysis. It traverses the CFG and generates the ExplodedGraph.
37922059dec59c7bed235da01aff75ae522a369811Ted Kremenek///   Program "states" are treated as opaque void pointers.
38d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis///   The template class CoreEngine (which subclasses CoreEngine)
39922059dec59c7bed235da01aff75ae522a369811Ted Kremenek///   provides the matching component to the engine that knows the actual types
40922059dec59c7bed235da01aff75ae522a369811Ted Kremenek///   for states.  Note that this engine only dispatches to transfer functions
41922059dec59c7bed235da01aff75ae522a369811Ted Kremenek///   at the statement and block-level.  The analyses themselves must implement
42922059dec59c7bed235da01aff75ae522a369811Ted Kremenek///   any transfer function logic and the sub-expression level (if any).
43d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass CoreEngine {
44ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  friend struct NodeBuilderContext;
45f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  friend class NodeBuilder;
46253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks  friend class ExprEngine;
47ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  friend class CommonNodeBuilder;
48d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  friend class IndirectGotoNodeBuilder;
49d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  friend class SwitchNodeBuilder;
50e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek  friend class EndOfFunctionNodeBuilder;
51a7a8a450d908b34fa5f569f2e694ebd4b61aae2fTom Carepublic:
52a7a8a450d908b34fa5f569f2e694ebd4b61aae2fTom Care  typedef std::vector<std::pair<BlockEdge, const ExplodedNode*> >
5366750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek            BlocksExhausted;
54422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek
55422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  typedef std::vector<std::pair<const CFGBlock*, const ExplodedNode*> >
56422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek            BlocksAborted;
57422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek
58a7a8a450d908b34fa5f569f2e694ebd4b61aae2fTom Careprivate:
59a7a8a450d908b34fa5f569f2e694ebd4b61aae2fTom Care
60d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  SubEngine& SubEng;
610111f575b968e423dccae439e501225b8314b257Zhongxing Xu
62f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  /// G - The simulation graph.  Each node is a (location,state) pair.
636f42b62b6194f53bcbc349f5d17388e1936535d7Dylan Noblesmith  OwningPtr<ExplodedGraph> G;
641eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
65f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  /// WList - A set of queued nodes that need to be processed by the
66f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  ///  worklist algorithm.  It is up to the implementation of WList to decide
67f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  ///  the order that nodes are processed.
688d0f528afd9fcb9ebb8ccb4b8a529a05375b628eJordan Rose  OwningPtr<WorkList> WList;
691eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
70d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  /// BCounterFactory - A factory object for created BlockCounter objects.
718e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek  ///   These are used to record for key nodes in the ExplodedGraph the
728e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek  ///   number of times different CFGBlocks have been visited along a path.
73d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  BlockCounter::Factory BCounterFactory;
74f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek
75f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek  /// The locations where we stopped doing work because we visited a location
76f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek  ///  too many times.
7766750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek  BlocksExhausted blocksExhausted;
78422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek
79422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  /// The locations where we stopped because the engine aborted analysis,
80422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  /// usually because it could not reason about something.
81422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  BlocksAborted blocksAborted;
821eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
833fd5f370a28552976c52e76c3035d79012d78ddaAnna Zaks  /// The functions which have been analyzed through inlining. This is owned by
843fd5f370a28552976c52e76c3035d79012d78ddaAnna Zaks  /// AnalysisConsumer. It can be null.
856a86082f3a06a2dcceaaf63f78a0e52d64bcbaa3Anna Zaks  SetOfConstDecls *AnalyzedCallees;
863fd5f370a28552976c52e76c3035d79012d78ddaAnna Zaks
87e62f048960645b79363408fdead53fec2a063c52Anna Zaks  /// The information about functions shared by the whole translation unit.
88e62f048960645b79363408fdead53fec2a063c52Anna Zaks  /// (This data is owned by AnalysisConsumer.)
89e62f048960645b79363408fdead53fec2a063c52Anna Zaks  FunctionSummariesTy *FunctionSummaries;
90e62f048960645b79363408fdead53fec2a063c52Anna Zaks
9118c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek  void generateNode(const ProgramPoint &Loc,
928bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                    ProgramStateRef State,
939c378f705405d37f49795d5e915989de774fe11fTed Kremenek                    ExplodedNode *Pred);
941eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
959c378f705405d37f49795d5e915989de774fe11fTed Kremenek  void HandleBlockEdge(const BlockEdge &E, ExplodedNode *Pred);
969c378f705405d37f49795d5e915989de774fe11fTed Kremenek  void HandleBlockEntrance(const BlockEntrance &E, ExplodedNode *Pred);
979c378f705405d37f49795d5e915989de774fe11fTed Kremenek  void HandleBlockExit(const CFGBlock *B, ExplodedNode *Pred);
989c378f705405d37f49795d5e915989de774fe11fTed Kremenek  void HandlePostStmt(const CFGBlock *B, unsigned StmtIdx, ExplodedNode *Pred);
991eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1009c378f705405d37f49795d5e915989de774fe11fTed Kremenek  void HandleBranch(const Stmt *Cond, const Stmt *Term, const CFGBlock *B,
1019c378f705405d37f49795d5e915989de774fe11fTed Kremenek                    ExplodedNode *Pred);
1020111f575b968e423dccae439e501225b8314b257Zhongxing Xu
103f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenekprivate:
104d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  CoreEngine(const CoreEngine&); // Do not implement.
105d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  CoreEngine& operator=(const CoreEngine&);
1061eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1070b3ade86a1c60cf0c7b56aa238aff458eb7f5974Anna Zaks  ExplodedNode *generateCallExitBeginNode(ExplodedNode *N);
1084d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks
109f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenekpublic:
1108d0f528afd9fcb9ebb8ccb4b8a529a05375b628eJordan Rose  /// Construct a CoreEngine object to analyze the provided CFG.
1116a86082f3a06a2dcceaaf63f78a0e52d64bcbaa3Anna Zaks  CoreEngine(SubEngine& subengine, SetOfConstDecls *VisitedCallees,
112e62f048960645b79363408fdead53fec2a063c52Anna Zaks             FunctionSummariesTy *FS)
113d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    : SubEng(subengine), G(new ExplodedGraph()),
1148d0f528afd9fcb9ebb8ccb4b8a529a05375b628eJordan Rose      WList(WorkList::makeDFS()),
1153fd5f370a28552976c52e76c3035d79012d78ddaAnna Zaks      BCounterFactory(G->getAllocator()),
116e62f048960645b79363408fdead53fec2a063c52Anna Zaks      AnalyzedCallees(VisitedCallees),
117e62f048960645b79363408fdead53fec2a063c52Anna Zaks      FunctionSummaries(FS){}
1180111f575b968e423dccae439e501225b8314b257Zhongxing Xu
1190111f575b968e423dccae439e501225b8314b257Zhongxing Xu  /// getGraph - Returns the exploded graph.
120031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  ExplodedGraph& getGraph() { return *G.get(); }
1211eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1220111f575b968e423dccae439e501225b8314b257Zhongxing Xu  /// takeGraph - Returns the exploded graph.  Ownership of the graph is
123fc8f0e14ad142ed811e90fbd9a30e419e301c717Chris Lattner  ///  transferred to the caller.
124031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  ExplodedGraph* takeGraph() { return G.take(); }
1250111f575b968e423dccae439e501225b8314b257Zhongxing Xu
126f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  /// ExecuteWorkList - Run the worklist algorithm for a maximum number of
127f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  ///  steps.  Returns true if there is still simulation state on the worklist.
1282ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu  bool ExecuteWorkList(const LocationContext *L, unsigned Steps,
1298bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                       ProgramStateRef InitState);
130253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks  /// Returns true if there is still simulation state on the worklist.
131253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks  bool ExecuteWorkListWithInitialState(const LocationContext *L,
13218c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek                                       unsigned Steps,
1338bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                       ProgramStateRef InitState,
1342ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu                                       ExplodedNodeSet &Dst);
135bc42c533e7d3d946704a49e242939dd232f33072Tom Care
1365903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  /// Dispatch the work list item based on the given location information.
1375903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  /// Use Pred parameter as the predecessor state.
1385903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  void dispatchWorkItem(ExplodedNode* Pred, ProgramPoint Loc,
1395903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks                        const WorkListUnit& WU);
1405903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks
141bc42c533e7d3d946704a49e242939dd232f33072Tom Care  // Functions for external checking of whether we have unfinished work
142422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  bool wasBlockAborted() const { return !blocksAborted.empty(); }
143422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  bool wasBlocksExhausted() const { return !blocksExhausted.empty(); }
144422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  bool hasWorkRemaining() const { return wasBlocksExhausted() ||
145422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek                                         WList->hasWork() ||
146422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek                                         wasBlockAborted(); }
147422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek
148422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  /// Inform the CoreEngine that a basic block was aborted because
149422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  /// it could not be completely analyzed.
150422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  void addAbortedBlock(const ExplodedNode *node, const CFGBlock *block) {
151422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek    blocksAborted.push_back(std::make_pair(block, node));
152422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  }
153422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek
1548d0f528afd9fcb9ebb8ccb4b8a529a05375b628eJordan Rose  WorkList *getWorkList() const { return WList.get(); }
155f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek
156422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  BlocksExhausted::const_iterator blocks_exhausted_begin() const {
15766750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek    return blocksExhausted.begin();
158f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek  }
159422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  BlocksExhausted::const_iterator blocks_exhausted_end() const {
16066750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek    return blocksExhausted.end();
161f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek  }
162422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  BlocksAborted::const_iterator blocks_aborted_begin() const {
163422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek    return blocksAborted.begin();
164422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  }
165422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  BlocksAborted::const_iterator blocks_aborted_end() const {
166422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek    return blocksAborted.end();
167422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  }
168a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks
169dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  /// \brief Enqueue the given set of nodes onto the work list.
1704d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  void enqueue(ExplodedNodeSet &Set);
171dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
172dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  /// \brief Enqueue nodes that were created as a result of processing
173dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  /// a statement onto the work list.
174dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  void enqueue(ExplodedNodeSet &Set, const CFGBlock *Block, unsigned Idx);
1754d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks
1764d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  /// \brief enqueue the nodes corresponding to the end of function onto the
1774d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  /// end of path / work list.
1784d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  void enqueueEndOfFunction(ExplodedNodeSet &Set);
1795903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks
1805903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  /// \brief Enqueue a single node created as a result of statement processing.
1815903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  void enqueueStmtNode(ExplodedNode *N, const CFGBlock *Block, unsigned Idx);
182a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks};
183a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks
184c03a39e16762627b421247b12a2658be630a3300Anna Zaks// TODO: Turn into a calss.
185a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksstruct NodeBuilderContext {
1865a878b2cabb940bf3c1ac420a52cac305765e3e2Anna Zaks  const CoreEngine &Eng;
187a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  const CFGBlock *Block;
188af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks  ExplodedNode *Pred;
1895a878b2cabb940bf3c1ac420a52cac305765e3e2Anna Zaks  NodeBuilderContext(const CoreEngine &E, const CFGBlock *B, ExplodedNode *N)
190af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks    : Eng(E), Block(B), Pred(N) { assert(B); assert(!N->isSink()); }
191ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
192c03a39e16762627b421247b12a2658be630a3300Anna Zaks  ExplodedNode *getPred() const { return Pred; }
193c03a39e16762627b421247b12a2658be630a3300Anna Zaks
194ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  /// \brief Return the CFGBlock associated with this builder.
195ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  const CFGBlock *getBlock() const { return Block; }
196ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
197ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  /// \brief Returns the number of times the current basic block has been
198ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  /// visited on the exploded graph path.
199ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  unsigned getCurrentBlockCount() const {
200ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    return Eng.WList->getBlockCounter().getNumVisited(
201af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks                    Pred->getLocationContext()->getCurrentStackFrame(),
202ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                    Block->getBlockID());
203ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
204f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek};
2051eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
206aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \class NodeBuilder
207aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \brief This is the simplest builder which generates nodes in the
208aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// ExplodedGraph.
209aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks///
210aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// The main benefit of the builder is that it automatically tracks the
211aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// frontier nodes (or destination set). This is the set of nodes which should
212aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// be propagated to the next step / builder. They are the nodes which have been
213aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// added to the builder (either as the input node set or as the newly
214aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// constructed nodes) but did not have any outgoing transitions added.
215f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaksclass NodeBuilder {
21699ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie  virtual void anchor();
217a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksprotected:
218cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks  const NodeBuilderContext &C;
219319a9184d5ca9f77622b45ae15c08f6b9ce01621Anna Zaks
2203152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  /// Specifies if the builder results have been finalized. For example, if it
2213152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  /// is set to false, autotransitions are yet to be generated.
222f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  bool Finalized;
2234e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks  bool HasGeneratedNodes;
224f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// \brief The frontier set - a set of nodes which need to be propagated after
225f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// the builder dies.
2261aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  ExplodedNodeSet &Frontier;
22771fdf469a3b6d7d557b0bfba36e8659f4966c565Anna Zaks
2283152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  /// Checkes if the results are ready.
2293152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  virtual bool checkResults() {
230a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    if (!Finalized)
231a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks      return false;
232a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    return true;
233a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  }
234f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
235aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  bool hasNoSinksInFrontier() {
2368ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks    for (iterator I = Frontier.begin(), E = Frontier.end(); I != E; ++I) {
2378ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks      if ((*I)->isSink())
2388ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks        return false;
2398ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks    }
2408ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks    return true;
2418ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks  }
2428ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks
2433152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  /// Allow subclasses to finalize results before result_begin() is executed.
2443152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  virtual void finalizeResults() {}
245f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
246f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  ExplodedNode *generateNodeImpl(const ProgramPoint &PP,
2478bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                 ProgramStateRef State,
248f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks                                 ExplodedNode *Pred,
249f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks                                 bool MarkAsSink = false);
250f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
251f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zakspublic:
2521aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  NodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet,
2531aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks              const NodeBuilderContext &Ctx, bool F = true)
2541aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    : C(Ctx), Finalized(F), HasGeneratedNodes(false), Frontier(DstSet) {
2558ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks    Frontier.Add(SrcNode);
256ad62deeb70e97da6bd514dd390ea1ce6af6ad81dAnna Zaks  }
257a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks
2581aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  NodeBuilder(const ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet,
2591aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks              const NodeBuilderContext &Ctx, bool F = true)
2601aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    : C(Ctx), Finalized(F), HasGeneratedNodes(false), Frontier(DstSet) {
2611aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    Frontier.insert(SrcSet);
262aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks    assert(hasNoSinksInFrontier());
263cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks  }
264cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks
265a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  virtual ~NodeBuilder() {}
266f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
267f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// \brief Generates a node in the ExplodedGraph.
268f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  ///
269f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// When a node is marked as sink, the exploration from the node is stopped -
270f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// the node becomes the last node on the path.
271f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  ExplodedNode *generateNode(const ProgramPoint &PP,
2728bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef State,
273f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks                             ExplodedNode *Pred,
274f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks                             bool MarkAsSink = false) {
275f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks    return generateNodeImpl(PP, State, Pred, MarkAsSink);
276f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  }
277f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
2781aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  const ExplodedNodeSet &getResults() {
2791aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    finalizeResults();
2801aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    assert(checkResults());
2811aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    return Frontier;
2821aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  }
2831aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks
2841aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  typedef ExplodedNodeSet::iterator iterator;
285f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// \brief Iterators through the results frontier.
2861aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  inline iterator begin() {
287a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    finalizeResults();
288a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    assert(checkResults());
2891aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    return Frontier.begin();
290a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  }
2911aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  inline iterator end() {
292a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    finalizeResults();
2931aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    return Frontier.end();
294a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  }
295f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
2961aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  const NodeBuilderContext &getContext() { return C; }
297aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  bool hasGeneratedNodes() { return HasGeneratedNodes; }
2981aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks
299d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks  void takeNodes(const ExplodedNodeSet &S) {
300d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks    for (ExplodedNodeSet::iterator I = S.begin(), E = S.end(); I != E; ++I )
301d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks      Frontier.erase(*I);
302d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks  }
303aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  void takeNodes(ExplodedNode *N) { Frontier.erase(N); }
304aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  void addNodes(const ExplodedNodeSet &S) { Frontier.insert(S); }
305aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  void addNodes(ExplodedNode *N) { Frontier.Add(N); }
306f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks};
307f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
308c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \class NodeBuilderWithSinks
309c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \brief This node builder keeps track of the generated sink nodes.
310c03a39e16762627b421247b12a2658be630a3300Anna Zaksclass NodeBuilderWithSinks: public NodeBuilder {
31199ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie  virtual void anchor();
312c03a39e16762627b421247b12a2658be630a3300Anna Zaksprotected:
313c03a39e16762627b421247b12a2658be630a3300Anna Zaks  SmallVector<ExplodedNode*, 2> sinksGenerated;
314c03a39e16762627b421247b12a2658be630a3300Anna Zaks  ProgramPoint &Location;
315c03a39e16762627b421247b12a2658be630a3300Anna Zaks
316c03a39e16762627b421247b12a2658be630a3300Anna Zakspublic:
317c03a39e16762627b421247b12a2658be630a3300Anna Zaks  NodeBuilderWithSinks(ExplodedNode *Pred, ExplodedNodeSet &DstSet,
318c03a39e16762627b421247b12a2658be630a3300Anna Zaks                       const NodeBuilderContext &Ctx, ProgramPoint &L)
319c03a39e16762627b421247b12a2658be630a3300Anna Zaks    : NodeBuilder(Pred, DstSet, Ctx), Location(L) {}
3208bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ExplodedNode *generateNode(ProgramStateRef State,
321c03a39e16762627b421247b12a2658be630a3300Anna Zaks                             ExplodedNode *Pred,
322c03a39e16762627b421247b12a2658be630a3300Anna Zaks                             const ProgramPointTag *Tag = 0,
323c03a39e16762627b421247b12a2658be630a3300Anna Zaks                             bool MarkAsSink = false) {
324c03a39e16762627b421247b12a2658be630a3300Anna Zaks    ProgramPoint LocalLoc = (Tag ? Location.withTag(Tag): Location);
325c03a39e16762627b421247b12a2658be630a3300Anna Zaks
326c03a39e16762627b421247b12a2658be630a3300Anna Zaks    ExplodedNode *N = generateNodeImpl(LocalLoc, State, Pred, MarkAsSink);
327c03a39e16762627b421247b12a2658be630a3300Anna Zaks    if (N && N->isSink())
328c03a39e16762627b421247b12a2658be630a3300Anna Zaks      sinksGenerated.push_back(N);
329c03a39e16762627b421247b12a2658be630a3300Anna Zaks    return N;
330c03a39e16762627b421247b12a2658be630a3300Anna Zaks  }
331c03a39e16762627b421247b12a2658be630a3300Anna Zaks
332c03a39e16762627b421247b12a2658be630a3300Anna Zaks  const SmallVectorImpl<ExplodedNode*> &getSinks() const {
333c03a39e16762627b421247b12a2658be630a3300Anna Zaks    return sinksGenerated;
334c03a39e16762627b421247b12a2658be630a3300Anna Zaks  }
335c03a39e16762627b421247b12a2658be630a3300Anna Zaks};
336c03a39e16762627b421247b12a2658be630a3300Anna Zaks
337aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \class StmtNodeBuilder
338aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \brief This builder class is useful for generating nodes that resulted from
339aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// visiting a statement. The main difference from it's parent NodeBuilder is
340aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// that it creates a statement specific ProgramPoint.
341aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaksclass StmtNodeBuilder: public NodeBuilder {
342ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  NodeBuilder *EnclosingBldr;
3438ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zakspublic:
344aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks
345aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  /// \brief Constructs a StmtNodeBuilder. If the builder is going to process
346aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  /// nodes currently owned by another builder(with larger scope), use
347aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  /// Enclosing builder to transfer ownership.
348aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  StmtNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet,
349ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                      const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0)
350ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    : NodeBuilder(SrcNode, DstSet, Ctx), EnclosingBldr(Enclosing) {
351ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    if (EnclosingBldr)
352ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks      EnclosingBldr->takeNodes(SrcNode);
353ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
3548ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks
355aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  StmtNodeBuilder(ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet,
356ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                      const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0)
357ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    : NodeBuilder(SrcSet, DstSet, Ctx), EnclosingBldr(Enclosing) {
358ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    if (EnclosingBldr)
359ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks      for (ExplodedNodeSet::iterator I = SrcSet.begin(),
360ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                                     E = SrcSet.end(); I != E; ++I )
361ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks        EnclosingBldr->takeNodes(*I);
362ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
363ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
364aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  virtual ~StmtNodeBuilder();
3656b6152ba96c164a292cc0b8d8b1d4cecbec27a60Anna Zaks
3668ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks  ExplodedNode *generateNode(const Stmt *S,
3678ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                             ExplodedNode *Pred,
3688bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef St,
3698ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                             bool MarkAsSink = false,
3708ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                             const ProgramPointTag *tag = 0,
371aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks                             ProgramPoint::Kind K = ProgramPoint::PostStmtKind){
3728ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks    const ProgramPoint &L = ProgramPoint::getProgramPoint(S, K,
3738ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                                  Pred->getLocationContext(), tag);
3748ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks    return generateNodeImpl(L, St, Pred, MarkAsSink);
3758ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks  }
376ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
377ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  ExplodedNode *generateNode(const ProgramPoint &PP,
378ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                             ExplodedNode *Pred,
3798bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef State,
380ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                             bool MarkAsSink = false) {
381ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    return generateNodeImpl(PP, State, Pred, MarkAsSink);
382ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
3838ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks};
3848ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks
385cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// \brief BranchNodeBuilder is responsible for constructing the nodes
386cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// corresponding to the two branches of the if statement - true and false.
387a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksclass BranchNodeBuilder: public NodeBuilder {
38899ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie  virtual void anchor();
3899c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *DstT;
3909c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *DstF;
39152a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek
392520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  bool InFeasibleTrue;
393520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  bool InFeasibleFalse;
3941eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
3957d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenekpublic:
3961aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  BranchNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet,
3971aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks                    const NodeBuilderContext &C,
398ad62deeb70e97da6bd514dd390ea1ce6af6ad81dAnna Zaks                    const CFGBlock *dstT, const CFGBlock *dstF)
3991aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  : NodeBuilder(SrcNode, DstSet, C), DstT(dstT), DstF(dstF),
400cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) {
4012d950b15b2b2b650b102ecf0c6b50b45e0cb6a8aAnna Zaks    // The branch node builder does not generate autotransitions.
402cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    // If there are no successors it means that both branches are infeasible.
403cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    takeNodes(SrcNode);
404cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks  }
405031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
4061aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  BranchNodeBuilder(const ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet,
4071aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks                    const NodeBuilderContext &C,
4081aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks                    const CFGBlock *dstT, const CFGBlock *dstF)
4091aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  : NodeBuilder(SrcSet, DstSet, C), DstT(dstT), DstF(dstF),
410cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) {
411cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    takeNodes(SrcSet);
412cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks  }
4138083414ee7cc8f5c807ed6a4e120fb4e0ab50ff8Ted Kremenek
4148bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ExplodedNode *generateNode(ProgramStateRef State, bool branch,
415c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks                             ExplodedNode *Pred);
4161eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4179c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *getTargetBlock(bool branch) const {
4188e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek    return branch ? DstT : DstF;
4191eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  }
4201eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
42152a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek  void markInfeasible(bool branch) {
422520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    if (branch)
4234e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks      InFeasibleTrue = true;
424520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    else
4254e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks      InFeasibleFalse = true;
426520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  }
4271eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
428520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  bool isFeasible(bool branch) {
429520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    return branch ? !InFeasibleTrue : !InFeasibleFalse;
43052a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek  }
4317d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek};
432031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
433d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass IndirectGotoNodeBuilder {
434d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  CoreEngine& Eng;
4359c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *Src;
4369c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock &DispatchBlock;
4379c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *E;
4389c378f705405d37f49795d5e915989de774fe11fTed Kremenek  ExplodedNode *Pred;
439031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
440754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenekpublic:
4419c378f705405d37f49795d5e915989de774fe11fTed Kremenek  IndirectGotoNodeBuilder(ExplodedNode *pred, const CFGBlock *src,
4429c378f705405d37f49795d5e915989de774fe11fTed Kremenek                    const Expr *e, const CFGBlock *dispatch, CoreEngine* eng)
44303509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    : Eng(*eng), Src(src), DispatchBlock(*dispatch), E(e), Pred(pred) {}
444754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek
445031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  class iterator {
44603509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    CFGBlock::const_succ_iterator I;
4471eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
448d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    friend class IndirectGotoNodeBuilder;
44903509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    iterator(CFGBlock::const_succ_iterator i) : I(i) {}
450754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek  public:
4511eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4529c378f705405d37f49795d5e915989de774fe11fTed Kremenek    iterator &operator++() { ++I; return *this; }
4539c378f705405d37f49795d5e915989de774fe11fTed Kremenek    bool operator!=(const iterator &X) const { return I != X.I; }
4541eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
455ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner    const LabelDecl *getLabel() const {
456ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner      return llvm::cast<LabelStmt>((*I)->getLabel())->getDecl();
45724f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek    }
4581eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
459ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner    const CFGBlock *getBlock() const {
46024f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek      return *I;
46124f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek    }
462754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek  };
4631eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
464031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator begin() { return iterator(DispatchBlock.succ_begin()); }
465031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator end() { return iterator(DispatchBlock.succ_end()); }
4661eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
46718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek  ExplodedNode *generateNode(const iterator &I,
4688bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef State,
469031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu                             bool isSink = false);
4701eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4719c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *getTarget() const { return E; }
472754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek
4738bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef getState() const { return Pred->State; }
4745eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek
4755eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  const LocationContext *getLocationContext() const {
4765eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek    return Pred->getLocationContext();
4775eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  }
478754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek};
4791eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
480d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass SwitchNodeBuilder {
481d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  CoreEngine& Eng;
4829c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *Src;
4839c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *Condition;
4849c378f705405d37f49795d5e915989de774fe11fTed Kremenek  ExplodedNode *Pred;
485031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
486daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenekpublic:
4879c378f705405d37f49795d5e915989de774fe11fTed Kremenek  SwitchNodeBuilder(ExplodedNode *pred, const CFGBlock *src,
4889c378f705405d37f49795d5e915989de774fe11fTed Kremenek                    const Expr *condition, CoreEngine* eng)
489daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  : Eng(*eng), Src(src), Condition(condition), Pred(pred) {}
4901eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
491031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  class iterator {
49203509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    CFGBlock::const_succ_reverse_iterator I;
4931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
494d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    friend class SwitchNodeBuilder;
49503509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    iterator(CFGBlock::const_succ_reverse_iterator i) : I(i) {}
496031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
497daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  public:
4989c378f705405d37f49795d5e915989de774fe11fTed Kremenek    iterator &operator++() { ++I; return *this; }
49934feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek    bool operator!=(const iterator &X) const { return I != X.I; }
50034feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek    bool operator==(const iterator &X) const { return I == X.I; }
5011eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5029c378f705405d37f49795d5e915989de774fe11fTed Kremenek    const CaseStmt *getCase() const {
503daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek      return llvm::cast<CaseStmt>((*I)->getLabel());
504daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek    }
5051eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5069c378f705405d37f49795d5e915989de774fe11fTed Kremenek    const CFGBlock *getBlock() const {
507daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek      return *I;
508daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek    }
509daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  };
5101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
511031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator begin() { return iterator(Src->succ_rbegin()+1); }
512031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator end() { return iterator(Src->succ_rend()); }
5131eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5144d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek  const SwitchStmt *getSwitch() const {
5154d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek    return llvm::cast<SwitchStmt>(Src->getTerminator());
5164d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek  }
5174d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek
51818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek  ExplodedNode *generateCaseStmtNode(const iterator &I,
5198bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                     ProgramStateRef State);
5201eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5218bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ExplodedNode *generateDefaultCaseNode(ProgramStateRef State,
522031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu                                        bool isSink = false);
5231eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5249c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *getCondition() const { return Condition; }
525daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek
5268bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef getState() const { return Pred->State; }
5275eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek
5285eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  const LocationContext *getLocationContext() const {
5295eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek    return Pred->getLocationContext();
5305eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  }
531daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek};
53211062b118476368fa5b294954713e5df97d8599fTed Kremenek
5333070e13dca5bbefa32acb80ce4a7b217a6220983Ted Kremenek} // end ento namespace
534f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek} // end clang namespace
535f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
536f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#endif
537