From b6ce6bb606058e3ffcf1ce09eb9c201f2e9c192d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 21 Jan 2021 10:55:48 +0100 Subject: [PATCH 1/3] Relax typing of classification instructions --- proposals/gc/MVP.md | 29 ++++++++++++++++++----------- 1 file changed, 18 insertions(+), 11 deletions(-) diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index 27cbd4d1b..5b4ab318b 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -325,32 +325,35 @@ Tentatively, support a type of guaranteed unboxed scalars. - `ref.is_i31 : [anyref] -> [i32]` * `br_on_func ` branches if a reference is a function - - `br_on_func $l : [anyref] -> [anyref]` - - iff `$l : [funcref]` + - `br_on_func $l : [(ref null ht)] -> [(ref null ht)]` + - iff `$l : [(ref null? ht')]` + - and `func <: ht'` - passes operand along with branch as a function * `br_on_data ` branches if a reference is compound data - - `br_on_data $l : [anyref] -> [anyref]` - - iff `$l : [dataref]` - - passes operand along with branch as a function + - `br_on_data $l : [(ref null ht)] -> [(ref null ht)]` + - iff `$l : [(ref null? ht')]` + - and `data <: ht'` + - passes operand along with branch as data * `br_on_i31 ` branches if a reference is an integer - - `br_on_func $l : [anyref] -> [anyref]` - - iff `$l : [i31ref]` - - passes operand along with branch as a function + - `br_on_i31 $l : [(ref null ht)] -> [(ref null ht)]` + - iff `$l : [(ref null? ht')]` + - and `i31 <: ht'` + - passes operand along with branch as a scalar * `ref.as_func` converts to a function reference - - `ref.as_func : [anyref] -> [funcref]` + - `ref.as_func : [anyref] -> [(ref func)]` - traps if reference is not a function - equivalent to `(block $l (param anyref) (result funcref) (br_on_func $l) (unreachable))` * `ref.as_data` converts to a data reference - - `ref.as_data : [anyref] -> [dataref]` + - `ref.as_data : [anyref] -> [(ref data)]` - traps if reference is not compound data - equivalent to `(block $l (param anyref) (result dataref) (br_on_data $l) (unreachable))` * `ref.as_i31` converts to an integer reference - - `ref.as_i31 : [anyref] -> [i31ref]` + - `ref.as_i31 : [anyref] -> [(ref i31)]` - traps if reference is not an integer - equivalent to `(block $l (param anyref) (result i31ref) (br_on_i31 $l) (unreachable))` @@ -358,6 +361,8 @@ Note: The [reference types](https://github.com/WebAssembly/reference-types) and Note: There are no instructions to check for `externref`, since that can consist of a diverse set of different object representations that would be costly to check for exhaustively. +Note: The `br_on_*` instructions allow an operand of unrelated reference type, even though this cannot possibly succeed. That's because subtyping allows to forget that information, so by the subtype substitutibility property, it would be accepted in any case. The given typing rules merely allow this type to also propagate to the result, which avoids the need to compute a least upper bound between the operand type and the target type in the typing algorithm. + #### Runtime Types @@ -439,6 +444,7 @@ This extends the [encodings](https://github.com/WebAssembly/function-references/ | -0x16 | `i31ref` | | | | -0x17 | `(rtt n $t)` | `n : u32`, `$t : typeidx` | | | -0x18 | `(rtt $t)` | `$t : typeidx` | | +| -0x19 | `dataref` | | | #### Heap Types @@ -452,6 +458,7 @@ The opcode for heap types is encoded as an `s33`. | -0x12 | `any` | | | | -0x13 | `eq` | | | | -0x16 | `i31` | | | +| -0x19 | `data` | | | #### Defined Types From d8fcbaa5c59559c69497e7397703f0c426961e2c Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 21 Jan 2021 14:04:57 +0100 Subject: [PATCH 2/3] Further relaxation --- proposals/gc/MVP.md | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index 5b4ab318b..5cd4b48cf 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -325,21 +325,24 @@ Tentatively, support a type of guaranteed unboxed scalars. - `ref.is_i31 : [anyref] -> [i32]` * `br_on_func ` branches if a reference is a function - - `br_on_func $l : [(ref null ht)] -> [(ref null ht)]` - - iff `$l : [(ref null? ht')]` - - and `func <: ht'` + - `br_on_func $l : [t] -> [t]` + - iff `$l : [t']` + - and `t <: anyref` + - and `(ref func) <: t'` - passes operand along with branch as a function * `br_on_data ` branches if a reference is compound data - - `br_on_data $l : [(ref null ht)] -> [(ref null ht)]` - - iff `$l : [(ref null? ht')]` - - and `data <: ht'` + - `br_on_data $l : [t] -> [t]` + - iff `$l : [t']` + - and `t <: anyref` + - and `(ref data) <: t'` - passes operand along with branch as data * `br_on_i31 ` branches if a reference is an integer - - `br_on_i31 $l : [(ref null ht)] -> [(ref null ht)]` - - iff `$l : [(ref null? ht')]` - - and `i31 <: ht'` + - `br_on_i31 $l : [t] -> [t]` + - iff `$l : [t']` + - and `t <: anyref` + - and `(ref i31) <: t'` - passes operand along with branch as a scalar * `ref.as_func` converts to a function reference From 265f3916ddb813f2aa1cba9ea6ff3a80b7ef0332 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 21 Jan 2021 15:32:49 +0100 Subject: [PATCH 3/3] Refine casts as well --- proposals/gc/MVP.md | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index 5cd4b48cf..56a3bf8ac 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -387,29 +387,27 @@ TODO: Add the ability to generate new (non-canonical) RTT values to implement ca RTT-based casts can only be performed with respect to concrete types, and require a data or function reference as input, which are known to carry an RTT. -* `ref.test ` tests whether a reference value's [runtime type](#values) is a [runtime subtype](#runtime) of a given RTT - - `ref.test $t : [(ref null ht) (rtt n? $t)] -> [i32]` - - iff `ht <: data` or `ht <: func` - - and `(type $t) <: ht` +* `ref.test` tests whether a reference value's [runtime type](#values) is a [runtime subtype](#runtime) of a given RTT + - `ref.test : [t' (rtt n? $t)] -> [i32]` + - iff `t' <: dataref` or `t' <: funcref` - returns 1 if the first operand is not null and its runtime type is a sub-RTT of the RTT operand, 0 otherwise -* `ref.cast ` casts a reference value down to a type given by a RTT representation - - `ref.cast $t : [(ref null1? ht) (rtt n? $t)] -> [(ref null2? $t)]` +* `ref.cast` casts a reference value down to a type given by a RTT representation + - `ref.cast : [(ref null1? ht) (rtt n? $t)] -> [(ref null2? $t)]` - iff `ht <: data` or `ht <: func` - - and `(type $t) <: ht` - and `null1? = null2?` - returns null if the first operand is null - traps if the first operand is not null and its runtime type is not a sub-RTT of the RTT operand -* `br_on_cast ` branches if a value can be cast down to a given reference type - - `br_on_cast $l $t : [(ref null ht) (rtt n? $t)] -> [(ref null ht)]` - - iff `ht <: data` or `ht <: func` - - and `(type $t) <: ht` - - and `$l : [(ref $t)]` +* `br_on_cast ` branches if a value can be cast down to a given reference type + - `br_on_cast $l : [t (rtt n? $t')] -> [t]` + - iff `$l : [t']` + - and `t <: dataref` or `t <: funcref` + - and `(ref $t) <: t'` - branches iff the first operand is not null and its runtime type is a sub-RTT of the RTT operand - passes cast operand along with branch -Note: The condition `(type $t) <: ht` isn't needed for soundness of any of the above instructions. If false, the check merely is statically known to fail. Should it be removed? +Note: These instructions allow an operand of unrelated reference type, even though this cannot possibly succeed. The reasoning is the same as for classification instructions. #### Constant Expressions