From b99ab2d66a59880bb8ffaf44ff70719372b6a1ca Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Fri, 24 May 2024 11:00:41 -0700 Subject: [PATCH] Allow table.copy between tables with different index types (#58) See #7, #6 --- interpreter/syntax/types.ml | 1 - interpreter/valid/valid.ml | 6 ++--- proposals/memory64/Overview.md | 6 ++--- test/core/table_copy_mixed.wast | 48 +++++++++++++++++++++++++++++++++ 4 files changed, 53 insertions(+), 8 deletions(-) create mode 100644 test/core/table_copy_mixed.wast diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index 493ebde96..0e5729089 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -106,7 +106,6 @@ let match_extern_type et1 et2 = | ExternGlobalType gt1, ExternGlobalType gt2 -> match_global_type gt1 gt2 | _, _ -> false - (* String conversion *) let string_of_num_type = function diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index be1966b08..c39e80dba 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -340,13 +340,11 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type | TableCopy (x, y) -> let TableType (_lim1, it1, t1) = table c x in let TableType (_lim2, it2, t2) = table c y in + let it3 = min it1 it2 in require (t1 = t2) x.at ("type mismatch: source element type " ^ string_of_ref_type t1 ^ " does not match destination element type " ^ string_of_ref_type t2); - require (it1 = it2) x.at - ("type mismatch: source index type " ^ string_of_index_type it1 ^ - " does not match destination index type " ^ string_of_index_type it2); - [value_type_of_index_type it1; value_type_of_index_type it1; value_type_of_index_type it1] --> [] + [value_type_of_index_type it1; value_type_of_index_type it2; value_type_of_index_type it3] --> [] | TableInit (x, y) -> let TableType (_lim, it, t1) = table c x in diff --git a/proposals/memory64/Overview.md b/proposals/memory64/Overview.md index ff4bfcfe5..23958bd84 100644 --- a/proposals/memory64/Overview.md +++ b/proposals/memory64/Overview.md @@ -203,9 +203,9 @@ have to support 32-bit memory addresses in their ABI. ``` - table.copy x y - ``` - C.tables[x] = it limits t - ---------------------------------- - C ⊦ table.copy x : [it it it] → [] + C.tables[d] = iN limits t C.tables[s] = iM limits t K = min {N, M} + ----------------------------------------------------------------------------- + C ⊦ table.copy d s : [iN iM iK] → [] ``` - table.init x y - ``` diff --git a/test/core/table_copy_mixed.wast b/test/core/table_copy_mixed.wast new file mode 100644 index 000000000..e34cde0d0 --- /dev/null +++ b/test/core/table_copy_mixed.wast @@ -0,0 +1,48 @@ +;; Valid cases +(module + (table $t32 30 30 funcref) + (table $t64 i64 30 30 funcref) + + (func (export "test32") + (table.copy $t32 $t32 (i32.const 13) (i32.const 2) (i32.const 3))) + + (func (export "test64") + (table.copy $t64 $t64 (i64.const 13) (i64.const 2) (i64.const 3))) + + (func (export "test_64to32") + (table.copy $t32 $t64 (i32.const 13) (i64.const 2) (i32.const 3))) + + (func (export "test_32to64") + (table.copy $t64 $t32 (i64.const 13) (i32.const 2) (i32.const 3))) +) + +;; Invalid cases +(assert_invalid (module + (table $t32 30 30 funcref) + (table $t64 i64 30 30 funcref) + + (func (export "bad_size_arg") + (table.copy $t32 $t64 (i32.const 13) (i64.const 2) (i64.const 3))) + ) + "type mismatch" +) + +(assert_invalid (module + (table $t32 30 30 funcref) + (table $t64 i64 30 30 funcref) + + (func (export "bad_src_idx") + (table.copy $t32 $t64 (i32.const 13) (i32.const 2) (i32.const 3))) + ) + "type mismatch" +) + +(assert_invalid (module + (table $t32 30 30 funcref) + (table $t64 i64 30 30 funcref) + + (func (export "bad_dst_idx") + (table.copy $t32 $t64 (i64.const 13) (i64.const 2) (i32.const 3))) + ) + "type mismatch" +)