Add PPX derivers for lattices of tuple and record types

[sim642]

This implements a big portion of #31 using my experimental ppx_easy_deriving library (EDIT: Necessary parts are now just vendored here for simplicity). The goal of the library is to provide a simpler ppx_type_directed_value-like interface with no performance penalty.
It is a revival of my two-year-old ppx-lattice branch in more polished state.

This PR changes record-valued domains to use [@@deriving lattice] and also changes the implementation of Lattice.Prod to do so. Over time, the amount of Lattice.Prod usage could be reduced by using records with meaningful field names instead.

TODO

• Publish ppx_easy_deriving on opam. Vendored.
• Fix opam pin in CI. Vendored.
• Derive pretty_diff. Needs leq to define pretty_diff.
• Check ppxlib best practices.
• Benchmark.
• Investigate outliers.

[jerhard]

At the Gobcon today you mentioned that there could be another attempt at this by you on this, that would be easier to maintain. Could you have a look, whether this indeed exists?

[sim642]

I did a sv-benchmarks run with 60s timeout and here's the CPU time before vs after plot:

On average there's no change to performance but there are some outliers (in both directions!)

All verdict changes except one are close to timeout jitter. One true changes into a quick OUT OF MEMORY which is odd.

I might try looking into some of the biggest outliers before clicking merge.

[sim642]

All verdict changes except one are close to timeout jitter. One true changes into a quick OUT OF MEMORY which is odd.

This task is c/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--input--joystick--turbografx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i. Running with -v to see OCaml allocation stats actually shows the memory usage being lower now. This might've just been that slight changes cause GC to trigger a bit later now and there's a moment with higher memory usage.

[sim642]

On average there's no change to performance but there are some outliers (in both directions!)

One of the biggest improvements (2× in time) is on /c/hardware-verification-bv/btor2c-lazyMod.driving_phils.5.prop1-func-interl.c where also the allocated memory amount is halved. This is actually orthogonal to the new deriver: it's just because in this PR I've also replaced the IntDomain hash function with a derived one, which seems to have this huge effect. Maybe the hand-written one has too many collisions or temporary stuff.

In others, e.g. c/goblint-regression/28-race_reach_71-funloop_racing.i there's a slowdown 29s → 36s, which seems to be due to the same hash change. So there seems to be surprisingly large variation in runtime from a single hash function. This might need a separate investigation.