Skip to content

Commit c066c64

Browse files
rossbergrossberg
authored
[spec] Fix limit validation for memory and table types (#2059)
1 parent 777e9c4 commit c066c64

File tree

6 files changed

+16
-16
lines changed

6 files changed

+16
-16
lines changed

‎specification/wasm-3.0/2.1-validation.types.spectec‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -222,11 +222,11 @@ rule Globaltype_ok:
222222

223223
rule Memtype_ok:
224224
C |- addrtype limits PAGE : OK
225-
-- Limits_ok: C |- limits : $(2^16)
225+
-- Limits_ok: C |- limits : $(2^($size(addrtype) - 16))
226226

227227
rule Tabletype_ok:
228228
C |- addrtype limits reftype : OK
229-
-- Limits_ok: C |- limits : $(2^32 - 1)
229+
-- Limits_ok: C |- limits : $(2^$size(addrtype) - 1)
230230
-- Reftype_ok: C |- reftype : OK
231231

232232

‎spectec/doc/example/output/NanoWasm.pdf‎

6 Bytes
Binary file not shown.

‎spectec/test-frontend/TEST.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3148,14 +3148,14 @@ relation Memtype_ok: `%|-%:OK`(context, memtype)
31483148
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
31493149
rule _{C : context, addrtype : addrtype, limits : limits}:
31503150
`%|-%:OK`(C, `%%PAGE`_memtype(addrtype, limits))
3151-
-- Limits_ok: `%|-%:%`(C, limits, (2 ^ 16))
3151+
-- Limits_ok: `%|-%:%`(C, limits, (2 ^ ((($size((addrtype : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat)))
31523152

31533153
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
31543154
relation Tabletype_ok: `%|-%:OK`(context, tabletype)
31553155
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
31563156
rule _{C : context, addrtype : addrtype, limits : limits, reftype : reftype}:
31573157
`%|-%:OK`(C, `%%%`_tabletype(addrtype, limits, reftype))
3158-
-- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ 32) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))
3158+
-- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ $size((addrtype : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))
31593159
-- Reftype_ok: `%|-%:OK`(C, reftype)
31603160

31613161
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec

‎spectec/test-latex/TEST.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5072,7 +5072,7 @@ $$
50725072
$$
50735073
\begin{array}{@{}c@{}}\displaystyle
50745074
\frac{
5075-
C \vdash {\mathit{limits}} : {2^{16}}
5075+
C \vdash {\mathit{limits}} : {2^{{|{\mathit{addrtype}}|} - 16}}
50765076
}{
50775077
C \vdash {\mathit{addrtype}}~{\mathit{limits}}~\mathsf{page} : \mathsf{ok}
50785078
} \, {[\textsc{\scriptsize K{-}mem}]}
@@ -5083,7 +5083,7 @@ $$
50835083
$$
50845084
\begin{array}{@{}c@{}}\displaystyle
50855085
\frac{
5086-
C \vdash {\mathit{limits}} : {2^{32}} - 1
5086+
C \vdash {\mathit{limits}} : {2^{{|{\mathit{addrtype}}|}}} - 1
50875087
\qquad
50885088
C \vdash {\mathit{reftype}} : \mathsf{ok}
50895089
}{

‎spectec/test-middlend/TEST.md‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3138,14 +3138,14 @@ relation Memtype_ok: `%|-%:OK`(context, memtype)
31383138
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
31393139
rule _{C : context, addrtype : addrtype, limits : limits}:
31403140
`%|-%:OK`(C, `%%PAGE`_memtype(addrtype, limits))
3141-
-- Limits_ok: `%|-%:%`(C, limits, (2 ^ 16))
3141+
-- Limits_ok: `%|-%:%`(C, limits, (2 ^ ((($size((addrtype : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat)))
31423142

31433143
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
31443144
relation Tabletype_ok: `%|-%:OK`(context, tabletype)
31453145
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
31463146
rule _{C : context, addrtype : addrtype, limits : limits, reftype : reftype}:
31473147
`%|-%:OK`(C, `%%%`_tabletype(addrtype, limits, reftype))
3148-
-- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ 32) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))
3148+
-- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ $size((addrtype : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))
31493149
-- Reftype_ok: `%|-%:OK`(C, reftype)
31503150

31513151
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
@@ -14492,14 +14492,14 @@ relation Memtype_ok: `%|-%:OK`(context, memtype)
1449214492
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
1449314493
rule _{C : context, addrtype : addrtype, limits : limits}:
1449414494
`%|-%:OK`(C, `%%PAGE`_memtype(addrtype, limits))
14495-
-- Limits_ok: `%|-%:%`(C, limits, (2 ^ 16))
14495+
-- Limits_ok: `%|-%:%`(C, limits, (2 ^ ((($size((addrtype : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat)))
1449614496

1449714497
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
1449814498
relation Tabletype_ok: `%|-%:OK`(context, tabletype)
1449914499
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
1450014500
rule _{C : context, addrtype : addrtype, limits : limits, reftype : reftype}:
1450114501
`%|-%:OK`(C, `%%%`_tabletype(addrtype, limits, reftype))
14502-
-- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ 32) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))
14502+
-- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ $size((addrtype : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))
1450314503
-- Reftype_ok: `%|-%:OK`(C, reftype)
1450414504

1450514505
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
@@ -25865,14 +25865,14 @@ relation Memtype_ok: `%|-%:OK`(context, memtype)
2586525865
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
2586625866
rule _{C : context, addrtype : addrtype, limits : limits}:
2586725867
`%|-%:OK`(C, `%%PAGE`_memtype(addrtype, limits))
25868-
-- Limits_ok: `%|-%:%`(C, limits, (2 ^ 16))
25868+
-- Limits_ok: `%|-%:%`(C, limits, (2 ^ ((($size((addrtype : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat)))
2586925869

2587025870
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
2587125871
relation Tabletype_ok: `%|-%:OK`(context, tabletype)
2587225872
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec
2587325873
rule _{C : context, addrtype : addrtype, limits : limits, reftype : reftype}:
2587425874
`%|-%:OK`(C, `%%%`_tabletype(addrtype, limits, reftype))
25875-
-- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ 32) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))
25875+
-- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ $size((addrtype : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))
2587625876
-- Reftype_ok: `%|-%:OK`(C, reftype)
2587725877

2587825878
;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec

‎spectec/test-prose/TEST.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14776,15 +14776,15 @@ The global type :math:`({\mathsf{mut}^?}~t)` is :ref:`valid <valid-val>` if:
1477614776
The memory type :math:`({\mathit{addrtype}}~{\mathit{limits}}~\mathsf{page})` is :ref:`valid <valid-val>` if:
1477714777

1477814778

14779-
* The limits range :math:`{\mathit{limits}}` is :ref:`valid <valid-val>` within :math:`{2^{16}}`.
14779+
* The limits range :math:`{\mathit{limits}}` is :ref:`valid <valid-val>` within :math:`{2^{{|{\mathit{addrtype}}|} - 16}}`.
1478014780

1478114781

1478214782

1478314783

1478414784
The table type :math:`({\mathit{addrtype}}~{\mathit{limits}}~{\mathit{reftype}})` is :ref:`valid <valid-val>` if:
1478514785

1478614786

14787-
* The limits range :math:`{\mathit{limits}}` is :ref:`valid <valid-val>` within :math:`{2^{32}} - 1`.
14787+
* The limits range :math:`{\mathit{limits}}` is :ref:`valid <valid-val>` within :math:`{2^{{|{\mathit{addrtype}}|}}} - 1`.
1478814788

1478914789
* The reference type :math:`{\mathit{reftype}}` is :ref:`valid <valid-val>`.
1479014790

@@ -27294,11 +27294,11 @@ Globaltype_ok
2729427294

2729527295
Memtype_ok
2729627296
- the memory type addrtype limits PAGE is valid if:
27297-
- the limits range limits is valid within (2 ^ 16).
27297+
- the limits range limits is valid within (2 ^ ($size(addrtype) - 16)).
2729827298

2729927299
Tabletype_ok
2730027300
- the table type (addrtype limits reftype) is valid if:
27301-
- the limits range limits is valid within ((2 ^ 32) - 1).
27301+
- the limits range limits is valid within ((2 ^ $size(addrtype)) - 1).
2730227302
- the reference type reftype is valid.
2730327303

2730427304
Externtype_ok

0 commit comments

Comments
 (0)