[PATCH] D140086: [analyzer][solver] Improve reasoning for not equal to operator

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

steakhal requested changes to this revision.
steakhal added a comment.
This revision now requires changes to proceed.

>>> Bitwidth was important because we should ideally cast smaller bitwidth type to bigger bitwidth type.
>>> Consider if we have LHS(u8), RHS(i32), then without checking for bitwidth, we would be casting RHS's maxValue to LHS's type, which will result in lose of information and will not serve our purpose.
>>
>> If you think we need that bitwidth check, why did you remove it?
>> I'd like to see test cases demonstrating what we are talking about and see if we want that behavior or not.
>
> This test fails.
>
>   void testfoo(unsigned char u, signed int s) {
>     if (u >= 253 && u <= 255 && s < INT_MAX - 2) {
>       // u: [253, 254], s: [INT_MIN, INT_MAX - 2]
>       clang_analyzer_eval(u != s); // expected-warning{{UNKNOWN}}
>                                    // but returns TRUE
>     }
>   }

I feel like we have something to talk about.
When I do the review pro bono, I'd like to focus on higher-level issues and let the submitter deal with the smaller concerns.
That's why I'm expecting the submitter to:

- Explain in the summary what the patch aims to solve (aka. why did your work on it)
- What & how it implemented it
- What obstacles you had when you tried to implement it? Because the reviewer will most likely think the same way, it's better to highlight what you tried and why you failed that way.
- Most importantly, attach the test cases you uncovered during development about the edge-cases of the previous point.

I'm also expecting that the change compiles, works, and is well-tested. This generally means that tests are covering all the branches in the modified parts and the change runs and are capable of analyzing non-trivial projects without crashing or producing unacceptable reports.
In particular, the `Core` and the range-based solver are the foundation of the engine, hence even more rigorous testing is required, so correctness is a must in these contexts.

Coming back to this review, I don't want to validate the correctness of the math. I trust you to do this, which you prove by tests or (Z3 solution in addition to that).
Getting more concrete, returning `Unknown` is fine, but returning the wrong answer like `True` for cases where we should not be able to deduce it, it's a serious issue.

I hope it helps to align us.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D140086