Z3's logical context is leaked

[qaristote]

Following (and as discussed in) #154, Pirouette does its SMT solving by inline-C-calling a binding from Z3's API, Z3_eval_smtlib2_string. This function expects a Z3_context, a C struct which we deal with in Haskell by maintaining a pointer. As such, it is not handled by Haskell's GC: only the pointer is garbage-collected. It must thus be freed manually, be inline-C-calling the binding Z3_del_context.

As of now, this is simply not taken care of, and the Z3_context is leaked. This is not a big deal because Pirouette is currently used so that a solver instance is only created a few times during a run, hence only a few of these contexts get leaked before the program terminates and the memory is effectively freed. But this could become a problem if Pirouette were used as a library and a lot of solver instances were created during the same run.

As discussed here, freeing the context inside the body of the solveOpts function after the problem has been solved was tried, but it leads to a segmentation fault.

[qaristote]

As discussed here, freeing the context inside the body of the solveOpts function after the problem has been solved was tried, but it leads to a segmentation fault.

It looks like the reason this doesn't work is that the result of solveOpts, a function of type Problem domain res -> res which comes with a Z3 instance attached internally, is used on two different problems: one generated by CheckPath and one generated by CheckProperty. Am I correct to assume this is the only way this output function is used more than once ?

A comment explains this output function is reused so that Pirouette only instantiates solvers once. Is the reason for that solely to avoid spawning too many external processes, or is there a deeper reason ? Perhaps the problems created by CheckPath and CheckProperty share some definitions ?

[Niols]

OCaml's GC can be made aware of such FFI pointers. Basically, you say “this is an OCaml value representing a C pointer and here is a function to call when you want to GC the value”. I would be surprised if there was no similar mechanism for Haskell's FFI.

[qaristote]

Haskell does have Foreign.ForeignPtr. Looks good, thanks !

[facundominguez]

I was expecting a solution to free the context explicitly. Using ForeignPtr is ok for now, but note that it has the problem of not releasing promptly.

If multiple contexts are created, the garbage collector has no incentive to run because the Z3 contexts do not reside in the managed heap. This leads to memory being exhausted depending on whether the GC decides to run on time.

[qaristote]

Would finding a way to use something like mallocForeignPtr solve this problem ?

[facundominguez]

Maybe, but then you have to convince the SMT solver to initialize a context in the memory that mallocForeignPtr provides. I think we also would have to ponder the consequences of pinning the memory.