tweak GC in OCaml bindings

[c-cube]

at Imandra we've had issues with recent versions of OCaml, where Z3 objects wouldn't be collected and would accumulate in RAM, eventually taking multiple GBs. There's some related issues for .NET I believe. This patch uses a different version of custom blocks (OCaml heap values that wrap foreign objects, such as a Z3 solver, expr, or context) with more explicit resource limits. I've hand picked limits that seem reasonable but it's subject to discussion. Pinging @ivg if he's interested.

[c-cube]

This actually requires OCaml >= 4.08 to benefit from the new allocation function.

[wintersteiger]

Conceptually this seems like a good idea, but I'd add some way for applications to tweak those numbers without making changes to the API code. I'm also slightly concerned that this breaks compatibility with older versions of OCaml, which may be a problem for some existing projects.

Minor: Why the change to Ubuntu 20? Does this hint at the fact that it won't work on Ubuntu 18 anymore? Also, I don't know what the guarantees of GC.finalise are, but in other systems (like .NET) this does not mean that an object is actually finalised at the request time (or indeed at all).

[c-cube]

@wintersteiger the Ubuntu 20.04 is just because it seems to use the system OCaml, which is 4.05 on Ubuntu 18.04 if I read the logs correctly.

I agree it's unfortunate to require a more recent OCaml, but at the same time the most recent version is 4.13 already. This change is important to us because we want to move to 4.12 from 4.08 and the default GC behavior on 4.12 makes Z3 bindings a giant memory leak. 4.08 is a very stable version which brought a lot of new features people have come to depend on, so I think it's fine to establish it as a lower bound if it means people using more recent versions of OCaml can use Z3 at all.

The finalizer seemed useful in local tests to keep RAM low. The interplay between OCaml finalizers (beeing called in a arbitrary order) and internal Z3 cleaning with refcountings is highly non trivial, so I'm not sure what's up. This ensures that the deletion code is run at least once at the moment the corresponding object is collected.

[NikolajBjorner]

If this works with you, very good.
These structures have shared sub-structures so their sizes aren't static. This can't be a unique problem to z3, but the size estimate interface I have seen so far (OCaml, .Net) are not equipped with some corresponding feature that would notify the gc.

For early projects such as Pex, we got much better performance by not relying on the GC.
It is then the client responsibility to not have any references to terms that are created within a scope.
Having the GC manage reference counts is a convenience, but anything that expects predictable behavior may as well manage their own regions (and lacking the grace of region type systems to provide guarantees, good luck debugging dangling pointers).

[c-cube]

Ah well, I was still working on fine tuning it, I'll probably open a second PR. Sadly it's difficult in OCaml to perform manual memory management so we're stuck with the GC.

Unless there is a way we can modify the bindings to make this easier. I can imagine, for example, having a level of indirection internally, where there's a context_option object that is used everywhere (instead of having a direct pointer to the context), so that expressions, solvers, etc. only deallocate the context if it's not null. But maybe that's not compatible with how expressions are deallocated (if they truly need the context, to find subterms, say).

Another way would be to have an explicit notion of "region" where the context and solver and expressions would live, so we can deallocate them all at once.

[NikolajBjorner]

Just open another PR.

The bare bones C API has it that expressions are pointers without pointers to contexts.
Contexts maintain hash-tables of expressions so need the reference decrement to point to a context. This is consistent with how dec_ref is exposed over the API, where it takes a context argument.

The "region" notion is already there in one way: you can allocate a context in a mode where expression lifetimes come with the context.

[c-cube]

Just open another PR.

I will!

The "region" notion is already there in one way: you can allocate a context in a mode where expression lifetimes come with the context.

In that case, what I can use to refer to an expression through a context? Is there an integer key or something like that? That would be optimal for me.