aboutsummaryrefslogtreecommitdiff
path: root/lib/Analysis/SimpleConstraintManager.cpp
diff options
context:
space:
mode:
authorTed Kremenek <kremenek@apple.com>2009-02-14 17:08:39 +0000
committerTed Kremenek <kremenek@apple.com>2009-02-14 17:08:39 +0000
commit4502195fecf399fdbbb9ee2393ad08148c394179 (patch)
treed82ef4dcd0e9bf66b87e423b96733f0843e48636 /lib/Analysis/SimpleConstraintManager.cpp
parent2793bda429909d0c5c73334342ac69672754d801 (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.cpp230
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