I now enforced MapDomain signatures and extracted OptHash into a functor to be just used for CPA. To my surprise, this can make CPA.hash a few times slower, which isn't great news.

Considering our heavy use of functors, maybe flambda would help a lot, especially if one level of functor can make such a difference.

I now tried hashconsing instead of my hash-caching. Obviously it makes equal and hash instant even on large maps, but all the slow hash computation is just shifted to the lift. Overall, this is much slower due to patterns like using add in a fold-loop to construct a new map: every intermediate add recalculates the hash slowly to lift the result. So hashconsing isn't actually the answer here!

Well, it may be the answer if we didn't use the add in a fold-loop pattern. I think we have often done that to combine filtering and mapping while avoiding the intermediate result between filter and map, whereas filter_map (if it were available on MapDomain) might be more appropriate. Although changes like this likely won't solve all the cases: sometimes such loops are over other data structures.

Another idea might be to combine the two approaches to get some kind of lazy hashconsing, which would only hashcons maps that hash is calculated on. It would avoid the slowdown of add in fold-loops as the map itself isn't hashed in such case intermediately. But it might further improve equal performance by replacing the still slow equal comparison (when not physically equal) with a comparison of tags. There are more cases there though, e.g. when calling equal with one hashconsed and one non-hashconsed map.

This has been sitting in the sidelines for now, but I think I'll have to see how this affects the newer heavy privatizations. I suppose they still can keep quite big CPAs around.

My biggest worry with this PR, is that the stricter interfacing of MapDomains broke the compilation of PathSensitive3 in witness generation, because it used the internals of a lifted map. Although I fixed it to at least compile, it's very probable that there things don't behave right anymore and witness generation would be broken. And for the time being, I don't really want to spend time trying to test and possibly fix it.

Here's a comparison on some benchmarks from goblint/bench that shows how more involved privatizations (global-history, mine-W, mine-lazy, mine-global) get around 50% time improvement just from this change.

Before

After