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

vsavchenko added a comment. I just noticed that I simply forgot to click submit yesterday  Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D102696/new/ https://reviews.llvm.org/D102696 ___ cfe-commits

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

vsavchenko added a comment. Oh, wow. Great plan! I'd like to participate.  I have a few comments: > Alright, I see your point. I agree that solving the problem of "$a +$b +$c > constrained and then $a + $c got constrained" requires canonicalization. That was actually not an example for

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

martong abandoned this revision. martong added a comment. Abandoning in favor of https://reviews.llvm.org/D103314 https://reviews.llvm.org/D103317 Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D102696/new/ https://reviews.llvm.org/D102696

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

martong added a comment. Alright, I see your point. I agree that solving the problem of "$a +$b +$c constrained and then $a + $c got constrained" requires canonicalization. However, canonicalization seems to be not trivial to implement. And there are some other easier cases that I think we could

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

vsavchenko added a comment. In D102696#2774169 , @martong wrote: > In D102696#2773340 , @vsavchenko > wrote: > >> In D102696#2773304 , @martong >> wrote: >> As for

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

steakhal added a comment. I think It would be also beneficial to document the semantics. Whenever we say `$x + $y` it's not entirely clear whether we talk about the addition operation in a mathematical sense or we follow C/C++ language semantics. Right now it's mostly mixed within the

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

martong added a comment. In D102696#2773340 , @vsavchenko wrote: > In D102696#2773304 , @martong wrote: > >>> As for the solver, it is something that tormented me for a long time. Is >>> there a way to avoid a

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

vsavchenko added a comment. In D102696#2773304 , @martong wrote: >> As for the solver, it is something that tormented me for a long time. Is >> there a way to avoid a full-blown brute force check of all existing >> constraints and get some knowledge

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

martong added a comment. > As for the solver, it is something that tormented me for a long time. Is > there a way to avoid a full-blown brute force check of all existing > constraints and get some knowledge about symbolic expressions by constraints > these symbolic expressions are actually

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

martong added a comment. In D102696#2769465 , @NoQ wrote: > In D102696#2767894 , @martong wrote: > >>> This happens for the same reason that your patch is needed in the first >>> place: we're eagerly

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

martong added a comment. In D102696#2768857 , @vsavchenko wrote: > My take on this: for whatever approach, we definitely will be able to > construct a more nested/complex example so that it doesn't work. > For this patch, I'm wondering about something

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

martong updated this revision to Diff 346966. martong added a comment. - Add test case for commutativity - Add test case for Valeriy's case Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D102696/new/ https://reviews.llvm.org/D102696 Files:

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

NoQ added a comment. In D102696#2767894 , @martong wrote: >> In this case the equations are $y == 0 and $x + 0 == 0 which is much easier >> to solve. > > Yes, you are right. > >> This happens for the same reason that your patch is needed in the first

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

vsavchenko added a comment. My take on this: for whatever approach, we definitely will be able to construct a more nested/complex example so that it doesn't work. For this patch, I'm wondering about something like this: int foo() { if (z != 0) return 0; if (x + y + z != 0)

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

martong added a comment. > In this case the equations are $y == 0 and $x + 0 == 0 which is much easier > to solve. Yes, you are right. > 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

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

NoQ added a comment. In D102696#2766765 , @martong wrote: > In 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

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

martong added a comment. In 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

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

NoQ added a comment. 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.

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

martong created this revision. martong added reviewers: steakhal, NoQ, vsavchenko. Herald added subscribers: ASDenysPetrov, gamesh411, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun, whisperity. Herald added a reviewer: Szelethus.