aboutsummaryrefslogtreecommitdiff
path: root/lib/Analysis/BasicConstraintManager.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Analysis/BasicConstraintManager.cpp')
-rw-r--r--lib/Analysis/BasicConstraintManager.cpp298
1 files changed, 298 insertions, 0 deletions
diff --git a/lib/Analysis/BasicConstraintManager.cpp b/lib/Analysis/BasicConstraintManager.cpp
new file mode 100644
index 0000000000..efe5b93da4
--- /dev/null
+++ b/lib/Analysis/BasicConstraintManager.cpp
@@ -0,0 +1,298 @@
+#include "clang/Analysis/PathSensitive/ConstraintManager.h"
+#include "clang/Analysis/PathSensitive/GRState.h"
+#include "llvm/Support/Compiler.h"
+
+using namespace clang;
+
+namespace {
+
+// BasicConstraintManager only tracks equality and inequality constraints of
+// constants and integer variables.
+class VISIBILITY_HIDDEN BasicConstraintManager : public ConstraintManager {
+ typedef llvm::ImmutableMap<SymbolID, GRState::IntSetTy> ConstNotEqTy;
+ typedef llvm::ImmutableMap<SymbolID, const llvm::APSInt*> ConstEqTy;
+
+ GRStateManager& StateMgr;
+
+public:
+ BasicConstraintManager(GRStateManager& statemgr) : StateMgr(statemgr) {}
+
+ virtual const GRState* Assume(const GRState* St, RVal Cond,
+ bool Assumption, bool& isFeasible);
+
+ const GRState* Assume(const GRState* St, LVal Cond, bool Assumption,
+ bool& isFeasible);
+
+ const GRState* AssumeAux(const GRState* St, LVal Cond,bool Assumption,
+ bool& isFeasible);
+
+ const GRState* Assume(const GRState* St, NonLVal Cond, bool Assumption,
+ bool& isFeasible);
+
+ const GRState* AssumeAux(const GRState* St, NonLVal Cond, bool Assumption,
+ bool& isFeasible);
+
+ const GRState* AssumeSymInt(const GRState* St, bool Assumption,
+ const SymIntConstraint& C, bool& isFeasible);
+
+ const GRState* AssumeSymNE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymEQ(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymLT(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymGT(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymGE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const GRState* AssumeSymLE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+ };
+
+} // end anonymous namespace
+
+ConstraintManager* clang::CreateBasicConstraintManager(GRStateManager& StateMgr)
+{
+ return new BasicConstraintManager(StateMgr);
+}
+
+const GRState* BasicConstraintManager::Assume(const GRState* St, RVal Cond,
+ bool Assumption, bool& isFeasible) {
+ if (Cond.isUnknown()) {
+ isFeasible = true;
+ return St;
+ }
+
+ if (isa<NonLVal>(Cond))
+ return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
+ else
+ return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
+}
+
+const GRState* BasicConstraintManager::Assume(const GRState* St, LVal Cond,
+ bool Assumption, bool& isFeasible) {
+ St = AssumeAux(St, Cond, Assumption, isFeasible);
+ // TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
+ return St;
+}
+
+const GRState* BasicConstraintManager::AssumeAux(const GRState* St, LVal Cond,
+ bool Assumption, bool& isFeasible) {
+ BasicValueFactory& BasicVals = StateMgr.getBasicVals();
+
+ switch (Cond.getSubKind()) {
+ default:
+ assert (false && "'Assume' not implemented for this LVal.");
+ return St;
+
+ case lval::SymbolValKind:
+ if (Assumption)
+ return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+ BasicVals.getZeroWithPtrWidth(), isFeasible);
+ else
+ return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+ BasicVals.getZeroWithPtrWidth(), isFeasible);
+
+ case lval::DeclValKind:
+ case lval::FuncValKind:
+ case lval::GotoLabelKind:
+ case lval::StringLiteralValKind:
+ isFeasible = Assumption;
+ return St;
+
+ case lval::FieldOffsetKind:
+ return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
+ Assumption, isFeasible);
+
+ case lval::ArrayOffsetKind:
+ return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
+ Assumption, isFeasible);
+
+ case lval::ConcreteIntKind: {
+ bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
+ isFeasible = b ? Assumption : !Assumption;
+ return St;
+ }
+ } // end switch
+}
+
+const GRState*
+BasicConstraintManager::Assume(const GRState* St, NonLVal Cond, bool Assumption,
+ bool& isFeasible) {
+ St = AssumeAux(St, Cond, Assumption, isFeasible);
+ // TF->EvalAssume() does nothing now.
+ return St;
+}
+
+const GRState*
+BasicConstraintManager::AssumeAux(const GRState* St,NonLVal Cond,
+ bool Assumption, bool& isFeasible) {
+ BasicValueFactory& BasicVals = StateMgr.getBasicVals();
+ SymbolManager& SymMgr = StateMgr.getSymbolManager();
+
+ switch (Cond.getSubKind()) {
+ default:
+ assert(false && "'Assume' not implemented for this NonLVal");
+
+ case nonlval::SymbolValKind: {
+ nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
+ SymbolID sym = SV.getSymbol();
+
+ if (Assumption)
+ return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
+ isFeasible);
+ else
+ return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
+ isFeasible);
+ }
+
+ case nonlval::SymIntConstraintValKind:
+ return
+ AssumeSymInt(St, Assumption,
+ cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
+ isFeasible);
+
+ case nonlval::ConcreteIntKind: {
+ bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
+ isFeasible = b ? Assumption : !Assumption;
+ return St;
+ }
+
+ case nonlval::LValAsIntegerKind:
+ return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
+ Assumption, isFeasible);
+ } // end switch
+}
+
+const GRState*
+BasicConstraintManager::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::GE:
+ if (Assumption)
+ return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
+ else
+ return AssumeSymLT(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*
+BasicConstraintManager::AssumeSymNE(const GRState* 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);
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymEQ(const GRState* 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);
+}
+
+// These logic will be handled in another ConstraintManager.
+const GRState*
+BasicConstraintManager::AssumeSymLT(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+
+ // FIXME: For now have assuming x < y be the same as assuming sym != V;
+ return AssumeSymNE(St, sym, V, isFeasible);
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymGT(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+
+ // FIXME: For now have assuming x > y be the same as assuming sym != V;
+ return AssumeSymNE(St, sym, V, isFeasible);
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+
+ // FIXME: Primitive logic for now. Only reject a path if the value of
+ // sym is a constant X and !(X >= V).
+
+ if (const llvm::APSInt* X = St->getSymVal(sym)) {
+ isFeasible = *X >= V;
+ return St;
+ }
+
+ isFeasible = true;
+ return St;
+}
+
+const GRState*
+BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible) {
+
+ // FIXME: Primitive logic for now. Only reject a path if the value of
+ // sym is a constant X and !(X <= V).
+
+ if (const llvm::APSInt* X = St->getSymVal(sym)) {
+ isFeasible = *X <= V;
+ return St;
+ }
+
+ isFeasible = true;
+ return St;
+}
generated by cgit v1.2.3-18-g5258 (git 2.32.0) at 2025-05-01 16:07:09 +0000