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

[Manas Gupta via Phabricator via cfe-commits]

manas updated this revision to Diff 375689.
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
@@ -21,8 +21,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>
@@ -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:
@@ -1029,6 +1031,27 @@
     return infer(T);
   }
 
+  template <>
+  RangeSet VisitBinaryOperator<BO_NE>(RangeSet LHS, RangeSet RHS, QualType T) {
+    // When both the RangeSets are non-overlapping then all possible pairs of
+    // (x, y) in LHS, RHS respectively, will satisfy expression (x != y).
+    if ((LHS.getMaxValue() < RHS.getMinValue()) ||
+        (LHS.getMinValue() > RHS.getMaxValue())) {
+      return getTrueRange(T);
+    }
+
+    // If both RangeSets contain only one Point which is equal then the
+    // expression will always return true.
+    if ((LHS.getMinValue() == RHS.getMaxValue()) &&
+        (LHS.getMaxValue() == RHS.getMaxValue()) &&
+        (LHS.getMinValue() == RHS.getMinValue())) {
+      return getFalseRange(T);
+    }
+
+    // In all other cases, the resulting range cannot be deduced.
+    return infer(T);
+  }
+
   /// Return a symmetrical range for the given range and type.
   ///
   /// If T is signed, return the smallest range [-x..x] that covers the original


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D106102.375689.patch
Type: text/x-patch
Size: 3566 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210928/0340bbfc/attachment.bin>