Guarantees on uniqueness of code pointers in closures

Learning
1

Suppose that we have some function

let rec f x y =
   ... (f z) ...

and we want to ensure that all the closures f v (whatever v) have a uniquely recognizable code pointer (word 0 of the block). In particular, the above does not work because the code pointer will point to something extremely common like caml_apply (or whatever it is called).

We could go for the following

let [@inline never] rec f x = (); fun y ->
  ... (f z) ...

but there are some concerns that Flambda breaks the “();fun” idiom.

So, what would be a foolproof way to do that?

(For more context, this comes from an attempt at getting rid of naked pointers in Coq.)

2

I’m confused by your question; there’s a finite number of code pointers, both in bytecode and native mode. You cannot create any new ones at runtime without compiling and linking code dynamically.
Could you explain a bit more what you’re trying to achieve ?

3

Up to now, Coq is retagging some closures with a non-closure tag, which will break the garbage collector in no-naked-pointer mode, since word 0 is a code pointer and thus points to a non-heap address. So, we want to remove this retagging. This means that we now need a new way to distinguish the special closures from the standard ones. (Before, we would just look at the tag.) So, we are looking at the code pointer instead. But that only works if we can predict which code pointer these special closures will have. Even if the number of code pointer is finite, if it is larger than one, that makes it next to impossible to know if it is our special closure or not.

4

I mistakenly thought you were trying to have a different code pointer for every closure; now your question makes sense.

I think that your solution will work as well with Flambda as without. Flambda doesn’t try to coalesce a function returning a function into a function taking more arguments. Some transformations earlier in the compiler do that, but at that point (); will not have been simplified yet so you should be fine.

5

You could also use Sys.opaque_identity for this purpose

let [@inline never] rec f x =
  Sys.opaque_identity (fun y ->
  ... (f z) ...

The main thing you have to watch out for is that the definition of this function (f) must not be inside a function (or functor) definition, because this function/functor could in turn become inlined and duplicate the code.