CoreEngine.h revision e62f048960645b79363408fdead53fec2a063c52
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.
68d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  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.
853fd5f370a28552976c52e76c3035d79012d78ddaAnna Zaks  SetOfDecls *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
1074d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  ExplodedNode *generateCallExitNode(ExplodedNode *N);
1084d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks
109f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenekpublic:
110d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  /// Construct a CoreEngine object to analyze the provided CFG using
1110111f575b968e423dccae439e501225b8314b257Zhongxing Xu  ///  a DFS exploration of the exploded graph.
112e62f048960645b79363408fdead53fec2a063c52Anna Zaks  CoreEngine(SubEngine& subengine, SetOfDecls *VisitedCallees,
113e62f048960645b79363408fdead53fec2a063c52Anna Zaks             FunctionSummariesTy *FS)
114d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    : SubEng(subengine), G(new ExplodedGraph()),
11555825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek      WList(WorkList::makeBFS()),
1163fd5f370a28552976c52e76c3035d79012d78ddaAnna Zaks      BCounterFactory(G->getAllocator()),
117e62f048960645b79363408fdead53fec2a063c52Anna Zaks      AnalyzedCallees(VisitedCallees),
118e62f048960645b79363408fdead53fec2a063c52Anna Zaks      FunctionSummaries(FS){}
1190111f575b968e423dccae439e501225b8314b257Zhongxing Xu
120d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  ~CoreEngine() {
1210111f575b968e423dccae439e501225b8314b257Zhongxing Xu    delete WList;
1220111f575b968e423dccae439e501225b8314b257Zhongxing Xu  }
1230111f575b968e423dccae439e501225b8314b257Zhongxing Xu
1240111f575b968e423dccae439e501225b8314b257Zhongxing Xu  /// getGraph - Returns the exploded graph.
125031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  ExplodedGraph& getGraph() { return *G.get(); }
1261eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1270111f575b968e423dccae439e501225b8314b257Zhongxing Xu  /// takeGraph - Returns the exploded graph.  Ownership of the graph is
128fc8f0e14ad142ed811e90fbd9a30e419e301c717Chris Lattner  ///  transferred to the caller.
129031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  ExplodedGraph* takeGraph() { return G.take(); }
1300111f575b968e423dccae439e501225b8314b257Zhongxing Xu
131f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  /// ExecuteWorkList - Run the worklist algorithm for a maximum number of
132f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek  ///  steps.  Returns true if there is still simulation state on the worklist.
1332ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu  bool ExecuteWorkList(const LocationContext *L, unsigned Steps,
1348bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                       ProgramStateRef InitState);
135253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks  /// Returns true if there is still simulation state on the worklist.
136253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks  bool ExecuteWorkListWithInitialState(const LocationContext *L,
13718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek                                       unsigned Steps,
1388bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                       ProgramStateRef InitState,
1392ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu                                       ExplodedNodeSet &Dst);
140bc42c533e7d3d946704a49e242939dd232f33072Tom Care
1415903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  /// Dispatch the work list item based on the given location information.
1425903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  /// Use Pred parameter as the predecessor state.
1435903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  void dispatchWorkItem(ExplodedNode* Pred, ProgramPoint Loc,
1445903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks                        const WorkListUnit& WU);
1455903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks
146bc42c533e7d3d946704a49e242939dd232f33072Tom Care  // Functions for external checking of whether we have unfinished work
147422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  bool wasBlockAborted() const { return !blocksAborted.empty(); }
148422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  bool wasBlocksExhausted() const { return !blocksExhausted.empty(); }
149422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  bool hasWorkRemaining() const { return wasBlocksExhausted() ||
150422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek                                         WList->hasWork() ||
151422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek                                         wasBlockAborted(); }
152422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek
153422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  /// Inform the CoreEngine that a basic block was aborted because
154422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  /// it could not be completely analyzed.
155422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  void addAbortedBlock(const ExplodedNode *node, const CFGBlock *block) {
156422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek    blocksAborted.push_back(std::make_pair(block, node));
157422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  }
158422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek
159d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  WorkList *getWorkList() const { return WList; }
160f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek
161422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  BlocksExhausted::const_iterator blocks_exhausted_begin() const {
16266750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek    return blocksExhausted.begin();
163f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek  }
164422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  BlocksExhausted::const_iterator blocks_exhausted_end() const {
16566750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek    return blocksExhausted.end();
166f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek  }
167422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  BlocksAborted::const_iterator blocks_aborted_begin() const {
168422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek    return blocksAborted.begin();
169422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  }
170422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  BlocksAborted::const_iterator blocks_aborted_end() const {
171422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek    return blocksAborted.end();
172422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek  }
173a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks
174dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  /// \brief Enqueue the given set of nodes onto the work list.
1754d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  void enqueue(ExplodedNodeSet &Set);
176dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks
177dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  /// \brief Enqueue nodes that were created as a result of processing
178dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  /// a statement onto the work list.
179dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks  void enqueue(ExplodedNodeSet &Set, const CFGBlock *Block, unsigned Idx);
1804d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks
1814d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  /// \brief enqueue the nodes corresponding to the end of function onto the
1824d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  /// end of path / work list.
1834d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks  void enqueueEndOfFunction(ExplodedNodeSet &Set);
1845903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks
1855903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  /// \brief Enqueue a single node created as a result of statement processing.
1865903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks  void enqueueStmtNode(ExplodedNode *N, const CFGBlock *Block, unsigned Idx);
187a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks};
188a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks
189c03a39e16762627b421247b12a2658be630a3300Anna Zaks// TODO: Turn into a calss.
190a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksstruct NodeBuilderContext {
191a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  CoreEngine &Eng;
192a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  const CFGBlock *Block;
193af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks  ExplodedNode *Pred;
194c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks  NodeBuilderContext(CoreEngine &E, const CFGBlock *B, ExplodedNode *N)
195af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks    : Eng(E), Block(B), Pred(N) { assert(B); assert(!N->isSink()); }
196ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
197c03a39e16762627b421247b12a2658be630a3300Anna Zaks  ExplodedNode *getPred() const { return Pred; }
198c03a39e16762627b421247b12a2658be630a3300Anna Zaks
199ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  /// \brief Return the CFGBlock associated with this builder.
200ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  const CFGBlock *getBlock() const { return Block; }
201ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
202ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  /// \brief Returns the number of times the current basic block has been
203ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  /// visited on the exploded graph path.
204ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  unsigned getCurrentBlockCount() const {
205ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    return Eng.WList->getBlockCounter().getNumVisited(
206af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks                    Pred->getLocationContext()->getCurrentStackFrame(),
207ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                    Block->getBlockID());
208ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
209f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek};
2101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
211aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \class NodeBuilder
212aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \brief This is the simplest builder which generates nodes in the
213aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// ExplodedGraph.
214aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks///
215aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// The main benefit of the builder is that it automatically tracks the
216aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// frontier nodes (or destination set). This is the set of nodes which should
217aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// be propagated to the next step / builder. They are the nodes which have been
218aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// added to the builder (either as the input node set or as the newly
219aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// constructed nodes) but did not have any outgoing transitions added.
220f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaksclass NodeBuilder {
22199ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie  virtual void anchor();
222a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksprotected:
223cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks  const NodeBuilderContext &C;
224319a9184d5ca9f77622b45ae15c08f6b9ce01621Anna Zaks
2253152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  /// Specifies if the builder results have been finalized. For example, if it
2263152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  /// is set to false, autotransitions are yet to be generated.
227f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  bool Finalized;
2284e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks  bool HasGeneratedNodes;
229f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// \brief The frontier set - a set of nodes which need to be propagated after
230f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// the builder dies.
2311aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  ExplodedNodeSet &Frontier;
23271fdf469a3b6d7d557b0bfba36e8659f4966c565Anna Zaks
2333152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  /// Checkes if the results are ready.
2343152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  virtual bool checkResults() {
235a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    if (!Finalized)
236a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks      return false;
237a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    return true;
238a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  }
239f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
240aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  bool hasNoSinksInFrontier() {
2418ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks    for (iterator I = Frontier.begin(), E = Frontier.end(); I != E; ++I) {
2428ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks      if ((*I)->isSink())
2438ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks        return false;
2448ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks    }
2458ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks    return true;
2468ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks  }
2478ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks
2483152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  /// Allow subclasses to finalize results before result_begin() is executed.
2493152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks  virtual void finalizeResults() {}
250f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
251f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  ExplodedNode *generateNodeImpl(const ProgramPoint &PP,
2528bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                 ProgramStateRef State,
253f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks                                 ExplodedNode *Pred,
254f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks                                 bool MarkAsSink = false);
255f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
256f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zakspublic:
2571aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  NodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet,
2581aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks              const NodeBuilderContext &Ctx, bool F = true)
2591aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    : C(Ctx), Finalized(F), HasGeneratedNodes(false), Frontier(DstSet) {
2608ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks    Frontier.Add(SrcNode);
261ad62deeb70e97da6bd514dd390ea1ce6af6ad81dAnna Zaks  }
262a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks
2631aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  NodeBuilder(const ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet,
2641aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks              const NodeBuilderContext &Ctx, bool F = true)
2651aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    : C(Ctx), Finalized(F), HasGeneratedNodes(false), Frontier(DstSet) {
2661aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    Frontier.insert(SrcSet);
267aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks    assert(hasNoSinksInFrontier());
268cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks  }
269cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks
270a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  virtual ~NodeBuilder() {}
271f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
272f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// \brief Generates a node in the ExplodedGraph.
273f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  ///
274f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// When a node is marked as sink, the exploration from the node is stopped -
275f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// the node becomes the last node on the path.
276f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  ExplodedNode *generateNode(const ProgramPoint &PP,
2778bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef State,
278f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks                             ExplodedNode *Pred,
279f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks                             bool MarkAsSink = false) {
280f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks    return generateNodeImpl(PP, State, Pred, MarkAsSink);
281f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  }
282f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
2831aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  const ExplodedNodeSet &getResults() {
2841aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    finalizeResults();
2851aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    assert(checkResults());
2861aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    return Frontier;
2871aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  }
2881aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks
2891aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  typedef ExplodedNodeSet::iterator iterator;
290f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// \brief Iterators through the results frontier.
2911aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  inline iterator begin() {
292a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    finalizeResults();
293a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    assert(checkResults());
2941aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    return Frontier.begin();
295a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  }
2961aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  inline iterator end() {
297a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    finalizeResults();
2981aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    return Frontier.end();
299a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  }
300f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
3011aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  const NodeBuilderContext &getContext() { return C; }
302aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  bool hasGeneratedNodes() { return HasGeneratedNodes; }
3031aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks
304d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks  void takeNodes(const ExplodedNodeSet &S) {
305d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks    for (ExplodedNodeSet::iterator I = S.begin(), E = S.end(); I != E; ++I )
306d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks      Frontier.erase(*I);
307d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks  }
308aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  void takeNodes(ExplodedNode *N) { Frontier.erase(N); }
309aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  void addNodes(const ExplodedNodeSet &S) { Frontier.insert(S); }
310aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  void addNodes(ExplodedNode *N) { Frontier.Add(N); }
311f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks};
312f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
313c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \class NodeBuilderWithSinks
314c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \brief This node builder keeps track of the generated sink nodes.
315c03a39e16762627b421247b12a2658be630a3300Anna Zaksclass NodeBuilderWithSinks: public NodeBuilder {
31699ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie  virtual void anchor();
317c03a39e16762627b421247b12a2658be630a3300Anna Zaksprotected:
318c03a39e16762627b421247b12a2658be630a3300Anna Zaks  SmallVector<ExplodedNode*, 2> sinksGenerated;
319c03a39e16762627b421247b12a2658be630a3300Anna Zaks  ProgramPoint &Location;
320c03a39e16762627b421247b12a2658be630a3300Anna Zaks
321c03a39e16762627b421247b12a2658be630a3300Anna Zakspublic:
322c03a39e16762627b421247b12a2658be630a3300Anna Zaks  NodeBuilderWithSinks(ExplodedNode *Pred, ExplodedNodeSet &DstSet,
323c03a39e16762627b421247b12a2658be630a3300Anna Zaks                       const NodeBuilderContext &Ctx, ProgramPoint &L)
324c03a39e16762627b421247b12a2658be630a3300Anna Zaks    : NodeBuilder(Pred, DstSet, Ctx), Location(L) {}
3258bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ExplodedNode *generateNode(ProgramStateRef State,
326c03a39e16762627b421247b12a2658be630a3300Anna Zaks                             ExplodedNode *Pred,
327c03a39e16762627b421247b12a2658be630a3300Anna Zaks                             const ProgramPointTag *Tag = 0,
328c03a39e16762627b421247b12a2658be630a3300Anna Zaks                             bool MarkAsSink = false) {
329c03a39e16762627b421247b12a2658be630a3300Anna Zaks    ProgramPoint LocalLoc = (Tag ? Location.withTag(Tag): Location);
330c03a39e16762627b421247b12a2658be630a3300Anna Zaks
331c03a39e16762627b421247b12a2658be630a3300Anna Zaks    ExplodedNode *N = generateNodeImpl(LocalLoc, State, Pred, MarkAsSink);
332c03a39e16762627b421247b12a2658be630a3300Anna Zaks    if (N && N->isSink())
333c03a39e16762627b421247b12a2658be630a3300Anna Zaks      sinksGenerated.push_back(N);
334c03a39e16762627b421247b12a2658be630a3300Anna Zaks    return N;
335c03a39e16762627b421247b12a2658be630a3300Anna Zaks  }
336c03a39e16762627b421247b12a2658be630a3300Anna Zaks
337c03a39e16762627b421247b12a2658be630a3300Anna Zaks  const SmallVectorImpl<ExplodedNode*> &getSinks() const {
338c03a39e16762627b421247b12a2658be630a3300Anna Zaks    return sinksGenerated;
339c03a39e16762627b421247b12a2658be630a3300Anna Zaks  }
340c03a39e16762627b421247b12a2658be630a3300Anna Zaks};
341c03a39e16762627b421247b12a2658be630a3300Anna Zaks
342aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \class StmtNodeBuilder
343aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \brief This builder class is useful for generating nodes that resulted from
344aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// visiting a statement. The main difference from it's parent NodeBuilder is
345aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// that it creates a statement specific ProgramPoint.
346aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaksclass StmtNodeBuilder: public NodeBuilder {
347ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  NodeBuilder *EnclosingBldr;
3488ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zakspublic:
349aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks
350aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  /// \brief Constructs a StmtNodeBuilder. If the builder is going to process
351aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  /// nodes currently owned by another builder(with larger scope), use
352aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  /// Enclosing builder to transfer ownership.
353aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  StmtNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet,
354ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                      const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0)
355ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    : NodeBuilder(SrcNode, DstSet, Ctx), EnclosingBldr(Enclosing) {
356ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    if (EnclosingBldr)
357ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks      EnclosingBldr->takeNodes(SrcNode);
358ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
3598ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks
360aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  StmtNodeBuilder(ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet,
361ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                      const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0)
362ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    : NodeBuilder(SrcSet, DstSet, Ctx), EnclosingBldr(Enclosing) {
363ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    if (EnclosingBldr)
364ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks      for (ExplodedNodeSet::iterator I = SrcSet.begin(),
365ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                                     E = SrcSet.end(); I != E; ++I )
366ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks        EnclosingBldr->takeNodes(*I);
367ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
368ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
369aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  virtual ~StmtNodeBuilder();
3706b6152ba96c164a292cc0b8d8b1d4cecbec27a60Anna Zaks
3718ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks  ExplodedNode *generateNode(const Stmt *S,
3728ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                             ExplodedNode *Pred,
3738bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef St,
3748ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                             bool MarkAsSink = false,
3758ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                             const ProgramPointTag *tag = 0,
376aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks                             ProgramPoint::Kind K = ProgramPoint::PostStmtKind){
3778ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks    const ProgramPoint &L = ProgramPoint::getProgramPoint(S, K,
3788ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                                  Pred->getLocationContext(), tag);
3798ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks    return generateNodeImpl(L, St, Pred, MarkAsSink);
3808ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks  }
381ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
382ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  ExplodedNode *generateNode(const ProgramPoint &PP,
383ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                             ExplodedNode *Pred,
3848bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef State,
385ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                             bool MarkAsSink = false) {
386ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    return generateNodeImpl(PP, State, Pred, MarkAsSink);
387ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
3888ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks};
3898ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks
390cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// \brief BranchNodeBuilder is responsible for constructing the nodes
391cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// corresponding to the two branches of the if statement - true and false.
392a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksclass BranchNodeBuilder: public NodeBuilder {
39399ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie  virtual void anchor();
3949c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *DstT;
3959c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *DstF;
39652a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek
397520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  bool InFeasibleTrue;
398520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  bool InFeasibleFalse;
3991eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4007d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenekpublic:
4011aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  BranchNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet,
4021aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks                    const NodeBuilderContext &C,
403ad62deeb70e97da6bd514dd390ea1ce6af6ad81dAnna Zaks                    const CFGBlock *dstT, const CFGBlock *dstF)
4041aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  : NodeBuilder(SrcNode, DstSet, C), DstT(dstT), DstF(dstF),
405cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) {
4062d950b15b2b2b650b102ecf0c6b50b45e0cb6a8aAnna Zaks    // The branch node builder does not generate autotransitions.
407cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    // If there are no successors it means that both branches are infeasible.
408cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    takeNodes(SrcNode);
409cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks  }
410031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
4111aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  BranchNodeBuilder(const ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet,
4121aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks                    const NodeBuilderContext &C,
4131aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks                    const CFGBlock *dstT, const CFGBlock *dstF)
4141aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  : NodeBuilder(SrcSet, DstSet, C), DstT(dstT), DstF(dstF),
415cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) {
416cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    takeNodes(SrcSet);
417cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks  }
4188083414ee7cc8f5c807ed6a4e120fb4e0ab50ff8Ted Kremenek
4198bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ExplodedNode *generateNode(ProgramStateRef State, bool branch,
420c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks                             ExplodedNode *Pred);
4211eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4229c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *getTargetBlock(bool branch) const {
4238e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek    return branch ? DstT : DstF;
4241eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  }
4251eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
42652a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek  void markInfeasible(bool branch) {
427520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    if (branch)
4284e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks      InFeasibleTrue = true;
429520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    else
4304e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks      InFeasibleFalse = true;
431520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  }
4321eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
433520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  bool isFeasible(bool branch) {
434520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    return branch ? !InFeasibleTrue : !InFeasibleFalse;
43552a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek  }
4367d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek};
437031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
438d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass IndirectGotoNodeBuilder {
439d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  CoreEngine& Eng;
4409c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *Src;
4419c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock &DispatchBlock;
4429c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *E;
4439c378f705405d37f49795d5e915989de774fe11fTed Kremenek  ExplodedNode *Pred;
444031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
445754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenekpublic:
4469c378f705405d37f49795d5e915989de774fe11fTed Kremenek  IndirectGotoNodeBuilder(ExplodedNode *pred, const CFGBlock *src,
4479c378f705405d37f49795d5e915989de774fe11fTed Kremenek                    const Expr *e, const CFGBlock *dispatch, CoreEngine* eng)
44803509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    : Eng(*eng), Src(src), DispatchBlock(*dispatch), E(e), Pred(pred) {}
449754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek
450031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  class iterator {
45103509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    CFGBlock::const_succ_iterator I;
4521eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
453d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    friend class IndirectGotoNodeBuilder;
45403509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    iterator(CFGBlock::const_succ_iterator i) : I(i) {}
455754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek  public:
4561eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4579c378f705405d37f49795d5e915989de774fe11fTed Kremenek    iterator &operator++() { ++I; return *this; }
4589c378f705405d37f49795d5e915989de774fe11fTed Kremenek    bool operator!=(const iterator &X) const { return I != X.I; }
4591eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
460ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner    const LabelDecl *getLabel() const {
461ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner      return llvm::cast<LabelStmt>((*I)->getLabel())->getDecl();
46224f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek    }
4631eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
464ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner    const CFGBlock *getBlock() const {
46524f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek      return *I;
46624f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek    }
467754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek  };
4681eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
469031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator begin() { return iterator(DispatchBlock.succ_begin()); }
470031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator end() { return iterator(DispatchBlock.succ_end()); }
4711eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
47218c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek  ExplodedNode *generateNode(const iterator &I,
4738bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef State,
474031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu                             bool isSink = false);
4751eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4769c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *getTarget() const { return E; }
477754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek
4788bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef getState() const { return Pred->State; }
4795eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek
4805eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  const LocationContext *getLocationContext() const {
4815eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek    return Pred->getLocationContext();
4825eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  }
483754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek};
4841eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
485d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass SwitchNodeBuilder {
486d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  CoreEngine& Eng;
4879c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *Src;
4889c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *Condition;
4899c378f705405d37f49795d5e915989de774fe11fTed Kremenek  ExplodedNode *Pred;
490031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
491daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenekpublic:
4929c378f705405d37f49795d5e915989de774fe11fTed Kremenek  SwitchNodeBuilder(ExplodedNode *pred, const CFGBlock *src,
4939c378f705405d37f49795d5e915989de774fe11fTed Kremenek                    const Expr *condition, CoreEngine* eng)
494daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  : Eng(*eng), Src(src), Condition(condition), Pred(pred) {}
4951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
496031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  class iterator {
49703509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    CFGBlock::const_succ_reverse_iterator I;
4981eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
499d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    friend class SwitchNodeBuilder;
50003509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    iterator(CFGBlock::const_succ_reverse_iterator i) : I(i) {}
501031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
502daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  public:
5039c378f705405d37f49795d5e915989de774fe11fTed Kremenek    iterator &operator++() { ++I; return *this; }
50434feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek    bool operator!=(const iterator &X) const { return I != X.I; }
50534feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek    bool operator==(const iterator &X) const { return I == X.I; }
5061eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5079c378f705405d37f49795d5e915989de774fe11fTed Kremenek    const CaseStmt *getCase() const {
508daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek      return llvm::cast<CaseStmt>((*I)->getLabel());
509daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek    }
5101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5119c378f705405d37f49795d5e915989de774fe11fTed Kremenek    const CFGBlock *getBlock() const {
512daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek      return *I;
513daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek    }
514daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  };
5151eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
516031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator begin() { return iterator(Src->succ_rbegin()+1); }
517031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator end() { return iterator(Src->succ_rend()); }
5181eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5194d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek  const SwitchStmt *getSwitch() const {
5204d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek    return llvm::cast<SwitchStmt>(Src->getTerminator());
5214d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek  }
5224d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek
52318c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek  ExplodedNode *generateCaseStmtNode(const iterator &I,
5248bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                     ProgramStateRef State);
5251eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5268bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ExplodedNode *generateDefaultCaseNode(ProgramStateRef State,
527031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu                                        bool isSink = false);
5281eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5299c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *getCondition() const { return Condition; }
530daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek
5318bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef getState() const { return Pred->State; }
5325eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek
5335eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  const LocationContext *getLocationContext() const {
5345eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek    return Pred->getLocationContext();
5355eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  }
536daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek};
53711062b118476368fa5b294954713e5df97d8599fTed Kremenek
5383070e13dca5bbefa32acb80ce4a7b217a6220983Ted Kremenek} // end ento namespace
539f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek} // end clang namespace
540f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
541f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#endif
542