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

[Manas Gupta via Phabricator via cfe-commits]

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) {


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