[PATCH] D106102: [analyzer][solver] Introduce reasoning for not equal to operator

[Manas Gupta via Phabricator via cfe-commits]

manas updated this revision to Diff 374746.
manas added a comment.

Rebase


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D106102/new/

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
@@ -466,3 +466,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
@@ -956,6 +956,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:
@@ -1226,6 +1228,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) {


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D106102.374746.patch
Type: text/x-patch
Size: 3316 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210924/4f871973/attachment.bin>