Compute sizes for recursive static bindings #12782

lthls · 2023-11-24T14:37:09Z

Two commits from #12596 that change the classifications computed in Value_rec_check.
Knowing the sizes is a pre-requisite for compiling these bindings, but it also gave us an opportunity to look again at all the cases allowed under the Static classification and make sure that we do indeed know their size.
As a result, we know properly treat object-related constructs as Not_recursive, and restrict a few other constructions that were broadly allowed to be Static to only the cases that fit the definition.

Fixes #12585 and #12592.

gasche

I reviewed this PR and believe that it is broadly correct -- see inline comments, including possibly some small minors in the module-expression stuff.

This PR is less clearly an unconditional improvement than the previous one. @lthls is moving in the direction of moving the recursive-value-compilation logic at the Lambda level instead of being duplicated in the two backends. The present PR is some buildup work that adds compilation logic in typing/rec_check (feels a bit inappropriate) and does not simplify anything in the backend yet: not clearly a win in isolation.

The overall plan is to continue with #12596 that adds the compiler in typing/ (or lambda?). In this perspective the current PR is a step towards this sizeable win. I think we could approve it now, even though #12596 is not reviewed yet and a showstopper could still show up -- sounds unlikely, but we never know.

Minor remark: we have a plan to move the compiler-y logic in rec_check (introduced in this PR) to a separate module, which would avoid the unpleasant mixing of concerns that is currently at play in this PR.

gasche · 2023-11-24T14:42:28Z

middle_end/closure/closure.ml


 and close_one_function env id funct =
-  match close_functions env [{ id; rkind = Static; def = funct }] with
+  match close_functions env [{ id; rkind = Static Function; def = funct }] with


Why are we using Static here instead of Not_recursive?

My reasoning was that it was obviously a function, so Static Function is obviously correct (just like Simplif.split_default_wrapper uses Static Function systematically).
And close_functions discards the kind anyway, so in the end it doesn't matter.

typing/value_rec_check.ml

gasche · 2023-11-24T15:22:07Z

typing/value_rec_check.ml

+                | Tstr_class cl_list ->
+                  acc + List.length cl_list
+                | Tstr_include incl ->
+                  let ids = bound_value_identifiers incl.incl_type in


Is bound_value_identifiers good enough here? For example, if I do include struct exception A end, does it count an item as expected?

It is. Translmod relies on the length of the result being equal to the size of the module block.

gasche · 2023-11-24T15:22:29Z

typing/value_rec_check.ml

+                  acc + List.length ids
+                | Tstr_open od ->
+                  let ids = bound_value_identifiers od.open_bound_items in
+                  acc + List.length ids


This case looks wrong from a distance, does open add any item to the current structure?

See #12785.
Summary: open sometimes does add items to the current structure, but in that case they must be removed from the signature and a coercion is generated. Since for the size computation, we never look at structures under a coercion, in practice ids should always be empty when we reach this case.
I could add an assertion (and a comment to go with that), or leave it like this so that it obviously mirrors Translmod.

I don't agree that the logic here mirrors the logic in translmod. The logic here is trying to compute the size of the resulting structure, while the code in translmod builds an ambient environment as a series of let-bindings, that is not related to the size of the output structure. The two cases here for open and include are arguably wrong: the case for open is clearly wrong¹, and I am doubtful about the case for include in cases such as include struct (open struct let x = 1 end) end where we include hidden items.

On the other hand, the type-checker computed a module signature that is stored with the coercion, and contains all the information we need to know the size of the resulting structure.

So I would prefer to see the following code:

a size_of_signature function

instead of computing of Texp_pack mexp from mexp.mod_desc, we compute it from mexp.mod_type.

a size_of_signature function

That looks reasonable. I'll see how easy it is, but hopefully it's something as simple as List.length (bound_value_identifiers sg). I expect that it will give the same result as my computation though.

instead of computing of Texp_pack mexp from mexp.mod_desc, we compute it from mexp.mod_type.

I decided against that because I didn't want to authorize more expressions than necessary (i.e. let rec m = (module F(X)) should be forbidden in my opinion, even if we have an explicit signature). But I can still use size_of_signature on Tmod_structure blocks that don't already have a coercion.

I decided against that because I didn't want to authorize more expressions than necessary (i.e. let rec m = (module F(X)) should be forbidden in my opinion, even if we have an explicit signature).

Why should that particular definition be forbidden?

In my mind the important point is not to accept more or less definitions in this corner case, but to keep the implementation as simple and safe as possible. Using the inferred module signature is both very simple and very safe; in particular, it does not rely on subtle invariants of the typedtree construction process.

I'm relatively confident that if we allow using the inferred signature to compute the size of the module, I can trigger segfaults with Closure (or assert failures with the debug runtime). See #11895 for more details.

gasche · 2023-11-24T15:31:13Z

typing/value_rec_check.ml

+          classify_expression env e
+      | `Other ->
+          (* other cases compile to a lazy block holding a function *)
+          Static (Regular_block 1)


I feel a bit nervous about those magic constants in the module. For example, we discussed changing the layout of lazy thunks to get two fields.

It would be nice to define those in lambda.mli:

val lazy_block_size : int val variant_block_size : arity:int -> int val extension_constructor_size : int ...

I have a patch for that, but currently it doesn't compile as it introduces a dependency from Value_rec_check to Lambda. I'll wait until the next PR to sort that out (as moving the size computation to the recursive value compiler will introduce the dependency transitively anyway).

Maybe we could already do the split in the current PR? I am hesitant about merging the current PR in a state that we don't find so satisfying, because the next one is larger and more invasive (it does change the generated code in a noticeable way) so it may take longer to get in.

Fun fact: we are already in a slightly unstable state regarding dependencies. Value_rec_check (previously Rec_check) depends on Lambda, but is linked before it.
It all works out because we actually only depend on constructors for pattern matching, so no runtime dependencies. We still have a dependency from value_rec_check.cmx to lambda.cmx in .depend, but that's "fine" again because the dependency doesn't actually get registered in the .cmx file.
On the other hand, introduing a real dependency from Value_rec_check to Lambda, even through indirections, will inevitably make the linker complain.

So I see three main solutions. One is to revert #12586 so that we can specify a link order that follows actual dependencies, not just directories. That would probably make @shindere sad though, so I don't advise it.
The second solution is to tweak our build system so that the dependencies and the link order agree with each other. This could mean moving files from one directory to another, splitting definitions into separate files, or adapting the Makefile. I'll let @shindere comment on which one is preferred.
The last solution is to do nothing, and give up on proper splitting. This is the most convenient for me because I don't have to do anything, but I agree it's not very satisfying.

I am probably overlooking other possible solutions, feel free to propose alternatives.

In this context, I agree with delaying the split.

I think that it is wise to avoid dependencies from the type-checking phase to the code production phase. This is not just a matter of build system, it makes the design simpler.

One approach could be to split the recursive_kind computation in two passes:

one running during type-checking that merely classifies value among Static, Not_recursive (maybe class?), without distinguishing between Constant and Static or trying to compute a size

one running during the typedtree->lambda compilation, that refines the first classification by distinguishing constants, computing sizes, etc.

The question then would be how to formulate this to avoid redundant computations (and a risk of mismatch) between the two phases. My suggestion would be to include in the first phase any part of the typedtree that we know will be relevant to refine the classification in the second class: Static of rec_shape, where rec_shape is a tailored AST supporting all interesting rec_check cases.

On paper, that looks very nice. It avoids estimating sizes on the typedtree, and on lambda sizes are already computed. Any mismatch will result in a fatal error at compilation (if we cannot compute the size of a Static binding), or "valid" recursive definitions getting rejected (if we classify them as Not_recursive even though they correspond to a simple allocation).

I don't think we actually need to store a shape; all these weird cases get resolved during translation to lambda anyway. However, we will likely need to keep the lazy classification code and the traversal of module expressions (without the size computation) in the typedtree version of Rec_check.

I'll try to implement it and see if it actually works.

I have implemented that on the main PR (#12596). I will now try to reduce this PR to the bugfixes only (finer grained classification for modules and lazy, to fix the two outstanding bugs).

I only skimmed the patch but I like where this is going, it looks simpler. (In particular, we don't have to second-guess what will become an Lconst anymore.)

typing/value_rec_check.ml

lthls · 2023-12-01T16:47:37Z

The PR has been cut down to only contain the fixes for the two bugs (plus a few very small changes that are good anyway).
I'll probably rebase it properly on Monday to remove all the back-and-forth.
The size computation will be done as part of the compilation of recursive values in Lambda, as shown in #12596.

gasche

Approved -- to be merged after the rebase, and possibly after you decide (or not) to act on some minor comments.

gasche · 2023-12-01T16:50:01Z

typing/typedtree.mli

 and module_binding =
    {
-     mb_id: Ident.t option;
+     mb_id: Ident.t option; (** [None] for module _ = struct ... end *)


Suggested change

mb_id: Ident.t option; (** [None] for module _ = struct ... end *)

mb_id: Ident.t option; (** [None] for [module _ = struct ... end] *)

typing/value_rec_check.ml

gasche · 2023-12-01T16:53:49Z

typing/value_rec_check.ml

+        | Tcoerce_primitive _ ->
+            Misc.fatal_error "letrec: primitive coercion on a module"
+        | Tcoerce_alias _ ->
+            Misc.fatal_error "letrec: alias coercion on a module"


I don't know what Tcoerce_{primitive,alias} are, would you mind looking it up and adding a comment in typedtree.mli for those as well?

Tcoerce_primitive is when you export an external in the structure as a value in the signature. Tcoerce_alias is when you have a module alias in a structure that is exported as a regular module in the signature.
I'll add some docs before rebasing.

(Both of those only make sense as sub-coercions of a Tcoerce_structure coercion)

(I asked for code examples and @lthls provided them.)

* Propagate the classification from Rec_check (ocaml#12551) * Add Constant and Class classifications for recursive bindings (ocaml#12608) * Fix Rec_check for lazy expressions and first-class modules (ocaml#12782) * Compile recursive bindings in Lambda (ocaml#12596) * Fixes * Add test * Remove outdated runtime assertion * Update comment + review

This change appeared in 5.2 in - ocaml#12551, ocaml#12608, ocaml#12782, ocaml#12596: Overhaul of recursive value compilation.

gasche reviewed Nov 24, 2023

View reviewed changes

gasche approved these changes Dec 1, 2023

View reviewed changes

Fix recursive classification for objects, modules and lazy expressions

a466d7d

lthls force-pushed the let-rec-classification-fixes branch from 4f7b8ed to 58d7554 Compare December 4, 2023 08:58

lthls added 2 commits December 4, 2023 14:16

Small doc comments

24b0871

Changes

4de28ed

lthls force-pushed the let-rec-classification-fixes branch from 58d7554 to 4de28ed Compare December 4, 2023 13:16

gasche added the merge-me label Dec 4, 2023

gasche merged commit 08069e6 into ocaml:trunk Dec 4, 2023

lthls mentioned this pull request Dec 4, 2023

Segmentation fault with recursive first class modules #12592

Closed

hhugo added a commit to hhugo/ocaml that referenced this pull request Nov 18, 2024

Remove unused runtime due to recursive value compilation changes.

cd48dc0

This change appeared in 5.2 in - ocaml#12551, ocaml#12608, ocaml#12782, ocaml#12596: Overhaul of recursive value compilation.

hhugo mentioned this pull request Nov 18, 2024

Remove unused runtime following recursive value compilation changes. #13617

Merged

	mb_id: Ident.t option; (** [None] for module _ = struct ... end *)
	mb_id: Ident.t option; (** [None] for [module _ = struct ... end] *)

Compute sizes for recursive static bindings #12782

Compute sizes for recursive static bindings #12782

Uh oh!

Conversation

lthls commented Nov 24, 2023

Uh oh!

gasche left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lthls Nov 27, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

lthls commented Dec 1, 2023

Uh oh!

gasche left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

lthls Nov 27, 2023 •

edited

Loading