[michael-schwarz]

Closes #2307.

I think this may be worth having for SV-COMP, it can in principle improve results for everything that uses the GenPMap.

[sim642]

It's a very good idea to fix these hash functions that have annihilators.

I haven't benchmarked this but I think we consistently should go with the 31 * x + y pattern: even though it's not the world's best hash function, we've used it in many places and it's now also what ppx_deriving_hash does.

Hashtbl.hash (x, y) is convenient for reusing the standard OCaml hash function but it allocates the pair and calls GC: https://godbolt.org/z/1467xaz6K (even with flambda there, Hashtbl.hash is implemented in C, so no amount of OCaml optimization can help). It could contribute to issues like ocaml/ocaml#13733 (comment) that equal/compare/hash allocate even though there's no reason to.

EDIT: hash allocating can be notable overhead in some (program analysis) applications at least: sim642/ppx_deriving_hash#7 (and ppx_deriving_hash isn't fully avoiding them currently either: sim642/ppx_deriving_hash#9).

[michael-schwarz]

Is it maybe worth to roll our own hash combination function here that inlines what ocaml does for it's in Ocaml code (which will hopefully not allocate)? Perhaps as a follow-up PR.

[sim642]

ppx_deriving_hash already includes the 31 * x + y one, which is essentially inlined everywhere, instead of being called (even as an OCaml function).
We could also just do [%hash: int * int] (x, y), which compiles down to the same assembly as 31 * x + y. Although it's a bit uglier than necessary, perhaps I should just expose [%hash_reduce] x y from ppx_deriving_hash as well.

what ocaml does for it's in Ocaml code

I'm not sure what you mean by that.
But if we want to improve the hash combination we should do it in ppx_deriving_hash to benefit all across the board, not in a handful of hand-written instances in Goblint.

ppx_deriving_hash currently doesn't have a way to configure the generated hash functions, but I should come up with a way. I've even thought about implementing the Hashtbl.hash algorithm there but I don't know how doable that is.

[michael-schwarz]

I used the proposed approach everywhere now. @sim642: If it looks good I'd like to merge in time for the weekly to see if it has any SV-COMP impact.

[michael-schwarz]

But if we want to improve the hash combination

Yeah, we could even thing of using the murmur3 package from OPAM.