[PATCH] D103317: [Analyzer][engine][solver] Simplify complex constraints

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

In D103317#2793911 <https://reviews.llvm.org/D103317#2793911>, @ASDenysPetrov wrote:

> In D103317#2793797 <https://reviews.llvm.org/D103317#2793797>, @vsavchenko wrote:
>
>> Hmm, Okay, but what about situations if you have: `a = a1 + a2` and `a = a3 + a4 + a5` are you going to throw away one of these constraints? And if so, how do you want to select which one?
>
> Are you talking about comparison or assignment? Both assignments can't be valid at the same time, and latter replaces bindings of former. In case of comparisons, they both can be valid.
> But we should keep in mind that **assignment** is a //write// operation which replaces and invalidates previous bindings, and **comparison** is a //read// operation. It can add new bindings but can not remove old ones.
> This is what I haven't dig deep enough yet. Let's do this together how we can handle that.

I replied to you earlier that assignments are not producing constraints.  The analyzer has some sort of SSA (not really, but anyways), so every time we reassign the variable it actually becomes a different symbol. So, from this perspective `DeclRefExpr` `x` and symbol `x` are two different things:

  int x = foo(); // after this DeclRefExpr and VarDecl x are associated with conjured symbol #1 (aka conj#1)
  int c = x + 10; // c is associated with `$conj#1 + 10`
  x = a + 1; // DeclRefExpr x is now associated with `$a + 1`
  x = c + x; // and now it is `conj#1 + 11`

There is no symbolic assignment in the static analyzer.  Symbols are values, values don't change.  We can only obtain more information of what particular symbolic value represents.

I hope it makes it more clear.

As for equality, we already track equivalence classes of symbols and they can have more than 2 symbols in them.  Actually, this whole data structure mostly makes sense for cases when the class has more than 2 elements in it.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103317