[PATCH] D102696: [Analyzer] Find constraints that are directly attached to a BinOp

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In D102696#2766765 <https://reviews.llvm.org/D102696#2766765>, @martong wrote:

> In D102696#2766337 <https://reviews.llvm.org/D102696#2766337>, @NoQ wrote:
>
>> Ok so the state has enough constraints. It's enough to know that `$x + $y == 0` and `$y == 0` in order to deduce that `$x + 0 == 0`. But you're saying that we don't know how to infer it so instead of making us able to infer it let's make us ask the solver easier questions. That's a terrible hack but at this point i think we might as well take it. @vsavchenko WDYT, what would it take to fix the solver instead?
>
> Actually, the problem is more subtle than that. The solver is already capable of solving such equations, the below test passes on the main branch:
>
>   int test(int x, int y) {
>     if (y != 0)
>       return 0;
>     if (x + y != 0)
>       return 0;
>     clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
>     clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
>     clang_analyzer_eval(x == 0);     // expected-warning{{TRUE}}
>     return 0;
>   }

In this case the equations are `$y == 0` and `$x + 0 == 0` which is much easier to solve. This happens for the same reason that your patch is needed in the first place: we're eagerly substituting a constant.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D102696