ocaml-ctypes
ocaml-ctypes copied to clipboard
ocamllabs
Calling Bigarray.sub on a ctypes-generated bigarray is unsafe
Ctypes.bigarray_of_ptr allocates a bigarray backed by arbitrary, externally-managed memory. The lifetime of the backing memory must exceed that of the bigarray. But how can the underlying memory be freed when the bigarray is gc-ed?
It may appear that this can be ensured by calling Gc.finalise and freeing the underlying memory in the finalizer. Unfortunately, Bigarray.sub allows for the creation of new OCaml objects that reference the same underlying memory but have lifetimes extending past that of the original array, so freeing this memory via Gc.finalise is unsafe.
Unfortunately, there is no good way to resolve this in the general case. Writing C stubs by hand lets you write a custom finalizer that tracks sub-arrays correctly, but that finalizer can't call back into ocaml. While you could in theory check from a finalizer whether this bigarray has any remaining proxy references, there would be no way to avoid leaking the memory when those proxies are in turn GC-ed.
Ultimately I think creating safe, leak-free bigarrays via ctypes is impossible. At very least there should be a big scary warning next to bigarray_of_ptr warning about this.
but have lifetimes extending past that of the original array, so freeing this memory via
Gc.finaliseis unsafe.
This is true in the general case, if you use ctypes to expose externally-managed memory as a bigarray to user code. But it's not true if you restrict the set of operations that can be performed on the bigarray, e.g. by means of a module interface:
module Interface :
sig
type t
(* carefully-chosen operations *)
end =
struct
type t = (...) Bigarray.Array1.t
(* carefully-chosen operations *)
end
In this case it's possible to ensure that operations like sub can't be called, so it's safe to use finalise to tie the lifetime of the underlying memory to the lifetime of the bigarray. It should also be possible to expose operations like sub in this way, attaching another finaliser when sub is called to prolong the lifetime of the underlying memory accordingly.
