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

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

For the test cases where we should be able to prove the case but return `Unknown` instead, should be marked by a FIXME stating the expected value.
Approximating a concrete value with `Unknown` is (almost) always correct. So, in this case, you don't need to go and fix them unless you want to do the extra mile.

The patch looks great!
And I think it's correct, but integral promotions <https://eel.is/c++draft/conv#prom> and standard conversions <https://eel.is/c++draft/conv#general-1> are always tricky.



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1627
+  if (LHS.getAPSIntType() == RHS.getAPSIntType()) {
+    if (intersect(RangeFactory, LHS, RHS) == RangeFactory.getEmptySet())
+      return getTrueRange(T);
----------------



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1638-1639
+
+    if (intersect(RangeFactory, CastedLHS, CastedRHS) ==
+        RangeFactory.getEmptySet())
+      return getTrueRange(T);
----------------



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1624
+  if (LHS.isEmpty() || RHS.isEmpty())
+    return RangeFactory.getEmptySet();
+
----------------
manas wrote:
> 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.
Let's replace it with an assertion then.


================
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}}
+  }
+
----------------
manas wrote:
> 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.
Indeed! My bad.

IDK why clang misses this. We should either ask about it on Discord (optimizations channel) or simply file a ticket asking about this. Feel free to ask them.


================
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}}
+  }
----------------
manas wrote:
> 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
Right!


================
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}}
+  }
----------------
manas wrote:
> 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
Right!


================
Comment at: clang/test/Analysis/constant-folding.c:328-332
+  if (((u1 >= 1 && u1 <= 2) || (u1 >= 8 && u1 <= 9)) &&
+      u2 >= 5 && u2 <= 6) {
+    // u1: [1, 2]U[8, 9], u2: [5, 6]
+    clang_analyzer_eval(u1 != u2); // expected-warning{{TRUE}}
+  }
----------------
steakhal wrote:
> Clang thinks it depends on the operands if `u1 != u2` is true.
> I believe, in such cases we should have returned `UNKNOWN`: https://godbolt.org/z/fxaT7YYob
Indeed correct.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D112621