Skip to content

Add Constant and Class classifications for recursive bindings#12608

Merged
lthls merged 3 commits intoocaml:trunkfrom
lthls:let-rec-constant-classification
Nov 24, 2023
Merged

Add Constant and Class classifications for recursive bindings#12608
lthls merged 3 commits intoocaml:trunkfrom
lthls:let-rec-constant-classification

Conversation

@lthls
Copy link
Copy Markdown
Contributor

@lthls lthls commented Sep 26, 2023

The next step in compilation of recursive bindings.

Class bindings are bindings that do not go through Rec_check. Although they do respect the same invariants, they currently end up matching either the Static or Not_recursive cases, and I ended up creating this special case rather than try to compute and propagate the correct kind from Translclass.
Both #12596 and #8956 end up treating them as Static bindings of size 4, but I can't do it in this PR because the recursive kinds don't carry sizes yet.

Constant bindings correspond to expressions that the compilers will not statically allocate. In some cases the constants do not have a computable size (typically, integer-like constants), but even for allocated constants the compilers use RHS_nonrec instead of a static size.
Most of the expressions that produce constants are classified as Static by Rec_check, which means that weird expressions like let rec x = while true do x done are allowed.
Some slightly less unlikely examples were discussed in #12153.

This PR preserves the currently accepted definitions, but switches the ones that will end up as constants to Constant (which is checked with the same constraints as Static).
This allows the compilers to check that Static bindings always have an actual size, with the following caveats:

  • The native compiler can transform non-constant expressions into constant ones. For flambda, this is trivial to fix: when rebuilding a Let_rec term, check if it is constant, and if it is change the recursive kind. For closure, this doesn't work, so I have turned the assertion off (the assertion would trigger on the test letrec-compilation/pr12153_miscompilation_of_recursive_atoms.ml).
  • Constructions in the object language are currently considered Static, but they're not. So the assertion can trigger on let rec x = object end, for instance.
  • The bugs reported in Segmentation fault with recursive lazy values #12585 and Segmentation fault with recursive first class modules #12592 will trigger the assertion (which is arguably better than generating wrong code).

I have some commits on #12596 that take care of the last two issues by fixing the classification, that I could include here if needed.

Copy link
Copy Markdown
Member

@gasche gasche left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I asked @lthls to document the recursive_kind type to explain what the (old and) new classifications mean. We decided to move it from typedtree to a new (very small) module value_rec_types.mli, and correspondingly move rec_check to value_rec_check.

be statically allocated with Closure.
Forthcoming patches will remove all this logic anyway. *)
if Config.flambda then
assert (result <> RHS_nonrec);
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The comment felt a bit cryptic to me. You are commenting on the fact that "Expressions classified Static by the frontend should not be compiled as RHS_nonrec: this is unsound, so we want to assert that this does not happen." I think that this should be said (in some way or another) at the beginning of the comment.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(This code is going away with #12596 anyway, so maybe this is not so important.)

match classify_expression env expr with
| Constant -> true
| _ -> false)
true exprs
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be List.for_all.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would suggest defining a is_constant : expr -> bool helper function (probably as a local binding below let rec classify_expression ... =?) to use here and below as well.

| _ -> Static
end
| Texp_variant (_, None) ->
Constant
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wish we had Option.for_all to use here.

| Texp_while _
| Texp_setinstvar _
| Texp_unreachable ->
Constant
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For readability I would suggest three groups, separated by a blank line: Texp_constant goes first (it is the canonical Constant construction), then all the unit-returning expressions, then Texp_unreachable which is weird. (Maybe there is a comment to add on the unreachable case?)

(* The expression will not be pre-allocated, but the result cannot
contain recursive references *)
let ty = expression expr Return in
if Env.unguarded ty idlist = [] then Some Constant else None
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that we could share the code with the Static case above -- in my mind we have Static of [block | constant] as two subcases of the same general idea.

  | (Static | Constant) as recursive_kind ->
        let ty = expression expr Return in
        if Env.unguarded ty idlist = [] then Some recursive_kind else None

we lose the comments, but the comments are not so helpful anyway at this point, they refer to the compilation scheme and not the code itself.

@lthls lthls force-pushed the let-rec-constant-classification branch from b228bb1 to b1da323 Compare November 24, 2023 12:58
Copy link
Copy Markdown
Member

@gasche gasche left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved (a mild history cleanup would be nice).

Use that to assert that Static bindings always have a known size
- Add Value_rec_types modules
- Rename Rec_check to Value_rec_check
@lthls lthls force-pushed the let-rec-constant-classification branch from b1800be to c3cf856 Compare November 24, 2023 13:16
Copy link
Copy Markdown
Member

@gasche gasche left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved. This PR includes a documentation of the recursive classification kinds, which I suspect is also very useful.

@lthls lthls merged commit 1537083 into ocaml:trunk Nov 24, 2023
sadiqj pushed a commit to sadiqj/ocaml that referenced this pull request Jun 1, 2024
* 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
hhugo added a commit to hhugo/ocaml that referenced this pull request Nov 18, 2024
This change appeared in 5.2 in

- ocaml#12551, ocaml#12608, ocaml#12782, ocaml#12596: Overhaul of recursive value compilation.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants