steakhal updated this revision to Diff 256551.
steakhal added a comment.
- rewritten the `RangeSet::compare` function and checked the assumptions on
WolframAlpha
- moved the `RangeSet::compare` function to a cpp file
- added comments to the `RangeSet::compare` function
- fixed the comment in `RangeConstraintManager::canReasonAbout` function
- introduced the `RangeSet::CompareResult::identical` enum value to be complete
- updated the `RangeConstraintManager::tryAssumeSymSymOp` accoding the
`identical` CompareResult.
- omited testing the `[2,5] < [5,10]` testcase, since that is covered by `[0,5]
< [5,10]`
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D77792/new/
https://reviews.llvm.org/D77792
Files:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
clang/test/Analysis/constraint-manager-sym-sym.c
Index: clang/test/Analysis/constraint-manager-sym-sym.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/constraint-manager-sym-sym.c
@@ -0,0 +1,189 @@
+// RUN: %clang_analyze_cc1 -verify -analyzer-checker=core,debug.ExprInspection \
+// RUN: -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+extern void __assert_fail(__const char *__assertion, __const char *__file,
+ unsigned int __line, __const char *__function)
+ __attribute__((__noreturn__));
+#define assert(expr) \
+ ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))
+
+// Given [a1,a2] and [b1,b2] intervals.
+// Pin the [b1,b2] interval to eg. [5,10]
+// Choose the a1,a2 points from 0,2,5,7,10,12 where a1 < a2.
+// There will be 5+4+3+2+1 cases.
+
+// [0,2] and [5,10]
+void test_range1(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(0 <= l && l <= 2);
+ clang_analyzer_eval(l < r); // expected-warning{{TRUE}}
+ clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+ clang_analyzer_eval(l > r); // expected-warning{{FALSE}}
+ clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// [0,5] and [5,10]
+void test_range2(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(0 <= l && l <= 5);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+ clang_analyzer_eval(l > r); // expected-warning{{FALSE}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,7] and [5,10]
+void test_range3(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(0 <= l && l <= 7);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,10] and [5,10]
+void test_range4(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(0 <= l && l <= 10);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,12] and [5,10]
+void test_range5(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(0 <= l && l <= 12);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,5] and [5,10] omitted because it is the same as the '[0,5] and [5,10]'
+
+// [2,7] and [5,10]
+void test_range7(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(2 <= l && l <= 7);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,10] and [5,10]
+void test_range8(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(2 <= l && l <= 10);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,12] and [5,10]
+void test_range9(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(2 <= l && l <= 12);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,7] and [5,10]
+void test_range10(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(5 <= l && l <= 7);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,10] and [5,10]
+void test_range11(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(5 <= l && l <= 10);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,12] and [5,10]
+void test_range12(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(5 <= l && l <= 12);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [7,10] and [5,10]
+void test_range13(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(7 <= l && l <= 10);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [7,12] and [5,10]
+void test_range14(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(7 <= l && l <= 12);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [10,12] and [5,10]
+void test_range15(int l, int r) {
+ assert(5 <= r && r <= 10);
+ assert(7 <= l && l <= 12);
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// {[0,1],[5,6]} and {[9,9],[11,42],[44,44]}
+void test_range16(int l, int r) {
+ assert((9 <= r && r <= 9) || (11 <= r && r <= 42) || (44 <= r && r <= 44));
+ assert((0 <= l && l <= 1) || (5 <= l && l <= 6));
+ clang_analyzer_eval(l < r); // expected-warning{{TRUE}}
+ clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+ clang_analyzer_eval(l > r); // expected-warning{{FALSE}}
+ clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// {[0,1],[5,10]} and {[9,9],[11,42],[44,44]}
+void test_range17(int l, int r) {
+ assert((9 <= r && r <= 9) || (11 <= r && r <= 42) || (44 <= r && r <= 44));
+ assert((0 <= l && l <= 1) || (5 <= l && l <= 10));
+
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}} expected-warning{{FALSE}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}} expected-warning{{FALSE}}
+}
+
+// {[0,1],[20,20]} and {[9,9],[11,42],[44,44]}
+void test_range18(int l, int r) {
+ assert((9 <= r && r <= 9) || (11 <= r && r <= 42) || (44 <= r && r <= 44));
+ assert((0 <= l && l <= 1) || (20 <= l && l <= 20));
+
+ clang_analyzer_eval(l < r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(l > r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}} expected-warning{{FALSE}}
+ clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}} expected-warning{{FALSE}}
+}
Index: clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -50,7 +50,7 @@
BinaryOperator::Opcode Op = SSE->getOpcode();
assert(BinaryOperator::isComparisonOp(Op));
- // For now, we only support comparing pointers.
+ // We support comparing pointers and...
if (Loc::isLocType(SSE->getLHS()->getType()) &&
Loc::isLocType(SSE->getRHS()->getType())) {
QualType DiffTy = SymMgr.getContext().getPointerDiffType();
@@ -63,6 +63,12 @@
Op = BinaryOperator::negateComparisonOp(Op);
return assumeSymRel(State, Subtraction, Op, Zero);
}
+
+ // We also support constrained symbols, which don't have any overlapping
+ // range intervals. Eg. {[0,1],[5,6]} < {[9,9],[11,42],[44,44]}
+ if (auto OptionalState = tryAssumeSymSymOp(State, Op, SSE->getLHS(),
+ SSE->getRHS(), Assumption))
+ return OptionalState.getValue();
}
// If we get here, there's nothing else we can do but treat the symbol as
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -23,6 +23,44 @@
using namespace clang;
using namespace ento;
+RangeSet::CompareResult RangeSet::compare(const RangeSet &other) const {
+ if (isEmpty() || other.isEmpty())
+ return CompareResult::unknown;
+
+ const int LMaxRMin =
+ llvm::APSInt::compareValues(getMaxValue(), other.getMinValue());
+ const int LMinRMax =
+ llvm::APSInt::compareValues(getMinValue(), other.getMaxValue());
+
+ // {-1,0,1}x{-1,0,1} has 9 combinations, so we will enumerate all of them.
+ // Given [a0,a1] and [b0,b1] ranges.
+ // Assuming that a0 <= a1 and b0 <= b1 (since ranges...)
+ // Than we examine the 'a1 <? b0' and the 'a0 <? b1' comparisons.
+ // Eg. if a1 <? b0 is -1, that means that a1 < b0; zero for equality; etc.
+ // Solving these 9 inequality systems we draw some conclusion and find some
+ // impossible cases (which are not satisfiable with any valid ranges).
+ if (LMaxRMin == -1 && LMinRMax == -1)
+ return CompareResult::less;
+ if (LMaxRMin == -1 && LMinRMax == 0)
+ llvm_unreachable("Impossible.");
+ if (LMaxRMin == -1 && LMinRMax == 1)
+ llvm_unreachable("Impossible.");
+
+ if (LMaxRMin == 0 && LMinRMax == -1)
+ return CompareResult::less_equal;
+ if (LMaxRMin == 0 && LMinRMax == 0)
+ return CompareResult::identical;
+ if (LMaxRMin == 0 && LMinRMax == 1)
+ llvm_unreachable("Impossible.");
+
+ if (LMaxRMin == 1 && LMinRMax == -1)
+ return CompareResult::unknown;
+ if (LMaxRMin == 1 && LMinRMax == 0)
+ return CompareResult::greater_equal;
+ assert(LMaxRMin == 1 && LMinRMax == 1);
+ return CompareResult::greater;
+}
+
void RangeSet::IntersectInRange(BasicValueFactory &BV, Factory &F,
const llvm::APSInt &Lower, const llvm::APSInt &Upper,
PrimRangeSet &newRanges, PrimRangeSet::iterator &i,
@@ -65,6 +103,14 @@
return ranges.begin()->From();
}
+const llvm::APSInt &RangeSet::getMaxValue() const {
+ assert(!isEmpty());
+ auto last = ranges.begin();
+ for (auto it = std::next(ranges.begin()); it != ranges.end(); ++it)
+ last = it;
+ return last->To();
+}
+
bool RangeSet::pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
// This function has nine cases, the cartesian product of range-testing
// both the upper and lower bounds against the symbol's type.
@@ -301,6 +347,12 @@
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+ Optional<ProgramStateRef> tryAssumeSymSymOp(ProgramStateRef State,
+ BinaryOperator::Opcode Op,
+ SymbolRef LHSSym,
+ SymbolRef RHSSym,
+ bool Assumption) override;
+
private:
RangeSet::Factory F;
@@ -363,13 +415,17 @@
// FIXME: Handle <=> here.
if (BinaryOperator::isEqualityOp(SSE->getOpcode()) ||
BinaryOperator::isRelationalOp(SSE->getOpcode())) {
- // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
- // We've recently started producing Loc <> NonLoc comparisons (that
- // result from casts of one of the operands between eg. intptr_t and
- // void *), but we can't reason about them yet.
+ // We handle Loc <> Loc comparisons.
if (Loc::isLocType(SSE->getLHS()->getType())) {
return Loc::isLocType(SSE->getRHS()->getType());
}
+
+ // We can handle certain NonLoc <> NonLoc comparisons, when the
+ // corresponding RangeSets are non-overlapping.
+ // We've recently started producing Loc <> NonLoc comparisons (that
+ // result from casts of one of the operands between eg. intptr_t and
+ // void *), but we can't reason about them yet.
+ return true;
}
}
@@ -755,6 +811,64 @@
return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
}
+Optional<ProgramStateRef> RangeConstraintManager::tryAssumeSymSymOp(
+ ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym,
+ SymbolRef RHSSym, bool Assumption) {
+ // FIXME: In C++20? replace with 'using RangeSet::CompareResult;'
+ using CR = RangeSet::CompareResult;
+ constexpr auto unknown = CR::unknown;
+ constexpr auto identical = CR::identical;
+ constexpr auto less = CR::less;
+ constexpr auto greater = CR::greater;
+ constexpr auto less_equal = CR::less_equal;
+ constexpr auto greater_equal = CR::greater_equal;
+
+ const auto InfeasibleState = Optional<ProgramStateRef>{nullptr};
+
+ const RangeSet LHSRange = getRange(State, LHSSym);
+ const RangeSet RHSRange = getRange(State, RHSSym);
+ const RangeSet::CompareResult Res = LHSRange.compare(RHSRange);
+
+ if (Res == unknown)
+ return llvm::None;
+
+ if (!Assumption)
+ Op = BinaryOperator::negateComparisonOp(Op);
+
+ switch (Op) {
+ case BO_LT:
+ if (Res == less)
+ return State;
+ if (Res == identical || Res == greater_equal || Res == greater)
+ return InfeasibleState;
+ assert(Res == less_equal);
+ return llvm::None;
+ case BO_GT:
+ if (Res == greater)
+ return State;
+ if (Res == identical || Res == less_equal || Res == less)
+ return InfeasibleState;
+ assert(Res == greater_equal);
+ return llvm::None;
+ case BO_LE:
+ if (Res == identical || Res == less_equal || Res == less)
+ return State;
+ if (Res == greater)
+ return InfeasibleState;
+ assert(Res == greater_equal);
+ return llvm::None;
+ case BO_GE:
+ if (Res == identical || Res == greater_equal || Res == greater)
+ return State;
+ if (Res == less)
+ return InfeasibleState;
+ assert(Res == less_equal);
+ return llvm::None;
+ default:
+ llvm_unreachable("Should not reach this with any other operators.");
+ }
+}
+
//===----------------------------------------------------------------------===//
// Pretty-printing.
//===----------------------------------------------------------------------===//
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -100,6 +100,20 @@
return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
}
+ enum class CompareResult {
+ unknown,
+ identical,
+ less,
+ less_equal,
+ greater,
+ greater_equal
+ };
+
+ // 'a < b' is true if the maximum value of 'a' is still (strictly) less than
+ // the minimum value of 'b'. The same logic applies for <=,>,>=,== operators.
+ // If there is no clear relation between the two RangeSet returns unknown.
+ CompareResult compare(const RangeSet &other) const;
+
private:
void IntersectInRange(BasicValueFactory &BV, Factory &F,
const llvm::APSInt &Lower, const llvm::APSInt &Upper,
@@ -107,6 +121,7 @@
PrimRangeSet::iterator &e) const;
const llvm::APSInt &getMinValue() const;
+ const llvm::APSInt &getMaxValue() const;
bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const;
@@ -202,6 +217,10 @@
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+ virtual Optional<ProgramStateRef>
+ tryAssumeSymSymOp(ProgramStateRef State, BinaryOperator::Opcode Op,
+ SymbolRef LHSSym, SymbolRef RHSSym, bool Assumption) = 0;
+
//===------------------------------------------------------------------===//
// Internal implementation.
//===------------------------------------------------------------------===//
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
