CoreEngine.h revision 5eca482fe895ea57bc82410222e6426c09e63284
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" 219b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/WorkList.h" 229b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/BlockCounter.h" 23f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#include "llvm/ADT/OwningPtr.h" 24f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek 25f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremeneknamespace clang { 260111f575b968e423dccae439e501225b8314b257Zhongxing Xu 27ca804539d908d3a0e8c72a0df5f1f571d29490bbTed Kremenekclass ProgramPointTag; 28ca804539d908d3a0e8c72a0df5f1f571d29490bbTed Kremenek 299ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento { 305a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 31a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksclass NodeBuilder; 32a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks 3324f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek//===----------------------------------------------------------------------===// 34d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis/// CoreEngine - Implements the core logic of the graph-reachability 35922059dec59c7bed235da01aff75ae522a369811Ted Kremenek/// analysis. It traverses the CFG and generates the ExplodedGraph. 36922059dec59c7bed235da01aff75ae522a369811Ted Kremenek/// Program "states" are treated as opaque void pointers. 37d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis/// The template class CoreEngine (which subclasses CoreEngine) 38922059dec59c7bed235da01aff75ae522a369811Ted Kremenek/// provides the matching component to the engine that knows the actual types 39922059dec59c7bed235da01aff75ae522a369811Ted Kremenek/// for states. Note that this engine only dispatches to transfer functions 40922059dec59c7bed235da01aff75ae522a369811Ted Kremenek/// at the statement and block-level. The analyses themselves must implement 41922059dec59c7bed235da01aff75ae522a369811Ted Kremenek/// any transfer function logic and the sub-expression level (if any). 42d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass CoreEngine { 43ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks friend struct NodeBuilderContext; 44f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks friend class NodeBuilder; 45ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks friend class CommonNodeBuilder; 46d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis friend class IndirectGotoNodeBuilder; 47d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis friend class SwitchNodeBuilder; 48e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek friend class EndOfFunctionNodeBuilder; 49d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis friend class CallEnterNodeBuilder; 50d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis friend class CallExitNodeBuilder; 510111f575b968e423dccae439e501225b8314b257Zhongxing Xu 52a7a8a450d908b34fa5f569f2e694ebd4b61aae2fTom Carepublic: 53a7a8a450d908b34fa5f569f2e694ebd4b61aae2fTom Care typedef std::vector<std::pair<BlockEdge, const ExplodedNode*> > 5466750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek BlocksExhausted; 55422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek 56422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek typedef std::vector<std::pair<const CFGBlock*, const ExplodedNode*> > 57422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksAborted; 58422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek 59a7a8a450d908b34fa5f569f2e694ebd4b61aae2fTom Careprivate: 60a7a8a450d908b34fa5f569f2e694ebd4b61aae2fTom Care 61d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis SubEngine& SubEng; 620111f575b968e423dccae439e501225b8314b257Zhongxing Xu 63f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek /// G - The simulation graph. Each node is a (location,state) pair. 6438b02b912e1a55c912f603c4369431264d36a381Zhongxing Xu llvm::OwningPtr<ExplodedGraph> G; 651eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 66f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek /// WList - A set of queued nodes that need to be processed by the 67f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek /// worklist algorithm. It is up to the implementation of WList to decide 68f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek /// the order that nodes are processed. 69d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis WorkList* WList; 701eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 71d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis /// BCounterFactory - A factory object for created BlockCounter objects. 728e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek /// These are used to record for key nodes in the ExplodedGraph the 738e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek /// number of times different CFGBlocks have been visited along a path. 74d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis BlockCounter::Factory BCounterFactory; 75f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek 76f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek /// The locations where we stopped doing work because we visited a location 77f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek /// too many times. 7866750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek BlocksExhausted blocksExhausted; 79422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek 80422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek /// The locations where we stopped because the engine aborted analysis, 81422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek /// usually because it could not reason about something. 82422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksAborted blocksAborted; 831eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 8418c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek void generateNode(const ProgramPoint &Loc, 8518c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const ProgramState *State, 869c378f705405d37f49795d5e915989de774fe11fTed Kremenek ExplodedNode *Pred); 871eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 889c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandleBlockEdge(const BlockEdge &E, ExplodedNode *Pred); 899c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandleBlockEntrance(const BlockEntrance &E, ExplodedNode *Pred); 909c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandleBlockExit(const CFGBlock *B, ExplodedNode *Pred); 919c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandlePostStmt(const CFGBlock *B, unsigned StmtIdx, ExplodedNode *Pred); 921eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 939c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandleBranch(const Stmt *Cond, const Stmt *Term, const CFGBlock *B, 949c378f705405d37f49795d5e915989de774fe11fTed Kremenek ExplodedNode *Pred); 95102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor void HandleCallEnter(const CallEnter &L, const CFGBlock *Block, 96102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor unsigned Index, ExplodedNode *Pred); 97102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor void HandleCallExit(const CallExit &L, ExplodedNode *Pred); 980111f575b968e423dccae439e501225b8314b257Zhongxing Xu 99f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenekprivate: 100d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine(const CoreEngine&); // Do not implement. 101d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine& operator=(const CoreEngine&); 1021eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 103dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks void enqueueStmtNode(ExplodedNode *N, 104dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks const CFGBlock *Block, unsigned Idx); 105dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks 1064d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks ExplodedNode *generateCallExitNode(ExplodedNode *N); 1074d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks 108f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenekpublic: 109d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis /// Construct a CoreEngine object to analyze the provided CFG using 1100111f575b968e423dccae439e501225b8314b257Zhongxing Xu /// a DFS exploration of the exploded graph. 111d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine(SubEngine& subengine) 112d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis : SubEng(subengine), G(new ExplodedGraph()), 11355825aa2d88fe82bf3622f195046ae48532d3106Ted Kremenek WList(WorkList::makeBFS()), 114f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek BCounterFactory(G->getAllocator()) {} 1150111f575b968e423dccae439e501225b8314b257Zhongxing Xu 116d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis /// Construct a CoreEngine object to analyze the provided CFG and to 1170111f575b968e423dccae439e501225b8314b257Zhongxing Xu /// use the provided worklist object to execute the worklist algorithm. 118d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis /// The CoreEngine object assumes ownership of 'wlist'. 119d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine(WorkList* wlist, SubEngine& subengine) 120d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis : SubEng(subengine), G(new ExplodedGraph()), WList(wlist), 121f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek BCounterFactory(G->getAllocator()) {} 1220111f575b968e423dccae439e501225b8314b257Zhongxing Xu 123d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis ~CoreEngine() { 1240111f575b968e423dccae439e501225b8314b257Zhongxing Xu delete WList; 1250111f575b968e423dccae439e501225b8314b257Zhongxing Xu } 1260111f575b968e423dccae439e501225b8314b257Zhongxing Xu 1270111f575b968e423dccae439e501225b8314b257Zhongxing Xu /// getGraph - Returns the exploded graph. 128031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu ExplodedGraph& getGraph() { return *G.get(); } 1291eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1300111f575b968e423dccae439e501225b8314b257Zhongxing Xu /// takeGraph - Returns the exploded graph. Ownership of the graph is 131fc8f0e14ad142ed811e90fbd9a30e419e301c717Chris Lattner /// transferred to the caller. 132031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu ExplodedGraph* takeGraph() { return G.take(); } 1330111f575b968e423dccae439e501225b8314b257Zhongxing Xu 134f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek /// ExecuteWorkList - Run the worklist algorithm for a maximum number of 135f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek /// steps. Returns true if there is still simulation state on the worklist. 1362ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu bool ExecuteWorkList(const LocationContext *L, unsigned Steps, 13718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const ProgramState *InitState); 13818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek void ExecuteWorkListWithInitialState(const LocationContext *L, 13918c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek unsigned Steps, 14018c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const ProgramState *InitState, 1412ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu ExplodedNodeSet &Dst); 142bc42c533e7d3d946704a49e242939dd232f33072Tom Care 143bc42c533e7d3d946704a49e242939dd232f33072Tom Care // Functions for external checking of whether we have unfinished work 144422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek bool wasBlockAborted() const { return !blocksAborted.empty(); } 145422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek bool wasBlocksExhausted() const { return !blocksExhausted.empty(); } 146422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek bool hasWorkRemaining() const { return wasBlocksExhausted() || 147422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek WList->hasWork() || 148422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek wasBlockAborted(); } 149422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek 150422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek /// Inform the CoreEngine that a basic block was aborted because 151422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek /// it could not be completely analyzed. 152422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek void addAbortedBlock(const ExplodedNode *node, const CFGBlock *block) { 153422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek blocksAborted.push_back(std::make_pair(block, node)); 154422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek } 155422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek 156d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis WorkList *getWorkList() const { return WList; } 157f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek 158422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksExhausted::const_iterator blocks_exhausted_begin() const { 15966750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek return blocksExhausted.begin(); 160f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek } 161422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksExhausted::const_iterator blocks_exhausted_end() const { 16266750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek return blocksExhausted.end(); 163f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek } 164422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksAborted::const_iterator blocks_aborted_begin() const { 165422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek return blocksAborted.begin(); 166422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek } 167422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksAborted::const_iterator blocks_aborted_end() const { 168422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek return blocksAborted.end(); 169422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek } 170a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks 171dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks /// \brief Enqueue the given set of nodes onto the work list. 1724d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks void enqueue(ExplodedNodeSet &Set); 173dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks 174dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks /// \brief Enqueue nodes that were created as a result of processing 175dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks /// a statement onto the work list. 176dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks void enqueue(ExplodedNodeSet &Set, const CFGBlock *Block, unsigned Idx); 1774d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks 1784d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks /// \brief enqueue the nodes corresponding to the end of function onto the 1794d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks /// end of path / work list. 1804d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks void enqueueEndOfFunction(ExplodedNodeSet &Set); 181a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks}; 182a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks 183c03a39e16762627b421247b12a2658be630a3300Anna Zaks// TODO: Turn into a calss. 184a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksstruct NodeBuilderContext { 185a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks CoreEngine &Eng; 186a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks const CFGBlock *Block; 187af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks ExplodedNode *Pred; 188c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks NodeBuilderContext(CoreEngine &E, const CFGBlock *B, ExplodedNode *N) 189af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks : Eng(E), Block(B), Pred(N) { assert(B); assert(!N->isSink()); } 190ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks 191c03a39e16762627b421247b12a2658be630a3300Anna Zaks ExplodedNode *getPred() const { return Pred; } 192c03a39e16762627b421247b12a2658be630a3300Anna Zaks 193ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks /// \brief Return the CFGBlock associated with this builder. 194ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks const CFGBlock *getBlock() const { return Block; } 195ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks 196ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks /// \brief Returns the number of times the current basic block has been 197ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks /// visited on the exploded graph path. 198ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks unsigned getCurrentBlockCount() const { 199ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks return Eng.WList->getBlockCounter().getNumVisited( 200af498a28797c075c48d7e943df5f5a8e78ed8eb0Anna Zaks Pred->getLocationContext()->getCurrentStackFrame(), 201ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks Block->getBlockID()); 202ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks } 203f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek}; 2041eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 205aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \class NodeBuilder 206aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \brief This is the simplest builder which generates nodes in the 207aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// ExplodedGraph. 208aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// 209aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// The main benefit of the builder is that it automatically tracks the 210aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// frontier nodes (or destination set). This is the set of nodes which should 211aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// be propagated to the next step / builder. They are the nodes which have been 212aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// added to the builder (either as the input node set or as the newly 213aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// constructed nodes) but did not have any outgoing transitions added. 214f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaksclass NodeBuilder { 21599ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie virtual void anchor(); 216a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksprotected: 217cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks const NodeBuilderContext &C; 218319a9184d5ca9f77622b45ae15c08f6b9ce01621Anna Zaks 2193152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks /// Specifies if the builder results have been finalized. For example, if it 2203152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks /// is set to false, autotransitions are yet to be generated. 221f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks bool Finalized; 2224e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks bool HasGeneratedNodes; 223f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// \brief The frontier set - a set of nodes which need to be propagated after 224f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// the builder dies. 2251aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks ExplodedNodeSet &Frontier; 22671fdf469a3b6d7d557b0bfba36e8659f4966c565Anna Zaks 2273152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks /// Checkes if the results are ready. 2283152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks virtual bool checkResults() { 229a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks if (!Finalized) 230a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks return false; 231a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks return true; 232a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks } 233f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 234aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks bool hasNoSinksInFrontier() { 2358ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks for (iterator I = Frontier.begin(), E = Frontier.end(); I != E; ++I) { 2368ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks if ((*I)->isSink()) 2378ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks return false; 2388ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks } 2398ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks return true; 2408ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks } 2418ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks 2423152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks /// Allow subclasses to finalize results before result_begin() is executed. 2433152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks virtual void finalizeResults() {} 244f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 245f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks ExplodedNode *generateNodeImpl(const ProgramPoint &PP, 246f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks const ProgramState *State, 247f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks ExplodedNode *Pred, 248f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks bool MarkAsSink = false); 249f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 250f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zakspublic: 2511aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks NodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet, 2521aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &Ctx, bool F = true) 2531aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks : C(Ctx), Finalized(F), HasGeneratedNodes(false), Frontier(DstSet) { 2548ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks Frontier.Add(SrcNode); 255ad62deeb70e97da6bd514dd390ea1ce6af6ad81dAnna Zaks } 256a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks 2571aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks NodeBuilder(const ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet, 2581aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &Ctx, bool F = true) 2591aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks : C(Ctx), Finalized(F), HasGeneratedNodes(false), Frontier(DstSet) { 2601aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks Frontier.insert(SrcSet); 261aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks assert(hasNoSinksInFrontier()); 262cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks } 263cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks 264a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks virtual ~NodeBuilder() {} 265f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 266f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// \brief Generates a node in the ExplodedGraph. 267f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// 268f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// When a node is marked as sink, the exploration from the node is stopped - 269f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// the node becomes the last node on the path. 270f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks ExplodedNode *generateNode(const ProgramPoint &PP, 271f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks const ProgramState *State, 272f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks ExplodedNode *Pred, 273f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks bool MarkAsSink = false) { 274f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks return generateNodeImpl(PP, State, Pred, MarkAsSink); 275f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks } 276f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 2771aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const ExplodedNodeSet &getResults() { 2781aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks finalizeResults(); 2791aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks assert(checkResults()); 2801aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks return Frontier; 2811aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks } 2821aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks 2831aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks typedef ExplodedNodeSet::iterator iterator; 284f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// \brief Iterators through the results frontier. 2851aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks inline iterator begin() { 286a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks finalizeResults(); 287a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks assert(checkResults()); 2881aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks return Frontier.begin(); 289a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks } 2901aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks inline iterator end() { 291a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks finalizeResults(); 2921aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks return Frontier.end(); 293a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks } 294f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 2951aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &getContext() { return C; } 296aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks bool hasGeneratedNodes() { return HasGeneratedNodes; } 2971aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks 298d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks void takeNodes(const ExplodedNodeSet &S) { 299d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks for (ExplodedNodeSet::iterator I = S.begin(), E = S.end(); I != E; ++I ) 300d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks Frontier.erase(*I); 301d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks } 302aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks void takeNodes(ExplodedNode *N) { Frontier.erase(N); } 303aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks void addNodes(const ExplodedNodeSet &S) { Frontier.insert(S); } 304aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks void addNodes(ExplodedNode *N) { Frontier.Add(N); } 305f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks}; 306f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 307c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \class NodeBuilderWithSinks 308c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \brief This node builder keeps track of the generated sink nodes. 309c03a39e16762627b421247b12a2658be630a3300Anna Zaksclass NodeBuilderWithSinks: public NodeBuilder { 31099ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie virtual void anchor(); 311c03a39e16762627b421247b12a2658be630a3300Anna Zaksprotected: 312c03a39e16762627b421247b12a2658be630a3300Anna Zaks SmallVector<ExplodedNode*, 2> sinksGenerated; 313c03a39e16762627b421247b12a2658be630a3300Anna Zaks ProgramPoint &Location; 314c03a39e16762627b421247b12a2658be630a3300Anna Zaks 315c03a39e16762627b421247b12a2658be630a3300Anna Zakspublic: 316c03a39e16762627b421247b12a2658be630a3300Anna Zaks NodeBuilderWithSinks(ExplodedNode *Pred, ExplodedNodeSet &DstSet, 317c03a39e16762627b421247b12a2658be630a3300Anna Zaks const NodeBuilderContext &Ctx, ProgramPoint &L) 318c03a39e16762627b421247b12a2658be630a3300Anna Zaks : NodeBuilder(Pred, DstSet, Ctx), Location(L) {} 319c03a39e16762627b421247b12a2658be630a3300Anna Zaks ExplodedNode *generateNode(const ProgramState *State, 320c03a39e16762627b421247b12a2658be630a3300Anna Zaks ExplodedNode *Pred, 321c03a39e16762627b421247b12a2658be630a3300Anna Zaks const ProgramPointTag *Tag = 0, 322c03a39e16762627b421247b12a2658be630a3300Anna Zaks bool MarkAsSink = false) { 323c03a39e16762627b421247b12a2658be630a3300Anna Zaks ProgramPoint LocalLoc = (Tag ? Location.withTag(Tag): Location); 324c03a39e16762627b421247b12a2658be630a3300Anna Zaks 325c03a39e16762627b421247b12a2658be630a3300Anna Zaks ExplodedNode *N = generateNodeImpl(LocalLoc, State, Pred, MarkAsSink); 326c03a39e16762627b421247b12a2658be630a3300Anna Zaks if (N && N->isSink()) 327c03a39e16762627b421247b12a2658be630a3300Anna Zaks sinksGenerated.push_back(N); 328c03a39e16762627b421247b12a2658be630a3300Anna Zaks return N; 329c03a39e16762627b421247b12a2658be630a3300Anna Zaks } 330c03a39e16762627b421247b12a2658be630a3300Anna Zaks 331c03a39e16762627b421247b12a2658be630a3300Anna Zaks const SmallVectorImpl<ExplodedNode*> &getSinks() const { 332c03a39e16762627b421247b12a2658be630a3300Anna Zaks return sinksGenerated; 333c03a39e16762627b421247b12a2658be630a3300Anna Zaks } 334c03a39e16762627b421247b12a2658be630a3300Anna Zaks}; 335c03a39e16762627b421247b12a2658be630a3300Anna Zaks 336aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \class StmtNodeBuilder 337aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \brief This builder class is useful for generating nodes that resulted from 338aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// visiting a statement. The main difference from it's parent NodeBuilder is 339aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// that it creates a statement specific ProgramPoint. 340aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaksclass StmtNodeBuilder: public NodeBuilder { 341ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks NodeBuilder *EnclosingBldr; 3428ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zakspublic: 343aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks 344aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks /// \brief Constructs a StmtNodeBuilder. If the builder is going to process 345aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks /// nodes currently owned by another builder(with larger scope), use 346aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks /// Enclosing builder to transfer ownership. 347aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks StmtNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet, 348ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0) 349ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks : NodeBuilder(SrcNode, DstSet, Ctx), EnclosingBldr(Enclosing) { 350ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks if (EnclosingBldr) 351ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks EnclosingBldr->takeNodes(SrcNode); 352ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks } 3538ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks 354aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks StmtNodeBuilder(ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet, 355ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0) 356ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks : NodeBuilder(SrcSet, DstSet, Ctx), EnclosingBldr(Enclosing) { 357ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks if (EnclosingBldr) 358ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks for (ExplodedNodeSet::iterator I = SrcSet.begin(), 359ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks E = SrcSet.end(); I != E; ++I ) 360ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks EnclosingBldr->takeNodes(*I); 361ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks } 362ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks 363aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks virtual ~StmtNodeBuilder(); 3646b6152ba96c164a292cc0b8d8b1d4cecbec27a60Anna Zaks 3658ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks ExplodedNode *generateNode(const Stmt *S, 3668ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks ExplodedNode *Pred, 3678ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks const ProgramState *St, 3688ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks bool MarkAsSink = false, 3698ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks const ProgramPointTag *tag = 0, 370aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks ProgramPoint::Kind K = ProgramPoint::PostStmtKind){ 3718ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks const ProgramPoint &L = ProgramPoint::getProgramPoint(S, K, 3728ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks Pred->getLocationContext(), tag); 3738ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks return generateNodeImpl(L, St, Pred, MarkAsSink); 3748ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks } 375ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks 376ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks ExplodedNode *generateNode(const ProgramPoint &PP, 377ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks ExplodedNode *Pred, 378ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks const ProgramState *State, 379ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks bool MarkAsSink = false) { 380ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks return generateNodeImpl(PP, State, Pred, MarkAsSink); 381ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks } 3828ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks}; 3838ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks 384cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// \brief BranchNodeBuilder is responsible for constructing the nodes 385cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// corresponding to the two branches of the if statement - true and false. 386a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksclass BranchNodeBuilder: public NodeBuilder { 38799ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie virtual void anchor(); 3889c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *DstT; 3899c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *DstF; 39052a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek 391520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek bool InFeasibleTrue; 392520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek bool InFeasibleFalse; 3931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3947d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenekpublic: 3951aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks BranchNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet, 3961aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &C, 397ad62deeb70e97da6bd514dd390ea1ce6af6ad81dAnna Zaks const CFGBlock *dstT, const CFGBlock *dstF) 3981aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks : NodeBuilder(SrcNode, DstSet, C), DstT(dstT), DstF(dstF), 399cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) { 4002d950b15b2b2b650b102ecf0c6b50b45e0cb6a8aAnna Zaks // The branch node builder does not generate autotransitions. 401cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks // If there are no successors it means that both branches are infeasible. 402cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks takeNodes(SrcNode); 403cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks } 404031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 4051aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks BranchNodeBuilder(const ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet, 4061aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &C, 4071aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const CFGBlock *dstT, const CFGBlock *dstF) 4081aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks : NodeBuilder(SrcSet, DstSet, C), DstT(dstT), DstF(dstF), 409cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) { 410cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks takeNodes(SrcSet); 411cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks } 4128083414ee7cc8f5c807ed6a4e120fb4e0ab50ff8Ted Kremenek 413a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks ExplodedNode *generateNode(const ProgramState *State, bool branch, 414c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks ExplodedNode *Pred); 4151eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4169c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *getTargetBlock(bool branch) const { 4178e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek return branch ? DstT : DstF; 4181eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 4191eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 42052a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek void markInfeasible(bool branch) { 421520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek if (branch) 4224e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks InFeasibleTrue = true; 423520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek else 4244e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks InFeasibleFalse = true; 425520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek } 4261eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 427520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek bool isFeasible(bool branch) { 428520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek return branch ? !InFeasibleTrue : !InFeasibleFalse; 42952a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek } 4307d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek}; 431031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 432d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass IndirectGotoNodeBuilder { 433d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine& Eng; 4349c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *Src; 4359c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock &DispatchBlock; 4369c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *E; 4379c378f705405d37f49795d5e915989de774fe11fTed Kremenek ExplodedNode *Pred; 438031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 439754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenekpublic: 4409c378f705405d37f49795d5e915989de774fe11fTed Kremenek IndirectGotoNodeBuilder(ExplodedNode *pred, const CFGBlock *src, 4419c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *e, const CFGBlock *dispatch, CoreEngine* eng) 44203509aea098772644bf4662dc1c88634818ceeccZhongxing Xu : Eng(*eng), Src(src), DispatchBlock(*dispatch), E(e), Pred(pred) {} 443754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek 444031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu class iterator { 44503509aea098772644bf4662dc1c88634818ceeccZhongxing Xu CFGBlock::const_succ_iterator I; 4461eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 447d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis friend class IndirectGotoNodeBuilder; 44803509aea098772644bf4662dc1c88634818ceeccZhongxing Xu iterator(CFGBlock::const_succ_iterator i) : I(i) {} 449754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek public: 4501eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4519c378f705405d37f49795d5e915989de774fe11fTed Kremenek iterator &operator++() { ++I; return *this; } 4529c378f705405d37f49795d5e915989de774fe11fTed Kremenek bool operator!=(const iterator &X) const { return I != X.I; } 4531eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 454ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner const LabelDecl *getLabel() const { 455ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner return llvm::cast<LabelStmt>((*I)->getLabel())->getDecl(); 45624f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek } 4571eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 458ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner const CFGBlock *getBlock() const { 45924f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek return *I; 46024f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek } 461754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek }; 4621eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 463031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu iterator begin() { return iterator(DispatchBlock.succ_begin()); } 464031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu iterator end() { return iterator(DispatchBlock.succ_end()); } 4651eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 46618c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek ExplodedNode *generateNode(const iterator &I, 46718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const ProgramState *State, 468031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu bool isSink = false); 4691eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4709c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *getTarget() const { return E; } 471754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek 47218c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const ProgramState *getState() const { return Pred->State; } 4735eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek 4745eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek const LocationContext *getLocationContext() const { 4755eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek return Pred->getLocationContext(); 4765eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek } 477754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek}; 4781eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 479d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass SwitchNodeBuilder { 480d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine& Eng; 4819c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *Src; 4829c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *Condition; 4839c378f705405d37f49795d5e915989de774fe11fTed Kremenek ExplodedNode *Pred; 484031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 485daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenekpublic: 4869c378f705405d37f49795d5e915989de774fe11fTed Kremenek SwitchNodeBuilder(ExplodedNode *pred, const CFGBlock *src, 4879c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *condition, CoreEngine* eng) 488daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek : Eng(*eng), Src(src), Condition(condition), Pred(pred) {} 4891eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 490031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu class iterator { 49103509aea098772644bf4662dc1c88634818ceeccZhongxing Xu CFGBlock::const_succ_reverse_iterator I; 4921eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 493d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis friend class SwitchNodeBuilder; 49403509aea098772644bf4662dc1c88634818ceeccZhongxing Xu iterator(CFGBlock::const_succ_reverse_iterator i) : I(i) {} 495031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 496daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek public: 4979c378f705405d37f49795d5e915989de774fe11fTed Kremenek iterator &operator++() { ++I; return *this; } 49834feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek bool operator!=(const iterator &X) const { return I != X.I; } 49934feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek bool operator==(const iterator &X) const { return I == X.I; } 5001eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5019c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CaseStmt *getCase() const { 502daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek return llvm::cast<CaseStmt>((*I)->getLabel()); 503daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek } 5041eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5059c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *getBlock() const { 506daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek return *I; 507daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek } 508daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek }; 5091eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 510031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu iterator begin() { return iterator(Src->succ_rbegin()+1); } 511031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu iterator end() { return iterator(Src->succ_rend()); } 5121eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5134d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek const SwitchStmt *getSwitch() const { 5144d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek return llvm::cast<SwitchStmt>(Src->getTerminator()); 5154d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek } 5164d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek 51718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek ExplodedNode *generateCaseStmtNode(const iterator &I, 51818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const ProgramState *State); 5191eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 52018c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek ExplodedNode *generateDefaultCaseNode(const ProgramState *State, 521031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu bool isSink = false); 5221eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5239c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *getCondition() const { return Condition; } 524daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek 52518c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const ProgramState *getState() const { return Pred->State; } 5265eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek 5275eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek const LocationContext *getLocationContext() const { 5285eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek return Pred->getLocationContext(); 5295eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek } 530daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek}; 53111062b118476368fa5b294954713e5df97d8599fTed Kremenek 532d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass CallEnterNodeBuilder { 533d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine &Eng; 534102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 535102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor const ExplodedNode *Pred; 536102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 53719b78d9e3dbbc27bbcbdd8c3017a00fe88849ecdZhongxing Xu // The call site. For implicit automatic object dtor, this is the trigger 53819b78d9e3dbbc27bbcbdd8c3017a00fe88849ecdZhongxing Xu // statement. 539102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor const Stmt *CE; 540102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 54119b78d9e3dbbc27bbcbdd8c3017a00fe88849ecdZhongxing Xu // The context of the callee. 54219b78d9e3dbbc27bbcbdd8c3017a00fe88849ecdZhongxing Xu const StackFrameContext *CalleeCtx; 543102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 544102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor // The parent block of the CallExpr. 545102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor const CFGBlock *Block; 546102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 547102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor // The CFGBlock index of the CallExpr. 548102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor unsigned Index; 549102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 550102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregorpublic: 551d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CallEnterNodeBuilder(CoreEngine &eng, const ExplodedNode *pred, 55219b78d9e3dbbc27bbcbdd8c3017a00fe88849ecdZhongxing Xu const Stmt *s, const StackFrameContext *callee, 553102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor const CFGBlock *blk, unsigned idx) 554c6238d2786cfd961b94580b3d3675a1b3ff0721cZhongxing Xu : Eng(eng), Pred(pred), CE(s), CalleeCtx(callee), Block(blk), Index(idx) {} 555102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 55618c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const ProgramState *getState() const { return Pred->getState(); } 557102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 558102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor const LocationContext *getLocationContext() const { 559102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor return Pred->getLocationContext(); 560102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor } 561102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 562102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor const Stmt *getCallExpr() const { return CE; } 563102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 56419b78d9e3dbbc27bbcbdd8c3017a00fe88849ecdZhongxing Xu const StackFrameContext *getCalleeContext() const { return CalleeCtx; } 565102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 566102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor const CFGBlock *getBlock() const { return Block; } 567102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 568102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor unsigned getIndex() const { return Index; } 569102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 57018c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek void generateNode(const ProgramState *state); 571102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor}; 572102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 573d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass CallExitNodeBuilder { 574d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine &Eng; 575102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor const ExplodedNode *Pred; 576102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 577102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregorpublic: 578d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CallExitNodeBuilder(CoreEngine &eng, const ExplodedNode *pred) 579102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor : Eng(eng), Pred(pred) {} 580102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 581102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor const ExplodedNode *getPredecessor() const { return Pred; } 582102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 58318c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const ProgramState *getState() const { return Pred->getState(); } 584102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor 58518c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek void generateNode(const ProgramState *state); 586102acd5369bbb17c0d6ab868af376671acff7a93Douglas Gregor}; 5875a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 5885a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end GR namespace 5895a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 590f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek} // end clang namespace 591f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek 592f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#endif 593