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

[Manas Gupta via Phabricator via cfe-commits]

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

Thanks @martong and @ASDenysPetrov for the feedback. I utilized `(u != n)` to disallow bifurcation in test cases.



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1630-1631
+
+  RangeSet CastedLHS = RangeFactory.castTo(LHS, ResultType);
+  RangeSet CastedRHS = RangeFactory.castTo(RHS, ResultType);
+
----------------
ASDenysPetrov wrote:
> 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.
So I figured out that according to [C standard]( https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf#%5B%7B%22num%22%3A194%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C-27%2C816%2Cnull%5D) an expression of `x != y` has `int` as resulting type, while [C++ standard](https://isocpp.org/files/papers/N4860.pdf#subsection.7.6.10) makes it a bool. And as test file `constant-folding.c` contains tests for C, I was unintentionally casting RangeSets to `int`, and that is why those tests were passing. Do you think we should add a C++ test file, similar to `constant-folding.c` in the suite?


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1630-1631
+
+  RangeSet CastedLHS = RangeFactory.castTo(LHS, ResultType);
+  RangeSet CastedRHS = RangeFactory.castTo(RHS, ResultType);
+
----------------
manas wrote:
> ASDenysPetrov wrote:
> > 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.
> So I figured out that according to [C standard]( https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf#%5B%7B%22num%22%3A194%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C-27%2C816%2Cnull%5D) an expression of `x != y` has `int` as resulting type, while [C++ standard](https://isocpp.org/files/papers/N4860.pdf#subsection.7.6.10) makes it a bool. And as test file `constant-folding.c` contains tests for C, I was unintentionally casting RangeSets to `int`, and that is why those tests were passing. Do you think we should add a C++ test file, similar to `constant-folding.c` in the suite?
Apart from the tests, consider the example of LHS (8-bit, signed) and RHS (16-bit, unsigned).

`LHS = [-2, -1]` and `RHS = [128, 129]` which ideally should produce `LHS != RHS -> true` but after casting smaller signed type to bigger unsigned type(`CastedLHS = [128,129]`), we may have incorrect information. Should we not cast to bigger **signed** type instead of bigger **unsigned** type?

Also, I think for cases where smaller bitwidth is signed(say type `T1`), and bigger bitwidth is unsigned(say type `T2`), we should "bisect" smaller signed type rangeset into following rangesets:

`bisect(LHS) => [LHS.MinValue, LHS.MaxNegativeValueLessThanZero] U [LHS.MinPositiveValueGreaterThanEqualToZero, LHS.MaxValue]`

and we can show that, first RangeSet of above can never have an intersection with RHS(unsigned) type, so we only care about the second RangeSet in `bisect(LHS)`.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D112621