freeing pointers in FFI

Stream: lean4

[Anders Christiansen Sørby]

I'm working on bindings to SDL2 which is a rather imperative C media library.
https://github.com/Anderssorby/SDL.lean
I'm having troubles unifying the manual memory freeing of SDL with the finalizer of Lean reference counter.
For example manually freeing the pointed data with SDL_FreeSurface leads to segfault

    SDL.freeSurface surf

when lean tries to free the lean_object* too later. Putting the SDL_FreeSurface inside the lean finalizer also leads to a segfault.
Do you have any tips?

[Arthur Paulino]

@Anders Christiansen Sørby you need to tell lean how to box/unbox objects

[Arthur Paulino]

Have you been able to make any of those C functions that rely on lean_get_external_data work?

[Gabriel Ebner]

I'm having troubles unifying the manual memory freeing of SDL with the finalizer of Lean reference counter.

Yes, that's because you're freeing it twice, once with SDL_FreeSurface and once with free. You should remove the SDL.freeSurface function and call SDL_FreeSurface from the finalizer instead.

[Arthur Paulino]

@Gabriel Ebner when is the finalizer called?

[Anders Christiansen Sørby]

Ok, that is ideal if I can avoid the manual freeing. I have been successfull with lean_get_external_data before

[Anders Christiansen Sørby]

The segfault happens in lean_ptr_tag so I'm not sure if the finalize function has been called yet

[Arthur Paulino]

To make it easier for me to have full control over what happens in C, I wrap everything inside a struct

[Anders Christiansen Sørby]

What does m_tag do and store btw? It isn't documented in lean.h

[Anders Christiansen Sørby]

Hm, I already have enough structs from SDL I think.

[Gabriel Ebner]

when is the finalizer called?

When the surface object is no longer referenced (i.e., the refcount reaches zero).

[Gabriel Ebner]

What does m_tag do and store btw? It isn't documented in lean.h

It stores whether the object is an external/bignum/task/constructor/etc.

[Gabriel Ebner]

If lean_ptr_tag segfaults, then that's because you pass it a null/invalid pointer. (Which you might have got from the Inhabited instance for Surface.)

[Gabriel Ebner]

The whole PointedType business is a giant footgun tbh.

[Anders Christiansen Sørby]

There is a segfault after lean_render_copy which is void

155 x_24 = lean_sdl_render_copy(x_9, x_22, x_23);
156 lean_dec(x_22);
157 lean_dec(x_9);
158 if (lean_obj_tag(x_24) == 0) <-- here

Why does it try to read a void value? I used IO Unit for void, but is there an explicit way to return unit?

[Gabriel Ebner]

That's IO Unit, not void. :smile:

[Gabriel Ebner]

but is there an explicit way to return unit?

io_result_mk_ok(box(0))

[Anders Christiansen Sørby]

Hm, but I need to make sure Window is not finalized before the program is over. For now it seems manually calling destroyWindow makes most sense.

[Gabriel Ebner]

As long as you use either the finalizer or a manual free function, you should be fine.

[Anders Christiansen Sørby]

Seems like this solved everything. Thanks

[Mario Carneiro]

Gabriel Ebner said:

The whole PointedType business is a giant footgun tbh.

Could you elaborate? I'm curious what problems you see and how you would address them with a different approach

[Gabriel Ebner]

The footgun is clear, I hope. If you do constant MyFfiType : PointedType, then you get MyFfiType.val : MyFfiType.type for free. And this is box(0) in the VM, so all your FFI functions will crash unless they handle this special case. Even worse, you typically define instance : Inhabited MyFfiType.type := ⟨MyFfiType.val⟩ which means that you only need an [Inhabited MyFfiType.type] argument to get this special value. It's the million-dollar mistake ("null") all over again.

[Anders Christiansen Sørby]

Is there some easy way I can convert an Option Data to a Data* ptr. So that none is NULL and some data is get_exteranl_data

[Gabriel Ebner]

My plan would be to replace PointedType with { α : Type // Nonempty α }. This doesn't give you access to any "null" value, but suffices for constant frob : MyFfiType.type → MyFfiType.type.

[Mario Carneiro]

Well, it seems the point is that we are explicitly asking for an inhabited type here, i.e. one with a null value. Ideally we should have a way to just have constant Foo : Type if Foo does not admit a null value

[Mario Carneiro]

The whole pattern with inhabited types seems to be that we want programmy types to have default values when possible

[Mario Carneiro]

If you replace Inhabited with Nonempty in PointedType, I think you also have to replace it in the checks on partial and constant

[Mario Carneiro]

Gabriel Ebner said:

The footgun is clear, I hope. If you do constant MyFfiType : PointedType, then you get MyFfiType.val : MyFfiType.type for free. And this is box(0) in the VM, so all your FFI functions will crash unless they handle this special case.

This seems odd to me (the part about the null value being box(0) specifically). Aren't you supposed to provide/override this function as part of the FFI implementation?

[Gabriel Ebner]

I think you also have to replace it in the checks on partial and constant

Indeed, that's what I want to do.

[Gabriel Ebner]

This seems odd to me (the part about the null value being box(0) specifically).

constant only hides the implementation (i.e., you can't prove that MyFfiType is the default PointedType value). But the implementation is still used by the VM.

[Gabriel Ebner]

Same thing if you define a natural number constant:

constant N : Nat := 42
#eval N -- 42

[Mario Carneiro]

But part of the "idiom" here is that you are replacing this function with something else, or else there is no point in the constant

[Gabriel Ebner]

Except that the default PointedType value consists of the type PUnit with PUnit.star as the value (which is represented as box(0))

[Mario Carneiro]

a constant with no definition and no implementedBy or extern seems like a very weird thing to do IMO

[Gabriel Ebner]

This is completely normal and idiomatic for FFI types though.

[Mario Carneiro]

don't FFI types always extern the constant?

[Gabriel Ebner]

Never for the type, as far as I can see. Only for the FFI functions.

[Mario Carneiro]

...I'm very confused how anything is supposed to work then

[Anders Christiansen Sørby]

You do want to have NULL pointers in some FFI scenarios though. Like I described. How is Option represented?

[Mario Carneiro]

Your type can explicitly do something with nulls if you want

[Mario Carneiro]

You can either put Option around your type, or just have an API that reflects the possibility that the type has a null value (and every function has to accommodate this)

[Gabriel Ebner]

...I'm very confused how anything is supposed to work then

The general idea is this (add coercions, definitions, etc. to your liking):

constant MyType : PointedType
@[extern "function1_impl"]
constant function1 : MyType.type → MyType.type
@[extern "function2_impl"]
constant function2 : MyType.type → MyType.type → MyType.type

[Mario Carneiro]

yeah, I see a bug there if you aren't adding an extern on the first constant

[Gabriel Ebner]

I think what you expected is this:

@[extern "mk_empty_mytype"]
constant MyType : PointedType

Note that this will only work if you can actually provide a default value. (And many FFI types don't have them.)

[Mario Carneiro]

What I would like to write in the case of no default is:

constant MyType : Type
@[extern "function1_impl"]
constant function1 : MyType → MyType
@[extern "function2_impl"]
constant function2 : MyType → MyType → MyType

[Mario Carneiro]

assuming that gives an error about non-inhabited types for the latter constants, you can also write

constant MyType : Type
@[extern "function1_impl"]
constant function1 : MyType → MyType := id
@[extern "function2_impl"]
constant function2 : MyType → MyType → MyType := fun _ => id

[Gabriel Ebner]

This doesn't let you write constant function3 : Nat → MyType though.

[Mario Carneiro]

True. But if your function has such an API then you can define MyType.val := function3 0

[Gabriel Ebner]

I think you have the order wrong, you'd need to write a C function function3_0_impl and say @[extern "function3_0_impl"] constant MyType : PointedType.

[Gabriel Ebner]

And then function3 is always executed on initialization, whether you want it or not.

[Mario Carneiro]

What if the constructor is in an IO action? Like function3 : Nat -> IO MyType

[Mario Carneiro]

can we have a default IO action for this case?

[Gabriel Ebner]

That would actually work (because IO happens to be inhabited), but Nat → BaseIO MyType runs into the same issues as Nat → MyType.

[Mario Carneiro]

If the constructor is pure, then evaluating it on startup is probably fine, and if it's not then you probably have the IO situation

[Mario Carneiro]

not sure how much to worry about the BaseIO version

[Mario Carneiro]

what happens when a BaseIO computation fails?

[Mario Carneiro]

is that just undefined behavior or something?

[Gabriel Ebner]

It can only abort or exit the process, not fail in the same sense as IO.

[Mario Carneiro]

I think the worst case scenario, if you have a complex not-necessarily-inhabited FFI type with a bunch of random functions on it, is that you put the whole API in a structure and make a constant for it. Then you have to prove that some type has a model for the whole thing, which is presumably possible unless the new type is literally inconsistent

[Gabriel Ebner]

and make a constant for it

That's a moderately bad idea because you'll have indirect function calls via closures instead of direct ones.

[Mario Carneiro]

I was hoping that would be optimized away

[Mario Carneiro]

they should still be calls to known functions, i.e. it is optimizable

[Mario Carneiro]

I feel like we still haven't found the best approach here for communicating an FFI interface to lean with suitable consistency checks

[Gabriel Ebner]

I'm not sure how you expect this to happen. It's an opaque definition in C. Lean can't see through it. And I wouldn't count on LTO being able to see through it (the lean_apply functions are huge and unlikely to be inlined);

[Gabriel Ebner]

I feel like we still haven't found the best approach here for communicating an FFI interface to lean with suitable consistency checks

What's wrong with my PointedType := { α // Nonempty α } proposal? That seems like the most incremental change which still gets rid of the initialization/default value issue.

[Anders Christiansen Sørby]

Is there some easy way to translate between lean structures and c structs with the same fields btw?

[Mario Carneiro]

I'm thinking something like this:

struct FooApi where
  T : Type
  f : T -> T

def FooModel := empty
@[extern "foo_f_impl"]
def FooModel.f : FooModel -> FooModel := id

constant FooWitness : FooApi := \<FooModel, FooModel.f\>

def Foo := FooWitness.T
def Foo.f : Foo -> Foo := FooWitness.f

The lean compiler should be able to work out that Foo.f is a direct call to foo_f_impl

[Mario Carneiro]

Gabriel Ebner said:

I feel like we still haven't found the best approach here for communicating an FFI interface to lean with suitable consistency checks

What's wrong with my PointedType := { α // Nonempty α } proposal? That seems like the most incremental change which still gets rid of the initialization/default value issue.

I think there should be a way to mark types as being FFI-overridden, such that lean can give an error/warning on any function that uses the type's "fake" definition and is not overridden

[Mario Carneiro]

Another alternative, similar to using Nonempty, is to use noncomputable constant Foo : PointedType to opt out of code generation for the .val function

[Gabriel Ebner]

I'm thinking something like this:

Indeed, it's possible to "launder" the API in this way. (Although NonScalar might be more useful than Empty, in general.) The setup is pretty cumbersome though.

[Mario Carneiro]

it does look like something that can/should be automated by a macro, especially because of the footguns

[Mario Carneiro]

but the macro expansion should hopefully not require too much analysis to get good code, so if as you say there is an inefficiency in going via the structure then this isn't the best solution

[Gabriel Ebner]

No the "laundering" should be zero-cost (or at least be zero-cost after adding enough @[inline]).

[Joe Hendrix]

I think there should be a way to mark *types* as being FFI-overridden, such that lean can give an error/warning on any function that uses the type's "fake" definition and is not overridden
````
Doesn't having `MyType` be a constant (e.g., `const MyType : PointedType`) prevent one from using the type's fake definition?

[Mario Carneiro]

No, that only prevents lean from being able to use the definition in proofs. The compiler will see through constant definitions

[Mario Carneiro]

For types, this is fine since types have no compiler content, but PointedType is a combination of a type and a value, so it is computationally relevant (and you can use #eval MyType.val to execute code producing this bad value)

[Anders Christiansen Sørby]

I used PointedType.val as an intentional NULL in SDL which is a very useful option to have.

[Gabriel Ebner]

Just (a related) fyi: you should never use (lean_object *) NULL. This is a special value reserved by the runtime.

[Joe Hendrix]

I get an error with #eval MyType.val due to the lack of Repr, but I see your point. From some limited testing, it seems like you could mark the constant as noncomputable and that will prevent the evaluator from synthesizing that code.
Does that have the semantics that you are looking for?

[Anders Christiansen Sørby]

Unfortnulately this wasn't as useful as I hoped. I wanted that only lean_get_external_data returned NULL

[Anders Christiansen Sørby]

If there was some way I could destructure lean types in C I could use an option type directly perhaps.

[Anders Christiansen Sørby]

I tried to do this to get a NULL pointer like this

/*
SDL.SDL_Rect_NULL : Thunk SDL_Rect
*/
lean_obj_res lean_sdl_rect_null() {
  return lean_alloc_external(get_sdl_rect_class(), (SDL_Rect *) NULL);
}

Which causes

src.c:351:25: error: called object type 'lean_object *' is not a function or function pointer
SDL-cc> x_1 = lean_sdl_rect_null();

[Arthur Paulino]

(deleted)

[Arthur Paulino]

But why are you trying to return NULL to Lean?

[Arthur Paulino]

I can't help but think there is some kind of conceptual misuse of the FFI

[Anders Christiansen Sørby]

Sure, there are ways to avoid using NULL which has a real meaning in the SDL API. But what would be the best way to do it? I would most want to ba able to convert an Option.none to a NULL pointer in those cases, but doing that requires destructuring the data representation of Option in C which is not so nice.

[Joe Hendrix]

@Anders Christiansen Sørby What is the type declaration in Lean for the function that binds to lean_sdl_rect_null? Is it pure or in IO?

[Joe Hendrix]

If it is in IO, then it should take an extra unused argument for the "RealWorld" argument, e.g., lean_obj_res lean_sdl_rect_null(lean_object* _rw).

[Arthur Paulino]

@Anders Christiansen Sørby I want to apologize upfront for not being able to understand your intent in the context of your lib, but I want to express a mental model that helps me to understand the FFI. Please take it with a grain of salt, for I'm not sure if it can help you.

I like to think of the FFI usage as something similar to object oriented programming. You have access to the objects and its methods, but you can't access its implementations. In this sense, any need to deal with NULL should be handled in C. Similarly, you don't want to be dealing with Java object pointers that point nowhere.

[Anders Christiansen Sørby]

Lean side

@[extern "lean_sdl_rect_null"]
def SDL_Rect_NULL : Thunk SDL_Rect := SDL_RectP.val

[Anders Christiansen Sørby]

This is probably not the ideal way to do this. But I need to represent NULL in some way since this means that the function uses a default.

[Anders Christiansen Sørby]

constant SDL_RectP : PointedType

def SDL_Rect := SDL_RectP.type

[Arthur Paulino]

Anders Christiansen Sørby said:

This is probably not the ideal way to do this. But I need to represent NULL in some way since this means that the function uses a default.

You need to pass something from Lean to C in a way that C understands it as NULL?

[Anders Christiansen Sørby]

Yes, or something I can translate to NULL

[Arthur Paulino]

I'd use a struct to encapsulate that info, with a field whose value is initiated with NULL

[Arthur Paulino]

typedef struct some_data {
    PTR_TYPE* ptr = NULL;
} some_data;

[Mario Carneiro]

Anders Christiansen Sørby said:

I tried to do this to get a NULL pointer like this <snip> Which causes

src.c:351:25: error: called object type 'lean_object *' is not a function or function pointer
SDL-cc> x_1 = lean_sdl_rect_null();

What is the code producing the latter error? it seems like you passed a lean_object * directly as an SDL_Rect * to an SDL function instead of unwrapping it like you should. Since the lean_external API accepts void * payloads, I suspect that using NULL in the way of your first code block is fine, but you are making a mistake somewhere else causing the error.

[Anders Christiansen Sørby]

@Arthur Paulino Sure, but I was looking for the minimal boilerplate solution.

[Anders Christiansen Sørby]

@Mario Carneiro Hm, I thought so too, but I can't see where...

[Mario Carneiro]

who is producing that error? What is src.c? I don't see it in your project

[Joe Hendrix]

I tested code generation and for a thunk, Lean expects it to be a constant.

[Joe Hendrix]

So the compiler is likely looking for a declaration such as LEAN_EXPORT lean_object* lean_sdl_rect_null

[Anders Christiansen Sørby]

I found the problem. I need to use a Unit -> SDL_Rect signature to make it behave like a function with no args

[Joe Hendrix]

Unit -> SDL_Rect will likely make it a function that takes a single argument, but the argument can be ignored.

[Anders Christiansen Sørby]

I thought so, but it does not. It works with no args.

[Mac]

Anders Christiansen Sørby said:

This is probably not the ideal way to do this. But I need to represent NULL in some way since this means that the function uses a default.

Why not just use Option SDL_Rect for functions that accept possibly NULL rect arguments?

[Joe Hendrix]

@Anders Christiansen Sørby What I meant by that is that if you look in the Lean generated C code, you'll see it declares a function like lean_object* lean_sdl_rect_null(lean_object*).

Of course, it's fine to link that against a function definition that takes no arguments, because that's ABI compatible when you don't actually use the argument.

[Anders Christiansen Sørby]

@Mac That is what I first tried, but I don't know how to unwrap an lean_object* which is an option on the C side.

[Anders Christiansen Sørby]

Would be nice if there was such a function. void *lean_option_unwrap(lean_obj_arg a)

[Anders Christiansen Sørby]

Which is NULL for none and get_external_data(b) for some b

[Mac]

@Anders Christiansen Sørby to unwrap an Option, first check if it is none (e.g., 1) by checking if the lean_object is a scalar (i.e., with lean_is_scalar). Otherwise, if the Option is instead a some, you can get the inner lean_object with some_val = lean_ctor_get(opt_obj, 0).

[Anders Christiansen Sørby]

Ok, thanks. That is what I've been looking for. Is this documented anywhere?

[Anders Christiansen Sørby]

So this should do it

/**
 * Unwrap an Option of an external object as data for some
 * or NULL for none. Unsafe.
 */
void *lean_option_unwrap(b_lean_obj_arg a) {
  if (lean_is_scalar(a) && lean_scalar_to_int(a)) {
    return NULL;
  } else {
    lean_object *some_val = lean_ctor_get(a, 0);
    return lean_get_external_data(some_val);
  }
}

[Mac]

@Anders Christiansen Sørby You don't need the lean_scalar_to_int. You just need lean_is_scalar.