veri: add bvsaddo spec operation #75
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
Oct 31, 2023
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Aug 8, 2024
In bytecodealliance#8873, we stopped tracking the wasi-nn's upstream WIT files temporarily because it was not clear to me at the time how to implement errors as CM resources. This PR fixes that, resuming tracking in the `vendor-wit.sh` and implementing what is needed in the wasi-nn crate. This leaves several threads unresolved, though: - it looks like the `vendor-wit.sh` has a new mechanism for retrieving files into `wit/deps`--at some point wasi-nn should migrate to use that (?) - it's not clear to me that "errors as resources" is even the best approach here; I've opened [avanhatt#75] to consider the possibility of using "errors as records" instead. - this PR identifies that the constructor for errors is in fact unnecessary, prompting an upstream change ([avanhatt#76]) that should eventually be implemented here. [avanhatt#75]: WebAssembly/wasi-nn#75 [avanhatt#76]: WebAssembly/wasi-nn#76 prtest:full
avanhatt
pushed a commit
to wellesley-prog-sys/wasmtime
that referenced
this pull request
Oct 9, 2024
Generate `aslp` test cases for load instructions. Updates avanhatt#35
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.
Adds the
bvsaddoSMT-LIB operator.This operator is due to be standardized in SMT-LIB 2.7, and is already supported in Z3.
https://groups.google.com/g/smt-lib/c/J4D99wT0aKI
Z3Prover/z3#6715