manas created this revision.
Herald added subscribers: steakhal, ASDenysPetrov, martong, dkrupp, donat.nagy,
Szelethus, mikhail.ramalho, a.sidorin, szepet, baloghadamsoftware, xazax.hun.
Herald added a reviewer: teemperor.
manas requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Prior to this, the solver was only able to verify whether two symbols
are equal/unequal, only when constants were involved. This patch allows
the solver to work over ranges as well.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D106102
Files:
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/test/Analysis/constant-folding.c
Index: clang/test/Analysis/constant-folding.c
===================================================================
--- clang/test/Analysis/constant-folding.c
+++ clang/test/Analysis/constant-folding.c
@@ -465,3 +465,41 @@
clang_analyzer_eval((c - d) > -71); // expected-warning{{FALSE}}
}
}
+
+void testEqualityRules(unsigned int a, unsigned int b, int c, int d) {
+ // Checks when ranges are not overlapping
+ if (a <= 10 && b >= 20) {
+ clang_analyzer_eval((a != b) != 0); // expected-warning{{TRUE}}
+ }
+
+ if (c <= INT_MIN + 10 && d >= INT_MAX - 10) {
+ clang_analyzer_eval((c != d) == 0); // expected-warning{{FALSE}}
+ }
+
+ // Checks when ranges are completely overlapping and have more than one point
+ if (a >= 20 && a <= 50 && b >= 20 && b <= 50) {
+ clang_analyzer_eval((a != b) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (c >= -20 && c <= 20 && d >= -20 && d <= 20) {
+ clang_analyzer_eval((c != d) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ // Checks when ranges are partially overlapping
+ if (a >= 100 && a <= 200 && b >= 150 && b <= 300) {
+ clang_analyzer_eval((a != b) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (c >= -80 && c <= -50 && d >= -100 && d <= -75) {
+ clang_analyzer_eval((c != d) == 0); // expected-warning{{UNKNOWN}}
+ }
+
+ // Checks for ranges which are subset of one-another
+ if (a >= 500 && a <= 1000 && b >= 750 && b <= 1000) {
+ clang_analyzer_eval((a != b) == 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (c >= -1000 && c <= -500 && d <= -500 && d >= -750) {
+ clang_analyzer_eval((c != d) == 0); // expected-warning{{UNKNOWN}}
+ }
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -952,6 +952,8 @@
RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode Op,
RangeSet RHS, QualType T) {
switch (Op) {
+ case BO_NE:
+ return VisitBinaryOperator<BO_NE>(LHS, RHS, T);
case BO_Or:
return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
case BO_And:
@@ -1218,6 +1220,27 @@
// Range-based reasoning about symbolic operations
//===----------------------------------------------------------------------===//
+template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(Range LHS, Range
RHS,
+ QualType T) {
+
+ // When both the ranges are non-overlapping then all possible pairs of (x, y)
+ // in LHS, RHS will satisfy expression (x != y)
+ if ((LHS.To() < RHS.From()) || (RHS.To() < LHS.From())) {
+ return getTrueRange(T);
+ }
+
+ // If both ranges contain only one same Point then the expression will always
+ // return true
+ if ((LHS.From() == RHS.To()) && (LHS.To() == RHS.To()) &&
+ (LHS.From() == RHS.From())) {
+ return getFalseRange(T);
+ }
+
+ // In all other cases, the resulting range cannot be deduced.
+ return RangeFactory.getEmptySet();
+}
+
template <>
RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range
RHS,
QualType T) {
Index: clang/test/Analysis/constant-folding.c
===================================================================
--- clang/test/Analysis/constant-folding.c
+++ clang/test/Analysis/constant-folding.c
@@ -465,3 +465,41 @@
clang_analyzer_eval((c - d) > -71); // expected-warning{{FALSE}}
}
}
+
+void testEqualityRules(unsigned int a, unsigned int b, int c, int d) {
+ // Checks when ranges are not overlapping
+ if (a <= 10 && b >= 20) {
+ clang_analyzer_eval((a != b) != 0); // expected-warning{{TRUE}}
+ }
+
+ if (c <= INT_MIN + 10 && d >= INT_MAX - 10) {
+ clang_analyzer_eval((c != d) == 0); // expected-warning{{FALSE}}
+ }
+
+ // Checks when ranges are completely overlapping and have more than one point
+ if (a >= 20 && a <= 50 && b >= 20 && b <= 50) {
+ clang_analyzer_eval((a != b) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (c >= -20 && c <= 20 && d >= -20 && d <= 20) {
+ clang_analyzer_eval((c != d) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ // Checks when ranges are partially overlapping
+ if (a >= 100 && a <= 200 && b >= 150 && b <= 300) {
+ clang_analyzer_eval((a != b) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (c >= -80 && c <= -50 && d >= -100 && d <= -75) {
+ clang_analyzer_eval((c != d) == 0); // expected-warning{{UNKNOWN}}
+ }
+
+ // Checks for ranges which are subset of one-another
+ if (a >= 500 && a <= 1000 && b >= 750 && b <= 1000) {
+ clang_analyzer_eval((a != b) == 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (c >= -1000 && c <= -500 && d <= -500 && d >= -750) {
+ clang_analyzer_eval((c != d) == 0); // expected-warning{{UNKNOWN}}
+ }
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -952,6 +952,8 @@
RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode Op,
RangeSet RHS, QualType T) {
switch (Op) {
+ case BO_NE:
+ return VisitBinaryOperator<BO_NE>(LHS, RHS, T);
case BO_Or:
return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
case BO_And:
@@ -1218,6 +1220,27 @@
// Range-based reasoning about symbolic operations
//===----------------------------------------------------------------------===//
+template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(Range LHS, Range RHS,
+ QualType T) {
+
+ // When both the ranges are non-overlapping then all possible pairs of (x, y)
+ // in LHS, RHS will satisfy expression (x != y)
+ if ((LHS.To() < RHS.From()) || (RHS.To() < LHS.From())) {
+ return getTrueRange(T);
+ }
+
+ // If both ranges contain only one same Point then the expression will always
+ // return true
+ if ((LHS.From() == RHS.To()) && (LHS.To() == RHS.To()) &&
+ (LHS.From() == RHS.From())) {
+ return getFalseRange(T);
+ }
+
+ // In all other cases, the resulting range cannot be deduced.
+ return RangeFactory.getEmptySet();
+}
+
template <>
RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range RHS,
QualType T) {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
