Actual assume vs assert distinction, named rules, move to aarch64 files
#62
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
pushed a commit
that referenced
this pull request
May 26, 2023
Add a `byte-array` proc-macro crate for converting strings into byte arrays that don't use static initializers, and use it to implement `eprintln`, an `unreachable` that prints the line number, and other macros.
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Sep 22, 2024
Ensure that `isaspec` output is deterministic. Previously `HashSet` iteration order was causing randomness. This PR sorts the outputs. Updates avanhatt#62
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Sep 22, 2024
When generating specs from ASLp, we have to define a mapping between spec inputs and variables in the derived constraints. Previously we would do this lazily by introducing equality constraints. This not only looks awful avanhatt#62, but anecdotally may also have solver performance implications. This PR updates the spec generation to substitute the mapped expressions for the variables instead. Updates avanhatt#62 avanhatt#37
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Sep 23, 2024
This PR changes the `isaspec` tool to generate multiple files. As we extend the use of ASLp, we are generating a lot of spec code. This is especially true for `BitRR` which we'll be adding soon. Allowing the tool to generate more than one file will hopefully make them a bit more manageable. Updates avanhatt#35 avanhatt#62
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Sep 23, 2024
Generate ASLp-based spec for the `BitRR` instruction `Cls` opcode. Updates avanhatt#35 avanhatt#42 avanhatt#62
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Oct 9, 2024
Now we have the `(with ...)` scope there is no need to use unique `v<i>_<j>` prefixes for temporary variables. This PR switches to use `t<i>` names. Aside from looking nicer it also removes a piece of config we need to track. Updates avanhatt#62
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Oct 9, 2024
Upgrade `aslp` to the latest version. No longer necessary to depend on fork since UQ-PAC/aslp#107 has landed. PR UQ-PAC/aslp#110 also made some helpful simplifications. Updates avanhatt#62 avanhatt#63
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
Make `isaspec` output line length configurable, and increase it to 120. Updates avanhatt#62
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.
No description provided.