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

[Gabor Marton via cfe-commits]

martong wrote:

> it'd be good to "strengthen" the equality classes and ensure that we assign the same RangeSet to each member of an EQClass (or, in other words, we assign the RangeSet to an EQClass instead of an individual symbol).

RangeSets (i.e. constraints) are assigned to EQClasses, checkout the State's `ConstraintRange`. So this is something that we have since EQClasses have been introduced. Now, you wonder why do we have then this miserable confusion? The problem starts at how we search for a constraint. We build a symbol and then we try to find it's EQClass, and via the class we will get the Range. The crux of the problem lies in building up that symbol in SValBuilder.
```
1  if (x != y) return; // x == y
2  if (z <= x) return; // z > x
3  if (z >= y) return; // z < y
```
At 3, we build `z < y` which is a completely new symbol, never seen before, we won't find an EQClass for it. Had we built `z < x` , we still would not find the EQClass. This is the reason for checking for reversed comparisons (see `getRangeForComparisonSymbol`). So, an alternative solution could be to patch this search (i.e the RangeInferrer) to be able to find the EQClass. This would have it's own complexity (would you want to search for reversed comparisoins as well for each EQClass member, etc). Also, there is the subtle problem of the eager simplification in SValBuilder: once a symbol is simplified, there is no easy way to build the original non-simplified symbol which has the constraint associated to it. E.g. after having an `assert(z == 1)` in the running example, you cannot query the range anymore for `z < y` , but only for `1 < y`.

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