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

[Gábor Horváth via cfe-commits]

Xazax-hun wrote:

> So, if I understand you correctly, at the 3rd if statement, we should canonicalize the symbol we are constraining by walking every sub-symbol and substituting it with its equivalent counterpart (if any), by basically with its eqclass' representative symbol.

I am not 100% sure if I'd go that far (doing canonicalization). Symbols carry a lot of information, like provenance. Bug reporters, or maybe even some custom checker state might rely on this. I am afraid that replacing/rewriting like that might have unexpected consequences, nothing we cannot solve, but I am not sure whether we want to solve them. What I'd suggest is more like always adding all the constraints to the representative, and lazily propagating those constraints to the other members of the equivalence classes, only when we mention them in a constraint.

This might also be challenging for bug reporters to explain in some scenarios, but at least we preserve the provenance information. 

@steakhal

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