Add short-circuit optimization for `leq` to `HConsed`

[jerhard]

Values that are physically equal or, for HConsed have the same tag, are also leq. We should exploit this by implementing a short-circuiting version of leq for HConsed.

[sim642]

I suppose it could also allow optimizing self joins and meets, although I'm not sure how often those really happen. Needs benchmarking to be sure.

[vogler]

There's some numbers for physical equality in https://github.com/goblint/analyzer/tree/master/bench/hashcons I still don't know why it doesn't do a == b || a = b for a = b by default.

[sim642]

There's some numbers for physical equality in https://github.com/goblint/analyzer/tree/master/bench/hashcons I still don't know why it doesn't do a == b || a = b for a = b by default.

That benchmark only checks the good case though, where a == b is always true. It doesn't check the bad case, where it's false and an extra branch has been missed. Not sure if that would change anything, but physical non-equality is probably much more frequent.

Also that applies to just the polymorphic comparison. If that actually would be an optimization, it would also have to be added into (non-primitive) cases of the derived equal and compare.

[sim642]

By the way, other operations like join could also be optimized: if the arguments are equal (based on hashconsed tags), then directly return (either) argument. Currently I think we call the inner joining (which can go very deep to do pointless idempotent joins) just to hashcons the result at the end to a value equal to the argument.

[michael-schwarz]

Is this maybe a good first improvement for the students working on the pratical to get familiar with our code base and benchmarking Goblint @jerhard ?

[jerhard]

Yes, that looks like a good starting point.

[michael-schwarz]

The students have unfortunately not investigated this in the practical, I will make some experiments.