From: Zhanyong Wan Date: Wed, 24 Nov 2010 03:33:10 +0000 (+0000) Subject: Improve comments in Clang static analyzer, based on kremenek's X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=834f9de3d3d76986d09f41725a70ba45a3e2aecd;p=clang Improve comments in Clang static analyzer, based on kremenek's explanation on how things work there. Reviewed by kremenek. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@120081 91177308-0d34-0410-b5e6-96231b3b80d8 --- diff --git a/include/clang/Checker/PathSensitive/Environment.h b/include/clang/Checker/PathSensitive/Environment.h index 3cb2611526..6340cbcdfc 100644 --- a/include/clang/Checker/PathSensitive/Environment.h +++ b/include/clang/Checker/PathSensitive/Environment.h @@ -27,7 +27,9 @@ class EnvironmentManager; class ValueManager; class LiveVariables; - +/// Environment - An immutable map from Stmts to their current +/// symbolic values (SVals). +/// class Environment { private: friend class EnvironmentManager; @@ -51,6 +53,8 @@ public: return X ? *X : UnknownVal(); } + /// GetSVal - Fetches the current binding of the expression in the + /// Environment. SVal GetSVal(const Stmt* Ex, ValueManager& ValMgr) const; /// Profile - Profile the contents of an Environment object for use diff --git a/include/clang/Checker/PathSensitive/GRExprEngine.h b/include/clang/Checker/PathSensitive/GRExprEngine.h index bb0c068057..04fce44480 100644 --- a/include/clang/Checker/PathSensitive/GRExprEngine.h +++ b/include/clang/Checker/PathSensitive/GRExprEngine.h @@ -517,6 +517,10 @@ protected: public: // FIXME: 'tag' should be removed, and a LocationContext should be used // instead. + // FIXME: Comment on the meaning of the arguments, when 'St' may not + // be the same as Pred->state, and when 'location' may not be the + // same as state->getLValue(Ex). + /// Simulate a read of the result of Ex. void EvalLoad(ExplodedNodeSet& Dst, const Expr* Ex, ExplodedNode* Pred, const GRState* St, SVal location, const void *tag = 0, QualType LoadTy = QualType()); @@ -526,7 +530,7 @@ public: void EvalStore(ExplodedNodeSet& Dst, const Expr* AssignE, const Expr* StoreE, ExplodedNode* Pred, const GRState* St, SVal TargetLV, SVal Val, const void *tag = 0); -private: +private: void EvalLoadCommon(ExplodedNodeSet& Dst, const Expr* Ex, ExplodedNode* Pred, const GRState* St, SVal location, const void *tag, QualType LoadTy); diff --git a/include/clang/Checker/PathSensitive/GRState.h b/include/clang/Checker/PathSensitive/GRState.h index 878f564491..8127649d77 100644 --- a/include/clang/Checker/PathSensitive/GRState.h +++ b/include/clang/Checker/PathSensitive/GRState.h @@ -1,4 +1,4 @@ -//== GRState*h - Path-Sens. "State" for tracking valuues -----*- C++ -*--==// +//== GRState.h - Path-sensitive "State" for tracking values -----*- C++ -*--==// // // The LLVM Compiler Infrastructure // @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// // -// This file defines SymbolRef, ExprBindKey, and GRState* +// This file defines SymbolRef, ExprBindKey, and GRState*. // //===----------------------------------------------------------------------===// @@ -52,16 +52,19 @@ template struct GRStateTrait { } }; -//===----------------------------------------------------------------------===// -// GRState- An ImmutableMap type Stmt*/Decl*/Symbols to SVals. -//===----------------------------------------------------------------------===// - class GRStateManager; -/// GRState - This class encapsulates the actual data values for -/// for a "state" in our symbolic value tracking. It is intended to be -/// used as a functional object; that is once it is created and made -/// "persistent" in a FoldingSet its values will never change. +/// GRState - This class encapsulates: +/// +/// 1. A mapping from expressions to values (Environment) +/// 2. A mapping from locations to values (Store) +/// 3. Constraints on symbolic values (GenericDataMap) +/// +/// Together these represent the "abstract state" of a program. +/// +/// GRState is intended to be used as a functional object; that is, +/// once it is created and made "persistent" in a FoldingSet, its +/// values will never change. class GRState : public llvm::FoldingSetNode { public: typedef llvm::ImmutableSet IntSetTy; @@ -73,9 +76,9 @@ private: friend class GRStateManager; GRStateManager *StateMgr; - Environment Env; - Store St; - GenericDataMap GDM; + Environment Env; // Maps a Stmt to its current SVal. + Store St; // Maps a location to its current value. + GenericDataMap GDM; // Custom data stored by a client of this class. /// makeWithStore - Return a GRState with the same values as the current /// state with the exception of using the specified Store. @@ -120,8 +123,9 @@ public: void setGDM(GenericDataMap gdm) { GDM = gdm; } - /// Profile - Profile the contents of a GRState object for use - /// in a FoldingSet. + /// Profile - Profile the contents of a GRState object for use in a + /// FoldingSet. Two GRState objects are considered equal if they + /// have the same Environment, Store, and GenericDataMap. static void Profile(llvm::FoldingSetNodeID& ID, const GRState* V) { V->Env.Profile(ID); ID.AddPointer(V->St); @@ -163,19 +167,15 @@ public: // (3) A binary value "Assumption" that indicates whether the constraint is // assumed to be true or false. // - // The output of "Assume" are two values: - // - // (a) "isFeasible" is set to true or false to indicate whether or not - // the assumption is feasible. - // - // (b) A new GRState object with the added constraints. - // - // FIXME: (a) should probably disappear since it is redundant with (b). - // (i.e., (b) could just be set to NULL). + // The output of "Assume*" is a new GRState object with the added constraints. + // If no new state is feasible, NULL is returned. // const GRState *Assume(DefinedOrUnknownSVal cond, bool assumption) const; - + + /// This method assumes both "true" and "false" for 'cond', and + /// returns both corresponding states. It's shorthand for doing + /// 'Assume' twice. std::pair Assume(DefinedOrUnknownSVal cond) const; @@ -194,9 +194,7 @@ public: //==---------------------------------------------------------------------==// /// BindCompoundLiteral - Return the state that has the bindings currently - /// in 'state' plus the bindings for the CompoundLiteral. 'R' is the region - /// for the compound literal and 'BegInit' and 'EndInit' represent an - /// array of initializer values. + /// in this state plus the bindings for the CompoundLiteral. const GRState *bindCompoundLiteral(const CompoundLiteralExpr* CL, const LocationContext *LC, SVal V) const; diff --git a/include/clang/Checker/PathSensitive/SVals.h b/include/clang/Checker/PathSensitive/SVals.h index cdb338a3f2..82a1b950b6 100644 --- a/include/clang/Checker/PathSensitive/SVals.h +++ b/include/clang/Checker/PathSensitive/SVals.h @@ -39,13 +39,26 @@ class MemRegionManager; class GRStateManager; class ValueManager; +/// SVal - This represents a symbolic expression, which can be either +/// an L-value or an R-value. +/// class SVal { public: - enum BaseKind { UndefinedKind, UnknownKind, LocKind, NonLocKind }; + enum BaseKind { + // The enumerators must be representable using 2 bits. + UndefinedKind = 0, // for subclass UndefinedVal (an uninitialized value) + UnknownKind = 1, // for subclass UnknownVal (a void value) + LocKind = 2, // for subclass Loc (an L-value) + NonLocKind = 3 // for subclass NonLoc (an R-value that's not + // an L-value) + }; enum { BaseBits = 2, BaseMask = 0x3 }; protected: const void* Data; + + /// The lowest 2 bits are a BaseKind (0 -- 3). + /// The higher bits are an unsigned "kind" value. unsigned Kind; protected: @@ -200,7 +213,7 @@ public: return V->getBaseKind() == UnknownKind; } }; - + class DefinedSVal : public DefinedOrUnknownSVal { private: // Do not implement. We want calling these methods to be a compiler diff --git a/include/clang/Checker/PathSensitive/Store.h b/include/clang/Checker/PathSensitive/Store.h index 1ead466136..8aad4ff251 100644 --- a/include/clang/Checker/PathSensitive/Store.h +++ b/include/clang/Checker/PathSensitive/Store.h @@ -22,6 +22,10 @@ namespace clang { +/// Store - This opaque type encapsulates an immutable mapping from +/// locations to values. At a high-level, it represents the symbolic +/// memory model. Different subclasses of StoreManager may choose +/// different types to represent the locations and values. typedef const void* Store; class GRState;