[cfe-commits] r54722 - in /cfe/trunk: include/clang/Analysis/PathSensitive/GRState.h include/clang/Analysis/PathSensitive/ValueState.h lib/Analysis/GRState.cpp lib/Analysis/ValueState.cpp
Ted Kremenek
kremenek at apple.com
Tue Aug 12 21:28:02 PDT 2008
Author: kremenek
Date: Tue Aug 12 23:28:02 2008
New Revision: 54722
URL: http://llvm.org/viewvc/llvm-project?rev=54722&view=rev
Log:
Rename ValueState.h -> GRState.h
Rename ValueState.cpp -> GRState.cpp
Added:
cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h (props changed)
- copied unchanged from r54721, cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h
cfe/trunk/lib/Analysis/GRState.cpp (props changed)
- copied unchanged from r54721, cfe/trunk/lib/Analysis/ValueState.cpp
Removed:
cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h
cfe/trunk/lib/Analysis/ValueState.cpp
Propchange: cfe/trunk/include/clang/Analysis/PathSensitive/GRState.h
------------------------------------------------------------------------------
svn:mergeinfo =
Removed: cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h?rev=54721&view=auto
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h (removed)
@@ -1,446 +0,0 @@
-//== GRState*h - Path-Sens. "State" for tracking valuues -----*- C++ -*--==//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// This file defines SymbolID, ExprBindKey, and GRState*
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef LLVM_CLANG_ANALYSIS_VALUESTATE_H
-#define LLVM_CLANG_ANALYSIS_VALUESTATE_H
-
-// FIXME: Reduce the number of includes.
-
-#include "clang/Analysis/PathSensitive/Environment.h"
-#include "clang/Analysis/PathSensitive/Store.h"
-#include "clang/Analysis/PathSensitive/RValues.h"
-#include "clang/Analysis/PathSensitive/GRCoreEngine.h"
-#include "clang/AST/Expr.h"
-#include "clang/AST/Decl.h"
-#include "clang/AST/ASTContext.h"
-#include "clang/Analysis/Analyses/LiveVariables.h"
-
-#include "llvm/Support/Casting.h"
-#include "llvm/Support/DataTypes.h"
-#include "llvm/ADT/APSInt.h"
-#include "llvm/ADT/FoldingSet.h"
-#include "llvm/ADT/ImmutableMap.h"
-#include "llvm/ADT/SmallVector.h"
-#include "llvm/ADT/DenseSet.h"
-#include "llvm/Support/Allocator.h"
-#include "llvm/Support/Compiler.h"
-#include "llvm/Support/Streams.h"
-
-#include <functional>
-
-namespace clang {
-
-class GRStateManager;
-class GRTransferFuncs;
-
-//===----------------------------------------------------------------------===//
-// GRState- An ImmutableMap type Stmt*/Decl*/Symbols to RVals.
-//===----------------------------------------------------------------------===//
-
-/// 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.
-class GRState : public llvm::FoldingSetNode {
-public:
- // Typedefs.
- typedef llvm::ImmutableSet<llvm::APSInt*> IntSetTy;
- typedef llvm::ImmutableMap<void*, void*> GenericDataMap;
- typedef llvm::ImmutableMap<SymbolID,IntSetTy> ConstNotEqTy;
- typedef llvm::ImmutableMap<SymbolID,const llvm::APSInt*> ConstEqTy;
-
- typedef GRStateManager ManagerTy;
-
-private:
- void operator=(const GRState& R) const;
-
- friend class GRStateManager;
-
- Environment Env;
- Store St;
-
- // FIXME: Make these private.
-public:
- GenericDataMap GDM;
- ConstNotEqTy ConstNotEq;
- ConstEqTy ConstEq;
- void* CheckerState;
-
-public:
-
- /// This ctor is used when creating the first GRState object.
- GRState(const Environment& env, Store st, GenericDataMap gdm,
- ConstNotEqTy CNE, ConstEqTy CE)
- : Env(env),
- St(st),
- GDM(gdm),
- ConstNotEq(CNE),
- ConstEq(CE),
- CheckerState(NULL) {}
-
- /// Copy ctor - We must explicitly define this or else the "Next" ptr
- /// in FoldingSetNode will also get copied.
- GRState(const GRState& RHS)
- : llvm::FoldingSetNode(),
- Env(RHS.Env),
- St(RHS.St),
- GDM(RHS.GDM),
- ConstNotEq(RHS.ConstNotEq),
- ConstEq(RHS.ConstEq),
- CheckerState(RHS.CheckerState) {}
-
- /// getEnvironment - Return the environment associated with this state.
- /// The environment is the mapping from expressions to values.
- const Environment& getEnvironment() const { return Env; }
-
- /// getStore - Return the store associated with this state. The store
- /// is a mapping from locations to values.
- Store getStore() const { return St; }
-
- /// getGDM - Return the generic data map associated with this state.
- GenericDataMap getGDM() const { return GDM; }
-
- /// Profile - Profile the contents of a GRState object for use
- /// in a FoldingSet.
- static void Profile(llvm::FoldingSetNodeID& ID, const GRState* V) {
- V->Env.Profile(ID);
- ID.AddPointer(V->St);
- V->GDM.Profile(ID);
- V->ConstNotEq.Profile(ID);
- V->ConstEq.Profile(ID);
- ID.AddPointer(V->CheckerState);
- }
-
- /// Profile - Used to profile the contents of this object for inclusion
- /// in a FoldingSet.
- void Profile(llvm::FoldingSetNodeID& ID) const {
- Profile(ID, this);
- }
-
- // Queries.
-
- bool isNotEqual(SymbolID sym, const llvm::APSInt& V) const;
- bool isEqual(SymbolID sym, const llvm::APSInt& V) const;
-
- const llvm::APSInt* getSymVal(SymbolID sym) const;
-
- RVal LookupExpr(Expr* E) const {
- return Env.LookupExpr(E);
- }
-
- // Iterators.
-
-
- // FIXME: We'll be removing the VarBindings iterator very soon. Right now
- // it assumes that Store is a VarBindingsTy.
- typedef llvm::ImmutableMap<VarDecl*,RVal> VarBindingsTy;
- typedef VarBindingsTy::iterator vb_iterator;
- vb_iterator vb_begin() const {
- VarBindingsTy B(static_cast<const VarBindingsTy::TreeTy*>(St));
- return B.begin();
- }
- vb_iterator vb_end() const {
- VarBindingsTy B(static_cast<const VarBindingsTy::TreeTy*>(St));
- return B.end();
- }
-
-
- typedef Environment::seb_iterator seb_iterator;
- seb_iterator seb_begin() const { return Env.seb_begin(); }
- seb_iterator seb_end() const { return Env.beb_end(); }
-
- typedef Environment::beb_iterator beb_iterator;
- beb_iterator beb_begin() const { return Env.beb_begin(); }
- beb_iterator beb_end() const { return Env.beb_end(); }
-
- typedef ConstNotEqTy::iterator cne_iterator;
- cne_iterator cne_begin() const { return ConstNotEq.begin(); }
- cne_iterator cne_end() const { return ConstNotEq.end(); }
-
- typedef ConstEqTy::iterator ce_iterator;
- ce_iterator ce_begin() const { return ConstEq.begin(); }
- ce_iterator ce_end() const { return ConstEq.end(); }
-
- class CheckerStatePrinter {
- public:
- virtual ~CheckerStatePrinter() {}
- virtual void PrintCheckerState(std::ostream& Out, void* State,
- const char* nl, const char* sep) = 0;
- };
-
- void print(std::ostream& Out, CheckerStatePrinter* P = NULL,
- const char* nl = "\n", const char* sep = "") const;
-
- void printStdErr(CheckerStatePrinter* P = NULL) const;
-
- void printDOT(std::ostream& Out, CheckerStatePrinter*P = NULL) const;
-};
-
-template<> struct GRTrait<GRState*> {
- static inline void* toPtr(GRState* St) { return (void*) St; }
- static inline GRState* toState(void* P) { return (GRState*) P; }
- static inline void Profile(llvm::FoldingSetNodeID& profile, GRState* St) {
- // At this point states have already been uniqued. Just
- // add the pointer.
- profile.AddPointer(St);
- }
-};
-
-class GRStateSet {
- typedef llvm::SmallPtrSet<const GRState*,5> ImplTy;
- ImplTy Impl;
-public:
- GRStateSet() {}
-
- inline void Add(const GRState* St) {
- Impl.insert(St);
- }
-
- typedef ImplTy::const_iterator iterator;
-
- inline unsigned size() const { return Impl.size(); }
- inline bool empty() const { return Impl.empty(); }
-
- inline iterator begin() const { return Impl.begin(); }
- inline iterator end() const { return Impl.end(); }
-
- class AutoPopulate {
- GRStateSet& S;
- unsigned StartSize;
- const GRState* St;
- public:
- AutoPopulate(GRStateSet& s, const GRState* st)
- : S(s), StartSize(S.size()), St(st) {}
-
- ~AutoPopulate() {
- if (StartSize == S.size())
- S.Add(St);
- }
- };
-};
-
-class GRStateManager {
- friend class GRExprEngine;
-
-private:
- EnvironmentManager EnvMgr;
- llvm::OwningPtr<StoreManager> StMgr;
- GRState::IntSetTy::Factory ISetFactory;
- GRState::GenericDataMap::Factory GDMFactory;
- GRState::ConstNotEqTy::Factory CNEFactory;
- GRState::ConstEqTy::Factory CEFactory;
-
- /// StateSet - FoldingSet containing all the states created for analyzing
- /// a particular function. This is used to unique states.
- llvm::FoldingSet<GRState> StateSet;
-
- /// ValueMgr - Object that manages the data for all created RVals.
- BasicValueFactory BasicVals;
-
- /// SymMgr - Object that manages the symbol information.
- SymbolManager SymMgr;
-
- /// Alloc - A BumpPtrAllocator to allocate states.
- llvm::BumpPtrAllocator& Alloc;
-
- /// DRoots - A vector to hold of worklist used by RemoveDeadSymbols.
- /// This vector is persistent because it is reused over and over.
- StoreManager::DeclRootsTy DRoots;
-
- /// CurrentStmt - The block-level statement currently being visited. This
- /// is set by GRExprEngine.
- Stmt* CurrentStmt;
-
- /// cfg - The CFG for the analyzed function/method.
- CFG& cfg;
-
- /// TF - Object that represents a bundle of transfer functions
- /// for manipulating and creating RVals.
- GRTransferFuncs* TF;
-
-private:
-
- Environment RemoveBlkExpr(const Environment& Env, Expr* E) {
- return EnvMgr.RemoveBlkExpr(Env, E);
- }
-
- // FIXME: Remove when we do lazy initializaton of variable bindings.
- const GRState* BindVar(const GRState* St, VarDecl* D, RVal V) {
- return SetRVal(St, lval::DeclVal(D), V);
- }
-
-public:
- GRStateManager(ASTContext& Ctx, StoreManager* stmgr,
- llvm::BumpPtrAllocator& alloc, CFG& c)
- : EnvMgr(alloc),
- StMgr(stmgr),
- ISetFactory(alloc),
- GDMFactory(alloc),
- CNEFactory(alloc),
- CEFactory(alloc),
- BasicVals(Ctx, alloc),
- SymMgr(alloc),
- Alloc(alloc),
- cfg(c) {}
-
- const GRState* getInitialState();
-
- BasicValueFactory& getBasicVals() { return BasicVals; }
- const BasicValueFactory& getBasicVals() const { return BasicVals; }
- SymbolManager& getSymbolManager() { return SymMgr; }
-
- typedef StoreManager::DeadSymbolsTy DeadSymbolsTy;
-
- const GRState* RemoveDeadBindings(const GRState* St, Stmt* Loc,
- const LiveVariables& Liveness,
- DeadSymbolsTy& DeadSyms);
-
- const GRState* RemoveSubExprBindings(const GRState* St) {
- GRState NewSt = *St;
- NewSt.Env = EnvMgr.RemoveSubExprBindings(NewSt.Env);
- return getPersistentState(NewSt);
- }
-
- // Methods that query & manipulate the Environment.
-
- RVal GetRVal(const GRState* St, Expr* Ex) {
- return St->getEnvironment().GetRVal(Ex, BasicVals);
- }
-
- RVal GetBlkExprRVal(const GRState* St, Expr* Ex) {
- return St->getEnvironment().GetBlkExprRVal(Ex, BasicVals);
- }
-
- const GRState* SetRVal(const GRState* St, Expr* Ex, RVal V,
- bool isBlkExpr, bool Invalidate) {
-
- const Environment& OldEnv = St->getEnvironment();
- Environment NewEnv = EnvMgr.SetRVal(OldEnv, Ex, V, isBlkExpr, Invalidate);
-
- if (NewEnv == OldEnv)
- return St;
-
- GRState NewSt = *St;
- NewSt.Env = NewEnv;
- return getPersistentState(NewSt);
- }
-
- const GRState* SetRVal(const GRState* St, Expr* Ex, RVal V) {
-
- bool isBlkExpr = false;
-
- if (Ex == CurrentStmt) {
- isBlkExpr = cfg.isBlkExpr(Ex);
-
- if (!isBlkExpr)
- return St;
- }
-
- return SetRVal(St, Ex, V, isBlkExpr, true);
- }
-
- // Methods that manipulate the GDM.
- const GRState* addGDM(const GRState* St, void* Key, void* Data) {
- GRState::GenericDataMap M1 = St->getGDM();
- GRState::GenericDataMap M2 = GDMFactory.Add(M2, Key, Data);
-
- if (M1 == M2)
- return St;
-
- GRState NewSt = *St;
- NewSt.GDM = M2;
- return getPersistentState(NewSt);
- }
-
- // Methods that query & manipulate the Store.
- RVal GetRVal(const GRState* St, LVal LV, QualType T = QualType()) {
- return StMgr->GetRVal(St->getStore(), LV, T);
- }
-
- void SetRVal(GRState& St, LVal LV, RVal V) {
- St.St = StMgr->SetRVal(St.St, LV, V);
- }
-
- const GRState* SetRVal(const GRState* St, LVal LV, RVal V);
-
- void Unbind(GRState& St, LVal LV) {
- St.St = StMgr->Remove(St.St, LV);
- }
-
- const GRState* Unbind(const GRState* St, LVal LV);
-
- const GRState* getPersistentState(GRState& Impl);
-
- const GRState* AddEQ(const GRState* St, SymbolID sym,
- const llvm::APSInt& V);
-
- const GRState* AddNE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V);
-
- bool isEqual(const GRState* state, Expr* Ex, const llvm::APSInt& V);
- bool isEqual(const GRState* state, Expr* Ex, uint64_t);
-
- // Assumption logic.
- const GRState* Assume(const GRState* St, RVal Cond, bool Assumption,
- bool& isFeasible) {
-
- if (Cond.isUnknown()) {
- isFeasible = true;
- return St;
- }
-
- if (isa<LVal>(Cond))
- return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
- else
- return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
- }
-
- const GRState* Assume(const GRState* St, LVal Cond, bool Assumption,
- bool& isFeasible);
-
- const GRState* Assume(const GRState* St, NonLVal Cond, bool Assumption,
- bool& isFeasible);
-
-private:
- const GRState* AssumeAux(const GRState* St, LVal Cond, bool Assumption,
- bool& isFeasible);
-
-
- const GRState* AssumeAux(const GRState* St, NonLVal Cond,
- bool Assumption, bool& isFeasible);
-
- const GRState* AssumeSymInt(const GRState* St, bool Assumption,
- const SymIntConstraint& C, bool& isFeasible);
-
- const GRState* AssumeSymNE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymEQ(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymLT(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymLE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymGT(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-
- const GRState* AssumeSymGE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible);
-};
-
-} // end clang namespace
-
-#endif
Propchange: cfe/trunk/lib/Analysis/GRState.cpp
------------------------------------------------------------------------------
svn:mergeinfo =
Removed: cfe/trunk/lib/Analysis/ValueState.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/ValueState.cpp?rev=54721&view=auto
==============================================================================
--- cfe/trunk/lib/Analysis/ValueState.cpp (original)
+++ cfe/trunk/lib/Analysis/ValueState.cpp (removed)
@@ -1,575 +0,0 @@
-//= GRState*cpp - Path-Sens. "State" for tracking valuues -----*- C++ -*--=//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// This file defines SymbolID, ExprBindKey, and GRState*
-//
-//===----------------------------------------------------------------------===//
-
-#include "clang/Analysis/PathSensitive/GRState.h"
-#include "llvm/ADT/SmallSet.h"
-#include "clang/Analysis/PathSensitive/GRTransferFuncs.h"
-
-using namespace clang;
-
-bool GRState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const {
-
- // Retrieve the NE-set associated with the given symbol.
- const ConstNotEqTy::data_type* T = ConstNotEq.lookup(sym);
-
- // See if V is present in the NE-set.
- return T ? T->contains(&V) : false;
-}
-
-bool GRState::isEqual(SymbolID sym, const llvm::APSInt& V) const {
-
- // Retrieve the EQ-set associated with the given symbol.
- const ConstEqTy::data_type* T = ConstEq.lookup(sym);
-
- // See if V is present in the EQ-set.
- return T ? **T == V : false;
-}
-
-const llvm::APSInt* GRState::getSymVal(SymbolID sym) const {
- ConstEqTy::data_type* T = ConstEq.lookup(sym);
- return T ? *T : NULL;
-}
-
-const GRState*
-GRStateManager::RemoveDeadBindings(const GRState* St, Stmt* Loc,
- const LiveVariables& Liveness,
- DeadSymbolsTy& DSymbols) {
-
- // This code essentially performs a "mark-and-sweep" of the VariableBindings.
- // The roots are any Block-level exprs and Decls that our liveness algorithm
- // tells us are live. We then see what Decls they may reference, and keep
- // those around. This code more than likely can be made faster, and the
- // frequency of which this method is called should be experimented with
- // for optimum performance.
- DRoots.clear();
- StoreManager::LiveSymbolsTy LSymbols;
-
- GRState NewSt = *St;
-
- // FIXME: Put this in environment.
- // Clean up the environment.
-
- // Drop bindings for subexpressions.
- NewSt.Env = EnvMgr.RemoveSubExprBindings(NewSt.Env);
-
- // Iterate over the block-expr bindings.
-
- for (GRState::beb_iterator I = St->beb_begin(), E = St->beb_end();
- I!=E ; ++I) {
- Expr* BlkExpr = I.getKey();
-
- if (Liveness.isLive(Loc, BlkExpr)) {
- RVal X = I.getData();
-
- if (isa<lval::DeclVal>(X)) {
- lval::DeclVal LV = cast<lval::DeclVal>(X);
- DRoots.push_back(LV.getDecl());
- }
-
- for (RVal::symbol_iterator SI = X.symbol_begin(), SE = X.symbol_end();
- SI != SE; ++SI) {
- LSymbols.insert(*SI);
- }
- }
- else {
- RVal X = I.getData();
-
- if (X.isUndef() && cast<UndefinedVal>(X).getData())
- continue;
-
- NewSt.Env = EnvMgr.RemoveBlkExpr(NewSt.Env, BlkExpr);
- }
- }
-
- // Clean up the store.
- DSymbols.clear();
- NewSt.St = StMgr->RemoveDeadBindings(St->getStore(), Loc, Liveness, DRoots,
- LSymbols, DSymbols);
-
- // Remove the dead symbols from the symbol tracker.
- for (GRState::ce_iterator I = St->ce_begin(), E=St->ce_end(); I!=E; ++I) {
-
- SymbolID sym = I.getKey();
-
- if (!LSymbols.count(sym)) {
- DSymbols.insert(sym);
- NewSt.ConstEq = CEFactory.Remove(NewSt.ConstEq, sym);
- }
- }
-
- for (GRState::cne_iterator I = St->cne_begin(), E=St->cne_end(); I!=E;++I){
-
- SymbolID sym = I.getKey();
-
- if (!LSymbols.count(sym)) {
- DSymbols.insert(sym);
- NewSt.ConstNotEq = CNEFactory.Remove(NewSt.ConstNotEq, sym);
- }
- }
-
- return getPersistentState(NewSt);
-}
-
-const GRState* GRStateManager::SetRVal(const GRState* St, LVal LV,
- RVal V) {
-
- Store OldStore = St->getStore();
- Store NewStore = StMgr->SetRVal(OldStore, LV, V);
-
- if (NewStore == OldStore)
- return St;
-
- GRState NewSt = *St;
- NewSt.St = NewStore;
- return getPersistentState(NewSt);
-}
-
-const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
- Store OldStore = St->getStore();
- Store NewStore = StMgr->Remove(OldStore, LV);
-
- if (NewStore == OldStore)
- return St;
-
- GRState NewSt = *St;
- NewSt.St = NewStore;
- return getPersistentState(NewSt);
-}
-
-
-const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V) {
-
- // First, retrieve the NE-set associated with the given symbol.
- GRState::ConstNotEqTy::data_type* T = St->ConstNotEq.lookup(sym);
- GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
-
- // Now add V to the NE set.
- S = ISetFactory.Add(S, &V);
-
- // Create a new state with the old binding replaced.
- GRState NewSt = *St;
- NewSt.ConstNotEq = CNEFactory.Add(NewSt.ConstNotEq, sym, S);
-
- // Get the persistent copy.
- return getPersistentState(NewSt);
-}
-
-const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
- const llvm::APSInt& V) {
-
- // Create a new state with the old binding replaced.
- GRState NewSt = *St;
- NewSt.ConstEq = CEFactory.Add(NewSt.ConstEq, sym, &V);
-
- // Get the persistent copy.
- return getPersistentState(NewSt);
-}
-
-const GRState* GRStateManager::getInitialState() {
-
- GRState StateImpl(EnvMgr.getInitialEnvironment(),
- StMgr->getInitialStore(),
- GDMFactory.GetEmptyMap(),
- CNEFactory.GetEmptyMap(),
- CEFactory.GetEmptyMap());
-
- return getPersistentState(StateImpl);
-}
-
-const GRState* GRStateManager::getPersistentState(GRState& State) {
-
- llvm::FoldingSetNodeID ID;
- State.Profile(ID);
- void* InsertPos;
-
- if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
- return I;
-
- GRState* I = (GRState*) Alloc.Allocate<GRState>();
- new (I) GRState(State);
- StateSet.InsertNode(I, InsertPos);
- return I;
-}
-
-void GRState::printDOT(std::ostream& Out, CheckerStatePrinter* P) const {
- print(Out, P, "\\l", "\\|");
-}
-
-void GRState::printStdErr(CheckerStatePrinter* P) const {
- print(*llvm::cerr, P);
-}
-
-void GRState::print(std::ostream& Out, CheckerStatePrinter* P,
- const char* nl, const char* sep) const {
-
- // Print Variable Bindings
- Out << "Variables:" << nl;
-
- bool isFirst = true;
-
- for (vb_iterator I = vb_begin(), E = vb_end(); I != E; ++I) {
-
- if (isFirst) isFirst = false;
- else Out << nl;
-
- Out << ' ' << I.getKey()->getName() << " : ";
- I.getData().print(Out);
- }
-
- // Print Subexpression bindings.
-
- isFirst = true;
-
- for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
-
- if (isFirst) {
- Out << nl << nl << "Sub-Expressions:" << nl;
- isFirst = false;
- }
- else { Out << nl; }
-
- Out << " (" << (void*) I.getKey() << ") ";
- I.getKey()->printPretty(Out);
- Out << " : ";
- I.getData().print(Out);
- }
-
- // Print block-expression bindings.
-
- isFirst = true;
-
- for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
-
- if (isFirst) {
- Out << nl << nl << "Block-level Expressions:" << nl;
- isFirst = false;
- }
- else { Out << nl; }
-
- Out << " (" << (void*) I.getKey() << ") ";
- I.getKey()->printPretty(Out);
- Out << " : ";
- I.getData().print(Out);
- }
-
- // Print equality constraints.
-
- if (!ConstEq.isEmpty()) {
-
- Out << nl << sep << "'==' constraints:";
-
- for (ConstEqTy::iterator I = ConstEq.begin(),
- E = ConstEq.end(); I!=E; ++I) {
-
- Out << nl << " $" << I.getKey()
- << " : " << I.getData()->toString();
- }
- }
-
- // Print != constraints.
-
- if (!ConstNotEq.isEmpty()) {
-
- Out << nl << sep << "'!=' constraints:";
-
- for (ConstNotEqTy::iterator I = ConstNotEq.begin(),
- EI = ConstNotEq.end(); I != EI; ++I) {
-
- Out << nl << " $" << I.getKey() << " : ";
- isFirst = true;
-
- IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
-
- for ( ; J != EJ; ++J) {
- if (isFirst) isFirst = false;
- else Out << ", ";
-
- Out << (*J)->toString();
- }
- }
- }
-
- // Print checker-specific data.
-
- if (P && CheckerState)
- P->PrintCheckerState(Out, CheckerState, nl, sep);
-}
-
-
-//===----------------------------------------------------------------------===//
-// Queries.
-//===----------------------------------------------------------------------===//
-
-bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
- const llvm::APSInt& Y) {
- RVal V = GetRVal(state, Ex);
-
- if (lval::ConcreteInt* X = dyn_cast<lval::ConcreteInt>(&V))
- return X->getValue() == Y;
-
- if (nonlval::ConcreteInt* X = dyn_cast<nonlval::ConcreteInt>(&V))
- return X->getValue() == Y;
-
- if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V))
- return state->isEqual(X->getSymbol(), Y);
-
- if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V))
- return state->isEqual(X->getSymbol(), Y);
-
- return false;
-}
-
-bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
- uint64_t x) {
- return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
-}
-
-//===----------------------------------------------------------------------===//
-// "Assume" logic.
-//===----------------------------------------------------------------------===//
-
-const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
- bool Assumption, bool& isFeasible) {
-
- St = AssumeAux(St, Cond, Assumption, isFeasible);
-
- return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
- : St;
-}
-
-const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
- bool Assumption, bool& isFeasible) {
-
- switch (Cond.getSubKind()) {
- default:
- assert (false && "'Assume' not implemented for this LVal.");
- return St;
-
- case lval::SymbolValKind:
- if (Assumption)
- return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
- BasicVals.getZeroWithPtrWidth(), isFeasible);
- else
- return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
- BasicVals.getZeroWithPtrWidth(), isFeasible);
-
-
- case lval::DeclValKind:
- case lval::FuncValKind:
- case lval::GotoLabelKind:
- case lval::StringLiteralValKind:
- isFeasible = Assumption;
- return St;
-
- case lval::FieldOffsetKind:
- return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
- Assumption, isFeasible);
-
- case lval::ArrayOffsetKind:
- return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
- Assumption, isFeasible);
-
- case lval::ConcreteIntKind: {
- bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
- isFeasible = b ? Assumption : !Assumption;
- return St;
- }
- }
-}
-
-const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
- bool Assumption, bool& isFeasible) {
-
- St = AssumeAux(St, Cond, Assumption, isFeasible);
-
- return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
- : St;
-}
-
-const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
- bool Assumption, bool& isFeasible) {
- switch (Cond.getSubKind()) {
- default:
- assert (false && "'Assume' not implemented for this NonLVal.");
- return St;
-
-
- case nonlval::SymbolValKind: {
- nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
- SymbolID sym = SV.getSymbol();
-
- if (Assumption)
- return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
- isFeasible);
- else
- return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
- isFeasible);
- }
-
- case nonlval::SymIntConstraintValKind:
- return
- AssumeSymInt(St, Assumption,
- cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
- isFeasible);
-
- case nonlval::ConcreteIntKind: {
- bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
- isFeasible = b ? Assumption : !Assumption;
- return St;
- }
-
- case nonlval::LValAsIntegerKind: {
- return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
- Assumption, isFeasible);
- }
- }
-}
-
-
-
-const GRState* GRStateManager::AssumeSymInt(const GRState* St,
- bool Assumption,
- const SymIntConstraint& C,
- bool& isFeasible) {
-
- switch (C.getOpcode()) {
- default:
- // No logic yet for other operators.
- isFeasible = true;
- return St;
-
- case BinaryOperator::EQ:
- if (Assumption)
- return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
- else
- return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
-
- case BinaryOperator::NE:
- if (Assumption)
- return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
- else
- return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
-
- case BinaryOperator::GE:
- if (Assumption)
- return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
- else
- return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
-
- case BinaryOperator::LE:
- if (Assumption)
- return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
- else
- return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
- }
-}
-
-//===----------------------------------------------------------------------===//
-// FIXME: This should go into a plug-in constraint engine.
-//===----------------------------------------------------------------------===//
-
-const GRState*
-GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // First, determine if sym == X, where X != V.
- if (const llvm::APSInt* X = St->getSymVal(sym)) {
- isFeasible = *X != V;
- return St;
- }
-
- // Second, determine if sym != V.
- if (St->isNotEqual(sym, V)) {
- isFeasible = true;
- return St;
- }
-
- // If we reach here, sym is not a constant and we don't know if it is != V.
- // Make that assumption.
-
- isFeasible = true;
- return AddNE(St, sym, V);
-}
-
-const GRState*
-GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // First, determine if sym == X, where X != V.
- if (const llvm::APSInt* X = St->getSymVal(sym)) {
- isFeasible = *X == V;
- return St;
- }
-
- // Second, determine if sym != V.
- if (St->isNotEqual(sym, V)) {
- isFeasible = false;
- return St;
- }
-
- // If we reach here, sym is not a constant and we don't know if it is == V.
- // Make that assumption.
-
- isFeasible = true;
- return AddEQ(St, sym, V);
-}
-
-const GRState*
-GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // FIXME: For now have assuming x < y be the same as assuming sym != V;
- return AssumeSymNE(St, sym, V, isFeasible);
-}
-
-const GRState*
-GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // FIXME: For now have assuming x > y be the same as assuming sym != V;
- return AssumeSymNE(St, sym, V, isFeasible);
-}
-
-const GRState*
-GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // FIXME: Primitive logic for now. Only reject a path if the value of
- // sym is a constant X and !(X >= V).
-
- if (const llvm::APSInt* X = St->getSymVal(sym)) {
- isFeasible = *X >= V;
- return St;
- }
-
- isFeasible = true;
- return St;
-}
-
-const GRState*
-GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
-
- // FIXME: Primitive logic for now. Only reject a path if the value of
- // sym is a constant X and !(X <= V).
-
- if (const llvm::APSInt* X = St->getSymVal(sym)) {
- isFeasible = *X <= V;
- return St;
- }
-
- isFeasible = true;
- return St;
-}
-
More information about the cfe-commits
mailing list