Stream: git-wasmtime

Topic: wasmtime / PR #9178 ISLE: upstream prototype ISLE verifie...

view this post on Zulip Wasmtime GitHub notifications bot (Sep 08 2024 at 17:11):

avanhatt edited PR #9178.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 09 2024 at 22:20):

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.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 09 2024 at 22:20):

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.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 09 2024 at 22:20):

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?

view this post on Zulip Wasmtime GitHub notifications bot (Sep 09 2024 at 22:20):

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?

view this post on Zulip Wasmtime GitHub notifications bot (Sep 09 2024 at 22:20):

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?

view this post on Zulip Wasmtime GitHub notifications bot (Sep 09 2024 at 22:20):

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 add authors as well if you'd like.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 09 2024 at 22:20):

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?

view this post on Zulip Wasmtime GitHub notifications bot (Sep 09 2024 at 22:20):

cfallin created PR review comment:

likewise here re: license and authors keys

view this post on Zulip Wasmtime GitHub notifications bot (Sep 09 2024 at 22:20):

cfallin created PR review comment:

I think we should be able to use cranelift-XXX = { workspace = true }-style dependencies here?

view this post on Zulip Wasmtime GitHub notifications bot (Sep 10 2024 at 13:44):

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:

To subscribe or unsubscribe from this label, edit the <code>.github/subscribe-to-label.json</code> configuration file.

Learn more.
</details>

view this post on Zulip Wasmtime GitHub notifications bot (Sep 10 2024 at 15:58):

avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 10 2024 at 15:58):

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 uses paths for within-Cranelift dependencies.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 10 2024 at 19:09):

cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 10 2024 at 19:09):

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...

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:49):

avanhatt updated PR #9178.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:50):

avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:50):

avanhatt created PR review comment:

Done!

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:51):

avanhatt created PR review comment:

Removed the entire directory, doesn't need to be upstreamed at this point.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:51):

avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:52):

avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:52):

avanhatt created PR review comment:

Done!

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:53):

avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:53):

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).

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:53):

avanhatt edited PR review comment.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:54):

avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:54):

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).

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 16:54):

avanhatt updated PR #9178.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 17:27):

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.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 17:47):

avanhatt updated PR #9178.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 17:57):

bjorn3 submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 17:57):

bjorn3 created PR review comment:

authors = ["Alexa VanHattum", "Monica Pardeshi", "Michael McLoughlin", "Wellesley Programming Systems Lab"]

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 18:06):

avanhatt updated PR #9178.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 18:06):

avanhatt submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 18:06):

avanhatt created PR review comment:

Ah, thank you! Fixing here and another spot.

view this post on Zulip Wasmtime GitHub notifications bot (Sep 24 2024 at 18:15):

cfallin has enabled auto merge for PR #9178.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 03 2024 at 23:57):

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.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 04 2024 at 00:52):

alexcrichton merged PR #9178.

Last updated: Oct 23 2024 at 20:03 UTC