From ec264380debc3cb82bead07f1660b1effee23802 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 23 Aug 2022 14:57:56 +0200 Subject: [PATCH 1/4] [interpreter/test] Fix scoping of non-import globals --- interpreter/valid/valid.ml | 8 ++++---- test/core/data.wast | 15 +++++++-------- test/core/elem.wast | 13 ++++++++----- 3 files changed, 19 insertions(+), 17 deletions(-) diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index cfe7f310f2..9cadd23e27 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -726,10 +726,10 @@ let check_module (m : module_) = in List.iter check_type types; List.iter (check_global c1) globals; - List.iter (check_table c1) tables; - List.iter (check_memory c1) memories; - List.iter (check_elem c1) elems; - List.iter (check_data c1) datas; + List.iter (check_table c) tables; + List.iter (check_memory c) memories; + List.iter (check_elem c) elems; + List.iter (check_data c) datas; List.iter (check_func c) funcs; Lib.Option.app (check_start c) start; ignore (List.fold_left (check_export c) NameSet.empty exports); diff --git a/test/core/data.wast b/test/core/data.wast index 4f339bed4d..e0fe651820 100644 --- a/test/core/data.wast +++ b/test/core/data.wast @@ -81,9 +81,9 @@ (data (global.get $g) "a") ) -;; Use of internal globals in constant expressions is not allowed in MVP. -;; (module (memory 1) (data (global.get 0) "a") (global i32 (i32.const 0))) -;; (module (memory 1) (data (global.get $g) "a") (global $g i32 (i32.const 0))) +(module (memory 1) (data (global.get 0) "a") (global i32 (i32.const 0))) +(module (memory 1) (data (global.get $g) "a") (global $g i32 (i32.const 0))) + ;; Corner cases @@ -456,11 +456,10 @@ "constant expression required" ) -;; Use of internal globals in constant expressions is not allowed in MVP. -;; (assert_invalid -;; (module (memory 1) (data (global.get $g)) (global $g (mut i32) (i32.const 0))) -;; "constant expression required" -;; ) +(assert_invalid + (module (memory 1) (data (global.get $g)) (global $g (mut i32) (i32.const 0))) + "constant expression required" +) (assert_invalid (module diff --git a/test/core/elem.wast b/test/core/elem.wast index 575ecef811..900022de00 100644 --- a/test/core/elem.wast +++ b/test/core/elem.wast @@ -148,6 +148,10 @@ (assert_return (invoke "call-7") (i32.const 65)) (assert_return (invoke "call-9") (i32.const 66)) +(module (table 1 funcref) (elem (global.get 0) $f) (global i32 (i32.const 0)) (func $f)) +(module (table 1 funcref) (elem (global.get $g) $f) (global $g i32 (i32.const 0)) (func $f)) + + ;; Corner cases (module @@ -425,11 +429,10 @@ "constant expression required" ) -;; Use of internal globals in constant expressions is not allowed in MVP. -;; (assert_invalid -;; (module (table 1 funcref) (elem (global.get $g)) (global $g i32 (i32.const 0))) -;; "constant expression required" -;; ) +(assert_invalid + (module (table 1 funcref) (elem (global.get $g)) (global $g (mut i32) (i32.const 0))) + "constant expression required" +) (assert_invalid (module From 13b34b4473c48257a78c4faeb52061e9ad204adb Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 23 Aug 2022 19:28:26 +0200 Subject: [PATCH 2/4] Resolve differently --- document/core/valid/instructions.rst | 2 +- document/core/valid/modules.rst | 44 ++++++++++++++-------------- interpreter/valid/valid.ml | 8 ++--- test/core/data.wast | 16 ++++++++-- test/core/elem.wast | 16 ++++++++-- test/core/global.wast | 9 ++++++ 6 files changed, 62 insertions(+), 33 deletions(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 2676905ff9..e6faba8e96 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1641,7 +1641,7 @@ Constant Expressions } .. note:: - Currently, constant expressions occurring as initializers of :ref:`globals ` are further constrained in that contained |GLOBALGET| instructions are only allowed to refer to *imported* globals. + Currently, constant expressions occurring as initializers of :ref:`globals ` or offsets in :ref:`element ` or :ref:`data ` segments are further constrained in that contained |GLOBALGET| instructions are only allowed to refer to *imported* globals. This is enforced in the :ref:`validation rule for modules ` by constraining the context :math:`C` accordingly. The definition of constant expression may be extended in future versions of WebAssembly. diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 5b13ae7fc5..4439938da7 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -546,24 +546,33 @@ Instead, the context :math:`C` for validation of the module's content is constru * all other fields are empty. -* Under the context :math:`C`: +* For each :math:`\functype_i` in :math:`\module.\MTYPES`, + the :ref:`function type ` :math:`\functype_i` must be :ref:`valid `. - * For each :math:`\functype_i` in :math:`\module.\MTYPES`, - the :ref:`function type ` :math:`\functype_i` must be :ref:`valid `. +* Under the context :math:`C`: * For each :math:`\func_i` in :math:`\module.\MFUNCS`, the definition :math:`\func_i` must be :ref:`valid ` with a :ref:`function type ` :math:`\X{ft}_i`. + * If :math:`\module.\MSTART` is non-empty, + then :math:`\module.\MSTART` must be :ref:`valid `. + + * For each :math:`\import_i` in :math:`\module.\MIMPORTS`, + the segment :math:`\import_i` must be :ref:`valid ` with an :ref:`external type ` :math:`\X{it}_i`. + + * For each :math:`\export_i` in :math:`\module.\MEXPORTS`, + the segment :math:`\export_i` must be :ref:`valid ` with :ref:`external type ` :math:`\X{et}_i`. + +* Under the context :math:`C'`: + * For each :math:`\table_i` in :math:`\module.\MTABLES`, the definition :math:`\table_i` must be :ref:`valid ` with a :ref:`table type ` :math:`\X{tt}_i`. * For each :math:`\mem_i` in :math:`\module.\MMEMS`, the definition :math:`\mem_i` must be :ref:`valid ` with a :ref:`memory type ` :math:`\X{mt}_i`. - * For each :math:`\global_i` in :math:`\module.\MGLOBALS`: - - * Under the context :math:`C'`, - the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\X{gt}_i`. + * For each :math:`\global_i` in :math:`\module.\MGLOBALS`, + the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\X{gt}_i`. * For each :math:`\elem_i` in :math:`\module.\MELEMS`, the segment :math:`\elem_i` must be :ref:`valid ` with :ref:`reference type ` :math:`\X{rt}_i`. @@ -571,15 +580,6 @@ Instead, the context :math:`C` for validation of the module's content is constru * For each :math:`\data_i` in :math:`\module.\MDATAS`, the segment :math:`\data_i` must be :ref:`valid `. - * If :math:`\module.\MSTART` is non-empty, - then :math:`\module.\MSTART` must be :ref:`valid `. - - * For each :math:`\import_i` in :math:`\module.\MIMPORTS`, - the segment :math:`\import_i` must be :ref:`valid ` with an :ref:`external type ` :math:`\X{it}_i`. - - * For each :math:`\export_i` in :math:`\module.\MEXPORTS`, - the segment :math:`\export_i` must be :ref:`valid ` with :ref:`external type ` :math:`\X{et}_i`. - * The length of :math:`C.\CMEMS` must not be larger than :math:`1`. * All export names :math:`\export_i.\ENAME` must be different. @@ -607,15 +607,15 @@ Instead, the context :math:`C` for validation of the module's content is constru \quad (C \vdashfunc \func : \X{ft})^\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 \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 @@ -667,8 +667,8 @@ Instead, the context :math:`C` for validation of the module's content is constru 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. - The effect of defining the limited context :math:`C'` for validating the module's globals is that their initialization expressions can only access functions and imported globals and nothing else. + Globals, however, are not recursive and not accessible within :ref:`constant expressions `. + The effect of defining the limited context :math:`C'` for validating certain definitions is that these can only access functions and imported globals and nothing else. .. note:: The restriction on the number of memories may be lifted in future versions of WebAssembly. diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 9cadd23e27..cfe7f310f2 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -726,10 +726,10 @@ let check_module (m : module_) = in List.iter check_type types; List.iter (check_global c1) globals; - List.iter (check_table c) tables; - List.iter (check_memory c) memories; - List.iter (check_elem c) elems; - List.iter (check_data c) datas; + List.iter (check_table c1) tables; + List.iter (check_memory c1) memories; + List.iter (check_elem c1) elems; + List.iter (check_data c1) datas; List.iter (check_func c) funcs; Lib.Option.app (check_start c) start; ignore (List.fold_left (check_export c) NameSet.empty exports); diff --git a/test/core/data.wast b/test/core/data.wast index e0fe651820..b1e1239753 100644 --- a/test/core/data.wast +++ b/test/core/data.wast @@ -81,8 +81,14 @@ (data (global.get $g) "a") ) -(module (memory 1) (data (global.get 0) "a") (global i32 (i32.const 0))) -(module (memory 1) (data (global.get $g) "a") (global $g i32 (i32.const 0))) +(assert_invalid + (module (memory 1) (global i32 (i32.const 0)) (data (global.get 0) "a")) + "unknown global" +) +(assert_invalid + (module (memory 1) (global $g i32 (i32.const 0)) (data (global.get $g) "a")) + "unknown global" +) ;; Corner cases @@ -457,7 +463,11 @@ ) (assert_invalid - (module (memory 1) (data (global.get $g)) (global $g (mut i32) (i32.const 0))) + (module + (global $g (import "test" "g") (mut i32)) + (memory 1) + (data (global.get $g)) + ) "constant expression required" ) diff --git a/test/core/elem.wast b/test/core/elem.wast index 900022de00..af12fec635 100644 --- a/test/core/elem.wast +++ b/test/core/elem.wast @@ -148,8 +148,14 @@ (assert_return (invoke "call-7") (i32.const 65)) (assert_return (invoke "call-9") (i32.const 66)) -(module (table 1 funcref) (elem (global.get 0) $f) (global i32 (i32.const 0)) (func $f)) -(module (table 1 funcref) (elem (global.get $g) $f) (global $g i32 (i32.const 0)) (func $f)) +(assert_invalid + (module (table 1 funcref) (global i32 (i32.const 0)) (elem (global.get 0) $f) (func $f)) + "unknown global" +) +(assert_invalid + (module (table 1 funcref) (global $g i32 (i32.const 0)) (elem (global.get $g) $f) (func $f)) + "unknown global" +) ;; Corner cases @@ -430,7 +436,11 @@ ) (assert_invalid - (module (table 1 funcref) (elem (global.get $g)) (global $g (mut i32) (i32.const 0))) + (module + (global $g (import "test" "g") (mut i32)) + (table 1 funcref) + (elem (global.get $g)) + ) "constant expression required" ) diff --git a/test/core/global.wast b/test/core/global.wast index 9fa5e22311..e40a305f16 100644 --- a/test/core/global.wast +++ b/test/core/global.wast @@ -348,6 +348,15 @@ "unknown global" ) +(assert_invalid + (module (global i32 (i32.const 0)) (global i32 (global.get 0))) + "unknown global" +) +(assert_invalid + (module (global $g i32 (i32.const 0)) (global i32 (global.get $g))) + "unknown global" +) + (assert_invalid (module (global i32 (global.get 1)) (global i32 (i32.const 0))) "unknown global" From 330eff9d272cc446afcb60a0648c640de59fa2e9 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 23 Aug 2022 20:18:10 +0200 Subject: [PATCH 3/4] Wording --- document/core/valid/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index e6faba8e96..d6d5590fd0 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1641,7 +1641,7 @@ Constant Expressions } .. note:: - Currently, constant expressions occurring as initializers of :ref:`globals ` or offsets in :ref:`element ` or :ref:`data ` segments are further constrained in that contained |GLOBALGET| instructions are only allowed to refer to *imported* globals. + Currently, constant expressions occurring in :ref:`globals `, :ref:`element `, or :ref:`data ` segments are further constrained in that contained |GLOBALGET| instructions are only allowed to refer to *imported* globals. This is enforced in the :ref:`validation rule for modules ` by constraining the context :math:`C` accordingly. The definition of constant expression may be extended in future versions of WebAssembly. From 4ef9835155242902456711a4cefa03c35092305f Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 23 Aug 2022 20:35:16 +0200 Subject: [PATCH 4/4] Wording2 --- document/core/valid/modules.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 4439938da7..4c8e7b6dd5 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -667,8 +667,8 @@ Instead, the context :math:`C` for validation of the module's content is constru 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 `. - The effect of defining the limited context :math:`C'` for validating certain definitions is that these can only access functions and imported globals and nothing else. + Globals, however, are not recursive and not accessible within :ref:`constant expressions ` 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. .. note:: The restriction on the number of memories may be lifted in future versions of WebAssembly.