bytecodealliance / bytecodealliance/wasmtime

ISLE: add flag for whether to expand internal constructors

Open
#4,089 0 comments 0 reactions 0 assignees View on GitHub
cranelift enhancement isle
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.