Skip to content

Commit d2906df

Browse files
rossbergrossberg
authored
[spec] Fix subtyping rules for bottom heaptypes (#2116)
1 parent da9ea89 commit d2906df

10 files changed

Lines changed: 211 additions & 102 deletions

File tree

‎document/core/valid/matching.rst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ $${rule:
4444
{Heaptype_sub/struct Heaptype_sub/array Heaptype_sub/func}
4545
{Heaptype_sub/typeidx-l Heaptype_sub/typeidx-r}
4646
{Heaptype_sub/rec}
47-
{Heaptype_sub/none Heaptype_sub/nofunc Heaptype_sub/noexn Heaptype_sub/noextern}
47+
{Heaptype_sub/none Heaptype_sub/nofunc} {Heaptype_sub/noexn Heaptype_sub/noextern}
4848
{Heaptype_sub/bot}
4949
}
5050
$${rule-ignore: Heaptype_sub/def}

‎interpreter/valid/match.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -83,10 +83,10 @@ let rec match_heaptype c t1 t2 =
8383
| I31HT, EqHT -> true
8484
| StructHT, EqHT -> true
8585
| ArrayHT, EqHT -> true
86-
| NoneHT, t -> match_heaptype c t AnyHT
87-
| NoFuncHT, t -> match_heaptype c t FuncHT
88-
| NoExnHT, t -> match_heaptype c t ExnHT
89-
| NoExternHT, t -> match_heaptype c t ExternHT
86+
| NoneHT, t when t <> BotHT -> match_heaptype c t AnyHT
87+
| NoFuncHT, t when t <> BotHT -> match_heaptype c t FuncHT
88+
| NoExnHT, t when t <> BotHT -> match_heaptype c t ExnHT
89+
| NoExternHT, t when t <> BotHT -> match_heaptype c t ExternHT
9090
| UseHT (Idx x1), _ -> match_heaptype c (UseHT (Def (lookup c x1))) t2
9191
| _, UseHT (Idx x2) -> match_heaptype c t1 (UseHT (Def (lookup c x2)))
9292
| UseHT (Def dt1), UseHT (Def dt2) -> match_deftype c dt1 dt2

‎specification/wasm-3.0/2.2-validation.subtyping.spectec‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,18 +69,22 @@ rule Heaptype_sub/rec:
6969
rule Heaptype_sub/none:
7070
C |- NONE <: heaptype
7171
-- Heaptype_sub: C |- heaptype <: ANY
72+
-- if heaptype =/= BOT
7273

7374
rule Heaptype_sub/nofunc:
7475
C |- NOFUNC <: heaptype
7576
-- Heaptype_sub: C |- heaptype <: FUNC
77+
-- if heaptype =/= BOT
7678

7779
rule Heaptype_sub/noexn:
7880
C |- NOEXN <: heaptype
7981
-- Heaptype_sub: C |- heaptype <: EXN
82+
-- if heaptype =/= BOT
8083

8184
rule Heaptype_sub/noextern:
8285
C |- NOEXTERN <: heaptype
8386
-- Heaptype_sub: C |- heaptype <: EXTERN
87+
-- if heaptype =/= BOT
8488

8589
rule Heaptype_sub/bot:
8690
C |- BOT <: heaptype

‎specification/wasm-latest/2.2-validation.subtyping.spectec‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,18 +69,22 @@ rule Heaptype_sub/rec:
6969
rule Heaptype_sub/none:
7070
C |- NONE <: heaptype
7171
-- Heaptype_sub: C |- heaptype <: ANY
72+
-- if heaptype =/= BOT
7273

7374
rule Heaptype_sub/nofunc:
7475
C |- NOFUNC <: heaptype
7576
-- Heaptype_sub: C |- heaptype <: FUNC
77+
-- if heaptype =/= BOT
7678

7779
rule Heaptype_sub/noexn:
7880
C |- NOEXN <: heaptype
7981
-- Heaptype_sub: C |- heaptype <: EXN
82+
-- if heaptype =/= BOT
8083

8184
rule Heaptype_sub/noextern:
8285
C |- NOEXTERN <: heaptype
8386
-- Heaptype_sub: C |- heaptype <: EXTERN
87+
-- if heaptype =/= BOT
8488

8589
rule Heaptype_sub/bot:
8690
C |- BOT <: heaptype

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

0 Bytes
Binary file not shown.

‎spectec/test-frontend/TEST.md‎

Lines changed: 28 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -2941,30 +2941,30 @@ relation Deftype_ok: `%|-%:OK`(context, deftype)
29412941

29422942
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:95.1-95.108
29432943
relation Comptype_sub: `%|-%<:%`(context, comptype, comptype)
2944-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:165.1-167.41
2944+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.41
29452945
rule struct{C : context, `ft_1*` : fieldtype*, `ft'_1*` : fieldtype*, `ft_2*` : fieldtype*}:
29462946
`%|-%<:%`(C, STRUCT_comptype(`%`_list(ft_1*{ft_1 <- `ft_1*`} ++ ft'_1*{ft'_1 <- `ft'_1*`})), STRUCT_comptype(`%`_list(ft_2*{ft_2 <- `ft_2*`})))
29472947
-- (Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2))*{ft_1 <- `ft_1*`, ft_2 <- `ft_2*`}
29482948

2949-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:169.1-171.38
2949+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-175.38
29502950
rule array{C : context, ft_1 : fieldtype, ft_2 : fieldtype}:
29512951
`%|-%<:%`(C, ARRAY_comptype(ft_1), ARRAY_comptype(ft_2))
29522952
-- Fieldtype_sub: `%|-%<:%`(C, ft_1, ft_2)
29532953

2954-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:173.1-176.41
2954+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:177.1-180.41
29552955
rule func{C : context, `t_11*` : valtype*, `t_12*` : valtype*, `t_21*` : valtype*, `t_22*` : valtype*}:
29562956
`%|-%<:%`(C, `FUNC%->%`_comptype(`%`_resulttype(t_11*{t_11 <- `t_11*`}), `%`_resulttype(t_12*{t_12 <- `t_12*`})), `FUNC%->%`_comptype(`%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_22*{t_22 <- `t_22*`})))
29572957
-- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_11*{t_11 <- `t_11*`}))
29582958
-- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_12*{t_12 <- `t_12*`}), `%`_resulttype(t_22*{t_22 <- `t_22*`}))
29592959

29602960
;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:96.1-96.107
29612961
relation Deftype_sub: `%|-%<:%`(context, deftype, deftype)
2962-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:179.1-181.66
2962+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-185.66
29632963
rule refl{C : context, deftype_1 : deftype, deftype_2 : deftype}:
29642964
`%|-%<:%`(C, deftype_1, deftype_2)
29652965
-- if ($clos_deftype(C, deftype_1) = $clos_deftype(C, deftype_2))
29662966

2967-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:183.1-186.49
2967+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:187.1-190.49
29682968
rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, `final?` : final?, `typeuse*` : typeuse*, ct : comptype, i : nat}:
29692969
`%|-%<:%`(C, deftype_1, deftype_2)
29702970
-- if ($unrolldt(deftype_1) = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct))
@@ -3034,90 +3034,94 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype)
30343034
`%|-%<:%`(C, REC_heaptype(i), (typeuse*{typeuse <- `typeuse*`}[j] : typeuse <: heaptype))
30353035
-- if (C.RECS_context[i] = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, ct))
30363036

3037-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-71.40
3037+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-72.25
30383038
rule none{C : context, heaptype : heaptype}:
30393039
`%|-%<:%`(C, NONE_heaptype, heaptype)
30403040
-- Heaptype_sub: `%|-%<:%`(C, heaptype, ANY_heaptype)
3041+
-- if (heaptype =/= BOT_heaptype)
30413042

3042-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:73.1-75.41
3043+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:74.1-77.25
30433044
rule nofunc{C : context, heaptype : heaptype}:
30443045
`%|-%<:%`(C, NOFUNC_heaptype, heaptype)
30453046
-- Heaptype_sub: `%|-%<:%`(C, heaptype, FUNC_heaptype)
3047+
-- if (heaptype =/= BOT_heaptype)
30463048

3047-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:77.1-79.40
3049+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:79.1-82.25
30483050
rule noexn{C : context, heaptype : heaptype}:
30493051
`%|-%<:%`(C, NOEXN_heaptype, heaptype)
30503052
-- Heaptype_sub: `%|-%<:%`(C, heaptype, EXN_heaptype)
3053+
-- if (heaptype =/= BOT_heaptype)
30513054

3052-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:81.1-83.43
3055+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:84.1-87.25
30533056
rule noextern{C : context, heaptype : heaptype}:
30543057
`%|-%<:%`(C, NOEXTERN_heaptype, heaptype)
30553058
-- Heaptype_sub: `%|-%<:%`(C, heaptype, EXTERN_heaptype)
3059+
-- if (heaptype =/= BOT_heaptype)
30563060

3057-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:85.1-86.23
3061+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-90.23
30583062
rule bot{C : context, heaptype : heaptype}:
30593063
`%|-%<:%`(C, BOT_heaptype, heaptype)
30603064

30613065
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:10.1-10.103
30623066
relation Reftype_sub: `%|-%<:%`(context, reftype, reftype)
3063-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:89.1-91.37
3067+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37
30643068
rule nonnull{C : context, ht_1 : heaptype, ht_2 : heaptype}:
30653069
`%|-%<:%`(C, REF_reftype(?(), ht_1), REF_reftype(?(), ht_2))
30663070
-- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2)
30673071

3068-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:93.1-95.37
3072+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:97.1-99.37
30693073
rule null{C : context, ht_1 : heaptype, ht_2 : heaptype}:
30703074
`%|-%<:%`(C, REF_reftype(NULL_null?{}, ht_1), REF_reftype(?(NULL_null), ht_2))
30713075
-- Heaptype_sub: `%|-%<:%`(C, ht_1, ht_2)
30723076

30733077
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:11.1-11.103
30743078
relation Valtype_sub: `%|-%<:%`(context, valtype, valtype)
3075-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:98.1-100.46
3079+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46
30763080
rule num{C : context, numtype_1 : numtype, numtype_2 : numtype}:
30773081
`%|-%<:%`(C, (numtype_1 : numtype <: valtype), (numtype_2 : numtype <: valtype))
30783082
-- Numtype_sub: `%|-%<:%`(C, numtype_1, numtype_2)
30793083

3080-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:102.1-104.46
3084+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46
30813085
rule vec{C : context, vectype_1 : vectype, vectype_2 : vectype}:
30823086
`%|-%<:%`(C, (vectype_1 : vectype <: valtype), (vectype_2 : vectype <: valtype))
30833087
-- Vectype_sub: `%|-%<:%`(C, vectype_1, vectype_2)
30843088

3085-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:106.1-108.46
3089+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-112.46
30863090
rule ref{C : context, reftype_1 : reftype, reftype_2 : reftype}:
30873091
`%|-%<:%`(C, (reftype_1 : reftype <: valtype), (reftype_2 : reftype <: valtype))
30883092
-- Reftype_sub: `%|-%<:%`(C, reftype_1, reftype_2)
30893093

3090-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:110.1-111.22
3094+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:114.1-115.22
30913095
rule bot{C : context, valtype : valtype}:
30923096
`%|-%<:%`(C, BOT_valtype, valtype)
30933097

3094-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:116.1-116.115
3098+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:120.1-120.115
30953099
relation Resulttype_sub: `%|-%<:%`(context, resulttype, resulttype)
3096-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:119.1-121.37
3100+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:123.1-125.37
30973101
rule _{C : context, `t_1*` : valtype*, `t_2*` : valtype*}:
30983102
`%|-%<:%`(C, `%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))
30993103
-- (Valtype_sub: `%|-%<:%`(C, t_1, t_2))*{t_1 <- `t_1*`, t_2 <- `t_2*`}
31003104

3101-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:134.1-134.119
3105+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:138.1-138.119
31023106
relation Storagetype_sub: `%|-%<:%`(context, storagetype, storagetype)
3103-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:146.1-148.46
3107+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.46
31043108
rule val{C : context, valtype_1 : valtype, valtype_2 : valtype}:
31053109
`%|-%<:%`(C, (valtype_1 : valtype <: storagetype), (valtype_2 : valtype <: storagetype))
31063110
-- Valtype_sub: `%|-%<:%`(C, valtype_1, valtype_2)
31073111

3108-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:150.1-152.49
3112+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:154.1-156.49
31093113
rule pack{C : context, packtype_1 : packtype, packtype_2 : packtype}:
31103114
`%|-%<:%`(C, (packtype_1 : packtype <: storagetype), (packtype_2 : packtype <: storagetype))
31113115
-- Packtype_sub: `%|-%<:%`(C, packtype_1, packtype_2)
31123116

3113-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:135.1-135.117
3117+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:139.1-139.117
31143118
relation Fieldtype_sub: `%|-%<:%`(context, fieldtype, fieldtype)
3115-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:155.1-157.40
3119+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-161.40
31163120
rule const{C : context, zt_1 : storagetype, zt_2 : storagetype}:
31173121
`%|-%<:%`(C, `%%`_fieldtype(?(), zt_1), `%%`_fieldtype(?(), zt_2))
31183122
-- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2)
31193123

3120-
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:159.1-162.40
3124+
;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:163.1-166.40
31213125
rule var{C : context, zt_1 : storagetype, zt_2 : storagetype}:
31223126
`%|-%<:%`(C, `%%`_fieldtype(?(MUT_mut), zt_1), `%%`_fieldtype(?(MUT_mut), zt_2))
31233127
-- Storagetype_sub: `%|-%<:%`(C, zt_1, zt_2)

‎spectec/test-latex/TEST.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5341,6 +5341,8 @@ $$
53415341
\begin{array}{@{}c@{}}\displaystyle
53425342
\frac{
53435343
C \vdash {\mathit{heaptype}} \leq \mathsf{any}
5344+
\qquad
5345+
{\mathit{heaptype}} \neq \mathsf{bot}
53445346
}{
53455347
C \vdash \mathsf{none} \leq {\mathit{heaptype}}
53465348
} \, {[\textsc{\scriptsize S{-}heap{-}none}]}
@@ -5352,6 +5354,8 @@ $$
53525354
\begin{array}{@{}c@{}}\displaystyle
53535355
\frac{
53545356
C \vdash {\mathit{heaptype}} \leq \mathsf{func}
5357+
\qquad
5358+
{\mathit{heaptype}} \neq \mathsf{bot}
53555359
}{
53565360
C \vdash \mathsf{nofunc} \leq {\mathit{heaptype}}
53575361
} \, {[\textsc{\scriptsize S{-}heap{-}nofunc}]}
@@ -5363,6 +5367,8 @@ $$
53635367
\begin{array}{@{}c@{}}\displaystyle
53645368
\frac{
53655369
C \vdash {\mathit{heaptype}} \leq \mathsf{exn}
5370+
\qquad
5371+
{\mathit{heaptype}} \neq \mathsf{bot}
53665372
}{
53675373
C \vdash \mathsf{noexn} \leq {\mathit{heaptype}}
53685374
} \, {[\textsc{\scriptsize S{-}heap{-}noexn}]}
@@ -5374,6 +5380,8 @@ $$
53745380
\begin{array}{@{}c@{}}\displaystyle
53755381
\frac{
53765382
C \vdash {\mathit{heaptype}} \leq \mathsf{extern}
5383+
\qquad
5384+
{\mathit{heaptype}} \neq \mathsf{bot}
53775385
}{
53785386
C \vdash \mathsf{noextern} \leq {\mathit{heaptype}}
53795387
} \, {[\textsc{\scriptsize S{-}heap{-}noextern}]}

0 commit comments

Comments
 (0)