veri: implies spec op #99
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
avanhatt
approved these changes
Mar 18, 2024
mmcloughlin
force-pushed
the
mbm/isle-printer
branch
from
d2cd480 to
826b847
Compare
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Oct 9, 2024
Change generation of specs split on match cases so the requires uses `match` also. The change in avanhatt#101 is actually broken, though it did't trigger any errors because the specs are unused on the main branch. When working on avanhatt#99 the error does manifest. Specifically, the error is in the generated requires clauses: https://github.com/mmcloughlin/veriisle-wasmtime/blob/432bd4a86635cd82c76857689ff67c77e99cbd4e/cranelift/codegen/src/isa/aarch64/spec/loads.isle#L111-L113 This references the variable `extendop`, which does not exist. It doesn't exist because it's a field of the enum variant, and we haven't brought its fields into scope. This change updates the match case spec generation to use a match in the requires as well. This is probably a cosmetic regression avanhatt#62. If we care to we could update this in future to only use a match statement in the case where the child requires accesses the variable, but it doesn't seem worth it for now. Updates avanhatt#35 avanhatt#48
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Oct 9, 2024
Introduces an explicit unspecified type in the spec language. This is motivated by work to model memory operations avanhatt#99, and in particular the use of the `AMode` enum and its many variants. Some of the variants are unused at the moment. The unspecified type is intended to allow us to define _some_ model for them, and therefore satisfy type inference. However, unspecified type is not allowed to be used for anything non-trivial, so we would be alerted in future if we need to revise the model to a correct type. Updates avanhatt#48 avanhatt#49
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Oct 9, 2024
Derive type constraints for struct types. This now allows an `instantiate` directive for example to contain a struct field. This arises in avanhatt#99 when specifying the type instantiations of a `load`, which takes `MemFlags`. Updates avanhatt#49
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR implements the implies
=>spec operator.Note this operator already exists in the annotation IR and veri IR levels, so
this PR just does the plumbing to connect up to the parser.