Skip to content

Static check for noalloc: ignore allocations post-dominated by a raise#863

Closed
gretay-js wants to merge 11 commits intooxcaml:mainfrom
gretay-js:alloc-check-exn
Closed

Static check for noalloc: ignore allocations post-dominated by a raise#863
gretay-js wants to merge 11 commits intooxcaml:mainfrom
gretay-js:alloc-check-exn

Conversation

@gretay-js
Copy link
Copy Markdown
Contributor

Adapted from another part of #707.

This PR adds attributes [@noalloc_exn ] and [@noalloc_exn assume] which are similar to [@noalloc] and [@noalloc assume], respectively, added in #825, except the allow allocation and indirect calls post-dominated by a raise.

The way we currently determine post-dominators is conservative around try-with and some other cases, so might not be able to prove everything that the user expects.

Same as [@noalloc_strict] except that it allows allocations
postdominated by a raise. In other words, when a function returns
normally, it is guaranteed not to allocate (i.e., allocations are
allowed upon exceptional return).

Enabled by the existing -alloc-check compiler flag.
otherwise all [raise] are compiled to [raise_notrace]
@gretay-js
Copy link
Copy Markdown
Contributor Author

Rebased on top of #870 to rename the attributes. This PR is now using [@noalloc] instead of [@noalloc_exn], as suggested by @lpw25. The motivation for this change is that this "relaxed" interpretation of the check is likely to be more useful in practice and should have a shorter name. Note that the meaning of this new attribute has already diverged from the meaning of [@@noalloc] on external which forbid raising exceptions from C stubs.

To distinguish the two, we could use [@zero_alloc] for the new attribute, with the corresponding [@zero_alloc_strict].

I've also updated the PR to check allocation paths on paths leading to [raise_notrace], so that allocations will only be ignored if postdominated by a raise with a backtrace, which is intended for error handling.

@gretay-js gretay-js marked this pull request as draft October 6, 2022 15:38
@gretay-js
Copy link
Copy Markdown
Contributor Author

The handling of try-with is not right, thanks @poechsel for this example:

try raise (Exn n) with Exn n -> n

the non-strict check passes, but the intended meaning here is for a check to fail because there is allocation on the “normal” return of this expression. Thanks @lpw25 for this definition. To implemented it not overly conservatively I think we can use the result of the strict check for the body of the try. I am making this PR into a Draft for now.

@Gbury
Copy link
Copy Markdown
Contributor

Gbury commented Apr 3, 2023

Can we close this one since #1157 has been opened ?

@gretay-js
Copy link
Copy Markdown
Contributor Author

superseded by #1157

@gretay-js gretay-js closed this Apr 7, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants