ISLE: upstream prototype ISLE verifier (Crocus) #9178
Conversation
modified: cranelift/filetests/filetests/isa/aarch64/user_stack_maps.`lif
avanhatt
force-pushed
the
upstream-08-28
branch
from
638394c
to
2fd06af
Compare
|
@avanhatt for the deny/vet CI errors I have two commits at https://github.com/alexcrichton/wasmtime/commits/verifier which should resolve the issues.
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.
@alexcrichton thanks so much for the help with these, passing all checks now! |
avanhatt
changed the title
There was a problem hiding this comment.
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.
| @@ -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. | |||
There was a problem hiding this comment.
We can cite the paper here too for folks who are curious about more details and how this has been applied, I suppose?
| @@ -0,0 +1,3 @@ | |||
| fn main() { | |||
There was a problem hiding this 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?
| Encodings Generation | ||
| ==================== | ||
|
|
||
| This directory contains some templatized SMT-LIBv2 code that encodes some operations we need in the verifier. |
There was a problem hiding this 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?
| name = "veri_engine" | ||
| version = "0.1.0" | ||
| edition = "2021" | ||
| publish = false |
There was a problem hiding this 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.
| } | ||
| generate_isle(gen_dir.as_path()).expect("Can't generate ISLE"); | ||
|
|
||
| let codegen_crate_dir = cur_dir.join("../../../codegen"); |
There was a problem hiding this 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.
| // 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. |
There was a problem hiding this 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?
| name = "veri_ir" | ||
| version = "0.1.0" | ||
| edition = "2021" | ||
| publish = false |
There was a problem hiding this comment.
likewise here re: license and authors keys
github-actions
bot
added
cranelift
Subscribe to Label Action
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 |
Draft 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.