From: Ted Kremenek Date: Wed, 9 Jan 2008 23:11:36 +0000 (+0000) Subject: Renamed various traits and classes. Added "Infeasible" bit to ExplodedNodeImpl X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=974c676306758c8c84f5c25e3708186557a678bd;p=clang Renamed various traits and classes. Added "Infeasible" bit to ExplodedNodeImpl so that nodes can be marked as representing an infeasible program point. This flag lets the path-sensitive solver know that no successors should be generated for such nodes. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@45788 91177308-0d34-0410-b5e6-96231b3b80d8 --- diff --git a/include/clang/Analysis/PathSensitive/ExplodedGraph.h b/include/clang/Analysis/PathSensitive/ExplodedGraph.h index 5420a6d87a..9c37039b7a 100644 --- a/include/clang/Analysis/PathSensitive/ExplodedGraph.h +++ b/include/clang/Analysis/PathSensitive/ExplodedGraph.h @@ -24,11 +24,11 @@ namespace clang { -class ReachabilityEngineImpl; +class GREngineImpl; class ExplodedGraphImpl { protected: - friend class ReachabilityEngineImpl; + friend class GREngineImpl; // Type definitions. typedef llvm::DenseMap EdgeNodeSetMap; @@ -59,9 +59,9 @@ protected: /// getNodeImpl - Retrieve the node associated with a (Location,State) /// pair, where 'State' is represented as an opaque void*. This method - /// is intended to be used only by ReachabilityEngineImpl. + /// is intended to be used only by GREngineImpl. virtual ExplodedNodeImpl* getNodeImpl(const ProgramEdge& L, void* State, - bool* IsNew) = 0; + bool* IsNew) = 0; /// addRoot - Add an untyped node to the set of roots. ExplodedNodeImpl* addRoot(ExplodedNodeImpl* V) { @@ -96,7 +96,7 @@ protected: protected: virtual ExplodedNodeImpl* getNodeImpl(const ProgramEdge& L, void* State, bool* IsNew) { - return getNode(L,ReachabilityTrait::toState(State),IsNew); + return getNode(L,GRTrait::toState(State),IsNew); } public: @@ -131,15 +131,15 @@ public: void* InsertPos = 0; StateTy::Profile(profile, State); - NodeTy* V = VSet.FindNodeOrInsertPos(profile,InsertPos); + NodeTy* V = VSet.FindNodeOrInsertPos(profile, InsertPos); if (!V) { // Allocate a new node. V = (NodeTy*) Allocator.Allocate(); - new (V) NodeTy(NodeCounter++,L,State); + new (V) NodeTy(NodeCounter++, L, State); // Insert the node into the node set and return it. - VSet.InsertNode(V,InsertPos); + VSet.InsertNode(V, InsertPos); if (IsNew) *IsNew = true; } diff --git a/include/clang/Analysis/PathSensitive/ExplodedNode.h b/include/clang/Analysis/PathSensitive/ExplodedNode.h index c8828347ff..48ba0e29bb 100644 --- a/include/clang/Analysis/PathSensitive/ExplodedNode.h +++ b/include/clang/Analysis/PathSensitive/ExplodedNode.h @@ -24,16 +24,20 @@ namespace clang { -class ReachabilityEngineImpl; +class GREngineImpl; class ExplodedNodeImpl : public llvm::FoldingSetNode { protected: - friend class ReachabilityEngineImpl; + friend class GREngineImpl; /// nodeID - A unique ID for the node. This number indicates the /// creation order of vertices, with lower numbers being created first. /// The first created node has nodeID == 0. - const unsigned nodeID; + const unsigned nodeID:30; + + /// IsInfeasible - Indicates whether the node represents an infeasible + /// program state. + unsigned IsInfeasible:1; /// Location - The program location (within a function body) associated /// with this node. The location is a 'ProgramEdge' in the CFG. @@ -57,13 +61,16 @@ protected: /// Construct a ExplodedNodeImpl with the given node ID, program edge, /// and state. explicit ExplodedNodeImpl(unsigned ID, const ProgramEdge& loc, void* state) - : nodeID(ID), Location(loc), State(state) {} + : nodeID(ID), IsInfeasible(0), Location(loc), State(state) {} /// addUntypedPredeccessor - Adds a predecessor to the current node, and /// in tandem add this node as a successor of the other node. This - /// "untyped" version is intended to be used only by ReachabilityEngineImpl; + /// "untyped" version is intended to be used only by GREngineImpl; /// normal clients should use 'addPredecessor' in ExplodedNode<>. void addUntypedPredecessor(ExplodedNodeImpl* V) { + assert (!V->isInfeasible() && + "Cannot add successors to an infeasible node."); + Preds.push_back(V); V->Succs.push_back(V); } @@ -72,18 +79,26 @@ public: /// getLocation - Returns the edge associated with the given node. const ProgramEdge& getLocation() const { return Location; } - /// getnodeID - Returns the unique ID of the node. These IDs reflect - /// the order in which vertices were generated by ReachabilityEngineImpl. - unsigned getnodeID() const { return nodeID; } + /// getNodeID - Returns the unique ID of the node. These IDs reflect + /// the order in which vertices were generated by GREngineImpl. + unsigned getNodeID() const { return nodeID; } + + /// isInfeasible - Returns true if the node represents an infeasible + /// program state. + bool isInfeasible() const { return IsInfeasible ? true : false; } + + /// markInfeasible - The node is marked as being an infeasible program + /// state. + void markInfeasible() { Infeasible = 1; } + }; template -struct ReachabilityTrait { +struct GRTrait { static inline void* toPtr(StateTy S) { return reinterpret_cast(S); - } - + } static inline StateTy toState(void* P) { return reinterpret_cast(P); } @@ -96,11 +111,11 @@ public: /// Construct a ExplodedNodeImpl with the given node ID, program edge, /// and state. explicit ExplodedNode(unsigned ID, const ProgramEdge& loc, StateTy state) - : ExplodedNodeImpl(ID,loc,ReachabilityTrait::toPtr(state)) {} + : ExplodedNodeImpl(ID,loc,GRTrait::toPtr(state)) {} /// getState - Returns the state associated with the node. inline StateTy getState() const { - return ReachabilityTrait::toState(State); + return GRTrait::toState(State); } // Profiling (for FoldingSet).