r177801 - [analyzer] Translate "a != b" to "(b - a) != 0" in the constraint manager.
Jordan Rose
jordan_rose at apple.com
Fri Mar 22 18:21:17 PDT 2013
Author: jrose
Date: Fri Mar 22 20:21:16 2013
New Revision: 177801
URL: http://llvm.org/viewvc/llvm-project?rev=177801&view=rev
Log:
[analyzer] Translate "a != b" to "(b - a) != 0" in the constraint manager.
Canonicalizing these two forms allows us to better model containers like
std::vector, which use "m_start != m_finish" to implement empty() but
"m_finish - m_start" to implement size(). The analyzer should have a
consistent interpretation of these two symbolic expressions, even though
it's not properly reasoning about either one yet.
The other unfortunate thing is that while the size() expression will only
ever be written "m_finish - m_start", the comparison may be written
"m_finish == m_start" or "m_start == m_finish". Right now the analyzer does
not attempt to canonicalize those two expressions, since it doesn't know
which length expression to pick. Doing this correctly will probably require
implementing unary minus as a new SymExpr kind (<rdar://problem/12351075>).
For now, the analyzer inverts the order of arguments in the comparison to
build the subtraction, on the assumption that "begin() != end()" is
written more often than "end() != begin()". This is purely speculation.
<rdar://problem/13239003>
Modified:
cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
cfe/trunk/test/Analysis/ptr-arith.c
Modified: cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp?rev=177801&r1=177800&r2=177801&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Fri Mar 22 20:21:16 2013
@@ -285,8 +285,8 @@ namespace {
class RangeConstraintManager : public SimpleConstraintManager{
RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
public:
- RangeConstraintManager(SubEngine *subengine, BasicValueFactory &BVF)
- : SimpleConstraintManager(subengine, BVF) {}
+ RangeConstraintManager(SubEngine *subengine, SValBuilder &SVB)
+ : SimpleConstraintManager(subengine, SVB) {}
ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
const llvm::APSInt& Int,
@@ -328,7 +328,7 @@ private:
ConstraintManager *
ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
- return new RangeConstraintManager(Eng, StMgr.getBasicVals());
+ return new RangeConstraintManager(Eng, StMgr.getSValBuilder());
}
const llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp?rev=177801&r1=177800&r2=177801&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp Fri Mar 22 20:21:16 2013
@@ -49,6 +49,11 @@ bool SimpleConstraintManager::canReasonA
}
}
+ if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
+ if (SSE->getOpcode() == BO_EQ || SSE->getOpcode() == BO_NE)
+ return true;
+ }
+
return false;
}
@@ -164,8 +169,6 @@ ProgramStateRef SimpleConstraintManager:
return assumeAuxForSymbol(state, sym, Assumption);
}
- BasicValueFactory &BasicVals = getBasicVals();
-
switch (Cond.getSubKind()) {
default:
llvm_unreachable("'Assume' not implemented for this NonLoc");
@@ -180,26 +183,43 @@ ProgramStateRef SimpleConstraintManager:
return assumeAuxForSymbol(state, sym, Assumption);
// Handle symbolic expression.
- } else {
+ } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) {
// We can only simplify expressions whose RHS is an integer.
- const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
- if (!SE)
- return assumeAuxForSymbol(state, sym, Assumption);
BinaryOperator::Opcode op = SE->getOpcode();
- // Implicitly compare non-comparison expressions to 0.
- if (!BinaryOperator::isComparisonOp(op)) {
- QualType T = SE->getType();
- const llvm::APSInt &zero = BasicVals.getValue(0, T);
- op = (Assumption ? BO_NE : BO_EQ);
- return assumeSymRel(state, SE, op, zero);
+ if (BinaryOperator::isComparisonOp(op)) {
+ if (!Assumption)
+ op = NegateComparison(op);
+
+ return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
}
- // From here on out, op is the real comparison we'll be testing.
- if (!Assumption)
- op = NegateComparison(op);
- return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
+ } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) {
+ BinaryOperator::Opcode Op = SSE->getOpcode();
+
+ // Translate "a != b" to "(b - a) != 0".
+ // We invert the order of the operands as a heuristic for how loop
+ // conditions are usually written ("begin != end") as compared to length
+ // calculations ("end - begin"). The more correct thing to do would be to
+ // canonicalize "a - b" and "b - a", which would allow us to treat
+ // "a != b" and "b != a" the same.
+ if (BinaryOperator::isEqualityOp(Op)) {
+ SymbolManager &SymMgr = getSymbolManager();
+
+ assert(Loc::isLocType(SSE->getLHS()->getType()));
+ assert(Loc::isLocType(SSE->getRHS()->getType()));
+ QualType DiffTy = SymMgr.getContext().getPointerDiffType();
+ SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
+ SSE->getLHS(), DiffTy);
+
+ Assumption ^= (SSE->getOpcode() == BO_EQ);
+ return assumeAuxForSymbol(state, Subtraction, Assumption);
+ }
}
+
+ // If we get here, there's nothing else we can do but treat the symbol as
+ // opaque.
+ return assumeAuxForSymbol(state, sym, Assumption);
}
case nonloc::ConcreteIntKind: {
Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h?rev=177801&r1=177800&r2=177801&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h Fri Mar 22 20:21:16 2013
@@ -23,10 +23,10 @@ namespace ento {
class SimpleConstraintManager : public ConstraintManager {
SubEngine *SU;
- BasicValueFactory &BVF;
+ SValBuilder &SVB;
public:
- SimpleConstraintManager(SubEngine *subengine, BasicValueFactory &BV)
- : SU(subengine), BVF(BV) {}
+ SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
+ : SU(subengine), SVB(SB) {}
virtual ~SimpleConstraintManager();
//===------------------------------------------------------------------===//
@@ -81,7 +81,8 @@ protected:
// Internal implementation.
//===------------------------------------------------------------------===//
- BasicValueFactory &getBasicVals() const { return BVF; }
+ BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
+ SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
bool canReasonAbout(SVal X) const;
Modified: cfe/trunk/test/Analysis/ptr-arith.c
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/ptr-arith.c?rev=177801&r1=177800&r2=177801&view=diff
==============================================================================
--- cfe/trunk/test/Analysis/ptr-arith.c (original)
+++ cfe/trunk/test/Analysis/ptr-arith.c Fri Mar 22 20:21:16 2013
@@ -179,3 +179,60 @@ void use_symbols(int *lhs, int *rhs) {
return;
clang_analyzer_eval((lhs - rhs) == 5); // expected-warning{{TRUE}}
}
+
+void equal_implies_zero(int *lhs, int *rhs) {
+ clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
+ if (lhs == rhs) {
+ clang_analyzer_eval(lhs != rhs); // expected-warning{{FALSE}}
+ clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{TRUE}}
+ return;
+ }
+ clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+ clang_analyzer_eval(lhs != rhs); // expected-warning{{TRUE}}
+ clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
+}
+
+void zero_implies_equal(int *lhs, int *rhs) {
+ clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
+ if ((rhs - lhs) == 0) {
+ clang_analyzer_eval(lhs != rhs); // expected-warning{{FALSE}}
+ clang_analyzer_eval(lhs == rhs); // expected-warning{{TRUE}}
+ return;
+ }
+ clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
+ clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+ clang_analyzer_eval(lhs != rhs); // expected-warning{{TRUE}}
+}
+
+//-------------------------------
+// False positives
+//-------------------------------
+
+void zero_implies_reversed_equal(int *lhs, int *rhs) {
+ clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
+ if ((rhs - lhs) == 0) {
+ // FIXME: Should be FALSE.
+ clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
+ // FIXME: Should be TRUE.
+ clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
+ return;
+ }
+ clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
+ // FIXME: Should be FALSE.
+ clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
+ // FIXME: Should be TRUE.
+ clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
+}
+
+void canonical_equal(int *lhs, int *rhs) {
+ clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
+ if (lhs == rhs) {
+ // FIXME: Should be TRUE.
+ clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
+ return;
+ }
+ clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+
+ // FIXME: Should be FALSE.
+ clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
+}
More information about the cfe-commits
mailing list