Merge pull request #420 from WebAssembly/spec.globals

Spec sequential visibility for globals

document/core/exec/modules.rst

@@ -291,7 +291,6 @@ Growing :ref:`memories <syntax-meminst>`
 ..................................
 
 .. todo:: update prose for types
-.. todo:: change semantics for globals
 
 The allocation function for :ref:`modules <syntax-module>` requires a suitable list of :ref:`external values <syntax-externval>` that are assumed to :ref:`match <match-externtype>` the :ref:`import <syntax-import>` vector of the module,
 a list of initialization :ref:`values <syntax-val>` for the module's :ref:`globals <syntax-global>`,
@@ -461,8 +460,6 @@ For types, however, allocation is defined in terms of :ref:`rolling <aux-roll-re
    x_{i+1} &=& x_i + m_i \land x_n = |\deftype^\ast| \\
    \end{array}
 
-.. todo:: unify with type closure somehow?
-
 
 .. scratch
    \begin{array}{rlll}
@@ -657,7 +654,7 @@ where:
 
    Similarly, module :ref:`allocation <alloc-module>` and the :ref:`evaluation <exec-expr>` of :ref:`global <syntax-global>` and :ref:`table <syntax-table>` initializers as well as :ref:`element segments <syntax-elem>` are mutually recursive because the global initialization :ref:`values <syntax-val>` :math:`\val_{\F{g}}^\ast`, :math:`\reff_{\F{t}}`, and element segment contents :math:`(\reff^\ast)^\ast` are passed to the module allocator while depending on the module instance :math:`\moduleinst` and store :math:`S'` returned by allocation.
    Again, this recursion is just a specification device.
-   In practice, the initialization values can :ref:`be determined <exec-initvals>` beforehand by staging module allocation further such that first, the module's own :math:`function instances <syntax-funcinst>` are pre-allocated in the store, then the initializer expressions are evaluated, then the rest of the module instance is allocated, and finally the new function instances' :math:`\AMODULE` fields are set to that module instance.
+   In practice, the initialization values can :ref:`be determined <exec-initvals>` beforehand by staging module allocation further such that first, the module's own :ref:`function instances <syntax-funcinst>` are pre-allocated in the store, then the initializer expressions are evaluated in order, allocating globals on the way, then the rest of the module instance is allocated, and finally the new function instances' :math:`\AMODULE` fields are set to that module instance.
    This is possible because :ref:`validation <valid-module>` ensures that initialization expressions cannot actually call a function, only take their reference.
 
    All failure conditions are checked before any observable mutation of the store takes place.

document/core/util/macros.def

@@ -1120,6 +1120,7 @@
 .. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash}
 .. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash}
 .. |vdashglobal| mathdef:: \xref{valid/modules}{valid-global}{\vdash}
+.. |vdashglobalseq| mathdef:: \xref{valid/modules}{valid-globalseq}{\vdash}
 .. |vdashelem| mathdef:: \xref{valid/modules}{valid-elem}{\vdash}
 .. |vdashelemmode| mathdef:: \xref{valid/modules}{valid-elemmode}{\vdash}
 .. |vdashdata| mathdef:: \xref{valid/modules}{valid-data}{\vdash}

document/core/valid/modules.rst

@@ -221,12 +221,15 @@ Memories :math:`\mem` are classified by :ref:`memory types <syntax-memtype>`.
    pair: validation; global
    single: abstract syntax; global
 .. _valid-global:
+.. _valid-globalseq:
 
 Globals
 ~~~~~~~
 
 Globals :math:`\global` are classified by :ref:`global types <syntax-globaltype>` of the form :math:`\mut~t`.
 
+Sequences of globals are handled incrementally, such that each definition has access to previous definitions.
+
 
 :math:`\{ \GTYPE~\mut~t, \GINIT~\expr \}`
 .........................................
@@ -251,6 +254,38 @@ Globals :math:`\global` are classified by :ref:`global types <syntax-globaltype>
    }
 
 
+:math:`\global^\ast`
+....................
+
+* If the sequence is empty, then it is valid with the empty sequence of :ref:`global types <syntax-globaltype>`.
+
+* Else:
+
+  * The first global definition must be :ref:`valid <valid-global>` with some type :ref:`global type <syntax-globaltype>` :math:`\X{gt}_1`.
+
+  * Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`global type <syntax-globaltype>` :math:`\X{gt}_1` apppended to the |CGLOBALS| vector.
+
+  * Under context :math:`C'`, the remainder of the sequence must be valid with some sequence :math:`\X{gt}^\ast` of :ref:`global types <syntax-globaltype>`.
+
+  * Then the sequence is valid with the sequence of :ref:`global types <syntax-globaltype>` consisting of :math:`\X{gt}_1` prepended to :math:`\X{gt}^\ast`.
+
+.. math::
+   ~\\
+   \frac{
+   }{
+     C \vdashglobalseq \epsilon : \epsilon
+   }
+   \qquad
+   \frac{
+     C \vdashglobal \global_1 : \X{gt}_1
+     \qquad
+     C \compose \{\CGLOBALS~\X{gt}_1\} \vdashglobalseq \global^\ast : \X{gt}^\ast
+   }{
+     C \vdashglobalseq \global_1~\global^\ast : \X{gt}_1~\X{gt}^\ast
+   }
+
+
+
 .. index:: element, table, table index, expression, constant, function index
    pair: validation; element
    single: abstract syntax; element
@@ -684,73 +719,69 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
 
   * all other fields are empty.
 
-* Under the context :math:`C`:
-
-  * For each :math:`\func_i` in :math:`\module.\MFUNCS`,
-    the definition :math:`\func_i` must be :ref:`valid <valid-func>` with a :ref:`function type <syntax-functype>` :math:`\X{ft}_i`.
-
-  * If :math:`\module.\MSTART` is non-empty,
-    then :math:`\module.\MSTART` must be :ref:`valid <valid-start>`.
-
-  * For each :math:`\import_i` in :math:`\module.\MIMPORTS`,
-    the segment :math:`\import_i` must be :ref:`valid <valid-import>` with an :ref:`external type <syntax-externtype>` :math:`\X{it}_i`.
-
-  * For each :math:`\export_i` in :math:`\module.\MEXPORTS`,
-    the segment :math:`\export_i` must be :ref:`valid <valid-export>` with :ref:`external type <syntax-externtype>` :math:`\X{et}_i`.
+* Under the context :math:`C'`,
+  the sequence :math:`\module.\MGLOBALS` of :ref:`globals <syntax-global>` must be :ref:`valid <valid-globalseq>` with a sequence :math:`\X{gt}^\ast` of :ref:`global types <syntax-globaltype>`.
 
-* Under the context :math:`C'`:
+* Under the context :math:`C`:
 
   * For each :math:`\table_i` in :math:`\module.\MTABLES`,
     the definition :math:`\table_i` must be :ref:`valid <valid-table>` with a :ref:`table type <syntax-tabletype>` :math:`\X{tt}_i`.
 
   * For each :math:`\mem_i` in :math:`\module.\MMEMS`,
     the definition :math:`\mem_i` must be :ref:`valid <valid-mem>` with a :ref:`memory type <syntax-memtype>` :math:`\X{mt}_i`.
 
-  * For each :math:`\global_i` in :math:`\module.\MGLOBALS`,
-    the definition :math:`\global_i` must be :ref:`valid <valid-global>` with a :ref:`global type <syntax-globaltype>` :math:`\X{gt}_i`.
+  * For each :math:`\func_i` in :math:`\module.\MFUNCS`,
+    the definition :math:`\func_i` must be :ref:`valid <valid-func>` with a :ref:`function type <syntax-functype>` :math:`\X{ft}_i`.
 
   * For each :math:`\elem_i` in :math:`\module.\MELEMS`,
     the segment :math:`\elem_i` must be :ref:`valid <valid-elem>` with :ref:`reference type <syntax-reftype>` :math:`\X{rt}_i`.
 
   * For each :math:`\data_i` in :math:`\module.\MDATAS`,
     the segment :math:`\data_i` must be :ref:`valid <valid-data>`.
 
-* The length of :math:`C.\CMEMS` must not be larger than :math:`1`.
+  * If :math:`\module.\MSTART` is non-empty,
+    then :math:`\module.\MSTART` must be :ref:`valid <valid-start>`.
 
-* All export names :math:`\export_i.\ENAME` must be different.
+  * For each :math:`\import_i` in :math:`\module.\MIMPORTS`,
+    the segment :math:`\import_i` must be :ref:`valid <valid-import>` with an :ref:`external type <syntax-externtype>` :math:`\X{it}_i`.
+
+  * For each :math:`\export_i` in :math:`\module.\MEXPORTS`,
+    the segment :math:`\export_i` must be :ref:`valid <valid-export>` with :ref:`external type <syntax-externtype>` :math:`\X{et}_i`.
 
 * Let :math:`\X{ft}^\ast` be the concatenation of the internal :ref:`function types <syntax-functype>` :math:`\X{ft}_i`, in index order.
 
 * Let :math:`\X{tt}^\ast` be the concatenation of the internal :ref:`table types <syntax-tabletype>` :math:`\X{tt}_i`, in index order.
 
 * Let :math:`\X{mt}^\ast` be the concatenation of the internal :ref:`memory types <syntax-memtype>` :math:`\X{mt}_i`, in index order.
 
-* Let :math:`\X{gt}^\ast` be the concatenation of the internal :ref:`global types <syntax-globaltype>` :math:`\X{gt}_i`, in index order.
-
 * Let :math:`\X{rt}^\ast` be the concatenation of the :ref:`reference types <syntax-reftype>` :math:`\X{rt}_i`, in index order.
 
 * Let :math:`\X{it}^\ast` be the concatenation of :ref:`external types <syntax-externtype>` :math:`\X{it}_i` of the imports, in index order.
 
 * Let :math:`\X{et}^\ast` be the concatenation of :ref:`external types <syntax-externtype>` :math:`\X{et}_i` of the exports, in index order.
 
+* The length of :math:`C.\CMEMS` must not be larger than :math:`1`.
+
+* All export names :math:`\export_i.\ENAME` must be different.
+
 * Then the module is valid with :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast \to \X{et}^\ast`.
 
 .. math::
    \frac{
      \begin{array}{@{}c@{}}
      C_0 \vdashtypes \type^\ast \ok
      \quad
-     (C \vdashfunc \func : \X{ft})^\ast
+     C' \vdashglobalseq \global^\ast : \X{gt}^\ast
      \quad
-     (C' \vdashtable \table : \X{tt})^\ast
+     (C \vdashtable \table : \X{tt})^\ast
      \quad
-     (C' \vdashmem \mem : \X{mt})^\ast
+     (C \vdashmem \mem : \X{mt})^\ast
      \quad
-     (C' \vdashglobal \global : \X{gt})^\ast
+     (C \vdashfunc \func : \X{ft})^\ast
      \\
-     (C' \vdashelem \elem : \X{rt})^\ast
+     (C \vdashelem \elem : \X{rt})^\ast
      \quad
-     (C' \vdashdata \data \ok)^n
+     (C \vdashdata \data \ok)^n
      \quad
      (C \vdashstart \start \ok)^?
      \quad
@@ -770,7 +801,7 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
      \\
      C = \{ \CTYPES~C_0.\CTYPES, \CFUNCS~\X{ift}^\ast\,\X{ft}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \}
      \\
-     C' = \{ \CTYPES~\type^\ast, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \}
+     C' = \{ \CTYPES~C_0.\CTYPES, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \}
      \qquad
      |C.\CMEMS| \leq 1
      \qquad
@@ -802,8 +833,7 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
    However, this recursion is just a specification device.
    All types needed to construct :math:`C` can easily be determined from a simple pre-pass over the module that does not perform any actual validation.
 
-   Globals, however, are not recursive and not accessible within :ref:`constant expressions <valid-const>` when they are defined locally.
-   The effect of defining the limited context :math:`C'` for validating certain definitions is that they can only access functions and imported globals and nothing else.
+   Globals, however, are not recursive but evaluated sequentially, such that each :ref:`constant expressions <valid-const>` only has access to imported or previously defined globals.
 
 .. note::
    The restriction on the number of memories may be lifted in future versions of WebAssembly.

test/core/global.wast

@@ -611,17 +611,76 @@
   "type mismatch"
 )
 
+
+;; Definition order
+
+(module
+  (global (export "g") i32 (i32.const 4))
+)
+(register "G")
+
+(module
+  (global $g0 (import "G" "g") i32)
+  (global $g1 i32 (i32.const 8))
+  (global $g2 i32 (global.get $g0))
+  (global $g3 i32 (global.get $g1))
+
+  (global $gn funcref (ref.null func))
+  (global $gf funcref (ref.func $f))
+  (func $f)
+
+  (table $t 10 funcref (global.get $gn))
+  (elem (table $t) (global.get $g2) funcref (ref.func $f))
+  (elem (table $t) (global.get $g3) funcref (global.get $gf))
+
+  (memory $m 1)
+  (data (global.get $g2) "\44\44\44\44")
+  (data (global.get $g3) "\88\88\88\88")
+
+  (func (export "get-elem") (param $i i32) (result funcref)
+    (table.get $t (local.get $i))
+  )
+  (func (export "get-data") (param $i i32) (result i32)
+    (i32.load (local.get $i))
+  )
+)
+
+(assert_return (invoke "get-elem" (i32.const 0)) (ref.null))
+(assert_return (invoke "get-elem" (i32.const 4)) (ref.func))
+(assert_return (invoke "get-elem" (i32.const 8)) (ref.func))
+
+(assert_return (invoke "get-data" (i32.const 4)) (i32.const 0x44444444))
+(assert_return (invoke "get-data" (i32.const 8)) (i32.const 0x88888888))
+
+(assert_invalid
+  (module 
+    (global $g1 i32 (global.get $g2))
+    (global $g2 i32 (i32.const 0))
+  )
+  "unknown global"
+)
+
+
 ;; Duplicate identifier errors
 
-(assert_malformed (module quote
-  "(global $foo i32 (i32.const 0))"
-  "(global $foo i32 (i32.const 0))")
-  "duplicate global")
-(assert_malformed (module quote
-  "(import \"\" \"\" (global $foo i32))"
-  "(global $foo i32 (i32.const 0))")
-  "duplicate global")
-(assert_malformed (module quote
-  "(import \"\" \"\" (global $foo i32))"
-  "(import \"\" \"\" (global $foo i32))")
-  "duplicate global")
+(assert_malformed
+  (module quote
+    "(global $foo i32 (i32.const 0))"
+    "(global $foo i32 (i32.const 0))"
+  )
+  "duplicate global"
+)
+(assert_malformed
+  (module quote
+    "(import \"\" \"\" (global $foo i32))"
+    "(global $foo i32 (i32.const 0))"
+  )
+  "duplicate global"
+)
+(assert_malformed
+  (module quote
+    "(import \"\" \"\" (global $foo i32))"
+    "(import \"\" \"\" (global $foo i32))"
+  )
+  "duplicate global"
+)