Stream: git-wasmtime

Topic: wasmtime / issue #4089 ISLE: add flag for whether to expa...

view this post on Zulip Wasmtime GitHub notifications bot (Apr 29 2022 at 20:38):

avanhatt opened issue #4089:

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:

(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:

(decl isub (Value Value) Inst)
(extractor
    (isub x y)
    (inst_data (InstructionData.Binary (Opcode.Isub) (value_array_2 x y)))
)

view this post on Zulip Wasmtime GitHub notifications bot (May 10 2022 at 03:47):

cfallin labeled issue #4089:

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:

(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:

(decl isub (Value Value) Inst)
(extractor
    (isub x y)
    (inst_data (InstructionData.Binary (Opcode.Isub) (value_array_2 x y)))
)

view this post on Zulip Wasmtime GitHub notifications bot (May 10 2022 at 03:47):

cfallin labeled issue #4089:

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:

(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:

(decl isub (Value Value) Inst)
(extractor
    (isub x y)
    (inst_data (InstructionData.Binary (Opcode.Isub) (value_array_2 x y)))
)

view this post on Zulip Wasmtime GitHub notifications bot (May 10 2022 at 03:47):

cfallin labeled issue #4089:

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:

(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:

(decl isub (Value Value) Inst)
(extractor
    (isub x y)
    (inst_data (InstructionData.Binary (Opcode.Isub) (value_array_2 x y)))
)

view this post on Zulip Wasmtime GitHub notifications bot (May 10 2022 at 03:47):

cfallin unlabeled issue #4089:

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:

(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:

(decl isub (Value Value) Inst)
(extractor
    (isub x y)
    (inst_data (InstructionData.Binary (Opcode.Isub) (value_array_2 x y)))
)

view this post on Zulip Wasmtime GitHub notifications bot (May 10 2022 at 03:48):

cfallin labeled issue #4089:

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:

(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:

(decl isub (Value Value) Inst)
(extractor
    (isub x y)
    (inst_data (InstructionData.Binary (Opcode.Isub) (value_array_2 x y)))
)

Last updated: Dec 23 2024 at 12:05 UTC