From a14861bc31c0fa42f9a8bf546fce8418d27bce2c Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 9 Dec 2022 15:00:16 +0100 Subject: [PATCH 1/3] Relax nullability for br_on_cast --- interpreter/syntax/types.ml | 4 ---- interpreter/valid/valid.ml | 20 ++++++++-------- proposals/gc/MVP.md | 33 ++++++++++++-------------- test/core/gc/br_on_cast.wast | 39 +++++++++++++++++++++++++++++++ test/core/gc/br_on_cast_fail.wast | 39 +++++++++++++++++++++++++++++++ 5 files changed, 103 insertions(+), 32 deletions(-) diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml index 6abb7cd61..ebc75133d 100644 --- a/interpreter/syntax/types.ml +++ b/interpreter/syntax/types.ml @@ -111,10 +111,6 @@ let defaultable = function (* Projections *) -let inv_null = function - | Null -> NoNull - | NoNull -> Null - let unpacked_storage_type = function | ValStorageT t -> t | PackStorageT _ -> NumT I32T diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index bfc404242..1557c4fc0 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -430,20 +430,20 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in (label c x @ [RefT (Null, ht)]) --> (label c x @ [RefT (NoNull, ht)]), [] | BrOnNonNull x -> - let (nul, ht) = peek_ref 0 s e.at in + let (_nul, ht) = peek_ref 0 s e.at in let t' = RefT (NoNull, ht) in require (label c x <> []) e.at ("type mismatch: instruction requires type " ^ string_of_val_type t' ^ " but label has " ^ string_of_result_type (label c x)); let ts0, t1 = Lib.List.split_last (label c x) in require (match_val_type c.types t' t1) e.at - ("type mismatch: instruction requires type " ^ string_of_val_type t' ^ + ("type mismatch: instruction requires type " ^ string_of_val_type t1 ^ " but label has " ^ string_of_result_type (label c x)); - (ts0 @ [RefT (nul, ht)]) --> ts0, [] + (ts0 @ [RefT (Null, ht)]) --> ts0, [] | BrOnCast (x, rt) -> - let (nul, ht) = rt in - let (nul', ht') as rt' = peek_ref 0 s e.at in + let (_nul, ht) = rt in + let rt' = peek_ref 0 s e.at in let tht = top_of_heap_type c.types ht in require (match_ref_type c.types rt' (Null, tht)) e.at @@ -457,11 +457,11 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in require (match_val_type c.types (RefT rt) t1) e.at ("type mismatch: instruction requires type " ^ string_of_ref_type rt ^ " but label has " ^ string_of_result_type (label c x)); - (ts0 @ [RefT rt']) --> (ts0 @ [RefT (inv_null nul, ht')]), [] + (ts0 @ [RefT rt']) --> (ts0 @ [RefT rt']), [] | BrOnCastFail (x, rt) -> - let (nul, ht) = rt in - let (nul', ht') as rt' = peek_ref 0 s e.at in + let (_nul, ht) = rt in + let rt' = peek_ref 0 s e.at in let tht = top_of_heap_type c.types ht in require (match_ref_type c.types rt' (Null, tht)) e.at @@ -472,8 +472,8 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : infer_in ("type mismatch: instruction requires type " ^ string_of_ref_type rt' ^ " but label has " ^ string_of_result_type (label c x)); let ts0, t1 = Lib.List.split_last (label c x) in - require (match_val_type c.types (RefT (inv_null nul, ht')) t1) e.at - ("type mismatch: instruction requires type " ^ string_of_ref_type (inv_null nul, ht') ^ + require (match_val_type c.types (RefT rt') t1) e.at + ("type mismatch: instruction requires type " ^ string_of_ref_type rt' ^ " but label has " ^ string_of_result_type (label c x)); (ts0 @ [RefT rt']) --> (ts0 @ [RefT rt]), [] diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index 029ba4bd8..9833d77ff 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -598,35 +598,32 @@ In particular, `ref.null` is typed as before, despite the introduction of `none` Casts work for both abstract and concrete types. In the latter case, they test if the operand's RTT is a sub-RTT of the target type. * `ref.test null? ` checks whether a reference has a given heap type - - `ref.test null? ht : [(ref null ht')] -> [i32]` - - iff `ht <: tht` and `ht' <: tht` where `tht` is a common super type - - if `null?` is present, returns 1 for null, otherwise 0 + - `ref.test rt : [(ref rt')] -> [i32]` + - iff `rt <: trt` and `rt' <: trt` for some `trt` + - if `rt` contains `null`, returns 1 for null, otherwise 0 * `ref.cast null? ` tries to convert to a given heap type - - `ref.cast null? ht : [(ref null ht')] -> [(ref null2? ht)]` - - iff `ht <: tht` and `ht' <: tht` where `tht` is a common super type - - and `null? = null2?` + - `ref.cast rt : [(ref rt')] -> [(ref rt)]` + - iff `rt <: trt` and `rt' <: trt` for some `tht` - traps if reference is not of requested type - - if `null?` is present, a null operand is passed through, otherwise traps on null - - equivalent to `(block $l (param anyref) (result (ref null? ht)) (br_on_cast null? ht $l) (unreachable))` + - if `rt` contains `null`, a null operand is passed through, otherwise traps on null + - equivalent to `(block $l (param anyref) (result (ref rt)) (br_on_cast rt $l) (unreachable))` * `br_on_cast null? ` branches if a reference has a given heap type - - `br_on_cast $l null? ht : [t0* (ref null ht')] -> [t0* (ref null2? ht')]` + - `br_on_cast $l rt : [t0* (ref rt')] -> [t0* (ref rt')]` - iff `$l : [t0* t']` - - and `(ref null3? ht) <: t'` - - and `ht <: tht` and `ht' <: tht` where `tht` is a common super type - - and `null? = null3? =/= null2?` + - and `(ref rt) <: t'` + - and `rt <: trt` and `rt' <: trt` for some `trt` - passes operand along with branch under target type, plus possible extra args - - if `null?` is present, branches on null, otherwise does not + - if `rt` contains `null`, branches on null, otherwise does not * `br_on_cast_fail null? ` branches if a reference does not have a given heap type - - `br_on_cast_fail $l null? ht : [t0* (ref null ht')] -> [t0* (ref null2? ht)]` + - `br_on_cast_fail $l rt : [t0* (ref rt')] -> [t0* (ref rt)]` - iff `$l : [t0* t']` - - and `(ref null3? ht') <: t'` - - and `ht <: tht` and `ht' <: tht` where `tht` is a common super type - - and `null? = null2? =/= null3?` + - and `(ref rt') <: t'` + - and `rt <: trt` and `rt' <: trt` for some `trt` - passes operand along with branch, plus possible extra args - - if `null?` is present, does not branch on null, otherwise does + - if `rt` contains `null`, does not branch on null, otherwise does Note: Cast instructions do _not_ require the operand's source type to be a supertype of the target type. It can also be a "sibling" in the same hierarchy, i.e., they only need to have a common supertype (in practice, it is sufficient to test that both types share the same top heap type.). Allowing so is necessary to maintain subtype substitutability, i.e., the ability to maintain well-typedness when operands are replaced by subtypes. diff --git a/test/core/gc/br_on_cast.wast b/test/core/gc/br_on_cast.wast index fd191dab6..6dfa9a26e 100644 --- a/test/core/gc/br_on_cast.wast +++ b/test/core/gc/br_on_cast.wast @@ -188,3 +188,42 @@ (invoke "test-sub") (invoke "test-canon") + + +;; Cases of nullability + +(module + (type $t (struct)) + + (func (param (ref any)) (result (ref $t)) + (block (result (ref any)) (br_on_cast 1 $t (local.get 0))) (unreachable) + ) + (func (param (ref null any)) (result (ref $t)) + (block (result (ref null any)) (br_on_cast 1 $t (local.get 0))) (unreachable) + ) + (func (param (ref any)) (result (ref null $t)) + (block (result (ref any)) (br_on_cast 1 null $t (local.get 0))) (unreachable) + ) + (func (param (ref null any)) (result (ref null $t)) + (block (result (ref null any)) (br_on_cast 1 null $t (local.get 0))) (unreachable) + ) +) + +(assert_invalid + (module + (type $t (struct)) + (func (param (ref any)) (result (ref $t)) + (block (result (ref any)) (br_on_cast 1 null $t (local.get 0))) (unreachable) + ) + ) + "type mismatch" +) +(assert_invalid + (module + (type $t (struct)) + (func (param (ref null any)) (result (ref $t)) + (block (result (ref any)) (br_on_cast 1 $t (local.get 0))) (unreachable) + ) + ) + "type mismatch" +) diff --git a/test/core/gc/br_on_cast_fail.wast b/test/core/gc/br_on_cast_fail.wast index 5c5199ac8..dbf8ccb2b 100644 --- a/test/core/gc/br_on_cast_fail.wast +++ b/test/core/gc/br_on_cast_fail.wast @@ -203,3 +203,42 @@ (invoke "test-sub") (invoke "test-canon") + + +;; Cases of nullability + +(module + (type $t (struct)) + + (func (param (ref any)) (result (ref any)) + (block (result (ref $t)) (br_on_cast_fail 1 $t (local.get 0))) + ) + (func (param (ref null any)) (result (ref null any)) + (block (result (ref $t)) (br_on_cast_fail 1 $t (local.get 0))) + ) + (func (param (ref any)) (result (ref any)) + (block (result (ref null $t)) (br_on_cast_fail 1 null $t (local.get 0))) (ref.as_non_null) + ) + (func (param (ref null any)) (result (ref null any)) + (block (result (ref null $t)) (br_on_cast_fail 1 null $t (local.get 0))) + ) +) + +(assert_invalid + (module + (type $t (struct)) + (func (param (ref any)) (result (ref any)) + (block (result (ref $t)) (br_on_cast_fail 1 null $t (local.get 0))) + ) + ) + "type mismatch" +) +(assert_invalid + (module + (type $t (struct)) + (func (param (ref null any)) (result (ref any)) + (block (result (ref $t)) (br_on_cast_fail 1 $t (local.get 0))) + ) + ) + "type mismatch" +) From 7844fd8a3cf5091ec728b2042e97aa7101da6ad9 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 9 Dec 2022 15:07:51 +0100 Subject: [PATCH 2/3] Typo --- proposals/gc/MVP.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index 9833d77ff..d65316375 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -604,7 +604,7 @@ Casts work for both abstract and concrete types. In the latter case, they test i * `ref.cast null? ` tries to convert to a given heap type - `ref.cast rt : [(ref rt')] -> [(ref rt)]` - - iff `rt <: trt` and `rt' <: trt` for some `tht` + - iff `rt <: trt` and `rt' <: trt` for some `trt` - traps if reference is not of requested type - if `rt` contains `null`, a null operand is passed through, otherwise traps on null - equivalent to `(block $l (param anyref) (result (ref rt)) (br_on_cast rt $l) (unreachable))` From c35baa4dfb096f8cbf26395c2004934693c51e84 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 9 Dec 2022 16:40:21 +0100 Subject: [PATCH 3/3] Rectify --- proposals/gc/MVP.md | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index d65316375..9dea55961 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -597,30 +597,30 @@ In particular, `ref.null` is typed as before, despite the introduction of `none` Casts work for both abstract and concrete types. In the latter case, they test if the operand's RTT is a sub-RTT of the target type. -* `ref.test null? ` checks whether a reference has a given heap type - - `ref.test rt : [(ref rt')] -> [i32]` +* `ref.test ` tests whether a reference has a given type + - `ref.test rt : [rt'] -> [i32]` - iff `rt <: trt` and `rt' <: trt` for some `trt` - if `rt` contains `null`, returns 1 for null, otherwise 0 -* `ref.cast null? ` tries to convert to a given heap type - - `ref.cast rt : [(ref rt')] -> [(ref rt)]` +* `ref.cast ` tries to convert a reference to a given type + - `ref.cast rt : [rt'] -> [rt]` - iff `rt <: trt` and `rt' <: trt` for some `trt` - traps if reference is not of requested type - if `rt` contains `null`, a null operand is passed through, otherwise traps on null - - equivalent to `(block $l (param anyref) (result (ref rt)) (br_on_cast rt $l) (unreachable))` + - equivalent to `(block $l (param anyref) (result rt) (br_on_cast $l rt) (unreachable))` -* `br_on_cast null? ` branches if a reference has a given heap type - - `br_on_cast $l rt : [t0* (ref rt')] -> [t0* (ref rt')]` +* `br_on_cast ` branches if a reference has a given type + - `br_on_cast $l rt : [t0* rt'] -> [t0* rt']` - iff `$l : [t0* t']` - - and `(ref rt) <: t'` + - and `rt <: t'` - and `rt <: trt` and `rt' <: trt` for some `trt` - passes operand along with branch under target type, plus possible extra args - if `rt` contains `null`, branches on null, otherwise does not -* `br_on_cast_fail null? ` branches if a reference does not have a given heap type - - `br_on_cast_fail $l rt : [t0* (ref rt')] -> [t0* (ref rt)]` +* `br_on_cast_fail ` branches if a reference does not have a given type + - `br_on_cast_fail $l rt : [t0* rt'] -> [t0* rt]` - iff `$l : [t0* t']` - - and `(ref rt') <: t'` + - and `rt' <: t'` - and `rt <: trt` and `rt' <: trt` for some `trt` - passes operand along with branch, plus possible extra args - if `rt` contains `null`, does not branch on null, otherwise does