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

[Manas Gupta via Phabricator via cfe-commits]

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

Rebase


Repository:
  rG LLVM Github Monorepo

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

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
@@ -293,13 +293,6 @@
     clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
   }
 
-  if (u1 > INT_MAX && u1 <= UINT_MAX / 2 + 4 && u1 != UINT_MAX / 2 + 2 &&
-      u1 != UINT_MAX / 2 + 3 && s1 >= INT_MIN + 1 && s1 <= INT_MIN + 2) {
-    // u1: [INT_MAX+1, INT_MAX+1]U[INT_MAX+4, INT_MAX+4],
-    // s1: [INT_MIN+1, INT_MIN+2]
-    clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
-  }
-
   if (u1 >= INT_MIN && u1 <= INT_MIN + 2 &&
       s1 > INT_MIN + 2 && s1 < INT_MIN + 4) {
     // u1: [INT_MAX+1, INT_MAX+1]U[INT_MAX+4, INT_MAX+4],
@@ -309,7 +302,7 @@
 
   if (s1 < 0 && s1 > -4 && u1 > UINT_MAX - 4 && u1 < UINT_MAX - 1) {
     // s1: [-3, -1], u1: [UINT_MAX - 3, UINT_MAX - 2]
-    clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
+    clang_analyzer_eval(u1 != s1); // expected-warning{{UNKNOWN}}
   }
 
   if (s1 < 1 && s1 > -6 && s1 != -4 && s1 != -3 &&
@@ -324,6 +317,11 @@
     clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
   }
 
+  if (s1 > 4 && u1 < 4) {
+    // s1: [4, INT_MAX], u1: [0, 3]
+    clang_analyzer_eval(s1 != u1); // expected-warning{{TRUE}}
+  }
+
   // Check when RHS is in between two Ranges in LHS
   if (((u1 >= 1 && u1 <= 2) || (u1 >= 8 && u1 <= 9)) &&
       u2 >= 5 && u2 <= 6) {
@@ -401,9 +399,12 @@
     clang_analyzer_eval(uch != sch); // expected-warning{{UNKNOWN}}
   }
 
+  // FIXME: Casting smaller signed types to unsigned one may leave us with
+  // overlapping values, falsely indicating UNKNOWN, where it is possible to
+  // assert TRUE.
   if (uch > 1 && sch < 1) {
-    // uch: [2, CHAR_MAX], sch: [SCHAR_MIN, 0]
-    clang_analyzer_eval(uch != sch); // expected-warning{{TRUE}}
+    // uch: [2, UCHAR_MAX], sch: [SCHAR_MIN, 0]
+    clang_analyzer_eval(uch != sch); // expected-warning{{UNKNOWN}}
   }
 
   if (uch <= 1 && uch >= 1 && sch <= 1 && sch >= 1) {
@@ -417,9 +418,10 @@
     clang_analyzer_eval(ush != ssh); // expected-warning{{UNKNOWN}}
   }
 
+  // FIXME: Casting leave us with overlapping values. Should be TRUE.
   if (ush > 1 && ssh < 1) {
     // ush: [2, USHRT_MAX], ssh: [SHRT_MIN, 0]
-    clang_analyzer_eval(ush != ssh); // expected-warning{{TRUE}}
+    clang_analyzer_eval(ush != ssh); // expected-warning{{UNKNOWN}}
   }
 
   if (ush <= 1 && ush >= 1 && ssh <= 1 && ssh >= 1) {
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1619,13 +1619,10 @@
                                                            RangeSet RHS,
                                                            QualType T) {
 
-  // We must check for empty RangeSets. This gets done via VisitBinaryOperator
-  // for other operators, but BO_NE is handled specifically.
-  if (LHS.isEmpty() || RHS.isEmpty())
-    return RangeFactory.getEmptySet();
+  assert(!LHS.isEmpty() && !RHS.isEmpty() && "Both ranges should be non-empty");
 
   if (LHS.getAPSIntType() == RHS.getAPSIntType()) {
-    if (intersect(RangeFactory, LHS, RHS) == RangeFactory.getEmptySet())
+    if (intersect(RangeFactory, LHS, RHS).isEmpty())
       return getTrueRange(T);
 
   } else {
@@ -1636,8 +1633,7 @@
     RangeSet CastedLHS = RangeFactory.castTo(LHS, CastingType);
     RangeSet CastedRHS = RangeFactory.castTo(RHS, CastingType);
 
-    if (intersect(RangeFactory, CastedLHS, CastedRHS) ==
-        RangeFactory.getEmptySet())
+    if (intersect(RangeFactory, CastedLHS, CastedRHS).isEmpty())
       return getTrueRange(T);
   }
 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D112621.481560.patch
Type: text/x-patch
Size: 3808 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20221209/44c9cec5/attachment.bin>