Stream: cranelift

Topic: Testing and Verifying ISLE rules


view this post on Zulip Bongjun Jang (Feb 04 2025 at 01:41):

hi everyone!
I want to listen how ISLE rules are maintained in terms of its correctness.
Is there anyone working on applying techniques such as fuzz-testing, translation validation or formal verification to ISLE rules?

thank you!

view this post on Zulip Chris Fallin (Feb 04 2025 at 01:57):

You may be interested in this talk, which I gave recently (two weeks ago) and which describes exactly this topic!

view this post on Zulip Chris Fallin (Feb 04 2025 at 01:57):

(slides here)

view this post on Zulip Chris Fallin (Feb 04 2025 at 01:58):

and you'll likely be interested in our paper here about SMT-based verification of lowering rules in ISLE; and my blog post here about translation validation in the register allocator

view this post on Zulip Chris Fallin (Feb 04 2025 at 01:58):

The ASPLOS paper project is still ongoing work, and we hope to have more at some point. I'm also continuing to push proof-carrying code forward in the background (as I described in that talk)

view this post on Zulip Chris Fallin (Feb 04 2025 at 01:59):

as far as fuzzing, it is done pervasively in the Cranelift+Wasmtime codebase; take a look at our fuzz-targets here

A lightweight WebAssembly runtime that is fast, secure, and standards-compliant - bytecodealliance/wasmtime

view this post on Zulip Bongjun Jang (Feb 04 2025 at 02:57):

I'll take a look into those, thank you!

view this post on Zulip fitzgen (he/him) (Feb 04 2025 at 21:50):

for a high level overview, there is also https://bytecodealliance.org/articles/security-and-correctness-in-wasmtime


Last updated: Feb 27 2025 at 23:03 UTC