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

[Manas Gupta via Phabricator via cfe-commits]

manas marked 5 inline comments as done.
manas added a comment.

Considering @ASDenysPetrov 's example of `LHS = [1, 2] U [8, 9]` and `RHS = [5, 6]`, I constructed a test case as following:

`(((u1 >= 1 && u1 <= 2) || (u1 >= 8 && u1 <= 9)) && u2 >= 5 && u2 <= 6)`

but I can see that the analyzer is bifurcating paths at the OR operator. Essentially, there are two diverged paths:

1. `1 <= u1 && u1 <= 2 && 5 <= u2 && u2 <= 6`

2. `8 <= u1 && u1 <= 9 && 5 <= u2 && u2 <= 6`

Separately, they hit `VisitBinaryOperator<BO_NE>` and in both cases, we get `TRUE` for `(u1 != u2)`.

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



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1420-1421
+
+  auto ConvertedCoarseLHS = convert(CoarseLHS, ResultType);
+  auto ConvertedCoarseRHS = convert(CoarseRHS, ResultType);
+
----------------
ASDenysPetrov wrote:
> The `ResultType` of `BO_NE` is `bool`. You don't need to convert your **integer **ranges to **boolean**. Otherwise, you'll lose the information to compare. 
I have utilized castTo method for conversion of different types so that they can be compared/intersected.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1437-1441
+  if (ConvertedCoarseLHS->getConcreteValue() &&
+      ConvertedCoarseLHS->getConcreteValue() ==
+          ConvertedCoarseRHS->getConcreteValue()) {
+    return getFalseRange(T);
+  }
----------------
ASDenysPetrov wrote:
> This is OK but check `ConvertedCoarseRHS->getConcreteValue()` for `nullptr` before getting the value.
> 
I have removed the concrete case handling as it was unreachable.


================
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)) &&
----------------
@ASDenysPetrov I have used your example, but I realized that the path bifurcates and sizeof `LHS` RangeSet is always 1 inside `VisitBinaryOperator<BO_NE>`.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D112621