mmcloughlin edited PR #12474.
mmcloughlin opened PR #12474 from mmcloughlin:isle-recursion-check to bytecodealliance:main:
Extends the ISLE compiler with a recursive terms check. Terms with rules that include a reference cycle are only allowed if the term explicitly opts in with the
recattribute.Recently, we have seen problems where recursive rules enable user-controlled recursion and therefore potential stack overflow enabling a compilation DoS. For example, see #12368, #12333, and #12369. With this additional compilation check, recursion is not disallowed but is more explicit, making audits easier and offering a path to eventually disallowing recursive rules altogether.
mmcloughlin updated PR #12474.
mmcloughlin updated PR #12474.
cfallin created PR review comment:
Ah, after reading further, I see that actually all terms in the cycle must have
rec, and all terms withrecmust participate in a cycle; is that right?
cfallin created PR review comment:
s/is recursive/is permitted to be recursive/, right?
If you wouldn't mind, it'd be great to update the langref at the same time (
cranelift/isle/docs/language-reference.md). In particular the semantics could use a little bit of preciseness: is it that in any cycle in the callgraph, at least one term must haverec?
cfallin created PR review comment:
In each case where we have a
rec, could we have a comment describing why it's bounded?In particular I'm thinking these should be modeled after something like Rust safety comments -- so e.g.
// Recursion: may recurse once to reuse implementation for F32 in the case of F16or// Recursion: bounded by explicit depth parameter 'depth'or// Recursion: each iteration of count_the_bits_in_isle removes one bit from value and completes when zeroor something like that.
cfallin created PR review comment:
I'm somewhat concerned about runtime here: for every term we're computing all reachable terms, which in the limit in an arbitrary graph has O(V^2) complexity, right?
Could we instead do a DFS over the forest (i.e., DFS with a toplevel loop over all nodes that starts a new DFS from a not-yet-visited node) to detect cycles? That should have O(V + E) complexity.
cfallin created PR review comment:
"or vice versa" implies that if a term is marked
recthen it must participate in a recursive cycle?
cfallin submitted PR review:
Thanks for this! I think this will be a great improvement in our ability to reason about lowering complexity.
My main question/concern is about the semantics. It appears (after reading through it all -- some comments below are written as I worked this out) that the semantics are: any term that participates in a
reccycle must haverec, and any term withrecmust participate in a recursive cycle, is that right?Naively, at least coming from experience with other "permissive superset" features of languages, I would expect
recto permit recursion but not require it (e.g.,unsafein Rust, orletrecchains of bindings in a Lisp/Scheme, or ...). But maybe this is actually good if it means it forces us to rethink carefully (and keep justifications up-to-date) if we remove the recursion, too. Regardless, I'd like to see a description of the precise semantics and a distillation of the thinking behind it in the langref, so we can preserve that intent going forward.A few other minor nits but otherwise seems fine -- thanks!
github-actions[bot] added the label cranelift:area:aarch64 on PR #12474.
github-actions[bot] added the label cranelift on PR #12474.
github-actions[bot] added the label cranelift:area:x64 on PR #12474.
github-actions[bot] added the label isle on PR #12474.
github-actions[bot] commented on PR #12474:
Subscribe to Label Action
cc @cfallin, @fitzgen
<details>
This issue or pull request has been labeled: "cranelift", "cranelift:area:aarch64", "cranelift:area:x64", "isle"Thus the following users have been cc'd because of the following labels:
- cfallin: isle
- fitzgen: isle
To subscribe or unsubscribe from this label, edit the <code>.github/subscribe-to-label.json</code> configuration file.
Learn more.
</details>
mmcloughlin updated PR #12474.
mmcloughlin updated PR #12474.
mmcloughlin commented on PR #12474:
Updated in response to review comments. Main changes:
Cycle finding via plain DFS with back-edge detection. Ideally we might use something like Johnson's Algorithm or a variant of Tarjan's, but DFS will find a cycle if there is one, and
should be good enough in practice for the term-reference graphs we have.Change
recattribute semantics to "permit recursion" rather than "permit and require recursion".- Add pass and fail test cases under
isle_examples.- Document the
recattribute in the language reference.- Provide safety comments for all existing uses of
recin ISLE backends.
mmcloughlin submitted PR review.
mmcloughlin created PR review comment:
Updated to the "permit recursion" semantics. Added a section to the language reference.
mmcloughlin created PR review comment:
Added
; Recursion: ...comments for all(decl rec ...)terms.
mmcloughlin created PR review comment:
Updated to use a DFS algorithm over the term-reference graph which should have
O(V+E)complexity.
mmcloughlin created PR review comment:
No longer has the "must participate" semantics. Updated comment accordingly.
cfallin submitted PR review:
LGTM; thanks!
cfallin added PR #12474 Cranelift: ISLE recursion check to the merge queue.
cfallin merged PR #12474.
cfallin removed PR #12474 Cranelift: ISLE recursion check from the merge queue.
Last updated: Feb 24 2026 at 04:36 UTC