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

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to