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.
With this patch, the solver can infer results for not equal to operator
over Ranges as well. This also fixes the issue of comparison between
different types, by first converting the RangeSets to resulting type,
which then can be used for comparisons.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D112621
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
@@ -281,3 +281,49 @@
clang_analyzer_eval((b % a) < x + 10); // expected-warning{{TRUE}}
}
}
+
+void testDisequalityRules(unsigned int u1, unsigned int u2, int s1, int s2) {
+ // Checks when ranges are not overlapping
+ if (u1 <= 10 && u2 >= 20) {
+ // u1: [0,10], u2: [20,UINT_MAX]
+ clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{TRUE}}
+ }
+
+ if (s1 <= INT_MIN + 10 && s2 >= INT_MAX - 10) {
+ // s1: [INT_MIN,INT_MIN + 10], s2: [INT_MAX - 10,INT_MAX]
+ clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{FALSE}}
+ }
+
+ // Checks when ranges are completely overlapping and have more than one point
+ if (u1 >= 20 && u1 <= 50 && u2 >= 20 && u2 <= 50) {
+ // u1: [20,50], u2: [20,50]
+ clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (s1 >= -20 && s1 <= 20 && s2 >= -20 && s2 <= 20) {
+ // s1: [-20,20], s2: [-20,20]
+ clang_analyzer_eval((s1 != s2) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ // Checks when ranges are partially overlapping
+ if (u1 >= 100 && u1 <= 200 && u2 >= 150 && u2 <= 300) {
+ // u1: [100,200], u2: [150,300]
+ clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (s1 >= -80 && s1 <= -50 && s2 >= -100 && s2 <= -75) {
+ // s1: [-80,-50], s2: [-100,-75]
+ clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{UNKNOWN}}
+ }
+
+ // Checks for ranges which are subset of one-another
+ if (u1 >= 500 && u1 <= 1000 && u2 >= 750 && u2 <= 1000) {
+ // u1: [500,1000], u2: [750,1000]
+ clang_analyzer_eval((u1 != u2) == 0); // expected-warning{{UNKNOWN}}
+ }
+
+ if (s1 >= -1000 && s1 <= -500 && s2 <= -500 && s2 >= -750) {
+ // s1: [-1000,-500], s2: [-500,-750]
+ clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{UNKNOWN}}
+ }
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -20,8 +20,8 @@
#include "llvm/ADT/FoldingSet.h"
#include "llvm/ADT/ImmutableSet.h"
#include "llvm/ADT/STLExtras.h"
-#include "llvm/ADT/StringExtras.h"
#include "llvm/ADT/SmallSet.h"
+#include "llvm/ADT/StringExtras.h"
#include "llvm/Support/Compiler.h"
#include "llvm/Support/raw_ostream.h"
#include <algorithm>
@@ -957,6 +957,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:
@@ -1231,6 +1233,26 @@
// 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 respectively, will satisfy expression (x != y).
+ if ((LHS.To() < RHS.From()) || (LHS.From() > RHS.To())) {
+ return getTrueRange(T);
+ }
+
+ // If both Ranges contain only one Point which is equal, 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 infer(T);
+}
+
template <>
RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range RHS,
QualType T) {
@@ -1721,7 +1743,6 @@
RangeSet::Factory &RangeFactory;
};
-
bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
const llvm::APSInt &Constraint) {
llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
