bytecodealliance / bytecodealliance/wasmtime
ISLE: add flag for whether to expand internal constructors
- Dominant language
- Rust
- Stars
- 18.6k
- Forks
- 1.8k
- Avg merge
- 1d 18h
- Merged PRs (30d)
- 126
Description
#### Feature:
I'm working on a PR to add a flag for optionally _not_ expand internal constructors.
As discussed in an ISLE-verification-focused meeting earlier this week, we'd like to be able to add semantic annotations to terms that are defined with internal extractors. That is, if we have a term like:
```lisp
(decl isub (i32 i32) B)
(extractor (isub x y)
(B.B x y))
```
We would like to be able to refer to `isub` in annotations. Currently, this is not possible, because the `sema::Pattern` representation already has the internal extractor expanded in place (like a macro).
#### Benefit
(a) This will enable easier downstream verification.
(b) From our discussion, ISLE may want to use this option in the codegen phase as well in the future in some circumstances.
#### Implementation
I have a WIP PR that adds this flag to the `TermEnv` and uses it in `translate_pattern`. When the flag is set to false, we can treat the internal extractor like an external one instead of expanding it.
In addition to sema's `compile`, I'm adding an `envs_for_analysis` that sets this flag to `false` and returns the type and term environments. I added a unit test for this but need to improve it (this is the WIP part).
#### Alternatives
We could now allow annotations on internal extractors, however, this introduces a lot of complexity around the underlying, large enums for CLIF and MInst opcodes.
For example, the actual CLIF `isub` expands like this, where the `inst_data` expression is harder to translate to something like SMT:
```lisp
(decl isub (Value Value) Inst)
(extractor
(isub x y)
(inst_data (InstructionData.Binary (Opcode.Isub) (value_array_2 x y)))
)
```
Contributor guide
Assessment
This issue has not been assessed yet.