CoreEngine.h revision fa06f0464a04bb7fce1fcfb3780d151bb029e00c
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.
268fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  ExplodedNode *generateNode(const ProgramPoint &PP,
269fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose                             ProgramStateRef State,
270fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose                             ExplodedNode *Pred) {
271fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose    return generateNodeImpl(PP, State, Pred, false);
272fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  }
273fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose
274fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  /// \brief Generates a sink in the ExplodedGraph.
275f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  ///
276f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// When a node is marked as sink, the exploration from the node is stopped -
277fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  /// the node becomes the last node on the path and certain kinds of bugs are
278fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  /// suppressed.
279fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  ExplodedNode *generateSink(const ProgramPoint &PP,
2808bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef State,
281fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose                             ExplodedNode *Pred) {
282fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose    return generateNodeImpl(PP, State, Pred, true);
283f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  }
284f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
2851aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  const ExplodedNodeSet &getResults() {
2861aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    finalizeResults();
2871aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    assert(checkResults());
2881aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    return Frontier;
2891aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  }
2901aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks
2911aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  typedef ExplodedNodeSet::iterator iterator;
292f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks  /// \brief Iterators through the results frontier.
2931aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  inline iterator begin() {
294a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    finalizeResults();
295a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    assert(checkResults());
2961aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    return Frontier.begin();
297a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  }
2981aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  inline iterator end() {
299a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks    finalizeResults();
3001aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks    return Frontier.end();
301a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks  }
302f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
3031aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  const NodeBuilderContext &getContext() { return C; }
304aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  bool hasGeneratedNodes() { return HasGeneratedNodes; }
3051aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks
306d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks  void takeNodes(const ExplodedNodeSet &S) {
307d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks    for (ExplodedNodeSet::iterator I = S.begin(), E = S.end(); I != E; ++I )
308d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks      Frontier.erase(*I);
309d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks  }
310aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  void takeNodes(ExplodedNode *N) { Frontier.erase(N); }
311aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  void addNodes(const ExplodedNodeSet &S) { Frontier.insert(S); }
312aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  void addNodes(ExplodedNode *N) { Frontier.Add(N); }
313f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks};
314f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks
315c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \class NodeBuilderWithSinks
316c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \brief This node builder keeps track of the generated sink nodes.
317c03a39e16762627b421247b12a2658be630a3300Anna Zaksclass NodeBuilderWithSinks: public NodeBuilder {
31899ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie  virtual void anchor();
319c03a39e16762627b421247b12a2658be630a3300Anna Zaksprotected:
320c03a39e16762627b421247b12a2658be630a3300Anna Zaks  SmallVector<ExplodedNode*, 2> sinksGenerated;
321c03a39e16762627b421247b12a2658be630a3300Anna Zaks  ProgramPoint &Location;
322c03a39e16762627b421247b12a2658be630a3300Anna Zaks
323c03a39e16762627b421247b12a2658be630a3300Anna Zakspublic:
324c03a39e16762627b421247b12a2658be630a3300Anna Zaks  NodeBuilderWithSinks(ExplodedNode *Pred, ExplodedNodeSet &DstSet,
325c03a39e16762627b421247b12a2658be630a3300Anna Zaks                       const NodeBuilderContext &Ctx, ProgramPoint &L)
326c03a39e16762627b421247b12a2658be630a3300Anna Zaks    : NodeBuilder(Pred, DstSet, Ctx), Location(L) {}
327fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose
3288bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ExplodedNode *generateNode(ProgramStateRef State,
329c03a39e16762627b421247b12a2658be630a3300Anna Zaks                             ExplodedNode *Pred,
330fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose                             const ProgramPointTag *Tag = 0) {
331fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose    const ProgramPoint &LocalLoc = (Tag ? Location.withTag(Tag) : Location);
332fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose    return NodeBuilder::generateNode(LocalLoc, State, Pred);
333fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  }
334c03a39e16762627b421247b12a2658be630a3300Anna Zaks
335fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  ExplodedNode *generateSink(ProgramStateRef State, ExplodedNode *Pred,
336fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose                             const ProgramPointTag *Tag = 0) {
337fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose    const ProgramPoint &LocalLoc = (Tag ? Location.withTag(Tag) : Location);
338fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose    ExplodedNode *N = NodeBuilder::generateSink(LocalLoc, State, Pred);
339c03a39e16762627b421247b12a2658be630a3300Anna Zaks    if (N && N->isSink())
340c03a39e16762627b421247b12a2658be630a3300Anna Zaks      sinksGenerated.push_back(N);
341c03a39e16762627b421247b12a2658be630a3300Anna Zaks    return N;
342c03a39e16762627b421247b12a2658be630a3300Anna Zaks  }
343c03a39e16762627b421247b12a2658be630a3300Anna Zaks
344c03a39e16762627b421247b12a2658be630a3300Anna Zaks  const SmallVectorImpl<ExplodedNode*> &getSinks() const {
345c03a39e16762627b421247b12a2658be630a3300Anna Zaks    return sinksGenerated;
346c03a39e16762627b421247b12a2658be630a3300Anna Zaks  }
347c03a39e16762627b421247b12a2658be630a3300Anna Zaks};
348c03a39e16762627b421247b12a2658be630a3300Anna Zaks
349aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \class StmtNodeBuilder
350aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \brief This builder class is useful for generating nodes that resulted from
351fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose/// visiting a statement. The main difference from its parent NodeBuilder is
352aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// that it creates a statement specific ProgramPoint.
353aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaksclass StmtNodeBuilder: public NodeBuilder {
354ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  NodeBuilder *EnclosingBldr;
3558ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zakspublic:
356aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks
357aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  /// \brief Constructs a StmtNodeBuilder. If the builder is going to process
358aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  /// nodes currently owned by another builder(with larger scope), use
359aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  /// Enclosing builder to transfer ownership.
360aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  StmtNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet,
361ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                      const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0)
362ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    : NodeBuilder(SrcNode, DstSet, Ctx), EnclosingBldr(Enclosing) {
363ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    if (EnclosingBldr)
364ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks      EnclosingBldr->takeNodes(SrcNode);
365ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
3668ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks
367aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  StmtNodeBuilder(ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet,
368ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                      const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0)
369ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    : NodeBuilder(SrcSet, DstSet, Ctx), EnclosingBldr(Enclosing) {
370ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks    if (EnclosingBldr)
371ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks      for (ExplodedNodeSet::iterator I = SrcSet.begin(),
372ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                                     E = SrcSet.end(); I != E; ++I )
373ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks        EnclosingBldr->takeNodes(*I);
374ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
375ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
376aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks  virtual ~StmtNodeBuilder();
3776b6152ba96c164a292cc0b8d8b1d4cecbec27a60Anna Zaks
378fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  using NodeBuilder::generateNode;
379fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  using NodeBuilder::generateSink;
380fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose
3818ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks  ExplodedNode *generateNode(const Stmt *S,
3828ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                             ExplodedNode *Pred,
3838bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef St,
3848ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                             const ProgramPointTag *tag = 0,
385aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks                             ProgramPoint::Kind K = ProgramPoint::PostStmtKind){
3868ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks    const ProgramPoint &L = ProgramPoint::getProgramPoint(S, K,
3878ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks                                  Pred->getLocationContext(), tag);
388fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose    return NodeBuilder::generateNode(L, St, Pred);
3898ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks  }
390ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks
391fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose  ExplodedNode *generateSink(const Stmt *S,
392ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks                             ExplodedNode *Pred,
393fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose                             ProgramStateRef St,
394fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose                             const ProgramPointTag *tag = 0,
395fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose                             ProgramPoint::Kind K = ProgramPoint::PostStmtKind){
396fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose    const ProgramPoint &L = ProgramPoint::getProgramPoint(S, K,
397fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose                                  Pred->getLocationContext(), tag);
398fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose    return NodeBuilder::generateSink(L, St, Pred);
399ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks  }
4008ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks};
4018ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks
402cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// \brief BranchNodeBuilder is responsible for constructing the nodes
403cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// corresponding to the two branches of the if statement - true and false.
404a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksclass BranchNodeBuilder: public NodeBuilder {
40599ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie  virtual void anchor();
4069c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *DstT;
4079c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *DstF;
40852a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek
409520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  bool InFeasibleTrue;
410520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  bool InFeasibleFalse;
4111eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4127d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenekpublic:
4131aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  BranchNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet,
4141aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks                    const NodeBuilderContext &C,
415ad62deeb70e97da6bd514dd390ea1ce6af6ad81dAnna Zaks                    const CFGBlock *dstT, const CFGBlock *dstF)
4161aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  : NodeBuilder(SrcNode, DstSet, C), DstT(dstT), DstF(dstF),
417cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) {
4182d950b15b2b2b650b102ecf0c6b50b45e0cb6a8aAnna Zaks    // The branch node builder does not generate autotransitions.
419cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    // If there are no successors it means that both branches are infeasible.
420cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    takeNodes(SrcNode);
421cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks  }
422031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
4231aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  BranchNodeBuilder(const ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet,
4241aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks                    const NodeBuilderContext &C,
4251aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks                    const CFGBlock *dstT, const CFGBlock *dstF)
4261aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks  : NodeBuilder(SrcSet, DstSet, C), DstT(dstT), DstF(dstF),
427cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) {
428cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks    takeNodes(SrcSet);
429cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks  }
4308083414ee7cc8f5c807ed6a4e120fb4e0ab50ff8Ted Kremenek
4318bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ExplodedNode *generateNode(ProgramStateRef State, bool branch,
432c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks                             ExplodedNode *Pred);
4331eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4349c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *getTargetBlock(bool branch) const {
4358e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek    return branch ? DstT : DstF;
4361eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  }
4371eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
43852a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek  void markInfeasible(bool branch) {
439520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    if (branch)
4404e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks      InFeasibleTrue = true;
441520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    else
4424e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks      InFeasibleFalse = true;
443520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  }
4441eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
445520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek  bool isFeasible(bool branch) {
446520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek    return branch ? !InFeasibleTrue : !InFeasibleFalse;
44752a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek  }
4487d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek};
449031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
450d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass IndirectGotoNodeBuilder {
451d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  CoreEngine& Eng;
4529c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *Src;
4539c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock &DispatchBlock;
4549c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *E;
4559c378f705405d37f49795d5e915989de774fe11fTed Kremenek  ExplodedNode *Pred;
456031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
457754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenekpublic:
4589c378f705405d37f49795d5e915989de774fe11fTed Kremenek  IndirectGotoNodeBuilder(ExplodedNode *pred, const CFGBlock *src,
4599c378f705405d37f49795d5e915989de774fe11fTed Kremenek                    const Expr *e, const CFGBlock *dispatch, CoreEngine* eng)
46003509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    : Eng(*eng), Src(src), DispatchBlock(*dispatch), E(e), Pred(pred) {}
461754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek
462031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  class iterator {
46303509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    CFGBlock::const_succ_iterator I;
4641eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
465d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    friend class IndirectGotoNodeBuilder;
46603509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    iterator(CFGBlock::const_succ_iterator i) : I(i) {}
467754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek  public:
4681eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4699c378f705405d37f49795d5e915989de774fe11fTed Kremenek    iterator &operator++() { ++I; return *this; }
4709c378f705405d37f49795d5e915989de774fe11fTed Kremenek    bool operator!=(const iterator &X) const { return I != X.I; }
4711eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
472ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner    const LabelDecl *getLabel() const {
473ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner      return llvm::cast<LabelStmt>((*I)->getLabel())->getDecl();
47424f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek    }
4751eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
476ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner    const CFGBlock *getBlock() const {
47724f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek      return *I;
47824f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek    }
479754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek  };
4801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
481031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator begin() { return iterator(DispatchBlock.succ_begin()); }
482031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator end() { return iterator(DispatchBlock.succ_end()); }
4831eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
48418c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek  ExplodedNode *generateNode(const iterator &I,
4858bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                             ProgramStateRef State,
486031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu                             bool isSink = false);
4871eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4889c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *getTarget() const { return E; }
489754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek
4908bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef getState() const { return Pred->State; }
4915eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek
4925eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  const LocationContext *getLocationContext() const {
4935eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek    return Pred->getLocationContext();
4945eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  }
495754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek};
4961eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
497d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass SwitchNodeBuilder {
498d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  CoreEngine& Eng;
4999c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const CFGBlock *Src;
5009c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *Condition;
5019c378f705405d37f49795d5e915989de774fe11fTed Kremenek  ExplodedNode *Pred;
502031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
503daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenekpublic:
5049c378f705405d37f49795d5e915989de774fe11fTed Kremenek  SwitchNodeBuilder(ExplodedNode *pred, const CFGBlock *src,
5059c378f705405d37f49795d5e915989de774fe11fTed Kremenek                    const Expr *condition, CoreEngine* eng)
506daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  : Eng(*eng), Src(src), Condition(condition), Pred(pred) {}
5071eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
508031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  class iterator {
50903509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    CFGBlock::const_succ_reverse_iterator I;
5101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
511d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis    friend class SwitchNodeBuilder;
51203509aea098772644bf4662dc1c88634818ceeccZhongxing Xu    iterator(CFGBlock::const_succ_reverse_iterator i) : I(i) {}
513031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu
514daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  public:
5159c378f705405d37f49795d5e915989de774fe11fTed Kremenek    iterator &operator++() { ++I; return *this; }
51634feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek    bool operator!=(const iterator &X) const { return I != X.I; }
51734feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek    bool operator==(const iterator &X) const { return I == X.I; }
5181eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5199c378f705405d37f49795d5e915989de774fe11fTed Kremenek    const CaseStmt *getCase() const {
520daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek      return llvm::cast<CaseStmt>((*I)->getLabel());
521daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek    }
5221eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5239c378f705405d37f49795d5e915989de774fe11fTed Kremenek    const CFGBlock *getBlock() const {
524daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek      return *I;
525daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek    }
526daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek  };
5271eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
528031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator begin() { return iterator(Src->succ_rbegin()+1); }
529031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu  iterator end() { return iterator(Src->succ_rend()); }
5301eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5314d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek  const SwitchStmt *getSwitch() const {
5324d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek    return llvm::cast<SwitchStmt>(Src->getTerminator());
5334d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek  }
5344d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek
53518c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek  ExplodedNode *generateCaseStmtNode(const iterator &I,
5368bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek                                     ProgramStateRef State);
5371eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5388bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ExplodedNode *generateDefaultCaseNode(ProgramStateRef State,
539031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu                                        bool isSink = false);
5401eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5419c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const Expr *getCondition() const { return Condition; }
542daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek
5438bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef getState() const { return Pred->State; }
5445eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek
5455eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  const LocationContext *getLocationContext() const {
5465eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek    return Pred->getLocationContext();
5475eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek  }
548daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek};
54911062b118476368fa5b294954713e5df97d8599fTed Kremenek
5503070e13dca5bbefa32acb80ce4a7b217a6220983Ted Kremenek} // end ento namespace
551f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek} // end clang namespace
552f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek
553f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#endif
554