From c2980899578c86a0e7fd74251532be94361b459c Mon Sep 17 00:00:00 2001 From: Conrad Watt Date: Sat, 17 Dec 2022 00:12:46 +0700 Subject: [PATCH 1/6] re-strengthen output null knowledge in cast instructions intended to address remaining concerns in #342 --- proposals/gc/MVP.md | 43 +++++++++++++++++++++++-------------------- 1 file changed, 23 insertions(+), 20 deletions(-) diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index a64ad58d7..ce80456ce 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -604,33 +604,36 @@ 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 ` 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 ` tries to convert a reference to a given type - - `ref.cast rt : [rt'] -> [rt]` - - iff `rt <: trt` and `rt' <: trt` for some `trt` +* `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.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?` - 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 trt) (result rt) (br_on_cast $l rt) (unreachable))` + - 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))` -* `br_on_cast ` branches if a reference has a given type - - `br_on_cast $l rt : [t0* rt'] -> [t0* rt']` +* `br_on_cast null? ` branches if a reference has a given heap type + - `br_on_cast $l null? ht : [t0* (ref null3? ht')] -> [t0* (ref null2? ht')]` - iff `$l : [t0* t']` - - and `rt <: t'` - - and `rt <: trt` and `rt' <: trt` for some `trt` + - and `(ref null4? ht) <: t'` + - and `ht <: tht` and `ht' <: tht` where `tht` is a common super type + - and `null? = null4? =/= null2? \/ null2? = null3? = null4? = epsilon` - passes operand along with branch under target type, plus possible extra args - - if `rt` contains `null`, branches on null, otherwise does not + - if `null?` is present, branches on null, otherwise does not -* `br_on_cast_fail ` branches if a reference does not have a given type - - `br_on_cast_fail $l rt : [t0* rt'] -> [t0* rt]` +* `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 null3? ht')] -> [t0* (ref null2? ht)]` - iff `$l : [t0* t']` - - and `rt' <: t'` - - and `rt <: trt` and `rt' <: trt` for some `trt` + - and `(ref null4? ht') <: t'` + - and `ht <: tht` and `ht' <: tht` where `tht` is a common super type + - and `null? = null2? =/= null4? \/ null2? = null3? = null4? = epsilon` - passes operand along with branch, plus possible extra args - - if `rt` contains `null`, does not branch on null, otherwise does + - if `null?` is present, 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. From 86308ef5265f0a20e6c2a52279be924e8b802292 Mon Sep 17 00:00:00 2001 From: Conrad Watt Date: Sat, 17 Dec 2022 00:23:36 +0700 Subject: [PATCH 2/6] fix desugaring --- 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 ce80456ce..5c4ac72e2 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -615,7 +615,7 @@ Casts work for both abstract and concrete types. In the latter case, they test i - and `null? = null2?` - 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))` + - equivalent to `(block $l (param null tht) (result ref null? ht) (br_on_cast $l null? ht) (unreachable))` * `br_on_cast null? ` branches if a reference has a given heap type - `br_on_cast $l null? ht : [t0* (ref null3? ht')] -> [t0* (ref null2? ht')]` From 547b3bfe90df7e6fe9a5bb2217194b6f220a080b Mon Sep 17 00:00:00 2001 From: Conrad Watt Date: Sat, 17 Dec 2022 00:25:11 +0700 Subject: [PATCH 3/6] fix fix desugaring --- 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 5c4ac72e2..c89deab81 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -615,7 +615,7 @@ Casts work for both abstract and concrete types. In the latter case, they test i - and `null? = null2?` - 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 null tht) (result ref null? ht) (br_on_cast $l null? ht) (unreachable))` + - equivalent to `(block $l (param (ref null tht)) (result (ref null? ht)) (br_on_cast $l null? ht) (unreachable))` * `br_on_cast null? ` branches if a reference has a given heap type - `br_on_cast $l null? ht : [t0* (ref null3? ht')] -> [t0* (ref null2? ht')]` From d6711b30bdb7357b5833d51e2b3a394e2cf4ba32 Mon Sep 17 00:00:00 2001 From: Conrad Watt Date: Sat, 17 Dec 2022 03:05:56 +0700 Subject: [PATCH 4/6] comments --- proposals/gc/MVP.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index c89deab81..c3351631d 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -610,9 +610,8 @@ Casts work for both abstract and concrete types. In the latter case, they test i - if `null?` is present, 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)]` + - `ref.cast null? ht : [(ref null ht')] -> [(ref null? ht)]` - iff `ht <: tht` and `ht' <: tht` where `tht` is a common super type - - and `null? = null2?` - 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 (ref null tht)) (result (ref null? ht)) (br_on_cast $l null? ht) (unreachable))` From 26c7f6fdc31d01c0ce4d0d31aed062d08338be05 Mon Sep 17 00:00:00 2001 From: Conrad Watt Date: Tue, 24 Jan 2023 21:56:55 +0000 Subject: [PATCH 5/6] Update MVP.md --- proposals/gc/MVP.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index c3351631d..21b95f419 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -602,6 +602,8 @@ In particular, `ref.null` is typed as before, despite the introduction of `none` #### Casts +TODO: ensure that this section is kept in sync with the results of the conversation [here](https://github.com/WebAssembly/gc/issues/342). + 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 From 15436cfe845dc56dbd31303ea32c4cfe56755af7 Mon Sep 17 00:00:00 2001 From: Conrad Watt Date: Tue, 24 Jan 2023 21:58:38 +0000 Subject: [PATCH 6/6] Update MVP.md --- 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 21b95f419..da0f29658 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -602,7 +602,7 @@ In particular, `ref.null` is typed as before, despite the introduction of `none` #### Casts -TODO: ensure that this section is kept in sync with the results of the conversation [here](https://github.com/WebAssembly/gc/issues/342). +TODO: ensure that this section (and implementations, and tests) is kept in sync with the results of the conversation [here](https://github.com/WebAssembly/gc/issues/342). 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.