[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

[via cfe-commits]

DonatNagyE wrote:

> I think we haven't discussed yet the approach of applying the constraint to every eqclass member. That would feel like defeating the purpose of eqclasses at all.

I only mentioned it because from a high-level perspective it's equivalent to applying the constraint on the eqclass representative (and acts as a "simplified description" of that approach); I don't think that we should use it as an actual implementation.

> To me, our best option so far is to keep the representative symbols alive and canonicalize (replace) all sub-symbols in constraints with representatives whenever we merge eqclasses or add constraints.

Yes, that seems to be the best way forward. It would probably imply that we introduce an "undead" (=no longer reachable, but kept as a representative) state for symbols which seems to be inelegant, but I think that it won't cause actual problems during the implementation.

https://github.com/llvm/llvm-project/pull/71284