Cranelift: ISLE recursion check #12474
Conversation
mmcloughlin
requested review from
alexcrichton
and removed request for
a team
cfallin
left a comment
cfallin
left a comment
There was a problem hiding this comment.
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 rec cycle must have rec, and any term with rec must participate in a recursive cycle, is that right?
Naively, at least coming from experience with other "permissive superset" features of languages, I would expect rec to permit recursion but not require it (e.g., unsafe in Rust, or letrec chains 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!
| pub multi: bool, | ||
| /// Whether this term's constructor can fail to match. | ||
| pub partial: bool, | ||
| /// Whether this term is recursive. |
There was a problem hiding this 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 have rec?
There was a problem hiding this comment.
Ah, after reading further, I see that actually all terms in the cycle must have rec, and all terms with rec must participate in a cycle; is that right?
| rules: Vec<Span>, | ||
| }, | ||
|
|
||
| /// Recurive rules error. Term is recursive without explicit opt-in, or vice versa. |
There was a problem hiding this comment.
"or vice versa" implies that if a term is marked rec then it must participate in a recursive cycle?
| let mut errors = Vec::new(); | ||
| for (term_id, _) in terms { | ||
| // Check if this term is involved in a reference cycle. | ||
| let reachable = terms_reachable_from(*term_id, &term_rule_sets); |
There was a problem hiding this 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.
| ;; Helper for emitting `MInst.FpuCSel16` / `MInst.FpuCSel32` / `MInst.FpuCSel64` | ||
| ;; instructions. | ||
| (decl fpu_csel (Type Cond Reg Reg) ConsumesFlags) | ||
| (decl rec fpu_csel (Type Cond Reg Reg) ConsumesFlags) |
There was a problem hiding this 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 F16 or // 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 zero or something like that.
github-actions
bot
added
cranelift
Subscribe to Label ActionDetailsThis 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:
To subscribe or unsubscribe from this label, edit the |
2 participants
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.