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

[Manas Gupta via Phabricator via cfe-commits]

manas marked 2 inline comments as done.
manas added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1624
+  if (LHS.isEmpty() || RHS.isEmpty())
+    return RangeFactory.getEmptySet();
+
----------------
steakhal wrote:
> This branch is uncovered by tests.
(Un)fortunately, empty rangesets don't go into `VisitBinaryOperator` at all. They are pre-checked and handled accordingly. I don't see any reasons not to remove this branch altogether.


================
Comment at: clang/test/Analysis/constant-folding.c:289-301
+  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}}
+  }
+
----------------
steakhal wrote:
> These two hunks seem to be the same. We should probably keep one.
> In addition to that, clang thinks the answer for `u1 != s1` depends on the operands.
> We should probably return `UNKNOWN` for such cases. https://godbolt.org/z/aG1oY5Mr4
My bad. Removed one hunk.

clang is unable to optimize but gcc does (https://godbolt.org/z/8TaaYa4M9). Is it something the llvm optimizer has not been fullfilling for now? Because to me, it looks fine as LHS and RHS cannot have any APSInt in common, so they will always be unequal in all possible scenarios.


================
Comment at: clang/test/Analysis/constant-folding.c:315-319
+  if (s1 < 1 && s1 > -6 && s1 != -4 && s1 != -3 &&
+      u1 > UINT_MAX - 4 && u1 < UINT_MAX - 1) {
+    // s1: [-5, -5]U[-2, 0], u1: [UINT_MAX - 3, UINT_MAX - 2]
+    clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
+  }
----------------
steakhal wrote:
> Clang thinks it depends on the operands if `u1 != s1` is true.
> https://godbolt.org/z/Pf3eYKnzd
clang is unable to optimize while gcc can. https://godbolt.org/z/zoe8ddqh4


================
Comment at: clang/test/Analysis/constant-folding.c:321-325
+  if (s1 < 1 && s1 > -7 && s1 != -4 && s1 != -3 &&
+      u1 > UINT_MAX - 4 && u1 < UINT_MAX - 1) {
+    // s1: [-6, -5]U[-2, 0], u1: [UINT_MAX - 3, UINT_MAX - 2]
+    clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}
+  }
----------------
steakhal wrote:
> Clang thinks it depends on the operands if `u1 != s1` is true.
> https://godbolt.org/z/1YYcd1EY8
clang can't optimize but gcc can. https://godbolt.org/z/hnahWPacr


================
Comment at: clang/test/Analysis/constant-folding.c:404-407
+  if (uch > 1 && sch < 1) {
+    // uch: [2, CHAR_MAX], sch: [SCHAR_MIN, 0]
+    clang_analyzer_eval(uch != sch); // expected-warning{{UNKNOWN}}
+  }
----------------
steakhal wrote:
> Shouldn't it print `TRUE`?
> Clang will optimize this to `return true`. https://godbolt.org/z/6c6EPYofY
> We should probably conclude the same here.
Yes, it ideally should be true. But current implementation is unable to figure that out. I will try to solve it differently.

The unknown cases are like this: bigger(or equal) bitwidth(say `LHS`) is unsigned and smaller(or equal) bitwidth(`RHS`) is signed, now if we cast `RHS` to `LHS` type, then all negative values in `RHS` will overlap with positive values of `LHS`, leading us to believe some values may overlap.

In this example, `uch: [2, CHAR_MAX], sch: [SCHAR_MIN, 0]`, when we cast `sch` (signed) to unsigned char type, then we get overlapping values between `casted_sch` and `uch`.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D112621