From 5344a275f3203b4188fac768ad78c01dbc42b940 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Fri, 22 Nov 2024 21:17:36 +0100
Subject: [PATCH 1/2] 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 https://github.com/WebAssembly/stack-switching/commit/70086b9093716c2ffc958eff06a8a3bb73b9a8a2. 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.
---
 interpreter/valid/valid.ml          |  7 +++---
 test/core/run.py                    |  3 ++-
 test/core/stack-switching/cont.wast | 37 ++++++++++++++++++++++++++++-
 3 files changed, 42 insertions(+), 5 deletions(-)

diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 15b18ae7..d4adf8f8 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -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 (match_result_type c.types [] 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
diff --git a/test/core/run.py b/test/core/run.py
index 8437837c..6a5350ec 100755
--- a/test/core/run.py
+++ b/test/core/run.py
@@ -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
diff --git a/test/core/stack-switching/cont.wast b/test/core/stack-switching/cont.wast
index cc84061f..f83dfa86 100644
--- a/test/core/stack-switching/cont.wast
+++ b/test/core/stack-switching/cont.wast
@@ -925,4 +925,39 @@
 
   (elem declare func $even $odd)
 )
-(assert_return (invoke "main") (i32.const 10))
\ No newline at end of file
+(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")
\ No newline at end of file

From 9e4201820949bb1bc181e9baaf1e5503d01c0bba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Mon, 25 Nov 2024 17:29:24 +0100
Subject: [PATCH 2/2] Update interpreter/valid/valid.ml

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
---
 interpreter/valid/valid.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index d4adf8f8..7b2351ff 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -652,7 +652,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in
      in
      let et = tag c y in
      let FuncT (ts31, t) = func_type_of_tag_type c et y.at in
-     require (match_result_type c.types [] ts31) y.at
+     require (ts31 = []) y.at
        "type mismatch in switch tag";
      require (match_result_type c.types ts12 t) y.at
        "type mismatch in continuation types";