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

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

In D102696#2773304 <https://reviews.llvm.org/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 about symbolic expressions by constraints these symbolic expressions are actually part of (right now we can reason about expressions if we know some information about its own parts aka operands)?
>
> Well, it is a hard question.
> I've been thinking about building a "parent" map for the sub-expressions, like we do in the AST (see clang::ParentMap). We could use this parent map to inject new constraints during the "constant folding" mechanism.
> So, let's say we have `$x + $y = 0` and then when we process `$y = 0` then we'd add a new constraint: `$x = 0`. We could add this new constraint by knowing that we have to visit `$x + $y` because `$y` is connected to that in the parent map.
> What do you think, could it work?

Yes, this was exactly my line of thinking.  Instead of trying to use hard logic every time we are asked a question, we can try to simplify existing constraints based on the new bit of information.
The main problem with this is the tree nature of symbolic expressions.  If we have something trivial like `$x + $y` - sure.  But something with lot more nested subexpressions can get tricky really fast.  That can be solved if we have a canonical form for the trees (this will resolve the problem with `$x + $y` versus `$y + $x` as well).  Right now, we have bits of this all around our codebase, but those are more like workarounds as opposed to one general approach.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D102696