aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/StaticAnalyzer/Core/RangeConstraintManager.cpp6
-rw-r--r--lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp52
-rw-r--r--lib/StaticAnalyzer/Core/SimpleConstraintManager.h9
-rw-r--r--test/Analysis/ptr-arith.c57
4 files changed, 101 insertions, 23 deletions
diff --git a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index d397e47224..216fb3d4b0 100644
--- a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -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,
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index de13241cac..86940a1e84 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -49,6 +49,11 @@ bool SimpleConstraintManager::canReasonAbout(SVal X) const {
}
}
+ 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::assumeAux(ProgramStateRef state,
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::assumeAux(ProgramStateRef state,
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: {
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
index 01f0b4e446..10ddef1341 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
@@ -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;
diff --git a/test/Analysis/ptr-arith.c b/test/Analysis/ptr-arith.c
index 7f2582dc24..d9c5a0ff99 100644
--- a/test/Analysis/ptr-arith.c
+++ b/test/Analysis/ptr-arith.c
@@ -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}}
+}
generated by cgit v1.2.3-18-g5258 (git 2.32.0) at 2025-08-03 13:32:53 +0000