CoreEngine.h revision 651f13cea278ec967336033dd032faef0e9fc2ec
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" 2030a2e16f6c27f888dd11eba6bbbae1e980078fcbChandler Carruth#include "clang/StaticAnalyzer/Core/PathSensitive/BlockCounter.h" 219b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h" 22e62f048960645b79363408fdead53fec2a063c52Anna Zaks#include "clang/StaticAnalyzer/Core/PathSensitive/FunctionSummary.h" 239b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/WorkList.h" 24651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines#include <memory> 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. 63651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines std::unique_ptr<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. 68651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines std::unique_ptr<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 83e62f048960645b79363408fdead53fec2a063c52Anna Zaks /// The information about functions shared by the whole translation unit. 84e62f048960645b79363408fdead53fec2a063c52Anna Zaks /// (This data is owned by AnalysisConsumer.) 85e62f048960645b79363408fdead53fec2a063c52Anna Zaks FunctionSummariesTy *FunctionSummaries; 86e62f048960645b79363408fdead53fec2a063c52Anna Zaks 8718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek void generateNode(const ProgramPoint &Loc, 888bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef State, 899c378f705405d37f49795d5e915989de774fe11fTed Kremenek ExplodedNode *Pred); 901eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 919c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandleBlockEdge(const BlockEdge &E, ExplodedNode *Pred); 929c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandleBlockEntrance(const BlockEntrance &E, ExplodedNode *Pred); 939c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandleBlockExit(const CFGBlock *B, ExplodedNode *Pred); 949c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandlePostStmt(const CFGBlock *B, unsigned StmtIdx, ExplodedNode *Pred); 951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 969c378f705405d37f49795d5e915989de774fe11fTed Kremenek void HandleBranch(const Stmt *Cond, const Stmt *Term, const CFGBlock *B, 979c378f705405d37f49795d5e915989de774fe11fTed Kremenek ExplodedNode *Pred); 980111f575b968e423dccae439e501225b8314b257Zhongxing Xu 990f5c5c60e9806d13f0907cd99d7204ffab0e08f7Ted Kremenek /// Handle conditional logic for running static initializers. 1000f5c5c60e9806d13f0907cd99d7204ffab0e08f7Ted Kremenek void HandleStaticInit(const DeclStmt *DS, const CFGBlock *B, 1010f5c5c60e9806d13f0907cd99d7204ffab0e08f7Ted Kremenek ExplodedNode *Pred); 1020f5c5c60e9806d13f0907cd99d7204ffab0e08f7Ted Kremenek 103f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenekprivate: 104f56faa01936b9cf909623d7f06e3c2569ca4a78eDmitri Gribenko CoreEngine(const CoreEngine &) LLVM_DELETED_FUNCTION; 105f56faa01936b9cf909623d7f06e3c2569ca4a78eDmitri Gribenko void operator=(const CoreEngine &) LLVM_DELETED_FUNCTION; 1061eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1070b3ade86a1c60cf0c7b56aa238aff458eb7f5974Anna Zaks ExplodedNode *generateCallExitBeginNode(ExplodedNode *N); 1084d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks 109f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenekpublic: 1108d0f528afd9fcb9ebb8ccb4b8a529a05375b628eJordan Rose /// Construct a CoreEngine object to analyze the provided CFG. 111fbcb3f11fc90e9f00e6074e9b118b8dc11ca604cAnna Zaks CoreEngine(SubEngine& subengine, 112e62f048960645b79363408fdead53fec2a063c52Anna Zaks FunctionSummariesTy *FS) 113d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis : SubEng(subengine), G(new ExplodedGraph()), 1148d0f528afd9fcb9ebb8ccb4b8a529a05375b628eJordan Rose WList(WorkList::makeDFS()), 1153fd5f370a28552976c52e76c3035d79012d78ddaAnna Zaks BCounterFactory(G->getAllocator()), 116e62f048960645b79363408fdead53fec2a063c52Anna Zaks FunctionSummaries(FS){} 1170111f575b968e423dccae439e501225b8314b257Zhongxing Xu 1180111f575b968e423dccae439e501225b8314b257Zhongxing Xu /// getGraph - Returns the exploded graph. 119031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu ExplodedGraph& getGraph() { return *G.get(); } 1201eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1210111f575b968e423dccae439e501225b8314b257Zhongxing Xu /// takeGraph - Returns the exploded graph. Ownership of the graph is 122fc8f0e14ad142ed811e90fbd9a30e419e301c717Chris Lattner /// transferred to the caller. 123651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines ExplodedGraph *takeGraph() { return G.release(); } 1240111f575b968e423dccae439e501225b8314b257Zhongxing Xu 125f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek /// ExecuteWorkList - Run the worklist algorithm for a maximum number of 126f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek /// steps. Returns true if there is still simulation state on the worklist. 1272ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu bool ExecuteWorkList(const LocationContext *L, unsigned Steps, 1288bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef InitState); 129253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks /// Returns true if there is still simulation state on the worklist. 130253955ca25c7e7049963b5db613c0cd15d66e4f8Anna Zaks bool ExecuteWorkListWithInitialState(const LocationContext *L, 13118c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek unsigned Steps, 1328bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef InitState, 1332ce43c8f43254a9edea53a20dc0e69195bc82ae0Zhongxing Xu ExplodedNodeSet &Dst); 134bc42c533e7d3d946704a49e242939dd232f33072Tom Care 1355903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks /// Dispatch the work list item based on the given location information. 1365903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks /// Use Pred parameter as the predecessor state. 1375903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks void dispatchWorkItem(ExplodedNode* Pred, ProgramPoint Loc, 1385903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks const WorkListUnit& WU); 1395903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks 140bc42c533e7d3d946704a49e242939dd232f33072Tom Care // Functions for external checking of whether we have unfinished work 141422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek bool wasBlockAborted() const { return !blocksAborted.empty(); } 142422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek bool wasBlocksExhausted() const { return !blocksExhausted.empty(); } 143422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek bool hasWorkRemaining() const { return wasBlocksExhausted() || 144422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek WList->hasWork() || 145422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek wasBlockAborted(); } 146422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek 147422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek /// Inform the CoreEngine that a basic block was aborted because 148422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek /// it could not be completely analyzed. 149422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek void addAbortedBlock(const ExplodedNode *node, const CFGBlock *block) { 150422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek blocksAborted.push_back(std::make_pair(block, node)); 151422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek } 152422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek 1538d0f528afd9fcb9ebb8ccb4b8a529a05375b628eJordan Rose WorkList *getWorkList() const { return WList.get(); } 154f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek 155422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksExhausted::const_iterator blocks_exhausted_begin() const { 15666750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek return blocksExhausted.begin(); 157f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek } 158422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksExhausted::const_iterator blocks_exhausted_end() const { 15966750fa464ace9f8c41666c8585ec71a248c1ccaTed Kremenek return blocksExhausted.end(); 160f598087b4adfea164acdd5b53ea2951bde740a2dTed Kremenek } 161422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksAborted::const_iterator blocks_aborted_begin() const { 162422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek return blocksAborted.begin(); 163422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek } 164422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek BlocksAborted::const_iterator blocks_aborted_end() const { 165422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek return blocksAborted.end(); 166422ab7a49a9a4252dbc6350e49d7a5708337b9c7Ted Kremenek } 167a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks 168dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks /// \brief Enqueue the given set of nodes onto the work list. 1694d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks void enqueue(ExplodedNodeSet &Set); 170dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks 171dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks /// \brief Enqueue nodes that were created as a result of processing 172dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks /// a statement onto the work list. 173dd7ddf2b2296f95e7591ca3f9791f0eb9a15ee42Anna Zaks void enqueue(ExplodedNodeSet &Set, const CFGBlock *Block, unsigned Idx); 1744d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks 1754d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks /// \brief enqueue the nodes corresponding to the end of function onto the 1764d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks /// end of path / work list. 1774d2ae4a70336dc2aa11389b34946be152bb454c9Anna Zaks void enqueueEndOfFunction(ExplodedNodeSet &Set); 1785903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks 1795903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks /// \brief Enqueue a single node created as a result of statement processing. 1805903a373db3d27794c90b25687e0dd6adb0e497dAnna Zaks void enqueueStmtNode(ExplodedNode *N, const CFGBlock *Block, unsigned Idx); 181a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks}; 182a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks 183c03a39e16762627b421247b12a2658be630a3300Anna Zaks// TODO: Turn into a calss. 184a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksstruct NodeBuilderContext { 1855a878b2cabb940bf3c1ac420a52cac305765e3e2Anna Zaks const CoreEngine &Eng; 186a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks const CFGBlock *Block; 187b355be838a22a511d078504b2277f70aea52ca85Anna Zaks const LocationContext *LC; 1885a878b2cabb940bf3c1ac420a52cac305765e3e2Anna Zaks NodeBuilderContext(const CoreEngine &E, const CFGBlock *B, ExplodedNode *N) 189b355be838a22a511d078504b2277f70aea52ca85Anna Zaks : Eng(E), Block(B), LC(N->getLocationContext()) { assert(B); } 190c03a39e16762627b421247b12a2658be630a3300Anna Zaks 191ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks /// \brief Return the CFGBlock associated with this builder. 192ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks const CFGBlock *getBlock() const { return Block; } 193ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks 194ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks /// \brief Returns the number of times the current basic block has been 195ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks /// visited on the exploded graph path. 19666c486f275531df6362b3511fc3af6563561801bTed Kremenek unsigned blockCount() const { 197ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks return Eng.WList->getBlockCounter().getNumVisited( 198b355be838a22a511d078504b2277f70aea52ca85Anna Zaks LC->getCurrentStackFrame(), 199ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks Block->getBlockID()); 200ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks } 201f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek}; 2021eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 203aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \class NodeBuilder 204aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \brief This is the simplest builder which generates nodes in the 205aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// ExplodedGraph. 206aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// 207aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// The main benefit of the builder is that it automatically tracks the 208aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// frontier nodes (or destination set). This is the set of nodes which should 209aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// be propagated to the next step / builder. They are the nodes which have been 210aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// added to the builder (either as the input node set or as the newly 211aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// constructed nodes) but did not have any outgoing transitions added. 212f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaksclass NodeBuilder { 21399ba9e3bd70671f3441fb974895f226a83ce0e66David Blaikie virtual void anchor(); 214a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksprotected: 215cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks const NodeBuilderContext &C; 216319a9184d5ca9f77622b45ae15c08f6b9ce01621Anna Zaks 2173152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks /// Specifies if the builder results have been finalized. For example, if it 2183152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks /// is set to false, autotransitions are yet to be generated. 219f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks bool Finalized; 2204e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks bool HasGeneratedNodes; 221f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// \brief The frontier set - a set of nodes which need to be propagated after 222f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// the builder dies. 2231aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks ExplodedNodeSet &Frontier; 22471fdf469a3b6d7d557b0bfba36e8659f4966c565Anna Zaks 2253152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks /// Checkes if the results are ready. 2263152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks virtual bool checkResults() { 227a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks if (!Finalized) 228a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks return false; 229a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks return true; 230a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks } 231f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 232aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks bool hasNoSinksInFrontier() { 2338ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks for (iterator I = Frontier.begin(), E = Frontier.end(); I != E; ++I) { 2348ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks if ((*I)->isSink()) 2358ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks return false; 2368ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks } 2378ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks return true; 2388ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks } 2398ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks 2403152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks /// Allow subclasses to finalize results before result_begin() is executed. 2413152b3cb5b6a2f797d0972c81a5eb3fd69c0d620Anna Zaks virtual void finalizeResults() {} 242f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 243f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks ExplodedNode *generateNodeImpl(const ProgramPoint &PP, 2448bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef State, 245f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks ExplodedNode *Pred, 246f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks bool MarkAsSink = false); 247f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 248f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zakspublic: 2491aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks NodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet, 2501aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &Ctx, bool F = true) 2511aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks : C(Ctx), Finalized(F), HasGeneratedNodes(false), Frontier(DstSet) { 2528ff5c41f2bde7ebbe568b4c15e59f14b8befae66Anna Zaks Frontier.Add(SrcNode); 253ad62deeb70e97da6bd514dd390ea1ce6af6ad81dAnna Zaks } 254a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks 2551aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks NodeBuilder(const ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet, 2561aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &Ctx, bool F = true) 2571aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks : C(Ctx), Finalized(F), HasGeneratedNodes(false), Frontier(DstSet) { 2581aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks Frontier.insert(SrcSet); 259aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks assert(hasNoSinksInFrontier()); 260cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks } 261cd656cab3fa3dd4b0c974c6ae1c0e60880b18c22Anna Zaks 262a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks virtual ~NodeBuilder() {} 263f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 264f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// \brief Generates a node in the ExplodedGraph. 265fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ExplodedNode *generateNode(const ProgramPoint &PP, 266fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ProgramStateRef State, 267fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ExplodedNode *Pred) { 268fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose return generateNodeImpl(PP, State, Pred, false); 269fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose } 270fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose 271fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose /// \brief Generates a sink in the ExplodedGraph. 272f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// 273f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// When a node is marked as sink, the exploration from the node is stopped - 274fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose /// the node becomes the last node on the path and certain kinds of bugs are 275fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose /// suppressed. 276fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ExplodedNode *generateSink(const ProgramPoint &PP, 2778bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef State, 278fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ExplodedNode *Pred) { 279fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose return generateNodeImpl(PP, State, Pred, true); 280f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks } 281f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 2821aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const ExplodedNodeSet &getResults() { 2831aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks finalizeResults(); 2841aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks assert(checkResults()); 2851aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks return Frontier; 2861aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks } 2871aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks 2881aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks typedef ExplodedNodeSet::iterator iterator; 289f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks /// \brief Iterators through the results frontier. 2901aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks inline iterator begin() { 291a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks finalizeResults(); 292a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks assert(checkResults()); 2931aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks return Frontier.begin(); 294a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks } 2951aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks inline iterator end() { 296a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks finalizeResults(); 2971aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks return Frontier.end(); 298a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaks } 299f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 3001aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &getContext() { return C; } 301aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks bool hasGeneratedNodes() { return HasGeneratedNodes; } 3021aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks 303d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks void takeNodes(const ExplodedNodeSet &S) { 304d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks for (ExplodedNodeSet::iterator I = S.begin(), E = S.end(); I != E; ++I ) 305d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks Frontier.erase(*I); 306d231d0130a95336610ab9a42eaeb2cdac19992f3Anna Zaks } 307aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks void takeNodes(ExplodedNode *N) { Frontier.erase(N); } 308aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks void addNodes(const ExplodedNodeSet &S) { Frontier.insert(S); } 309aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks void addNodes(ExplodedNode *N) { Frontier.Add(N); } 310f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks}; 311f05aac8472d8ed081a361a218fd14d59ddc91b85Anna Zaks 312c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \class NodeBuilderWithSinks 313c03a39e16762627b421247b12a2658be630a3300Anna Zaks/// \brief This node builder keeps track of the generated sink nodes. 314c03a39e16762627b421247b12a2658be630a3300Anna Zaksclass NodeBuilderWithSinks: public NodeBuilder { 315651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines void anchor() override; 316c03a39e16762627b421247b12a2658be630a3300Anna Zaksprotected: 317c03a39e16762627b421247b12a2658be630a3300Anna Zaks SmallVector<ExplodedNode*, 2> sinksGenerated; 318c03a39e16762627b421247b12a2658be630a3300Anna Zaks ProgramPoint &Location; 319c03a39e16762627b421247b12a2658be630a3300Anna Zaks 320c03a39e16762627b421247b12a2658be630a3300Anna Zakspublic: 321c03a39e16762627b421247b12a2658be630a3300Anna Zaks NodeBuilderWithSinks(ExplodedNode *Pred, ExplodedNodeSet &DstSet, 322c03a39e16762627b421247b12a2658be630a3300Anna Zaks const NodeBuilderContext &Ctx, ProgramPoint &L) 323c03a39e16762627b421247b12a2658be630a3300Anna Zaks : NodeBuilder(Pred, DstSet, Ctx), Location(L) {} 324fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose 3258bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ExplodedNode *generateNode(ProgramStateRef State, 326c03a39e16762627b421247b12a2658be630a3300Anna Zaks ExplodedNode *Pred, 327fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose const ProgramPointTag *Tag = 0) { 328fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose const ProgramPoint &LocalLoc = (Tag ? Location.withTag(Tag) : Location); 329fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose return NodeBuilder::generateNode(LocalLoc, State, Pred); 330fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose } 331c03a39e16762627b421247b12a2658be630a3300Anna Zaks 332fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ExplodedNode *generateSink(ProgramStateRef State, ExplodedNode *Pred, 333fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose const ProgramPointTag *Tag = 0) { 334fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose const ProgramPoint &LocalLoc = (Tag ? Location.withTag(Tag) : Location); 335fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ExplodedNode *N = NodeBuilder::generateSink(LocalLoc, State, Pred); 336c03a39e16762627b421247b12a2658be630a3300Anna Zaks if (N && N->isSink()) 337c03a39e16762627b421247b12a2658be630a3300Anna Zaks sinksGenerated.push_back(N); 338c03a39e16762627b421247b12a2658be630a3300Anna Zaks return N; 339c03a39e16762627b421247b12a2658be630a3300Anna Zaks } 340c03a39e16762627b421247b12a2658be630a3300Anna Zaks 341c03a39e16762627b421247b12a2658be630a3300Anna Zaks const SmallVectorImpl<ExplodedNode*> &getSinks() const { 342c03a39e16762627b421247b12a2658be630a3300Anna Zaks return sinksGenerated; 343c03a39e16762627b421247b12a2658be630a3300Anna Zaks } 344c03a39e16762627b421247b12a2658be630a3300Anna Zaks}; 345c03a39e16762627b421247b12a2658be630a3300Anna Zaks 346aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \class StmtNodeBuilder 347aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// \brief This builder class is useful for generating nodes that resulted from 348fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose/// visiting a statement. The main difference from its parent NodeBuilder is 349aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks/// that it creates a statement specific ProgramPoint. 350aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaksclass StmtNodeBuilder: public NodeBuilder { 351ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks NodeBuilder *EnclosingBldr; 3528ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zakspublic: 353aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks 354aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks /// \brief Constructs a StmtNodeBuilder. If the builder is going to process 355aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks /// nodes currently owned by another builder(with larger scope), use 356aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks /// Enclosing builder to transfer ownership. 357aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks StmtNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet, 358ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0) 359ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks : NodeBuilder(SrcNode, DstSet, Ctx), EnclosingBldr(Enclosing) { 360ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks if (EnclosingBldr) 361ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks EnclosingBldr->takeNodes(SrcNode); 362ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks } 3638ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks 364aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks StmtNodeBuilder(ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet, 365ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks const NodeBuilderContext &Ctx, NodeBuilder *Enclosing = 0) 366ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks : NodeBuilder(SrcSet, DstSet, Ctx), EnclosingBldr(Enclosing) { 367ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks if (EnclosingBldr) 368ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks for (ExplodedNodeSet::iterator I = SrcSet.begin(), 369ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks E = SrcSet.end(); I != E; ++I ) 370ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks EnclosingBldr->takeNodes(*I); 371ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks } 372ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks 373aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks virtual ~StmtNodeBuilder(); 3746b6152ba96c164a292cc0b8d8b1d4cecbec27a60Anna Zaks 375fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose using NodeBuilder::generateNode; 376fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose using NodeBuilder::generateSink; 377fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose 3788ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks ExplodedNode *generateNode(const Stmt *S, 3798ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks ExplodedNode *Pred, 3808bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef St, 3818ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks const ProgramPointTag *tag = 0, 382aa0aeb1cbe117db68d35700cb3a34aace0f99b99Anna Zaks ProgramPoint::Kind K = ProgramPoint::PostStmtKind){ 3838ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks const ProgramPoint &L = ProgramPoint::getProgramPoint(S, K, 3848ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks Pred->getLocationContext(), tag); 385fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose return NodeBuilder::generateNode(L, St, Pred); 3868ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks } 387ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks 388fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ExplodedNode *generateSink(const Stmt *S, 389ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks ExplodedNode *Pred, 390fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ProgramStateRef St, 391fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose const ProgramPointTag *tag = 0, 392fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose ProgramPoint::Kind K = ProgramPoint::PostStmtKind){ 393fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose const ProgramPoint &L = ProgramPoint::getProgramPoint(S, K, 394fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose Pred->getLocationContext(), tag); 395fa06f0464a04bb7fce1fcfb3780d151bb029e00cJordan Rose return NodeBuilder::generateSink(L, St, Pred); 396ebae6d0209e1ec3d5ea14f9e63bd0d740218ed14Anna Zaks } 3978ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks}; 3988ad8c546372fe602708cb7ceeaf0ebbb866735c6Anna Zaks 399cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// \brief BranchNodeBuilder is responsible for constructing the nodes 400cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks/// corresponding to the two branches of the if statement - true and false. 401a19f4af7a94835ce4693bfe12d6270754e79eb56Anna Zaksclass BranchNodeBuilder: public NodeBuilder { 402651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines void anchor() override; 4039c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *DstT; 4049c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *DstF; 40552a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek 406520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek bool InFeasibleTrue; 407520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek bool InFeasibleFalse; 4081eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4097d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenekpublic: 4101aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks BranchNodeBuilder(ExplodedNode *SrcNode, ExplodedNodeSet &DstSet, 4111aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &C, 412ad62deeb70e97da6bd514dd390ea1ce6af6ad81dAnna Zaks const CFGBlock *dstT, const CFGBlock *dstF) 4131aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks : NodeBuilder(SrcNode, DstSet, C), DstT(dstT), DstF(dstF), 414cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) { 4152d950b15b2b2b650b102ecf0c6b50b45e0cb6a8aAnna Zaks // The branch node builder does not generate autotransitions. 416cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks // If there are no successors it means that both branches are infeasible. 417cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks takeNodes(SrcNode); 418cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks } 419031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 4201aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks BranchNodeBuilder(const ExplodedNodeSet &SrcSet, ExplodedNodeSet &DstSet, 4211aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const NodeBuilderContext &C, 4221aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks const CFGBlock *dstT, const CFGBlock *dstF) 4231aae01a8308d2f8e31adab3f4d7ac35543aac680Anna Zaks : NodeBuilder(SrcSet, DstSet, C), DstT(dstT), DstF(dstF), 424cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks InFeasibleTrue(!DstT), InFeasibleFalse(!DstF) { 425cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks takeNodes(SrcSet); 426cdcc653642d4ac9255c574fabe74a48149e06733Anna Zaks } 4278083414ee7cc8f5c807ed6a4e120fb4e0ab50ff8Ted Kremenek 4288bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ExplodedNode *generateNode(ProgramStateRef State, bool branch, 429c9003c89c7aead1686aba89c8e3ddcea1f2bec54Anna Zaks ExplodedNode *Pred); 4301eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4319c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *getTargetBlock(bool branch) const { 4328e49dd6e7e73b275a74338a5127a524f0765303cTed Kremenek return branch ? DstT : DstF; 4331eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 4341eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 43552a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek void markInfeasible(bool branch) { 436520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek if (branch) 4374e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks InFeasibleTrue = true; 438520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek else 4394e82d3cf6fd4c907265e3fa3aac0a835c35dc759Anna Zaks InFeasibleFalse = true; 440520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek } 4411eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 442520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek bool isFeasible(bool branch) { 443520035439d7133064325c4df6378c5a8f2f05539Ted Kremenek return branch ? !InFeasibleTrue : !InFeasibleFalse; 44452a16499df87730c0252b431abdf2b2e32d756a6Ted Kremenek } 4457d7fe6d539b3bdb1701835223cca306c325614a7Ted Kremenek}; 446031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 447d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass IndirectGotoNodeBuilder { 448d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine& Eng; 4499c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *Src; 4509c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock &DispatchBlock; 4519c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *E; 4529c378f705405d37f49795d5e915989de774fe11fTed Kremenek ExplodedNode *Pred; 453031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 454754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenekpublic: 4559c378f705405d37f49795d5e915989de774fe11fTed Kremenek IndirectGotoNodeBuilder(ExplodedNode *pred, const CFGBlock *src, 4569c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *e, const CFGBlock *dispatch, CoreEngine* eng) 45703509aea098772644bf4662dc1c88634818ceeccZhongxing Xu : Eng(*eng), Src(src), DispatchBlock(*dispatch), E(e), Pred(pred) {} 458754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek 459031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu class iterator { 46003509aea098772644bf4662dc1c88634818ceeccZhongxing Xu CFGBlock::const_succ_iterator I; 4611eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 462d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis friend class IndirectGotoNodeBuilder; 46303509aea098772644bf4662dc1c88634818ceeccZhongxing Xu iterator(CFGBlock::const_succ_iterator i) : I(i) {} 464754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek public: 4651eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4669c378f705405d37f49795d5e915989de774fe11fTed Kremenek iterator &operator++() { ++I; return *this; } 4679c378f705405d37f49795d5e915989de774fe11fTed Kremenek bool operator!=(const iterator &X) const { return I != X.I; } 4681eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 469ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner const LabelDecl *getLabel() const { 470cfa88f893915ceb8ae4ce2f17c46c24a4d67502fDmitri Gribenko return cast<LabelStmt>((*I)->getLabel())->getDecl(); 47124f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek } 4721eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 473ad8dcf4a9df0e24051dc31bf9e6f3cd138a34298Chris Lattner const CFGBlock *getBlock() const { 47424f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek return *I; 47524f1a967741ff9f8025ee23be12ba6feacc31f77Ted Kremenek } 476754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek }; 4771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 478031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu iterator begin() { return iterator(DispatchBlock.succ_begin()); } 479031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu iterator end() { return iterator(DispatchBlock.succ_end()); } 4801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 48118c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek ExplodedNode *generateNode(const iterator &I, 4828bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef State, 483031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu bool isSink = false); 4841eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 4859c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *getTarget() const { return E; } 486754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek 4878bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef getState() const { return Pred->State; } 4885eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek 4895eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek const LocationContext *getLocationContext() const { 4905eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek return Pred->getLocationContext(); 4915eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek } 492754607e7cff2d902d9af8b771409449fb2f8d2bfTed Kremenek}; 4931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 494d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass SwitchNodeBuilder { 495d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis CoreEngine& Eng; 4969c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *Src; 4979c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *Condition; 4989c378f705405d37f49795d5e915989de774fe11fTed Kremenek ExplodedNode *Pred; 499031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 500daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenekpublic: 5019c378f705405d37f49795d5e915989de774fe11fTed Kremenek SwitchNodeBuilder(ExplodedNode *pred, const CFGBlock *src, 5029c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *condition, CoreEngine* eng) 503daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek : Eng(*eng), Src(src), Condition(condition), Pred(pred) {} 5041eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 505031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu class iterator { 50603509aea098772644bf4662dc1c88634818ceeccZhongxing Xu CFGBlock::const_succ_reverse_iterator I; 5071eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 508d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis friend class SwitchNodeBuilder; 50903509aea098772644bf4662dc1c88634818ceeccZhongxing Xu iterator(CFGBlock::const_succ_reverse_iterator i) : I(i) {} 510031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu 511daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek public: 5129c378f705405d37f49795d5e915989de774fe11fTed Kremenek iterator &operator++() { ++I; return *this; } 51334feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek bool operator!=(const iterator &X) const { return I != X.I; } 51434feff654c6304e0a59ceb1376989d28dbc956ffTed Kremenek bool operator==(const iterator &X) const { return I == X.I; } 5151eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5169c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CaseStmt *getCase() const { 517cfa88f893915ceb8ae4ce2f17c46c24a4d67502fDmitri Gribenko return cast<CaseStmt>((*I)->getLabel()); 518daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek } 5191eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5209c378f705405d37f49795d5e915989de774fe11fTed Kremenek const CFGBlock *getBlock() const { 521daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek return *I; 522daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek } 523daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek }; 5241eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 525031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu iterator begin() { return iterator(Src->succ_rbegin()+1); } 526031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu iterator end() { return iterator(Src->succ_rend()); } 5271eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5284d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek const SwitchStmt *getSwitch() const { 529cfa88f893915ceb8ae4ce2f17c46c24a4d67502fDmitri Gribenko return cast<SwitchStmt>(Src->getTerminator()); 5304d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek } 5314d3175c1e5a44251ea97b0c81e80f060629d9c08Ted Kremenek 53218c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek ExplodedNode *generateCaseStmtNode(const iterator &I, 5338bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef State); 5341eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5358bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ExplodedNode *generateDefaultCaseNode(ProgramStateRef State, 536031ccc0555a82afc2e8afe29e19dd57ff204e2deZhongxing Xu bool isSink = false); 5371eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5389c378f705405d37f49795d5e915989de774fe11fTed Kremenek const Expr *getCondition() const { return Condition; } 539daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek 5408bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef getState() const { return Pred->State; } 5415eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek 5425eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek const LocationContext *getLocationContext() const { 5435eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek return Pred->getLocationContext(); 5445eca482fe895ea57bc82410222e6426c09e63284Ted Kremenek } 545daeb9a7376830d637e02b5bc51faf4750a7bce70Ted Kremenek}; 54611062b118476368fa5b294954713e5df97d8599fTed Kremenek 5473070e13dca5bbefa32acb80ce4a7b217a6220983Ted Kremenek} // end ento namespace 548f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek} // end clang namespace 549f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek 550f24af5bc2e01ca8e7396ed997378a77fddfa521eTed Kremenek#endif 551