Skip to content

Commit 9979256

Browse files
raoxiaojiaraoxiaojia
authored
[spec] Add valtype validity guard to Local_ok (#2195)
1 parent ec055c0 commit 9979256

6 files changed

Lines changed: 49 additions & 24 deletions

File tree

‎specification/wasm-3.0/2.4-validation.modules.spectec‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,10 +45,12 @@ rule Table_ok:
4545

4646
rule Local_ok/set:
4747
C |- LOCAL t : SET t
48+
-- Valtype_ok: C |- t : OK
4849
-- Defaultable: |- t DEFAULTABLE
4950

5051
rule Local_ok/unset:
5152
C |- LOCAL t : UNSET t
53+
-- Valtype_ok: C |- t : OK
5254
-- Nondefaultable: |- t NONDEFAULTABLE
5355

5456
rule Func_ok:

‎specification/wasm-latest/2.4-validation.modules.spectec‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,10 +45,12 @@ rule Table_ok:
4545

4646
rule Local_ok/set:
4747
C |- LOCAL t : SET t
48+
-- Valtype_ok: C |- t : OK
4849
-- Defaultable: |- t DEFAULTABLE
4950

5051
rule Local_ok/unset:
5152
C |- LOCAL t : UNSET t
53+
-- Valtype_ok: C |- t : OK
5254
-- Nondefaultable: |- t NONDEFAULTABLE
5355

5456
rule Func_ok:

‎spectec/test-frontend/TEST.md‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4620,11 +4620,13 @@ relation Local_ok: `%|-%:%`(context, local, localtype)
46204620
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
46214621
rule set{C : context, t : valtype}:
46224622
`%|-%:%`(C, LOCAL_local(t), `%%`_localtype(SET_init, t))
4623+
-- Valtype_ok: `%|-%:OK`(C, t)
46234624
-- Defaultable: `|-%DEFAULTABLE`(t,)
46244625

46254626
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
46264627
rule unset{C : context, t : valtype}:
46274628
`%|-%:%`(C, LOCAL_local(t), `%%`_localtype(UNSET_init, t))
4629+
-- Valtype_ok: `%|-%:OK`(C, t)
46284630
-- Nondefaultable: `|-%NONDEFAULTABLE`(t,)
46294631

46304632
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
@@ -4732,13 +4734,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype)
47324734
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
47334735
rec {
47344736

4735-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:136.1-136.100
4737+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:138.1-138.100
47364738
relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
4737-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:181.1-182.17
4739+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:183.1-184.17
47384740
rule empty{C : context}:
47394741
`%|-%:%`(C, [], [])
47404742

4741-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:184.1-187.54
4743+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:186.1-189.54
47424744
rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}:
47434745
`%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`})
47444746
-- Global_ok: `%|-%:%`(C, global_1, gt_1)
@@ -4748,13 +4750,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
47484750
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
47494751
rec {
47504752

4751-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:135.1-135.98
4753+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:137.1-137.98
47524754
relation Types_ok: `%|-%:%`(context, type*, deftype*)
4753-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:173.1-174.17
4755+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:175.1-176.17
47544756
rule empty{C : context}:
47554757
`%|-%:%`(C, [], [])
47564758

4757-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:176.1-179.49
4759+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:178.1-181.49
47584760
rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}:
47594761
`%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`})
47604762
-- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`})

‎spectec/test-latex/TEST.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7661,6 +7661,8 @@ $$
76617661
$$
76627662
\begin{array}{@{}c@{}}\displaystyle
76637663
\frac{
7664+
C \vdash t : \mathsf{ok}
7665+
\qquad
76647666
{{\mathrm{default}}}_{t} \neq \epsilon
76657667
}{
76667668
C \vdash \mathsf{local}~t : \mathsf{set}~t
@@ -7672,6 +7674,8 @@ $$
76727674
$$
76737675
\begin{array}{@{}c@{}}\displaystyle
76747676
\frac{
7677+
C \vdash t : \mathsf{ok}
7678+
\qquad
76757679
{{\mathrm{default}}}_{t} = \epsilon
76767680
}{
76777681
C \vdash \mathsf{local}~t : \mathsf{unset}~t

‎spectec/test-middlend/TEST.md‎

Lines changed: 24 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -4143,11 +4143,13 @@ relation Local_ok: `%|-%:%`(context, local, localtype)
41434143
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
41444144
rule set{C : context, t : valtype}:
41454145
`%|-%:%`(C, LOCAL_local(t), `%%`_localtype(SET_init, t))
4146+
-- Valtype_ok: `%|-%:OK`(C, t)
41464147
-- Defaultable: `|-%DEFAULTABLE`(t,)
41474148

41484149
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
41494150
rule unset{C : context, t : valtype}:
41504151
`%|-%:%`(C, LOCAL_local(t), `%%`_localtype(UNSET_init, t))
4152+
-- Valtype_ok: `%|-%:OK`(C, t)
41514153
-- Nondefaultable: `|-%NONDEFAULTABLE`(t,)
41524154

41534155
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
@@ -4255,13 +4257,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype)
42554257
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
42564258
rec {
42574259

4258-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:136.1-136.100
4260+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:138.1-138.100
42594261
relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
4260-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:181.1-182.17
4262+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:183.1-184.17
42614263
rule empty{C : context}:
42624264
`%|-%:%`(C, [], [])
42634265

4264-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:184.1-187.54
4266+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:186.1-189.54
42654267
rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}:
42664268
`%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`})
42674269
-- Global_ok: `%|-%:%`(C, global_1, gt_1)
@@ -4271,13 +4273,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
42714273
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
42724274
rec {
42734275

4274-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:135.1-135.98
4276+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:137.1-137.98
42754277
relation Types_ok: `%|-%:%`(context, type*, deftype*)
4276-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:173.1-174.17
4278+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:175.1-176.17
42774279
rule empty{C : context}:
42784280
`%|-%:%`(C, [], [])
42794281

4280-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:176.1-179.49
4282+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:178.1-181.49
42814283
rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}:
42824284
`%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`})
42834285
-- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`})
@@ -16010,11 +16012,13 @@ relation Local_ok: `%|-%:%`(context, local, localtype)
1601016012
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
1601116013
rule set{C : context, t : valtype}:
1601216014
`%|-%:%`(C, LOCAL_local(t), `%%`_localtype(SET_init, t))
16015+
-- Valtype_ok: `%|-%:OK`(C, t)
1601316016
-- Defaultable: `|-%DEFAULTABLE`(t,)
1601416017

1601516018
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
1601616019
rule unset{C : context, t : valtype}:
1601716020
`%|-%:%`(C, LOCAL_local(t), `%%`_localtype(UNSET_init, t))
16021+
-- Valtype_ok: `%|-%:OK`(C, t)
1601816022
-- Nondefaultable: `|-%NONDEFAULTABLE`(t,)
1601916023

1602016024
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
@@ -16122,13 +16126,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype)
1612216126
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
1612316127
rec {
1612416128

16125-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:136.1-136.100
16129+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:138.1-138.100
1612616130
relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
16127-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:181.1-182.17
16131+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:183.1-184.17
1612816132
rule empty{C : context}:
1612916133
`%|-%:%`(C, [], [])
1613016134

16131-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:184.1-187.54
16135+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:186.1-189.54
1613216136
rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}:
1613316137
`%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`})
1613416138
-- Global_ok: `%|-%:%`(C, global_1, gt_1)
@@ -16138,13 +16142,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
1613816142
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
1613916143
rec {
1614016144

16141-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:135.1-135.98
16145+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:137.1-137.98
1614216146
relation Types_ok: `%|-%:%`(context, type*, deftype*)
16143-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:173.1-174.17
16147+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:175.1-176.17
1614416148
rule empty{C : context}:
1614516149
`%|-%:%`(C, [], [])
1614616150

16147-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:176.1-179.49
16151+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:178.1-181.49
1614816152
rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}:
1614916153
`%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`})
1615016154
-- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`})
@@ -27987,11 +27991,13 @@ relation Local_ok: `%|-%:%`(context, local, localtype)
2798727991
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
2798827992
rule set{C : context, t : valtype}:
2798927993
`%|-%:%`(C, LOCAL_local(t), `%%`_localtype(SET_init, t))
27994+
-- Valtype_ok: `%|-%:OK`(C, t)
2799027995
-- Defaultable: `|-%DEFAULTABLE`(t,)
2799127996

2799227997
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
2799327998
rule unset{C : context, t : valtype}:
2799427999
`%|-%:%`(C, LOCAL_local(t), `%%`_localtype(UNSET_init, t))
28000+
-- Valtype_ok: `%|-%:OK`(C, t)
2799528001
-- Nondefaultable: `|-%NONDEFAULTABLE`(t,)
2799628002

2799728003
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
@@ -28109,13 +28115,13 @@ relation Export_ok: `%|-%:%%`(context, export, name, externtype)
2810928115
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
2811028116
rec {
2811128117

28112-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:136.1-136.100
28118+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:138.1-138.100
2811328119
relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
28114-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:181.1-182.17
28120+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:183.1-184.17
2811528121
rule empty{C : context}:
2811628122
`%|-%:%`(C, [], [])
2811728123

28118-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:184.1-187.54
28124+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:186.1-189.54
2811928125
rule cons{C : context, global_1 : global, `global*` : global*, gt_1 : globaltype, `gt*` : globaltype*}:
2812028126
`%|-%:%`(C, [global_1] ++ global*{global <- `global*`}, [gt_1] ++ gt*{gt <- `gt*`})
2812128127
-- Global_ok: `%|-%:%`(C, global_1, gt_1)
@@ -28125,13 +28131,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
2812528131
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
2812628132
rec {
2812728133

28128-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:135.1-135.98
28134+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:137.1-137.98
2812928135
relation Types_ok: `%|-%:%`(context, type*, deftype*)
28130-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:173.1-174.17
28136+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:175.1-176.17
2813128137
rule empty{C : context}:
2813228138
`%|-%:%`(C, [], [])
2813328139

28134-
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:176.1-179.49
28140+
;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec:178.1-181.49
2813528141
rule cons{C : context, type_1 : type, `type*` : type*, `dt_1*` : deftype*, `dt*` : deftype*}:
2813628142
`%|-%:%`(C, [type_1] ++ type*{type <- `type*`}, dt_1*{dt_1 <- `dt_1*`} ++ dt*{dt <- `dt*`})
2813728143
-- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 <- `dt_1*`})

‎spectec/test-prose/TEST.md‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16881,6 +16881,8 @@ The table :math:`(\mathsf{table}~{\mathit{tabletype}}~{\mathit{expr}})` is :ref:
1688116881
The local :math:`(\mathsf{local}~t)` is :ref:`valid <valid-val>` with the local type :math:`({\mathit{init}}~t)` if:
1688216882

1688316883

16884+
* The value type :math:`t` is :ref:`valid <valid-val>`.
16885+
1688416886
* Either:
1688516887

1688616888
* The initialization status :math:`{\mathit{init}}` is of the form :math:`\mathsf{set}`.
@@ -16899,6 +16901,8 @@ The local :math:`(\mathsf{local}~t)` is :ref:`valid <valid-val>` with the local
1689916901
The local :math:`(\mathsf{local}~t)` is :ref:`valid <valid-val>` with the local type :math:`(\mathsf{set}~t)` if:
1690016902

1690116903

16904+
* The value type :math:`t` is :ref:`valid <valid-val>`.
16905+
1690216906
* A :ref:`default value <aux-default>` for :math:`t` is defined.
1690316907

1690416908

@@ -16907,6 +16911,8 @@ The local :math:`(\mathsf{local}~t)` is :ref:`valid <valid-val>` with the local
1690716911
The local :math:`(\mathsf{local}~t)` is :ref:`valid <valid-val>` with the local type :math:`(\mathsf{unset}~t)` if:
1690816912

1690916913

16914+
* The value type :math:`t` is :ref:`valid <valid-val>`.
16915+
1691016916
* A :ref:`default value <aux-default>` for :math:`t` is not defined.
1691116917

1691216918

@@ -29257,6 +29263,7 @@ Table_ok
2925729263

2925829264
Local_ok
2925929265
- the local (LOCAL t) is valid with the local type (init t) if:
29266+
- the value type t is valid.
2926029267
- Either:
2926129268
- the initialization status init is SET.
2926229269
- A :ref:`default value <aux-default>` for t is defined.
@@ -29266,10 +29273,12 @@ Local_ok
2926629273

2926729274
Local_ok/set
2926829275
- the local (LOCAL t) is valid with the local type (SET t) if:
29276+
- the value type t is valid.
2926929277
- A :ref:`default value <aux-default>` for t is defined.
2927029278

2927129279
Local_ok/unset
2927229280
- the local (LOCAL t) is valid with the local type (UNSET t) if:
29281+
- the value type t is valid.
2927329282
- A :ref:`default value <aux-default>` for t is not defined.
2927429283

2927529284
Func_ok

0 commit comments

Comments
 (0)