ISLE: inlining terms

[jameysharp]

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 or multi, 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, the Rule::visit method is almost exactly what we need for inlining a rule. The key difference is that instead of calling visitor.add_arg to create a fresh PatternId for each argument, we need to provide a PatternId from the caller. This method will then return an Expr to the caller, which it can use in subsequent bindings.

wasmtime/cranelift/isle/isle/src/sema.rs

Line 870 in 7e8abe3

let value = visitor.add_arg(i, arg_ty);

For 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]

Subscribe to Label Action

cc @cfallin, @fitzgen

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 .github/subscribe-to-label.json configuration file.

Learn more.