[cfe-commits] r54493 - in /cfe/trunk: include/clang/Analysis/PathSensitive/ValueState.h lib/Analysis/ValueState.cpp
Ted Kremenek
kremenek at apple.com
Thu Aug 7 15:30:22 PDT 2008
Author: kremenek
Date: Thu Aug 7 17:30:22 2008
New Revision: 54493
URL: http://llvm.org/viewvc/llvm-project?rev=54493&view=rev
Log:
Added AssumeSymGT, AssumeSymGE, AssumeSymLT, AssumeSymLE to add some minor improvements to path-sensitivity. Right now we basically treat 'x > y' and 'x < y' as implying 'x != y', but this restriction will only inevitably apply to our must rudimentary value tracking component (we'll implement more advanced value reasoning later).
Modified:
cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h
cfe/trunk/lib/Analysis/ValueState.cpp
Modified: cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h?rev=54493&r1=54492&r2=54493&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/ValueState.h Thu Aug 7 17:30:22 2008
@@ -365,7 +365,6 @@
const ValueState* AddNE(const ValueState* St, SymbolID sym,
const llvm::APSInt& V);
-
bool isEqual(const ValueState* state, Expr* Ex, const llvm::APSInt& V);
bool isEqual(const ValueState* state, Expr* Ex, uint64_t);
@@ -397,6 +396,9 @@
const ValueState* AssumeAux(const ValueState* St, NonLVal Cond,
bool Assumption, bool& isFeasible);
+
+ const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,
+ const SymIntConstraint& C, bool& isFeasible);
const ValueState* AssumeSymNE(const ValueState* St, SymbolID sym,
const llvm::APSInt& V, bool& isFeasible);
@@ -404,8 +406,17 @@
const ValueState* AssumeSymEQ(const ValueState* St, SymbolID sym,
const llvm::APSInt& V, bool& isFeasible);
- const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,
- const SymIntConstraint& C, bool& isFeasible);
+ const ValueState* AssumeSymLT(const ValueState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const ValueState* AssumeSymLE(const ValueState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const ValueState* AssumeSymGT(const ValueState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
+
+ const ValueState* AssumeSymGE(const ValueState* St, SymbolID sym,
+ const llvm::APSInt& V, bool& isFeasible);
};
} // end clang namespace
Modified: cfe/trunk/lib/Analysis/ValueState.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/ValueState.cpp?rev=54493&r1=54492&r2=54493&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/ValueState.cpp (original)
+++ cfe/trunk/lib/Analysis/ValueState.cpp Thu Aug 7 17:30:22 2008
@@ -435,9 +435,52 @@
}
}
-const ValueState* ValueStateManager::AssumeSymNE(const ValueState* St,
- SymbolID sym, const llvm::APSInt& V,
- bool& isFeasible) {
+
+
+const ValueState* ValueStateManager::AssumeSymInt(const ValueState* 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);
+ }
+}
+
+//===----------------------------------------------------------------------===//
+// FIXME: This should go into a plug-in constraint engine.
+//===----------------------------------------------------------------------===//
+
+const ValueState*
+ValueStateManager::AssumeSymNE(const ValueState* 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)) {
@@ -458,8 +501,9 @@
return AddNE(St, sym, V);
}
-const ValueState* ValueStateManager::AssumeSymEQ(const ValueState* St, SymbolID sym,
- const llvm::APSInt& V, bool& isFeasible) {
+const ValueState*
+ValueStateManager::AssumeSymEQ(const ValueState* 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)) {
@@ -480,27 +524,51 @@
return AddEQ(St, sym, V);
}
-const ValueState* ValueStateManager::AssumeSymInt(const ValueState* St,
- bool Assumption,
- const SymIntConstraint& C,
- bool& isFeasible) {
+const ValueState*
+ValueStateManager::AssumeSymLT(const ValueState* St, SymbolID sym,
+ const llvm::APSInt& V, 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);
+ // FIXME: For now have assuming x < y be the same as assuming sym != V;
+ return AssumeSymNE(St, sym, V, isFeasible);
+}
+
+const ValueState*
+ValueStateManager::AssumeSymGT(const ValueState* 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 ValueState*
+ValueStateManager::AssumeSymGE(const ValueState* 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 ValueState*
+ValueStateManager::AssumeSymLE(const ValueState* 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;
}
+
More information about the cfe-commits
mailing list