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

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

In D112621#3660256 <https://reviews.llvm.org/D112621#3660256>, @manas wrote:

> Is there any other way to formulate the expression so that it constructs `LHS = [1, 2] U [8, 9]` and doesn't bifurcate?

Try this `u1 > 0 && u1 < 10 && u1 != 3 && u1 != 4 && u1 != 5 && u1 != 6 && u1 != 7 && u2 > 4 && u2 < 7`. This is a bit verbose but it will avoid bifurcating.



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1624-1626
+  if (LHS.isEmpty() || RHS.isEmpty()) {
+    return RangeFactory.getEmptySet();
+  }
----------------
Syntax: We usually don't use braces for single-line statements.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1630-1631
+
+  RangeSet CastedLHS = RangeFactory.castTo(LHS, ResultType);
+  RangeSet CastedRHS = RangeFactory.castTo(RHS, ResultType);
+
----------------
And again. This is incorrect to cast your `un/signeds` to `bool`.
First, `castTo` currently does not support this operation correctly AFAIR (My fault. I'll add the support later). And thus, I've no idea why your tests pass.
Second, you will get from e.g. `u32[1,9]`  -  `bool[1,1]` and from `i32[42, 45]` - `bool[1,1]`. Then `bool[1,1]` would be equal to `bool[1,1]`, but it shouldn't in terms of `u/i32`.

Here you should emulate the behavior of C++ abstract machine, hence cast both to the biggest type or unsigned one.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1633-1636
+  if (CastedLHS == RangeFactory.getEmptySet() ||
+      CastedRHS == RangeFactory.getEmptySet()) {
+    return infer(T);
+  }
----------------
`castTo` won't produce you empty RangeSets unless the originals were already empty, but we checked for this previously.  So, you don't need this check.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1415-1416
+
+  Range CoarseLHS = fillGaps(LHS);
+  Range CoarseRHS = fillGaps(RHS);
+
----------------
manas wrote:
> ASDenysPetrov wrote:
> > Avoid filling the gaps, because it's completely possible to compare all the ranges.
> > E.g. //LHS //`[1,2]U[8,9]`  and  //RHS //`[5,6]` are not equal.
> > And you don't need to fiil the gap in LHS, because it will lead you to a wrong answer, like `[1,9] != [5,6]` => **UNKNOWN** instead of **TRUE**.
> If we don't fill gaps, then we will be making this method O(n) instead of O(1) as of now. As I see it, filling RHS (and not filling LHS), it can iterate over all ranges in LHS, and check each range's intersection with CoarseRHS.
> 
> Before, I do this, I just wanted to point out the unreachability of concrete cases to this method. I have tried to explain this below.
Here I'd rather get a correct result and wait a bit then contra-versa.


================
Comment at: clang/test/Analysis/constant-folding.c:289
+
+  // Check when RHS is in between two Ranges in LHS
+  if (((u1 >= 1 && u1 <= 2) || (u1 >= 8 && u1 <= 9)) &&
----------------
manas wrote:
> @ASDenysPetrov I have used your example, but I realized that the path bifurcates and sizeof `LHS` RangeSet is always 1 inside `VisitBinaryOperator<BO_NE>`.
Just do as I advised in the main comment.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D112621