diff options
author | Ted Kremenek <kremenek@apple.com> | 2009-02-14 17:08:39 +0000 |
---|---|---|
committer | Ted Kremenek <kremenek@apple.com> | 2009-02-14 17:08:39 +0000 |
commit | 4502195fecf399fdbbb9ee2393ad08148c394179 (patch) | |
tree | d82ef4dcd0e9bf66b87e423b96733f0843e48636 /lib/Analysis/SimpleConstraintManager.cpp | |
parent | 2793bda429909d0c5c73334342ac69672754d801 (diff) |
Patch by Ben Laurie:
ConstraintManager:
- constify getSymVal()
BasicConstraintManager:
- Pull out logic that would be common to ConstraintManagers of a similar nature
and put them in a parent class called 'SimpleConstraintManager'.
RangeConstraintManager:
- Added a new prototype ConstraintManager to track ranges of variables! This
ConstraintManager keeps tracks of ranges of concrete integers that a symbolic
integer may have.
AnalysisConsumer:
- Add driver option to use RangeConstraintManager with GRExprEngine-based
analyses.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@64558 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Analysis/SimpleConstraintManager.cpp')
-rw-r--r-- | lib/Analysis/SimpleConstraintManager.cpp | 230 |
1 files changed, 230 insertions, 0 deletions
diff --git a/lib/Analysis/SimpleConstraintManager.cpp b/lib/Analysis/SimpleConstraintManager.cpp new file mode 100644 index 0000000000..c72f39c2fc --- /dev/null +++ b/lib/Analysis/SimpleConstraintManager.cpp @@ -0,0 +1,230 @@ +//== SimpleConstraintManager.cpp --------------------------------*- 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 SimpleConstraintManager, a class that holds code shared +// between BasicConstraintManager and RangeConstraintManager. +// +//===----------------------------------------------------------------------===// + +#include "SimpleConstraintManager.h" +#include "clang/Analysis/PathSensitive/GRExprEngine.h" +#include "clang/Analysis/PathSensitive/GRState.h" + +namespace clang { + +SimpleConstraintManager::~SimpleConstraintManager() {} + +const GRState* +SimpleConstraintManager::Assume(const GRState* St, SVal Cond, bool Assumption, + bool& isFeasible) { + if (Cond.isUnknown()) { + isFeasible = true; + return St; + } + + if (isa<NonLoc>(Cond)) + return Assume(St, cast<NonLoc>(Cond), Assumption, isFeasible); + else + return Assume(St, cast<Loc>(Cond), Assumption, isFeasible); +} + +const GRState* +SimpleConstraintManager::Assume(const GRState* St, Loc Cond, bool Assumption, + bool& isFeasible) { + St = AssumeAux(St, Cond, Assumption, isFeasible); + + if (!isFeasible) + return St; + + // EvalAssume is used to call into the GRTransferFunction object to perform + // any checker-specific update of the state based on this assumption being + // true or false. + return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption, + isFeasible); +} + +const GRState* +SimpleConstraintManager::AssumeAux(const GRState* St, Loc Cond, bool Assumption, + bool& isFeasible) { + BasicValueFactory& BasicVals = StateMgr.getBasicVals(); + + switch (Cond.getSubKind()) { + default: + assert (false && "'Assume' not implemented for this Loc."); + return St; + + case loc::SymbolValKind: + if (Assumption) + return AssumeSymNE(St, cast<loc::SymbolVal>(Cond).getSymbol(), + BasicVals.getZeroWithPtrWidth(), isFeasible); + else + return AssumeSymEQ(St, cast<loc::SymbolVal>(Cond).getSymbol(), + BasicVals.getZeroWithPtrWidth(), isFeasible); + + case loc::MemRegionKind: { + // FIXME: Should this go into the storemanager? + + const MemRegion* R = cast<loc::MemRegionVal>(Cond).getRegion(); + const SubRegion* SubR = dyn_cast<SubRegion>(R); + + while (SubR) { + // FIXME: now we only find the first symbolic region. + if (const SymbolicRegion* SymR = dyn_cast<SymbolicRegion>(SubR)) + return AssumeAux(St, loc::SymbolVal(SymR->getSymbol()), Assumption, + isFeasible); + SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); + } + + // FALL-THROUGH. + } + + case loc::FuncValKind: + case loc::GotoLabelKind: + isFeasible = Assumption; + return St; + + case loc::ConcreteIntKind: { + bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; + isFeasible = b ? Assumption : !Assumption; + return St; + } + } // end switch +} + +const GRState* +SimpleConstraintManager::Assume(const GRState* St, NonLoc Cond, bool Assumption, + bool& isFeasible) { + St = AssumeAux(St, Cond, Assumption, isFeasible); + + if (!isFeasible) + return St; + + // EvalAssume is used to call into the GRTransferFunction object to perform + // any checker-specific update of the state based on this assumption being + // true or false. + return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption, + isFeasible); +} + +const GRState* +SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond, + bool Assumption, bool& isFeasible) { + BasicValueFactory& BasicVals = StateMgr.getBasicVals(); + SymbolManager& SymMgr = StateMgr.getSymbolManager(); + + switch (Cond.getSubKind()) { + default: + assert(false && "'Assume' not implemented for this NonLoc"); + + case nonloc::SymbolValKind: { + nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); + SymbolRef sym = SV.getSymbol(); + QualType T = SymMgr.getType(sym); + + if (Assumption) + return AssumeSymNE(St, sym, BasicVals.getValue(0, T), isFeasible); + else + return AssumeSymEQ(St, sym, BasicVals.getValue(0, T), isFeasible); + } + + case nonloc::SymIntConstraintValKind: + return + AssumeSymInt(St, Assumption, + cast<nonloc::SymIntConstraintVal>(Cond).getConstraint(), + isFeasible); + + case nonloc::ConcreteIntKind: { + bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; + isFeasible = b ? Assumption : !Assumption; + return St; + } + + case nonloc::LocAsIntegerKind: + return AssumeAux(St, cast<nonloc::LocAsInteger>(Cond).getLoc(), + Assumption, isFeasible); + } // end switch +} + +const GRState* +SimpleConstraintManager::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::GT: + if (Assumption) + return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible); + else + return AssumeSymLE(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::LT: + if (Assumption) + return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible); + else + return AssumeSymGE(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); + } // end switch +} + +const GRState* +SimpleConstraintManager::AssumeInBound(const GRState* St, SVal Idx, + SVal UpperBound, bool Assumption, + bool& isFeasible) { + // Only support ConcreteInt for now. + if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))){ + isFeasible = true; + return St; + } + + const llvm::APSInt& Zero = getBasicVals().getZeroWithPtrWidth(false); + llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue(); + // IdxV might be too narrow. + if (IdxV.getBitWidth() < Zero.getBitWidth()) + IdxV.extend(Zero.getBitWidth()); + // UBV might be too narrow, too. + llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue(); + if (UBV.getBitWidth() < Zero.getBitWidth()) + UBV.extend(Zero.getBitWidth()); + + bool InBound = (Zero <= IdxV) && (IdxV < UBV); + + isFeasible = Assumption ? InBound : !InBound; + + return St; +} + +} // end of namespace clang |