avanhatt edited PR #9178.
cfallin submitted PR review:
This generally looks great -- thanks so much for the efforts (almost three years now?) to develop this and demonstrate its benefit with real-world verification results!
My comments are mostly around the integration points and diffs to existing ISLE compiler machinery, and that's also where I focused most of my energy here -- the core of the SMT lowering, type inference and related analysis was reviewed at a "looks plausible" level, as I've not been as deep into the code as you all have been. Nevertheless, that part is "self-checking" to some degree, and also not in Cranelift's critical path, so I'm not as worried about doing a fine-tooth-comb pass.
cfallin created PR review comment:
Rather than relying on the current directory to be a certain place in the tree, can we take an argument that points to the codegen crate, or the Wasmtime repo root, or something of the sort? Generally I find "must be run from this directory"-style tools to be brittle and a little annoying as the requirement isn't self-documenting, and doesn't interact well with various sorts of more complex build systems stuff or containerization or ... etc.
cfallin created PR review comment:
I think/hope we can delete this stub binary -- we don't need
cranelift/isle/veri
to be a crate, just a directory that contains other crates, right?
cfallin created PR review comment:
We can cite the paper here too for folks who are curious about more details and how this has been applied, I suppose?
cfallin created PR review comment:
I don't see any SMT-LIB code in this directory -- are there examples of input to
convert.py
? Or if no longer used, could we remove?
cfallin created PR review comment:
we'll want at least a
license
key here (hopefully same as the rest of Cranelift, "Apache-2.0 WITH LLVM-exception"), and feel free to addauthors
as well if you'd like.
cfallin created PR review comment:
perfectly fine to upstream this for now, but idle question: are there any thoughts or potential plans to have a "prelude" in native SMT-LIB that we feed to the solver, or some other way to avoid having to open-code these inlined algorithms?
cfallin created PR review comment:
likewise here re: license and authors keys
cfallin created PR review comment:
I think we should be able to use
cranelift-XXX = { workspace = true }
-style dependencies here?
github-actions[bot] commented on PR #9178:
Subscribe to Label Action
cc @cfallin, @fitzgen
<details>
This issue or pull request has been labeled: "cranelift", "cranelift:area:aarch64", "cranelift:area:x64", "cranelift:meta", "isle"Thus the following users have been cc'd because of the following labels:
- cfallin: isle
- fitzgen: isle
To subscribe or unsubscribe from this label, edit the <code>.github/subscribe-to-label.json</code> configuration file.
Learn more.
</details>
avanhatt submitted PR review.
avanhatt created PR review comment:
Currently fails with:
Caused by: error inheriting `cranelift-isle` from workspace root manifest's `workspace.dependencies.cranelift-isle`
(Also, looks like
cranelift/isle/fuzz/Cargo.toml
also usespath
s for within-Cranelift dependencies.
cfallin submitted PR review.
cfallin created PR review comment:
Ah, interesting, it looks like not all crates are part of the workspace -- there's probably a good reason for this (transitive closure of what's needed for
wasmtime
/ our public API maybe?) so I'm happy for it to stay as-is then...
avanhatt updated PR #9178.
avanhatt submitted PR review.
avanhatt created PR review comment:
Done!
avanhatt created PR review comment:
Removed the entire directory, doesn't need to be upstreamed at this point.
avanhatt submitted PR review.
avanhatt submitted PR review.
avanhatt created PR review comment:
Done!
avanhatt submitted PR review.
avanhatt created PR review comment:
Done (for here, did leave the hard-coded paths in in for the cargo tests that are disabled in CI).
avanhatt edited PR review comment.
avanhatt submitted PR review.
avanhatt created PR review comment:
Added some comments to that effect. We would eventually like the express these in the annotation language, but it's not quite there yet (we also expect
subs
to not be needed once we have rule chaining).
avanhatt updated PR #9178.
avanhatt edited PR #9178:
PR to upstream the ongoing ISLE verification work, as described in our ASPLOS 2024 paper: Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection. The motivation for this work is described in detail in the paper.
Using the tool is described in detail at cranelift/isle/veri/README.md.
Alternatives considered
We could continue to develop this work in a fork, but that runs the risk of becoming quickly out-of-date. In discussions with @cfallin, @fitzgen, and @jameysharp, we have designed the specifications and verification to sit alongside the ISLE source.
However, we have also discussed delaying the upstreaming effort to instead upstream the newer version under development by @mmcloughlin. But, this version is much further from having the coverage of the original prototype.
avanhatt updated PR #9178.
bjorn3 submitted PR review.
bjorn3 created PR review comment:
authors = ["Alexa VanHattum", "Monica Pardeshi", "Michael McLoughlin", "Wellesley Programming Systems Lab"]
avanhatt updated PR #9178.
avanhatt submitted PR review.
avanhatt created PR review comment:
Ah, thank you! Fixing here and another spot.
cfallin has enabled auto merge for PR #9178.
alexcrichton commented on PR #9178:
@avanhatt looks like this PR got unlucky and exposed a preexisting problem. Sorry about that! I've tried to fix that in https://github.com/bytecodealliance/wasmtime/pull/9372 so once that lands this should be re-queue-able.
alexcrichton merged PR #9178.
Last updated: Dec 23 2024 at 12:05 UTC