Open qaristote opened 2 years ago
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 ?
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.
Haskell does have Foreign.ForeignPtr
. Looks good, thanks !
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.
Would finding a way to use something like mallocForeignPtr
solve this problem ?
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.
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 aZ3_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 bindingZ3_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.