ISLE: Add a flag to not expand interal extractors for analysis/verification (#4089)

[avanhatt]

This is a WIP PR for ISLE to add a flag to optionally not expand inline constructors.

The full details are in #4089, but the main idea is that we'd like to keep the actual term around (rather than expanding it like a macro) so that we can have annotations on the term. Rather than expanding, we treat the term like an external extractor. This change adds a flag to the TermEnv and exposes a new public function (alongside compile) called envs_for_analysis that sets the flag to false. Draft for now to get feedback on approach and improve the unit testing.

[github-actions[bot]]

Subscribe to Label Action

cc @cfallin, @fitzgen

This issue or pull request has been labeled: "cranelift", "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.

[cfallin]

I think this general approach is sound -- thanks for the early-feedback pass @avanhatt!

One general thought: I have a sense that internal-extractors-as-macro-expansion should not be special-cased, in the long run. In other words, a call to an internal extractor should happen just like a call to an external one, and it should be generated as a separate Rust function. (Just as internal constructors are handled today.) The main reason this is not the case today is that we need the inlining in order to put all of the opcode-match cases together in the trie and allow efficient instruction matching. (Otherwise, each "helper" extractor that wraps "get the inst and see if its opcode is Add" will be called, one at a time in a linear sequence.) But this is kind of a special case and really we should have a notion of "this extractor should be inlined"; it shouldn't be the default.

All of this to say: I think a refactor toward my goal, which would simultaneously serve the needs here, would be to (i) create sema::Pattern nodes for internal extractor invocations, just as we do in sema::Expr for internal constructor invocations; (ii) factor the macro-expansion bit out into a separate inlining pass. That's enough to do what you need here (omit the inlining pass invocation when doing analysis). Then the final step for my goal above is to add an inline flag to extractors, and make it non-default.

(Part of my motivation for the above is to allow if-lets in internal extractors too, but that's neither here nor there!)

If you'd be up for that as an alternative approach, I'd be grateful; if not, no worries, we can probably land a shorter-term hack if that's what is needed.

Also, this will merge-conflict with #4091; not sure which will go in first, but I'm happy to help resolve merge conflicts here if needed!

[avanhatt]

Thanks for the feedback, @cfallin!

I agree that adding this as an explicit construct at the sema level would be nicer. I'll take a stab at that refactor and circle back if that ends up being too time consuming for unblocking our verification path.

[jameysharp]

Just glancing at older PRs: is this still a direction you're interested in, @avanhatt? Or have you all found a different direction that's meeting your needs?

[avanhatt]

@jameysharp I'm still using this code on our fork, but I'll close this PR for now until we are actually at the point of merging back. Thanks!