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());
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);
-//== GRState*h - Path-Sens. "State" for tracking valuues -----*- C++ -*--==//
+//== GRState.h - Path-sensitive "State" for tracking values -----*- C++ -*--==//
//
// The LLVM Compiler Infrastructure
//
//
//===----------------------------------------------------------------------===//
//
-// This file defines SymbolRef, ExprBindKey, and GRState*
+// This file defines SymbolRef, ExprBindKey, and GRState*.
//
//===----------------------------------------------------------------------===//
}
};
-//===----------------------------------------------------------------------===//
-// 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<llvm::APSInt*> IntSetTy;
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.
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);
// (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<const GRState*, const GRState*>
Assume(DefinedOrUnknownSVal cond) const;
//==---------------------------------------------------------------------==//
/// 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;
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:
return V->getBaseKind() == UnknownKind;
}
};
-
+
class DefinedSVal : public DefinedOrUnknownSVal {
private:
// Do not implement. We want calling these methods to be a compiler