ISLE: upstream prototype ISLE verifier (Crocus) #9178

avanhatt · 2024-08-28T17:19:53Z

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.

modified: cranelift/filetests/filetests/isa/aarch64/user_stack_maps.`lif

alexcrichton · 2024-09-04T16:39:17Z

@avanhatt for the deny/vet CI errors I have two commits at https://github.com/alexcrichton/wasmtime/commits/verifier which should resolve the issues.

alexcrichton@9c54672 - this undoes what looks like a cargo update that may have been performed during development? If you need the updates though let me know and we can try to get that working. That fixes both cargo deny and cargo vet
alexcrichton@f8e5f3e - this flags the two new crates as publish = false to fix integration with the auto-publish workflow that we have. If you want these crates published though just let me know and I can help out with that too

No need to preserve authorship on those, feel free to include the commits here however's easiest to you!

Undoes a seeming `cargo update` that was performed previously and then adds a vet for the new crate added.

This reverts commit df7b540.

avanhatt · 2024-09-08T17:11:09Z

@avanhatt for the deny/vet CI errors I have two commits at https://github.com/alexcrichton/wasmtime/commits/verifier which should resolve the issues.

@alexcrichton thanks so much for the help with these, passing all checks now!

cfallin

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 · 2024-09-09T21:45:40Z

cranelift/isle/veri/README.md

@@ -0,0 +1,287 @@
+# Crocus: An SMT-based ISLE verification tool
+
+This directory contains Crocus, a tool for verifying instruction lowering and transformation rules written in ISLE. Crocus uses an underlying SMT solver to model ISLE rules in as logical bitvectors; searching over all possible inputs to find potential soundness counterexamples.


We can cite the paper here too for folks who are curious about more details and how this has been applied, I suppose?

cfallin · 2024-09-09T21:48:22Z

cranelift/isle/veri/src/main.rs

@@ -0,0 +1,3 @@
+fn main() {


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 · 2024-09-09T21:49:22Z

cranelift/isle/veri/encodings/README.md

+Encodings Generation
+====================
+
+This directory contains some templatized SMT-LIBv2 code that encodes some operations we need in the verifier.


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?

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

cfallin · 2024-09-09T21:50:48Z

cranelift/isle/veri/veri_engine/Cargo.toml

+name = "veri_engine"
+version = "0.1.0"
+edition = "2021"
+publish = false


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.

cranelift/isle/veri/veri_engine/Cargo.toml

cfallin · 2024-09-09T21:58:01Z

cranelift/isle/veri/veri_engine/src/main.rs

+        }
+        generate_isle(gen_dir.as_path()).expect("Can't generate ISLE");
+
+        let codegen_crate_dir = cur_dir.join("../../../codegen");


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.

Done (for here, did leave the hard-coded paths in for the cargo tests that are disabled in CI).

cfallin · 2024-09-09T22:00:42Z

cranelift/isle/veri/veri_engine/src/solver/encoded_ops/cls.rs

+// Adapted from https://stackoverflow.com/questions/23856596/how-to-count-leading-zeros-in-a-32-bit-unsigned-integer
+
+pub fn cls64(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
+    // Generated code.


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?

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

cfallin · 2024-09-09T22:06:20Z

cranelift/isle/veri/veri_ir/Cargo.toml

+name = "veri_ir"
+version = "0.1.0"
+edition = "2021"
+publish = false


likewise here re: license and authors keys

github-actions · 2024-09-10T13:44:48Z

Subscribe to Label Action

cc @cfallin, @fitzgen

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 .github/subscribe-to-label.json configuration file.

Learn more.

bjorn3 · 2024-09-24T17:57:16Z

cranelift/isle/veri/veri_engine/Cargo.toml

@@ -1,5 +1,7 @@
 [package]
 name = "veri_engine"
+license = "Apache-2.0 WITH LLVM-exception"
+authors = ["Alexa VanHattum, Monica Pardeshi, Michael McLoughlin, Wellesley Programming Systems Lab"]


Suggested change

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

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

Ah, thank you! Fixing here and another spot.

This PR is intended to help unblock bytecodealliance#9178. That PR uncovered the consequence that testing the `cranelift-reader` crate alone does not work on non-x86_64 platforms. One of its tests relies on parsing the `x86_64` target specification to work, and that only works if the `x86` feature of the cranelift-codegen crate is enabled. This PR unconditionally enables this feature when testing. This was uncovered on bytecodealliance#9178 because the set of crates tested in each shard of our sharded builders depends on the set of crates in the workspace. When a new crate is added it may shuffle around which crates are tested in which location. Previously `cranelift-reader` must have been always tested with a crate that unconditionally enables `cranelift-codegen/x86` as a feature, but bytecodealliance#9178 got unlucky where it moved to a set that didn't include this, thus exposing the failure.

alexcrichton · 2024-10-03T23:57:25Z

@avanhatt looks like this PR got unlucky and exposed a preexisting problem. Sorry about that! I've tried to fix that in #9372 so once that lands this should be re-queue-able.

This PR is intended to help unblock #9178. That PR uncovered the consequence that testing the `cranelift-reader` crate alone does not work on non-x86_64 platforms. One of its tests relies on parsing the `x86_64` target specification to work, and that only works if the `x86` feature of the cranelift-codegen crate is enabled. This PR unconditionally enables this feature when testing. This was uncovered on #9178 because the set of crates tested in each shard of our sharded builders depends on the set of crates in the workspace. When a new crate is added it may shuffle around which crates are tested in which location. Previously `cranelift-reader` must have been always tested with a crate that unconditionally enables `cranelift-codegen/x86` as a feature, but #9178 got unlucky where it moved to a set that didn't include this, thus exposing the failure.

avanhatt added 4 commits August 28, 2024 13:06

Squash of verification changes 2024-08-28

2738df0

Cleanup

5d65ec7

fmt

84a5d70

More cleanup

b00271d

cfallin self-requested a review August 28, 2024 17:36

avanhatt added 8 commits August 28, 2024 13:37

clippy

e17c682

update example spec

34f769a

fmt

69122d9

null

4eeaee8

clippy part 1

67e3cd3

clippy fix, null

3f1b517

clippy part 3

63c82cc

Merge branch 'main' into upstream-08-28

2fd06af

modified: cranelift/filetests/filetests/isa/aarch64/user_stack_maps.`lif

avanhatt force-pushed the upstream-08-28 branch from 638394c to 2fd06af Compare August 30, 2024 19:07

avanhatt added 7 commits August 30, 2024 15:26

fmt

8e641dc

disable veri_engine tests in CI

d4de74d

Merge branch 'main' into upstream-08-28

d97062c

clap dependency

8183720

remove strum

df7b540

use easy-smt version

3c485c4

Merge branch 'main' into upstream-08-28

70ff965

alexcrichton and others added 4 commits September 7, 2024 20:32

Get cargo vet/deny working and passing

316aee1

Undoes a seeming `cargo update` that was performed previously and then adds a vet for the new crate added.

Flag new crates as not published

5dd1158

Revert "remove strum"

a39586e

This reverts commit df7b540.

itertools

af5512d

avanhatt marked this pull request as ready for review September 8, 2024 17:11

avanhatt requested review from a team as code owners September 8, 2024 17:11

avanhatt changed the title ~~(Draft) ISLE: upstream prototype ISLE verifier (Crocus)~~ ISLE: upstream prototype ISLE verifier (Crocus) Sep 8, 2024

cfallin approved these changes Sep 9, 2024

View reviewed changes

avanhatt added 5 commits September 24, 2024 12:46

Review feedback

24aec7e

Future work comments for encodings

a8f1d25

fmt

3fc9b68

Merge branch 'main' into upstream-08-28

15e3488

post merge Cargo.lock updates

eebfae6

bjorn3 reviewed Sep 24, 2024

View reviewed changes

authors

d7652ef

cfallin enabled auto-merge September 24, 2024 18:15

cfallin added this pull request to the merge queue Sep 24, 2024

github-merge-queue bot removed this pull request from the merge queue due to failed status checks Sep 24, 2024

alexcrichton mentioned this pull request Oct 3, 2024

Fix testing the cranelift-reader test alone #9372

Merged

alexcrichton added this pull request to the merge queue Oct 4, 2024

Merged via the queue into bytecodealliance:main with commit e498087 Oct 4, 2024
39 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

ISLE: upstream prototype ISLE verifier (Crocus) #9178

ISLE: upstream prototype ISLE verifier (Crocus) #9178

avanhatt commented Aug 28, 2024 •

edited

Loading

alexcrichton commented Sep 4, 2024

avanhatt commented Sep 8, 2024

cfallin left a comment

cfallin Sep 9, 2024

avanhatt Sep 24, 2024

cfallin Sep 9, 2024

cfallin Sep 9, 2024

avanhatt Sep 24, 2024

cfallin Sep 9, 2024

avanhatt Sep 24, 2024

cfallin Sep 9, 2024

avanhatt Sep 24, 2024 •

edited

Loading

cfallin Sep 9, 2024

avanhatt Sep 24, 2024

cfallin Sep 9, 2024

github-actions bot commented Sep 10, 2024

bjorn3 Sep 24, 2024

avanhatt Sep 24, 2024

alexcrichton commented Oct 3, 2024

		@@ -0,0 +1,287 @@
		# Crocus: An SMT-based ISLE verification tool

		This directory contains Crocus, a tool for verifying instruction lowering and transformation rules written in ISLE. Crocus uses an underlying SMT solver to model ISLE rules in as logical bitvectors; searching over all possible inputs to find potential soundness counterexamples.

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

ISLE: upstream prototype ISLE verifier (Crocus) #9178

ISLE: upstream prototype ISLE verifier (Crocus) #9178

Conversation

avanhatt commented Aug 28, 2024 • edited Loading

Alternatives considered

alexcrichton commented Sep 4, 2024

avanhatt commented Sep 8, 2024

cfallin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

avanhatt Sep 24, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

github-actions bot commented Sep 10, 2024

Subscribe to Label Action

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alexcrichton commented Oct 3, 2024

avanhatt commented Aug 28, 2024 •

edited

Loading

avanhatt Sep 24, 2024 •

edited

Loading