The wasm-redex from takikawa

wasm-redex's People

Contributors

Stargazers

Watchers

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

Recommend Projects