+++ /dev/null
-//== 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.
- }
- }
- }
-}
projects / clang / commitdiff