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

[Balazs Benics via cfe-commits]

steakhal 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

It wasn't actually what I had in mind. I wanted to assign constraints to canonicalized symexprs instead of to the symexpr the API gets from the assume call. And for lookups, we would again do the same thing, canonicalize and only then do the lookup - or let the lookup (rather infer do the canonicalization on the fly). So to be explicit, no other component would know what canonicalization happens within the range-based solver.

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