diff options
Diffstat (limited to 'lib/StaticAnalyzer/Core/BasicConstraintManager.cpp')
| -rw-r--r-- | lib/StaticAnalyzer/Core/BasicConstraintManager.cpp | 446 |
1 files changed, 0 insertions, 446 deletions
diff --git a/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp b/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp deleted file mode 100644 index 8897756..0000000 --- a/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp +++ /dev/null @@ -1,446 +0,0 @@ -//== BasicConstraintManager.cpp - Manage basic constraints.------*- 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 BasicConstraintManager, a class that tracks simple -// equality and inequality constraints on symbolic values of ProgramState. -// -//===----------------------------------------------------------------------===// - -#include "SimpleConstraintManager.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" -#include "llvm/Support/raw_ostream.h" - -using namespace clang; -using namespace ento; - - -namespace { class ConstNotEq {}; } -namespace { class ConstEq {}; } - -typedef llvm::ImmutableMap<SymbolRef,ProgramState::IntSetTy> ConstNotEqTy; -typedef llvm::ImmutableMap<SymbolRef,const llvm::APSInt*> ConstEqTy; - -static int ConstEqIndex = 0; -static int ConstNotEqIndex = 0; - -namespace clang { -namespace ento { -template<> -struct ProgramStateTrait<ConstNotEq> : - public ProgramStatePartialTrait<ConstNotEqTy> { - static inline void *GDMIndex() { return &ConstNotEqIndex; } -}; - -template<> -struct ProgramStateTrait<ConstEq> : public ProgramStatePartialTrait<ConstEqTy> { - static inline void *GDMIndex() { return &ConstEqIndex; } -}; -} -} - -namespace { -// BasicConstraintManager only tracks equality and inequality constraints of -// constants and integer variables. -class BasicConstraintManager - : public SimpleConstraintManager { - ProgramState::IntSetTy::Factory ISetFactory; -public: - BasicConstraintManager(ProgramStateManager &statemgr, SubEngine &subengine) - : SimpleConstraintManager(subengine, statemgr.getBasicVals()), - ISetFactory(statemgr.getAllocator()) {} - - ProgramStateRef assumeSymEquality(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment, - bool Assumption); - - ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) { - return assumeSymEquality(State, Sym, V, Adjustment, false); - } - - ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) { - return assumeSymEquality(State, Sym, V, Adjustment, true); - } - - ProgramStateRef assumeSymLT(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V, - const llvm::APSInt& Adjustment); - - ProgramStateRef assumeSymGT(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V, - const llvm::APSInt& Adjustment); - - ProgramStateRef assumeSymGE(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V, - const llvm::APSInt& Adjustment); - - ProgramStateRef assumeSymLE(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V, - const llvm::APSInt& Adjustment); - - ProgramStateRef AddEQ(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V); - - ProgramStateRef AddNE(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V); - - const llvm::APSInt* getSymVal(ProgramStateRef state, - SymbolRef sym) const; - - bool isNotEqual(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V) const; - - bool isEqual(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V) const; - - ProgramStateRef removeDeadBindings(ProgramStateRef state, - SymbolReaper& SymReaper); - - bool performTest(llvm::APSInt SymVal, llvm::APSInt Adjustment, - BinaryOperator::Opcode Op, llvm::APSInt ComparisonVal); - - void print(ProgramStateRef state, - raw_ostream &Out, - const char* nl, - const char *sep); -}; - -} // end anonymous namespace - -ConstraintManager* -ento::CreateBasicConstraintManager(ProgramStateManager& statemgr, - SubEngine &subengine) { - return new BasicConstraintManager(statemgr, subengine); -} - -// FIXME: This is a more general utility and should live somewhere else. -bool BasicConstraintManager::performTest(llvm::APSInt SymVal, - llvm::APSInt Adjustment, - BinaryOperator::Opcode Op, - llvm::APSInt ComparisonVal) { - APSIntType Type(Adjustment); - Type.apply(SymVal); - Type.apply(ComparisonVal); - SymVal += Adjustment; - - assert(BinaryOperator::isComparisonOp(Op)); - BasicValueFactory &BVF = getBasicVals(); - const llvm::APSInt *Result = BVF.evalAPSInt(Op, SymVal, ComparisonVal); - assert(Result && "Comparisons should always have valid results."); - - return Result->getBoolValue(); -} - -ProgramStateRef -BasicConstraintManager::assumeSymEquality(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment, - bool Assumption) { - // Before we do any real work, see if the value can even show up. - APSIntType AdjustmentType(Adjustment); - if (AdjustmentType.testInRange(V) != APSIntType::RTR_Within) - return Assumption ? NULL : State; - - // Get the symbol type. - BasicValueFactory &BVF = getBasicVals(); - ASTContext &Ctx = BVF.getContext(); - APSIntType SymbolType = BVF.getAPSIntType(Sym->getType(Ctx)); - - // First, see if the adjusted value is within range for the symbol. - llvm::APSInt Adjusted = AdjustmentType.convert(V) - Adjustment; - if (SymbolType.testInRange(Adjusted) != APSIntType::RTR_Within) - return Assumption ? NULL : State; - - // Now we can do things properly in the symbol space. - SymbolType.apply(Adjusted); - - // Second, determine if sym == X, where X+Adjustment != V. - if (const llvm::APSInt *X = getSymVal(State, Sym)) { - bool IsFeasible = (*X == Adjusted); - return (IsFeasible == Assumption) ? State : NULL; - } - - // Third, determine if we already know sym+Adjustment != V. - if (isNotEqual(State, Sym, Adjusted)) - return Assumption ? NULL : State; - - // If we reach here, sym is not a constant and we don't know if it is != V. - // Make the correct assumption. - if (Assumption) - return AddEQ(State, Sym, Adjusted); - else - return AddNE(State, Sym, Adjusted); -} - -// The logic for these will be handled in another ConstraintManager. -// Approximate it here anyway by handling some edge cases. -ProgramStateRef -BasicConstraintManager::assumeSymLT(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) { - APSIntType ComparisonType(V), AdjustmentType(Adjustment); - - // Is 'V' out of range above the type? - llvm::APSInt Max = AdjustmentType.getMaxValue(); - if (V > ComparisonType.convert(Max)) { - // This path is trivially feasible. - return state; - } - - // Is 'V' the smallest possible value, or out of range below the type? - llvm::APSInt Min = AdjustmentType.getMinValue(); - if (V <= ComparisonType.convert(Min)) { - // sym cannot be any value less than 'V'. This path is infeasible. - return NULL; - } - - // Reject a path if the value of sym is a constant X and !(X+Adj < V). - if (const llvm::APSInt *X = getSymVal(state, sym)) { - bool isFeasible = performTest(*X, Adjustment, BO_LT, V); - return isFeasible ? state : NULL; - } - - // FIXME: For now have assuming x < y be the same as assuming sym != V; - return assumeSymNE(state, sym, V, Adjustment); -} - -ProgramStateRef -BasicConstraintManager::assumeSymGT(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) { - APSIntType ComparisonType(V), AdjustmentType(Adjustment); - - // Is 'V' the largest possible value, or out of range above the type? - llvm::APSInt Max = AdjustmentType.getMaxValue(); - if (V >= ComparisonType.convert(Max)) { - // sym cannot be any value greater than 'V'. This path is infeasible. - return NULL; - } - - // Is 'V' out of range below the type? - llvm::APSInt Min = AdjustmentType.getMinValue(); - if (V < ComparisonType.convert(Min)) { - // This path is trivially feasible. - return state; - } - - // Reject a path if the value of sym is a constant X and !(X+Adj > V). - if (const llvm::APSInt *X = getSymVal(state, sym)) { - bool isFeasible = performTest(*X, Adjustment, BO_GT, V); - return isFeasible ? state : NULL; - } - - // FIXME: For now have assuming x > y be the same as assuming sym != V; - return assumeSymNE(state, sym, V, Adjustment); -} - -ProgramStateRef -BasicConstraintManager::assumeSymGE(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) { - APSIntType ComparisonType(V), AdjustmentType(Adjustment); - - // Is 'V' the largest possible value, or out of range above the type? - llvm::APSInt Max = AdjustmentType.getMaxValue(); - ComparisonType.apply(Max); - - if (V > Max) { - // sym cannot be any value greater than 'V'. This path is infeasible. - return NULL; - } else if (V == Max) { - // If the path is feasible then as a consequence we know that - // 'sym+Adjustment == V' because there are no larger values. - // Add this constraint. - return assumeSymEQ(state, sym, V, Adjustment); - } - - // Is 'V' out of range below the type? - llvm::APSInt Min = AdjustmentType.getMinValue(); - if (V < ComparisonType.convert(Min)) { - // This path is trivially feasible. - return state; - } - - // Reject a path if the value of sym is a constant X and !(X+Adj >= V). - if (const llvm::APSInt *X = getSymVal(state, sym)) { - bool isFeasible = performTest(*X, Adjustment, BO_GE, V); - return isFeasible ? state : NULL; - } - - return state; -} - -ProgramStateRef -BasicConstraintManager::assumeSymLE(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt &V, - const llvm::APSInt &Adjustment) { - APSIntType ComparisonType(V), AdjustmentType(Adjustment); - - // Is 'V' out of range above the type? - llvm::APSInt Max = AdjustmentType.getMaxValue(); - if (V > ComparisonType.convert(Max)) { - // This path is trivially feasible. - return state; - } - - // Is 'V' the smallest possible value, or out of range below the type? - llvm::APSInt Min = AdjustmentType.getMinValue(); - ComparisonType.apply(Min); - - if (V < Min) { - // sym cannot be any value less than 'V'. This path is infeasible. - return NULL; - } else if (V == Min) { - // If the path is feasible then as a consequence we know that - // 'sym+Adjustment == V' because there are no smaller values. - // Add this constraint. - return assumeSymEQ(state, sym, V, Adjustment); - } - - // Reject a path if the value of sym is a constant X and !(X+Adj >= V). - if (const llvm::APSInt *X = getSymVal(state, sym)) { - bool isFeasible = performTest(*X, Adjustment, BO_LE, V); - return isFeasible ? state : NULL; - } - - return state; -} - -ProgramStateRef BasicConstraintManager::AddEQ(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V) { - // Now that we have an actual value, we can throw out the NE-set. - // Create a new state with the old bindings replaced. - state = state->remove<ConstNotEq>(sym); - return state->set<ConstEq>(sym, &getBasicVals().getValue(V)); -} - -ProgramStateRef BasicConstraintManager::AddNE(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V) { - - // First, retrieve the NE-set associated with the given symbol. - ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym); - ProgramState::IntSetTy S = T ? *T : ISetFactory.getEmptySet(); - - // Now add V to the NE set. - S = ISetFactory.add(S, &getBasicVals().getValue(V)); - - // Create a new state with the old binding replaced. - return state->set<ConstNotEq>(sym, S); -} - -const llvm::APSInt* BasicConstraintManager::getSymVal(ProgramStateRef state, - SymbolRef sym) const { - const ConstEqTy::data_type* T = state->get<ConstEq>(sym); - return T ? *T : NULL; -} - -bool BasicConstraintManager::isNotEqual(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V) const { - - // Retrieve the NE-set associated with the given symbol. - const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym); - - // See if V is present in the NE-set. - return T ? T->contains(&getBasicVals().getValue(V)) : false; -} - -bool BasicConstraintManager::isEqual(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V) const { - // Retrieve the EQ-set associated with the given symbol. - const ConstEqTy::data_type* T = state->get<ConstEq>(sym); - // See if V is present in the EQ-set. - return T ? **T == V : false; -} - -/// Scan all symbols referenced by the constraints. If the symbol is not alive -/// as marked in LSymbols, mark it as dead in DSymbols. -ProgramStateRef -BasicConstraintManager::removeDeadBindings(ProgramStateRef state, - SymbolReaper& SymReaper) { - - ConstEqTy CE = state->get<ConstEq>(); - ConstEqTy::Factory& CEFactory = state->get_context<ConstEq>(); - - for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) { - SymbolRef sym = I.getKey(); - if (SymReaper.maybeDead(sym)) - CE = CEFactory.remove(CE, sym); - } - state = state->set<ConstEq>(CE); - - ConstNotEqTy CNE = state->get<ConstNotEq>(); - ConstNotEqTy::Factory& CNEFactory = state->get_context<ConstNotEq>(); - - for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) { - SymbolRef sym = I.getKey(); - if (SymReaper.maybeDead(sym)) - CNE = CNEFactory.remove(CNE, sym); - } - - return state->set<ConstNotEq>(CNE); -} - -void BasicConstraintManager::print(ProgramStateRef state, - raw_ostream &Out, - const char* nl, const char *sep) { - // Print equality constraints. - - ConstEqTy CE = state->get<ConstEq>(); - - if (!CE.isEmpty()) { - Out << nl << sep << "'==' constraints:"; - for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) - Out << nl << " $" << I.getKey() << " : " << *I.getData(); - } - - // Print != constraints. - - ConstNotEqTy CNE = state->get<ConstNotEq>(); - - if (!CNE.isEmpty()) { - Out << nl << sep << "'!=' constraints:"; - - for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) { - Out << nl << " $" << I.getKey() << " : "; - bool isFirst = true; - - ProgramState::IntSetTy::iterator J = I.getData().begin(), - EJ = I.getData().end(); - - for ( ; J != EJ; ++J) { - if (isFirst) isFirst = false; - else Out << ", "; - - Out << (*J)->getSExtValue(); // Hack: should print to raw_ostream. - } - } - } -} |
