Skip to content

veri: replace TestResult::MultiType with callback#86

Merged
mmcloughlin merged 1 commit intoverify-mainfrom
mbm/test-result-expect
Nov 29, 2023
Merged

veri: replace TestResult::MultiType with callback#86
mmcloughlin merged 1 commit intoverify-mainfrom
mbm/test-result-expect

Conversation

@mmcloughlin
Copy link
Copy Markdown
Collaborator

This PR replaces the TestResult::MultiType variant with a callback that
computes the expected VerificationResult for a provided TermSignature.

The MultiType variant was only used in a single test, where it was used to
provide a list of expectations derived from isle_inst_types().

#[test]
fn test_broken_uextend() {
// In the spec for extend, zero_extend and sign_extend are swapped.
// However, this should still succeed if the input and output
// widths are the same
let instantiations: Vec<(TermSignature, VerificationResult)> = isle_inst_types()
.get(&"uextend")
.unwrap()
.iter()
.map(|sig| {
let expected = if sig.args[0] == sig.ret {
VerificationResult::Success
} else {
VerificationResult::Failure(Counterexample {})
};
(sig.clone(), expected)
})
.collect();
test_from_file_with_lhs_termname(
"./examples/broken/broken_uextend.isle",
"uextend".to_string(),
TestResult::MultiType(instantiations),
);
}

The motivation for this change is that this approach will no longer work
if we provide ISLE term signatures in the source code instead, as implemented
in #82. The term signatures will only be known later, at which point we can
use the TestResult::Expect callback to derive the expectation.

@mmcloughlin mmcloughlin changed the title replace TestResult::MultiType with callback veri: replace TestResult::MultiType with callback Nov 28, 2023
@mmcloughlin mmcloughlin requested a review from avanhatt November 28, 2023 01:00
@mmcloughlin mmcloughlin marked this pull request as ready for review November 28, 2023 01:00
@mmcloughlin mmcloughlin merged commit f87461e into verify-main Nov 29, 2023
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
Refactor `isaspec` builder to introduce explicit types for case
splitting.

This PR is a no-op for the generated specs, but it is intended to enable
a future change to support splitting over enum `match` statements
(recently added in avanhatt#85).

The `substitute` function is also moved to the `isaspec::spec` module,
alongside other helpers for manipulating spec ASTs.

Updates avanhatt#48
avanhatt pushed a commit that referenced this pull request Jan 11, 2026
The changes included in 2.0.1 are:

-  Update wasmtime/wasm-tools dependencies ([#86](bytecodealliance/wizer#86))

-  Add prebuilt packages for aarch64-unknown-linux-gnu and s390x-unknown-linux-gnu ([#87 ](bytecodealliance/wizer#87))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants