takikawa / wasm-redex

WebAssembly model in Redex

wasm-redex

This is a (unofficial) Redex model of the WebAssembly formalism from the paper

"Bringing the Web up to Speed with WebAssembly" by Haas et al.

It aims to model the reduction semantics of wasm but it doesn't quite cover everything in the paper. It's missing the following at least:

• module instantiation semantics
• static type system / validation

and of course likely has various bugs.

See also: the wasm reference interpreter & spec.

---

Copyright © 2019 Asumu Takikawa

Licensed under Apache License 2.0, the same as the reference interpreter & tests.

Attribution: many of the tests are derived from the reference tests.

wasm-redex's Issues

Bugs in loop and block reduction

Hi :-)!

I'm rather sure that there's a couple of bugs in your reductions for loops and blocks, at least they don't match the paper!

Consider this:

Now consider your code [0]:

   (++> (in-hole E ((block (-> (t_1 ...) (t_2 ...)) e*_0) e*_1))
        (in-hole E_outer (seq* (label k {ϵ} (in-hole E_v e*_0)) e*_1))

        (where l             ,(length (term (t_2 ...))))
        (where k             ,(length (term (t_1 ...))))
        (where (E_outer E_v) (v-split E k))
        block)

In the resulting reduction (label k ...) should be (label l ...)

[0] https://github.com/takikawa/wasm-redex/blob/master/main.rkt#L711

Onwards consider this [1]:

   (++> (in-hole E ((name e_loop (loop (-> (t_1 ...) (t_2 ...)) e*_0)) e*_1))
        (in-hole E_outer (seq* e_lbl e*_1))

        (where l             ,(length (term (t_2 ...))))
        (where k             ,(length (term (t_1 ...))))
        (where (E_outer E_v) (v-split E k))
        (where e_lbl         (label l {(seq e_loop)} (in-hole E_v e*_0)))
        loop)

In e_lbl (label l ...) ought to be (label k ...).

[1] https://github.com/takikawa/wasm-redex/blob/master/main.rkt#L719

The difference in label arity is because of blocks being "forward-jumping" and loops being "backward-jumping".

Would you like me to make a pull request for these changes?

Regards, Johan