free memory in the ffi

Stream: lean4

[Remy Citerin]

Hi !
I tried to use the FFI to import functions coded in C, I spent some time there and now I can create functions, constructors / destructors but I have a problem, I can't to free the memory I allocated in these functions (initially I wanted to redo my own vector class which uses std::vector and forall x:Fin n, a as model, instead of List a ), I looked at the code and found that it is this function that frees the memory:

extern "C" LEAN_EXPORT void lean_free_object(lean_object * o) {
    switch (lean_ptr_tag(o)) {
    case LeanArray:       return lean_dealloc(o, lean_array_byte_size(o));
    case LeanScalarArray: return lean_dealloc(o, lean_sarray_byte_size(o));
    case LeanString:      return lean_dealloc(o, lean_string_byte_size(o));
    case LeanMPZ:         to_mpz(o)->m_value.~mpz(); return lean_free_small_object(o);
    default:              return lean_free_small_object(o);
    }
}

it is therefore possible to free memory that matches on existing types but without the possibility of adding cases or redirecting the pointer to lean_free_small_object to a new function, which is problematic for managing external libraries that depend on their own allocators. Do you think this can be fixed in a next version of lean? One solution I've thought of is to have something like LeanCustom and one can reinterpret cast o to a struct that contains a pointer to its free memory function, but there may be a other solutions

#define LeanCustom 4242

typedef void (*DeallocFun)(lean_object* o);

typedef struct {
    lean_object obj;
    DeallocFun custom_free;
} lean_custom;

extern "C" LEAN_EXPORT void lean_free_object(lean_object *o) {
    /* same at the original */
    case LeanCustom:
        lean_custom *custom = (lean_custom*)o;
        return custom->custom_free(o);
    default: /* same at the oringinal */
}

[James Gallicchio]

When you register external classes, you also can register handlers for freeing your external objects.

Example: https://github.com/JamesGallicchio/LeanColls/blob/main/bindings/leancolls_array.c

[James Gallicchio]

(that's my reimplementation of arrays... :big_smile:)

[Remy Citerin]

oh I didn't see that, thanks for the help!

[James Gallicchio]

FFI stuff is very minimally documented, so if you have questions don't hesitate to ask -- I spent way too much time trying to dig through lean.h for answers instead of bugging people on Zulip like I should have!

This thread is also a good general source of answers on FFI stuff: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/C.20FFI.20usage

[Remy Citerin]

I just went to see the code and I hadn't seen that LeanExternal existed :sweat_smile: (it is in runtime/object.cpp and not lean.h), and lean_del_core check if the tag is LeanExternal before calling lean_free_object and does something similar by looking for the function pointer in the class definition :upside_down: