Skip to content

Commit

Permalink
Fix validation of switch. (#99)
Browse files Browse the repository at this point in the history
* Fix validation of `switch`.

The validation of `switch` was not working as intended when the
"switcher" and "switchee" had different continuation type immediates.

The fix is to replace the current continuation from the argument list
with the switched-to continuation. The previous thing happened to be
working when the "switcher" and "switchee" used the same continuation
type immediate.

I also noticed a bug in the testsuite runner. It was not running the stack switching tests since commit 70086b9. I have added the "stack-switching" subdirectory to the test script runner such that the tests are now being run again by `make test`.

Resolves #98.

* Update interpreter/valid/valid.ml

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

---------

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
  • Loading branch information
dhil and rossberg authored Nov 27, 2024
1 parent 8cd685b commit 3ac42d8
Show file tree
Hide file tree
Showing 3 changed files with 42 additions and 5 deletions.
7 changes: 4 additions & 3 deletions interpreter/valid/valid.ml
Original file line number Diff line number Diff line change
Expand Up @@ -651,14 +651,15 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
" but the type annotation has " ^ string_of_result_type ts11)
in
let et = tag c y in
let FuncT (_, t) as ft = func_type_of_tag_type c et y.at in
require (match_func_type c.types (FuncT ([], t)) ft) y.at
let FuncT (ts31, t) = func_type_of_tag_type c et y.at in
require (ts31 = []) y.at
"type mismatch in switch tag";
require (match_result_type c.types ts12 t) y.at
"type mismatch in continuation types";
require (match_result_type c.types t ts22) y.at
"type mismatch in continuation types";
ts11 --> ts21, []
let ts11' = Lib.List.lead ts11 in
(ts11' @ [RefT (Null, VarHT (StatX x.it))]) --> ts21, []

| Throw x ->
let FuncT (ts1, ts2) = func_type_of_tag_type c (tag c x) x.at in
Expand Down
3 changes: 2 additions & 1 deletion test/core/run.py
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,8 @@
simd_test_files = glob.glob(os.path.join(inputDir, "simd", "*.wast"))
gc_test_files = glob.glob(os.path.join(inputDir, "gc", "*.wast"))
multi_memory_test_files = glob.glob(os.path.join(inputDir, "multi-memory", "*.wast"))
all_test_files = main_test_files + simd_test_files + gc_test_files + multi_memory_test_files
stack_switching_test_files = glob.glob(os.path.join(inputDir, "stack-switching", "*.wast"))
all_test_files = main_test_files + simd_test_files + gc_test_files + multi_memory_test_files + stack_switching_test_files

wasmExec = arguments.wasm
wasmCommand = wasmExec + " " + arguments.opts
Expand Down
37 changes: 36 additions & 1 deletion test/core/stack-switching/cont.wast
Original file line number Diff line number Diff line change
Expand Up @@ -925,4 +925,39 @@

(elem declare func $even $odd)
)
(assert_return (invoke "main") (i32.const 10))
(assert_return (invoke "main") (i32.const 10))

(module
(type $ft0 (func))
(type $ct0 (cont $ft0))

(type $ft1 (func (param (ref $ct0))))
(type $ct1 (cont $ft1))

(tag $t)

(func $f
(cont.new $ct1 (ref.func $g))
(switch $ct1 $t)
)
(elem declare func $f)

(func $g (param (ref $ct0)))
(elem declare func $g)

(func $entry
(cont.new $ct0 (ref.func $f))
(resume $ct0 (on $t switch))
)
)

(assert_invalid
(module
(rec
(type $ft (func (param (ref $ct))))
(type $ct (cont $ft)))
(tag $t (param i32))

(func (param $k (ref $ct))
(switch $ct $t)))
"type mismatch in switch tag")

0 comments on commit 3ac42d8

Please sign in to comment.