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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D102696#2769465 <https://reviews.llvm.org/D102696#2769465>, @NoQ wrote:

> In D102696#2767894 <https://reviews.llvm.org/D102696#2767894>, @martong wrote:
>
>>> This happens for the same reason that your patch is needed in the first place: we're eagerly substituting a constant.
>>
>> Absolutely, that's the point. On the other hand, it is very important to emphasize that we cannot solve this problem with a stronger solver, see my example with 3 variables and two equations above.
>
> Well, in that other example, we should be asking about `$x + $y + 0 == 0` at some point. And then the solver should be able to deduce it from `$x + $y + $z == 0` and `$z == 0`. If we're not asking this question, that's obviously the first problem to get out of our way.

Yeah, you are right and my analysis was not precise enough. I confirm that currently - at main - we do query `$x + $y + 0 == 0`. And the solver is incapable of solving it from the given constraints. So, yes, this patch is a "workaround" to ask the solver what does it know from the value of the verbatim expression. And this has it's limitation (see the test case for commutativity), still I think it could make the analyzer more precise.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D102696