From 862d5bbd90f6bdf18246f0e774d745e8c15cf31d Mon Sep 17 00:00:00 2001 From: Ted Kremenek Date: Wed, 6 Feb 2008 00:54:14 +0000 Subject: [PATCH] Added some skeleton code for performing "assume" on symbols: e.g. assume($0 != 0). This action will add constraints to the possible values of a symbol. Still needs to be debugged. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@46789 91177308-0d34-0410-b5e6-96231b3b80d8 --- Analysis/GRConstants.cpp | 69 +++++++++++++++++++++++++++++++++++++--- Analysis/RValues.h | 4 +++ Analysis/ValueState.cpp | 51 ++++++++++++++++++++++++++++- Analysis/ValueState.h | 30 ++++++++++++++--- 4 files changed, 144 insertions(+), 10 deletions(-) diff --git a/Analysis/GRConstants.cpp b/Analysis/GRConstants.cpp index d841eec801..5116499f17 100644 --- a/Analysis/GRConstants.cpp +++ b/Analysis/GRConstants.cpp @@ -228,6 +228,12 @@ public: StateTy Assume(StateTy St, LValue Cond, bool Assumption, bool& isFeasible); StateTy Assume(StateTy St, NonLValue Cond, bool Assumption, bool& isFeasible); + StateTy AssumeSymNE(StateTy St, SymbolID sym, const llvm::APSInt& V, + bool& isFeasible); + + StateTy AssumeSymEQ(StateTy St, SymbolID sym, const llvm::APSInt& V, + bool& isFeasible); + void Nodify(NodeSet& Dst, Stmt* S, NodeTy* Pred, StateTy St); /// Nodify - This version of Nodify is used to batch process a set of states. @@ -851,18 +857,27 @@ void GRConstants::Visit(Stmt* S, GRConstants::NodeTy* Pred, // "Assume" logic. //===----------------------------------------------------------------------===// -GRConstants::StateTy GRConstants::Assume(StateTy St, LValue Cond, bool Assumption, +GRConstants::StateTy GRConstants::Assume(StateTy St, LValue Cond, + bool Assumption, bool& isFeasible) { switch (Cond.getSubKind()) { default: - assert (false && "'Assume' not implemented for this NonLValue."); + assert (false && "'Assume' not implemented for this LValue."); return St; + case lval::SymbolValKind: + if (Assumption) + return AssumeSymNE(St, cast(Cond).getSymbol(), + ValMgr.getZeroWithPtrWidth(), isFeasible); + else + return AssumeSymEQ(St, cast(Cond).getSymbol(), + ValMgr.getZeroWithPtrWidth(), isFeasible); + case lval::DeclValKind: isFeasible = Assumption; return St; - + case lval::ConcreteIntKind: { bool b = cast(Cond).getValue() != 0; isFeasible = b ? Assumption : !Assumption; @@ -871,7 +886,8 @@ GRConstants::StateTy GRConstants::Assume(StateTy St, LValue Cond, bool Assumptio } } -GRConstants::StateTy GRConstants::Assume(StateTy St, NonLValue Cond, bool Assumption, +GRConstants::StateTy GRConstants::Assume(StateTy St, NonLValue Cond, + bool Assumption, bool& isFeasible) { switch (Cond.getSubKind()) { @@ -887,6 +903,51 @@ GRConstants::StateTy GRConstants::Assume(StateTy St, NonLValue Cond, bool Assump } } +GRConstants::StateTy +GRConstants::AssumeSymNE(StateTy 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 StateMgr.AddNE(St, sym, V); +} + +GRConstants::StateTy +GRConstants::AssumeSymEQ(StateTy 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 StateMgr.AddEQ(St, sym, V); +} //===----------------------------------------------------------------------===// // Driver. diff --git a/Analysis/RValues.h b/Analysis/RValues.h index 9c788cac35..cd74262384 100644 --- a/Analysis/RValues.h +++ b/Analysis/RValues.h @@ -149,6 +149,10 @@ public: const llvm::APSInt& getValue(uint64_t X, QualType T, SourceLocation Loc = SourceLocation()); + inline const llvm::APSInt& getZeroWithPtrWidth() { + return getValue(0, Ctx.getTypeSize(Ctx.VoidPtrTy, SourceLocation()), true); + } + const SymIntConstraint& getConstraint(SymbolID sym, BinaryOperator::Opcode Op, const llvm::APSInt& V); }; diff --git a/Analysis/ValueState.cpp b/Analysis/ValueState.cpp index aa6ddbdd53..418b06e725 100644 --- a/Analysis/ValueState.cpp +++ b/Analysis/ValueState.cpp @@ -15,6 +15,24 @@ using namespace clang; +bool ValueState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const { + // First, retrieve the NE-set associated with the given symbol. + ConstantNotEqTy::TreeTy* T = Data->ConstantNotEq.SlimFind(sym); + + if (!T) + return false; + + // Second, see if V is present in the NE-set. + return T->getValue().second.contains(&V); +} + +const llvm::APSInt* ValueState::getSymVal(SymbolID sym) const { + ConstantEqTy::TreeTy* T = Data->ConstantEq.SlimFind(sym); + return T ? T->getValue().second : NULL; +} + + + RValue ValueStateManager::GetValue(const StateTy& St, const LValue& LV) { switch (LV.getSubKind()) { case lval::DeclValKind: { @@ -31,6 +49,36 @@ RValue ValueStateManager::GetValue(const StateTy& St, const LValue& LV) { return InvalidValue(); } +ValueStateManager::StateTy +ValueStateManager::AddNE(StateTy St, SymbolID sym, const llvm::APSInt& V) { + // First, retrieve the NE-set associated with the given symbol. + ValueState::ConstantNotEqTy::TreeTy* T = + St.getImpl()->ConstantNotEq.SlimFind(sym); + + ValueState::IntSetTy S = T ? T->getValue().second : ISetFactory.GetEmptySet(); + + // Now add V to the NE set. + S = ISetFactory.Add(S, &V); + + // Create a new state with the old binding replaced. + ValueStateImpl NewStateImpl = *St.getImpl(); + NewStateImpl.ConstantNotEq = CNEFactory.Add(NewStateImpl.ConstantNotEq, + sym, S); + + // Get the persistent copy. + return getPersistentState(NewStateImpl); +} + +ValueStateManager::StateTy +ValueStateManager::AddEQ(StateTy St, SymbolID sym, const llvm::APSInt& V) { + // Create a new state with the old binding replaced. + ValueStateImpl NewStateImpl = *St.getImpl(); + NewStateImpl.ConstantEq = CEFactory.Add(NewStateImpl.ConstantEq, sym, &V); + + // Get the persistent copy. + return getPersistentState(NewStateImpl); +} + RValue ValueStateManager::GetValue(const StateTy& St, Stmt* S, bool* hasVal) { for (;;) { switch (S->getStmtClass()) { @@ -163,7 +211,8 @@ ValueStateManager::getInitialState() { // Create a state with empty variable bindings. ValueStateImpl StateImpl(VBFactory.GetEmptyMap(), - CNEFactory.GetEmptyMap()); + CNEFactory.GetEmptyMap(), + CEFactory.GetEmptyMap()); return getPersistentState(StateImpl); } diff --git a/Analysis/ValueState.h b/Analysis/ValueState.h index 10abdceb32..b452979e2e 100644 --- a/Analysis/ValueState.h +++ b/Analysis/ValueState.h @@ -116,8 +116,9 @@ public: namespace vstate { typedef llvm::ImmutableSet IntSetTy; - typedef llvm::ImmutableMap VariableBindingsTy; - typedef llvm::ImmutableMap ConstantNotEqTy; + typedef llvm::ImmutableMap VariableBindingsTy; + typedef llvm::ImmutableMap ConstantNotEqTy; + typedef llvm::ImmutableMap ConstantEqTy; } /// ValueStateImpl - This class encapsulates the actual data values for @@ -127,22 +128,28 @@ namespace vstate { struct ValueStateImpl : public llvm::FoldingSetNode { vstate::VariableBindingsTy VariableBindings; vstate::ConstantNotEqTy ConstantNotEq; + vstate::ConstantEqTy ConstantEq; /// This ctor is used when creating the first ValueStateImpl object. - ValueStateImpl(vstate::VariableBindingsTy VB, vstate::ConstantNotEqTy CNE) - : VariableBindings(VB), ConstantNotEq(CNE) {} + ValueStateImpl(vstate::VariableBindingsTy VB, + vstate::ConstantNotEqTy CNE, + vstate::ConstantEqTy CE) + : VariableBindings(VB), ConstantNotEq(CNE), ConstantEq(CE) {} /// Copy ctor - We must explicitly define this or else the "Next" ptr /// in FoldingSetNode will also get copied. ValueStateImpl(const ValueStateImpl& RHS) : llvm::FoldingSetNode(), VariableBindings(RHS.VariableBindings), - ConstantNotEq(RHS.ConstantNotEq) {} + ConstantNotEq(RHS.ConstantNotEq), + ConstantEq(RHS.ConstantEq) {} /// Profile - Profile the contents of a ValueStateImpl object for use /// in a FoldingSet. static void Profile(llvm::FoldingSetNodeID& ID, const ValueStateImpl& V) { V.VariableBindings.Profile(ID); + V.ConstantNotEq.Profile(ID); + V.ConstantEq.Profile(ID); } /// Profile - Used to profile the contents of this object for inclusion @@ -171,10 +178,18 @@ public: ValueStateImpl* getImpl() const { return Data; } // Typedefs. + typedef vstate::IntSetTy IntSetTy; typedef vstate::VariableBindingsTy VariableBindingsTy; typedef vstate::ConstantNotEqTy ConstantNotEqTy; + typedef vstate::ConstantEqTy ConstantEqTy; + typedef llvm::SmallVector BufferTy; + // Queries. + + bool isNotEqual(SymbolID sym, const llvm::APSInt& V) const; + const llvm::APSInt* getSymVal(SymbolID sym) const; + // Iterators. typedef VariableBindingsTy::iterator vb_iterator; @@ -211,8 +226,10 @@ public: typedef ValueState StateTy; private: + ValueState::IntSetTy::Factory ISetFactory; ValueState::VariableBindingsTy::Factory VBFactory; ValueState::ConstantNotEqTy::Factory CNEFactory; + ValueState::ConstantEqTy::Factory CEFactory; /// StateSet - FoldingSet containing all the states created for analyzing /// a particular function. This is used to unique states. @@ -249,6 +266,9 @@ public: StateTy Add(StateTy St, VarBindKey K, const RValue& V); StateTy Remove(StateTy St, VarBindKey K); StateTy getPersistentState(const ValueStateImpl& Impl); + + StateTy AddEQ(StateTy St, SymbolID sym, const llvm::APSInt& V); + StateTy AddNE(StateTy St, SymbolID sym, const llvm::APSInt& V); }; } // end clang namespace -- 2.40.0