jameysharp added the isle label to Issue #8651.
jameysharp opened issue #8651:
Feature
Instead of emitting a function call when a constructor or extractor is used, under some circumstances ISLE should inline the body of the term at the call site. It currently does this for all internal extractors, but not for anything else.
Which terms are useful to inline varies depending on whether the ISLE source is being used for code generation or for formal verification, so we should figure out how best to specify that.
Benefit
If inlining is done before building the "trie-again" representation, then overlap checking can be more precise, allowing fewer rules to have priorities. The following step, of serializing the trie-again sea of nodes into a decision tree, also relies on overlap checking for optimization and can generate better code.
For the purposes of formal verification, inlining a term means that term does not need a hand-written spec because it can just be incorporated into a larger verification query.
See also #8599.
Implementation
With our current representations, inlining a term preserves semantics as long as the term is declared either
partial
ormulti
, or we can prove that for every possible input there is some rule in the term which will match that input. A reasonable approximation to the latter condition is to check if there is some rule which can match all inputs. If we add the ability to represent cases where terms currently may panic then we can inline all terms, but we can cover a lot of useful cases without doing that.Our current strategy for building a
trie_again::RuleSet
doesn't give us an easy way to inline terms which are defined by more than one rule. I'd like to see a first implementation of inlining supporting only single-rule terms; let's come back to the multi-rule terms later.In
sema.rs
, theRule::visit
method is almost exactly what we need for inlining a rule. The key difference is that instead of callingvisitor.add_arg
to create a freshPatternId
for each argument, we need to provide aPatternId
from the caller. This method will then return anExpr
to the caller, which it can use in subsequent bindings. https://github.com/bytecodealliance/wasmtime/blob/7e8abe388e7bd6ae28d4335a3cd89c8692c5c98f/cranelift/isle/isle/src/sema.rs#L870For multi-rule terms, I think the relatively simplest thing to do is add "push" and "pop" operations to the visitor traits. In
trie_again
's implementation of those traits, instead of keeping a single current rule, it would keep a collection of rules.push
would clone all of them and keep a stack of pending partial rules;pop
would add all the current rules to the rule set and restore the top group from the stack as the new current rules; and all the other visitor methods would apply to all rules in the current rules group.In the future though, I'd like to explore unifying alternatives within bindings and constraints. I think it's always possible to introduce "union" binding/constraints over a list of alternatives, and have later parts of the rule use only the values introduced by the union binding. That way there's no combinatorial explosion from inlining. It makes overlap checking and serialization more confusing though.
cc: @avanhatt @mmcloughlin
github-actions[bot] commented on issue #8651:
Subscribe to Label Action
cc @cfallin, @fitzgen
<details>
This issue or pull request has been labeled: "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>
Last updated: Dec 23 2024 at 12:05 UTC