From 8b04c3c08da0047551dcbe9e660a273da93a1bcd Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Thu, 14 Mar 2024 18:20:06 -0700 Subject: [PATCH] [Draft][spec] Improve typing of `br_if` `br_if` previously had type `[t* i32] -> [t*]` where `[t*]` was the type of its target label. This typing unnecessarily lost type information in cases where the actual input result type is a strict subtype of the label result type, requiring casts to recover the types that the validation algorithm already knew about before the `br_if`. Update the type of `br_if` to be `[t1* i32] -> [t1*]` where `[t*]` is a subtype of the label type `[t*]`. This type preserves types that were present before the `br_if`, even when they are strict subsets of the label result types. Update the description of principle types in the appendix to allow type variables to be constrained by upper bounds and update the validation algorithm to reflect the new typing. This current PR illustrates the intended changes only for `br_if`, but the full intended change would similarly improve the types of `br_on_null`, `br_on_non_null`, `br_on_cast`, `br_on_cast_fail`, and `local.tee`. --- document/core/appendix/algorithm.rst | 4 ++-- document/core/appendix/properties.rst | 6 +++--- document/core/valid/instructions.rst | 6 ++++-- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index 72f9eda2e..179077ac6 100644 --- a/document/core/appendix/algorithm.rst +++ b/document/core/appendix/algorithm.rst @@ -380,8 +380,8 @@ Other instructions are checked in a similar manner. case (br_if n) error_if(ctrls.size() < n) pop_val(I32) - pop_vals(label_types(ctrls[n])) - push_vals(label_types(ctrls[n])) + let vts = pop_vals(label_types(ctrls[n])) + push_vals(vts) case (br_table n* m) pop_val(I32) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 1067ff2b0..88cda94f8 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -1344,7 +1344,7 @@ The :ref:`type system ` of WebAssembly features both :ref:`subtypin That has the effect that every instruction or instruction sequence can be classified with multiple different instruction types. However, the typing rules still allow deriving *principal types* for instruction sequences. -That is, every valid instruction sequence has one particular type scheme, possibly containing some unconstrained place holder *type variables*, that is a subtype of all its valid instruction types, after substituting its type variables with suitable specific types. +That is, every valid instruction sequence has one particular type scheme, possibly containing some place holder *type variables*, that is a subtype of all its valid instruction types, after substituting its type variables with suitable specific types. Type variables may only be constrained by closed upper bounds they must :ref:`match `. Moreover, when deriving an instruction type in a "forward" manner, i.e., the *input* of the instruction sequence is already fixed to specific types, then it has a principal *output* type expressible without type variables, up to a possibly :ref:`polymorphic stack ` bottom representable with one single variable. @@ -1358,7 +1358,7 @@ In other words, "forward" principal types are effectively *closed*. A typing algorithm capable of handling *partial* instruction sequences (as might be considered for program analysis or program manipulation) needs to introduce type variables and perform substitutions, - but it does not need to perform backtracking or record any non-syntactic constraints on these type variables. + but it does not need to perform backtracking or record any non-syntactic constraints other than upper bounds on these type variables. Technically, the :ref:`syntax ` of :ref:`heap `, :ref:`value `, and :ref:`result ` types can be enriched with type variables as follows: @@ -1373,7 +1373,7 @@ Technically, the :ref:`syntax ` of :ref:`heap `, : \production{value type} & \valtype &::=& \dots ~|~ \alpha_{\valtype} ~|~ \alpha_{\X{numvectype}} \\ \production{result type} & \resulttype &::=& - [\alpha_{\valtype^\ast}^?~\valtype^\ast] \\ + [(\alpha_\valtype \matchesvaltype \valtype)^\ast~\valtype^\ast]~\text{TODO:\ ensure\ bounds\ are\ closed} \\ \end{array} where each :math:`\alpha_{\X{xyz}}` ranges over a set of type variables for syntactic class :math:`\X{xyz}`, respectively. diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 5ab841a60..316fb8204 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1960,13 +1960,15 @@ Control Instructions * Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. -* Then the instruction is valid with type :math:`[t^\ast~\I32] \to [t^\ast]`. +* Then the instruction is valid with type :math:`[t_1^\ast~\I32] \to [t_1^\ast]` for any :ref:`valid ` :ref:`result type ` :math:`[t_1^\ast]` that :ref:`matches ` :math:`[t^\ast]`. .. math:: \frac{ C.\CLABELS[l] = [t^\ast] + \qquad + C \vdashresulttypematch [t_1^\ast] \matchesresulttype [t^\ast] }{ - C \vdashinstr \BRIF~l : [t^\ast~\I32] \to [t^\ast] + C \vdashinstr \BRIF~l : [t_1^\ast~\I32] \to [t_1^\ast] } .. note::