From 70d2af731eba74c44820c01b2c76ff09bb4423dd Mon Sep 17 00:00:00 2001 From: rajdakin Date: Mon, 7 Jul 2025 17:50:05 +0100 Subject: [PATCH 1/3] Fixed tags with recursive type definitions --- interpreter/valid/valid.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 90bf74a0..570c1447 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -125,6 +125,10 @@ let check_limits {min; max} range at msg = require (I64.le_u min max) at "size minimum must not be greater than maximum" +let check_def_type (c : context) (t : def_type) at = + match t with + | DefT (RecT sts, i) -> assert Int32.(compare i (of_int (List.length sts)) < 0) + let check_num_type (c : context) (t : num_type) at = () @@ -139,7 +143,8 @@ let check_heap_type (c : context) (t : heap_type) at = | ExnHT | NoExnHT | ExternHT | NoExternHT -> () | VarHT (StatX x) -> let _dt = type_ c (x @@ at) in () - | VarHT (RecX _) | DefHT _ -> assert false + | VarHT (RecX _) -> assert false + | DefHT dt -> check_def_type c dt at | BotHT -> () let check_ref_type (c : context) (t : ref_type) at = @@ -180,9 +185,7 @@ let check_func_type (c : context) (ft : func_type) at = let check_cont_type (c : context) (ct : cont_type) at = match ct with - | ContT (VarHT (StatX x)) -> - let _dt = func_type c (x @@ at) in () - | _ -> assert false + | ContT ht -> let _dt = func_type_of_heap_type c ht at in () let check_table_type (c : context) (tt : table_type) at = let TableT (at_, lim, t) = tt in From b34c4beef39b784cbd650fa8bc00d21310e89aad Mon Sep 17 00:00:00 2001 From: rajdakin Date: Tue, 8 Jul 2025 12:33:41 +0100 Subject: [PATCH 2/3] Fixed PR review comments --- interpreter/valid/valid.ml | 2 +- test/core/tag.wast | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 570c1447..052b2ec5 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -127,7 +127,7 @@ let check_limits {min; max} range at msg = let check_def_type (c : context) (t : def_type) at = match t with - | DefT (RecT sts, i) -> assert Int32.(compare i (of_int (List.length sts)) < 0) + | DefT (RecT sts, i) -> assert (i < Lib.List32.length sts) let check_num_type (c : context) (t : num_type) at = () diff --git a/test/core/tag.wast b/test/core/tag.wast index e970c1f4..e29c27d6 100644 --- a/test/core/tag.wast +++ b/test/core/tag.wast @@ -21,6 +21,14 @@ ;; "non-empty tag result type" ;; ) +;; Mutually recursive types +(module + (rec + (type $f (func (param (ref null $c)))) + (type $c (cont $f)) + ) + (tag (type $f)) +) ;; Link-time typing From 5d03dbadc021f35a6dd685ff30e9f7f924119864 Mon Sep 17 00:00:00 2001 From: rajdakin Date: Wed, 9 Jul 2025 11:42:40 +0100 Subject: [PATCH 3/3] Fixed PR review comment --- interpreter/valid/valid.ml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 052b2ec5..9c07c003 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -125,10 +125,6 @@ let check_limits {min; max} range at msg = require (I64.le_u min max) at "size minimum must not be greater than maximum" -let check_def_type (c : context) (t : def_type) at = - match t with - | DefT (RecT sts, i) -> assert (i < Lib.List32.length sts) - let check_num_type (c : context) (t : num_type) at = () @@ -143,8 +139,7 @@ let check_heap_type (c : context) (t : heap_type) at = | ExnHT | NoExnHT | ExternHT | NoExternHT -> () | VarHT (StatX x) -> let _dt = type_ c (x @@ at) in () - | VarHT (RecX _) -> assert false - | DefHT dt -> check_def_type c dt at + | VarHT (RecX _) | DefHT _ -> assert false | BotHT -> () let check_ref_type (c : context) (t : ref_type) at = @@ -185,7 +180,9 @@ let check_func_type (c : context) (ft : func_type) at = let check_cont_type (c : context) (ct : cont_type) at = match ct with - | ContT ht -> let _dt = func_type_of_heap_type c ht at in () + | ContT (VarHT (StatX x)) -> + let _dt = func_type c (x @@ at) in () + | _ -> assert false let check_table_type (c : context) (tt : table_type) at = let TableT (at_, lim, t) = tt in @@ -208,7 +205,7 @@ let check_memory_type (c : context) (mt : memory_type) at = let check_tag_type (c : context) (et : tag_type) at = match et with - | TagT dt -> check_func_type c (as_func_str_type (expand_def_type dt)) at + | TagT dt -> let _ft = as_func_str_type (expand_def_type dt) in () let check_global_type (c : context) (gt : global_type) at = let GlobalT (_mut, t) = gt in