Skip to content

Commit 25134ea

Browse files
rossberglzy0505
rossberg
and
lzy0505
authored
[spectec] Backport missing instantiation checks to Wasm 1.0/2.0 specs (#2248)
Co-authored-by: Zongyuan Liu <liuzongyuan0505@gmail.com>
1 parent b0ec1f3 commit 25134ea

11 files changed

Lines changed: 792 additions & 82 deletions

File tree

‎specification/wasm-1.0/0-aux.spectec‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,3 +40,7 @@ def $list_(syntax X, w) = w
4040
def $concat_(syntax X, (X*)*) : X* hint(show $concat(%2))
4141
def $concat_(syntax X, eps) = eps
4242
def $concat_(syntax X, (w*) (w'*)*) = w* $concat_(X, (w'*)*)
43+
44+
def $disjoint_(syntax X, X*) : bool hint(show %2 $disjoint) hint(macro none)
45+
def $disjoint_(syntax X, eps) = true
46+
def $disjoint_(syntax X, w w'*) = ~(w <- w'*) /\ $disjoint_(X, w'*)

‎specification/wasm-1.0/1-syntax.spectec‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,8 @@ syntax memtype hint(desc "memory type") =
130130
limits
131131
syntax externtype hint(desc "external type") =
132132
| FUNC functype | GLOBAL globaltype | TABLE tabletype | MEM memtype
133+
syntax moduletype hint(desc "module type") =
134+
externtype* -> externtype*
133135

134136
var lim : limits
135137
var ft : functype

‎specification/wasm-1.0/6-typing.spectec‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -404,15 +404,15 @@ rule Start_ok:
404404
;; Module im/exports
405405

406406
relation Import_ok: context |- import : externtype hint(show "T-import")
407-
relation Export_ok: context |- export : externtype hint(show "T-export")
407+
relation Export_ok: context |- export : name externtype hint(show "T-export")
408408
relation Externidx_ok: context |- externidx : externtype hint(show "T-externidx")
409409

410410
rule Import_ok:
411411
C |- IMPORT name_1 name_2 xt : xt
412412
-- Externtype_ok: |- xt : OK
413413

414414
rule Export_ok:
415-
C |- EXPORT name externidx : xt
415+
C |- EXPORT name externidx : name xt
416416
-- Externidx_ok: C |- externidx : xt
417417

418418

@@ -435,7 +435,7 @@ rule Externidx_ok/mem:
435435

436436
;; Modules proper
437437

438-
relation Module_ok: |- module : externtype* -> externtype* hint(show "T-module")
438+
relation Module_ok: |- module : moduletype hint(show "T-module")
439439

440440
rule Module_ok:
441441
|- MODULE type* import* func* global* table* mem* elem* data* start? export* : ixt* -> xt*
@@ -450,11 +450,11 @@ rule Module_ok:
450450
-- (Elem_ok: C |- elem : OK)*
451451
-- (Data_ok: C |- data : OK)*
452452
-- (Start_ok: C |- start : OK)?
453-
-- (Export_ok: C |- export : xt)*
453+
-- (Export_ok: C |- export : nm xt)*
454454
----
455455
-- if |tt*| <= 1
456456
-- if |mt*| <= 1
457-
;; -- TODO: disjoint export names
457+
-- if $disjoint_(name, nm*)
458458
----
459459
-- if C = {TYPES ft'*, FUNCS ift* ft*, GLOBALS igt* gt*, TABLES itt* tt*, MEMS imt* mt*}
460460
----

‎specification/wasm-1.0/9-module.spectec‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,32 @@
1+
;;
2+
;; External addresses
3+
;;
4+
5+
relation Externaddr_ok: store |- externaddr : externtype hint(macro "%externaddr")
6+
7+
rule Externaddr_ok/global:
8+
s |- GLOBAL a : GLOBAL globalinst.TYPE
9+
-- if s.GLOBALS[a] = globalinst
10+
11+
rule Externaddr_ok/mem:
12+
s |- MEM a : MEM meminst.TYPE
13+
-- if s.MEMS[a] = meminst
14+
15+
rule Externaddr_ok/table:
16+
s |- TABLE a : TABLE tableinst.TYPE
17+
-- if s.TABLES[a] = tableinst
18+
19+
rule Externaddr_ok/func:
20+
s |- FUNC a : FUNC funcinst.TYPE
21+
-- if s.FUNCS[a] = funcinst
22+
23+
rule Externaddr_ok/sub:
24+
s |- externaddr : xt
25+
-- Externaddr_ok: s |- externaddr : xt'
26+
-- Externtype_ok: |- xt : OK
27+
-- Externtype_sub: |- xt' <: xt
28+
29+
130
;;
231
;; Projections
332
;;
@@ -139,6 +168,8 @@ def $initdata(s, moduleinst, i i'*, (b*) (b'*)*) = s_2
139168

140169
def $instantiate(store, module, externaddr*) : config
141170
def $instantiate(s, module, externaddr*) = s_3; f; (CALL x')?
171+
-- Module_ok: |- module : xt_I* -> xt_E*
172+
-- (Externaddr_ok: s |- externaddr : xt_I)*
142173
-- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
143174
-- if type* = (TYPE functype)*
144175
-- if global* = (GLOBAL globaltype expr_G)*

‎specification/wasm-2.0/0-aux.spectec‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,10 @@ def $concat_(syntax X, (w*) (w'*)*) = w* $concat_(X, (w'*)*)
4343
def $inv_concat_(syntax X, X*) : (X*)*
4444
def $inv_concat_ hint(builtin)
4545

46+
def $disjoint_(syntax X, X*) : bool hint(show %2 $disjoint) hint(macro none)
47+
def $disjoint_(syntax X, eps) = true
48+
def $disjoint_(syntax X, w w'*) = ~(w <- w'*) /\ $disjoint_(X, w'*)
49+
4650

4751
;; [{1, 2}, {a, b, c}] -> {[1, a], [1, b], [1, c], [2, a], [2, b], [2, c]}
4852
def $setproduct_(syntax X, (X*)*) : (X*)* hint(show %latex("{\\Large\\times}") %2)

‎specification/wasm-2.0/1-syntax.spectec‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,8 @@ syntax datatype hint(desc "data type") =
178178
OK
179179
syntax externtype hint(desc "external type") =
180180
| FUNC functype | GLOBAL globaltype | TABLE tabletype | MEM memtype
181+
syntax moduletype hint(desc "module type") =
182+
externtype* -> externtype*
181183

182184

183185
;; Meta variables

‎specification/wasm-2.0/6-typing.spectec‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -645,15 +645,15 @@ rule Start_ok:
645645
;; Module im/exports
646646

647647
relation Import_ok: context |- import : externtype hint(show "T-import")
648-
relation Export_ok: context |- export : externtype hint(show "T-export")
648+
relation Export_ok: context |- export : name externtype hint(show "T-export")
649649
relation Externidx_ok: context |- externidx : externtype hint(show "T-externidx")
650650

651651
rule Import_ok:
652652
C |- IMPORT name_1 name_2 xt : xt
653653
-- Externtype_ok: |- xt : OK
654654

655655
rule Export_ok:
656-
C |- EXPORT name externidx : xt
656+
C |- EXPORT name externidx : name xt
657657
-- Externidx_ok: C |- externidx : xt
658658

659659

@@ -676,7 +676,7 @@ rule Externidx_ok/mem:
676676

677677
;; Modules proper
678678

679-
relation Module_ok: |- module : externtype* -> externtype* hint(show "T-module")
679+
relation Module_ok: |- module : moduletype hint(show "T-module")
680680

681681
;; TODO: refs
682682
rule Module_ok:
@@ -693,10 +693,10 @@ rule Module_ok:
693693
----
694694
-- (Func_ok: C |- func : ft)*
695695
-- (Start_ok: C |- start : OK)?
696-
-- (Export_ok: C |- export : xt)*
696+
-- (Export_ok: C |- export : nm xt)*
697697
----
698698
-- if |mt*| <= 1
699-
;; -- TODO: disjoint export names
699+
-- if $disjoint_(name, nm*)
700700
----
701701
-- if C = {TYPES ft'*, FUNCS ift* ft*, GLOBALS igt* gt*, TABLES itt* tt*, MEMS imt* mt*, ELEMS rt*, DATAS OK^n}
702702
----

‎specification/wasm-2.0/9-module.spectec‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,32 @@
1+
;;
2+
;; External addresses
3+
;;
4+
5+
relation Externaddr_ok: store |- externaddr : externtype hint(macro "%externaddr")
6+
7+
rule Externaddr_ok/global:
8+
s |- GLOBAL a : GLOBAL globalinst.TYPE
9+
-- if s.GLOBALS[a] = globalinst
10+
11+
rule Externaddr_ok/mem:
12+
s |- MEM a : MEM meminst.TYPE
13+
-- if s.MEMS[a] = meminst
14+
15+
rule Externaddr_ok/table:
16+
s |- TABLE a : TABLE tableinst.TYPE
17+
-- if s.TABLES[a] = tableinst
18+
19+
rule Externaddr_ok/func:
20+
s |- FUNC a : FUNC funcinst.TYPE
21+
-- if s.FUNCS[a] = funcinst
22+
23+
rule Externaddr_ok/sub:
24+
s |- externaddr : xt
25+
-- Externaddr_ok: s |- externaddr : xt'
26+
-- Externtype_ok: |- xt : OK
27+
-- Externtype_sub: |- xt' <: xt
28+
29+
130
;;
231
;; Projections
332
;;
@@ -166,6 +195,8 @@ def $rundata(DATA byte* (ACTIVE 0 instr*), i) =
166195

167196
def $instantiate(store, module, externaddr*) : config
168197
def $instantiate(s, module, externaddr*) = s'; f; instr_E* instr_D* (CALL x)?
198+
-- Module_ok: |- module : xt_I* -> xt_E*
199+
-- (Externaddr_ok: s |- externaddr : xt_I)*
169200
-- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
170201
-- if type* = (TYPE functype)*
171202
-- if global* = (GLOBAL globaltype expr_G)*

‎spectec/src/backend-interpreter/construct.ml‎

Lines changed: 31 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -173,6 +173,8 @@ and al_to_heaptype: value -> heaptype = function
173173
| v -> error_value "heaptype" v
174174

175175
and al_to_reftype: value -> reftype = function
176+
| CaseV ("FUNCREF", []) -> Null, FuncHT
177+
| CaseV ("EXTERNREF", []) -> Null, ExternHT
176178
| CaseV ("REF", [ n; ht ]) -> al_to_null n, al_to_heaptype ht
177179
| v -> error_value "reftype" v
178180

@@ -197,11 +199,12 @@ and al_to_valtype: value -> valtype = function
197199
| CaseV ("I32", _) | CaseV ("I64", _)
198200
| CaseV ("F32", _) | CaseV ("F64", _) as v -> NumT (al_to_numtype v)
199201
| CaseV ("V128", []) -> VecT V128T
200-
| CaseV ("REF", _) as v -> RefT (al_to_reftype v)
202+
| CaseV (("REF" | "FUNCREF" | "EXTERNREF"), _) as v -> RefT (al_to_reftype v)
201203
| CaseV ("BOT", []) -> BotT
202204
| v -> error_value "valtype" v
203205

204206
let al_to_blocktype: value -> blocktype = function
207+
| OptV _ as v when !version = 1 -> ValBlockType (al_to_opt al_to_valtype v)
205208
| CaseV ("_IDX", [ idx ]) -> VarBlockType (al_to_idx idx)
206209
| CaseV ("_RESULT", [ vt_opt ]) -> ValBlockType (al_to_opt al_to_valtype vt_opt)
207210
| v -> error_value "blocktype" v
@@ -216,10 +219,14 @@ let al_to_globaltype: value -> globaltype = function
216219
| v -> error_value "globaltype" v
217220

218221
let al_to_tabletype: value -> tabletype = function
222+
| CaseV ("[", _) as v when !version = 1 -> TableT (I32AT, al_to_limits v, (Null, FuncHT))
223+
| TupV [ limits; rt ] | CaseV ("", [ limits; rt ]) -> TableT (I32AT, al_to_limits limits, al_to_reftype rt)
219224
| TupV [ at; limits; rt ] | CaseV (_, [ at; limits; rt ]) -> TableT (al_to_addrtype at, al_to_limits limits, al_to_reftype rt)
220225
| v -> error_value "tabletype" v
221226

222227
let al_to_memorytype: value -> memorytype = function
228+
| CaseV ("[", _) as v when !version = 1 -> MemoryT (I32AT, al_to_limits v)
229+
| CaseV ("PAGE", [ limits ]) -> MemoryT (I32AT, al_to_limits limits)
223230
| CaseV ("PAGE", [ at; limits ]) -> MemoryT (al_to_addrtype at, al_to_limits limits)
224231
| v -> error_value "memorytype" v
225232

@@ -792,6 +799,8 @@ and al_to_instr': value -> Ast.instr' = function
792799
| CaseV ("RETURN", []) -> Return
793800
| CaseV ("CALL", [ idx ]) -> Call (al_to_idx idx)
794801
| CaseV ("CALL_REF", [ typeuse ]) -> CallRef (al_to_idx_of_typeuse typeuse)
802+
| CaseV ("CALL_INDIRECT", [ idx ]) when !version = 1 ->
803+
CallIndirect (0l @@ no_region, al_to_idx idx)
795804
| CaseV ("CALL_INDIRECT", [ idx1; typeuse2 ]) ->
796805
CallIndirect (al_to_idx idx1, al_to_idx_of_typeuse typeuse2)
797806
| CaseV ("RETURN_CALL", [ idx ]) -> ReturnCall (al_to_idx idx)
@@ -810,8 +819,13 @@ and al_to_instr': value -> Ast.instr' = function
810819
| CaseV ("VSTORE", vstoreop) -> let idx, op = al_to_vstoreop vstoreop in VecStore (idx, op)
811820
| CaseV ("VSTORE_LANE", vlaneop) ->
812821
let idx, op, i = al_to_vlaneop vlaneop in VecStoreLane (idx, op, i)
822+
| CaseV ("MEMORY.SIZE", []) when !version <= 2 -> MemorySize (0l @@ no_region)
823+
| CaseV ("MEMORY.GROW", []) when !version <= 2 -> MemoryGrow (0l @@ no_region)
813824
| CaseV ("MEMORY.SIZE", [ idx ]) -> MemorySize (al_to_idx idx)
814825
| CaseV ("MEMORY.GROW", [ idx ]) -> MemoryGrow (al_to_idx idx)
826+
| CaseV ("MEMORY.FILL", []) when !version <= 2 -> MemoryFill (0l @@ no_region)
827+
| CaseV ("MEMORY.COPY", []) when !version <= 2 -> MemoryCopy (0l @@ no_region, 0l @@ no_region)
828+
| CaseV ("MEMORY.INIT", [ idx ]) when !version <= 2 -> MemoryInit (0l @@ no_region, al_to_idx idx)
815829
| CaseV ("MEMORY.FILL", [ idx ]) -> MemoryFill (al_to_idx idx)
816830
| CaseV ("MEMORY.COPY", [ idx1; idx2 ]) -> MemoryCopy (al_to_idx idx1, al_to_idx idx2)
817831
| CaseV ("MEMORY.INIT", [ idx1; idx2 ]) -> MemoryInit (al_to_idx idx1, al_to_idx idx2)
@@ -855,6 +869,8 @@ let al_to_const: value -> const = al_to_list al_to_instr |> al_to_phrase
855869
(* Deconstruct module *)
856870

857871
let al_to_type: value -> type_ = function
872+
| CaseV ("TYPE", [ ft ]) when !version <= 2 ->
873+
RecT [SubT (Final, [], al_to_comptype ft)] @@ no_region
858874
| CaseV ("TYPE", [ rt ]) -> al_to_phrase al_to_rectype rt
859875
| v -> error_value "type" v
860876

@@ -876,6 +892,10 @@ let al_to_global': value -> global' = function
876892
let al_to_global: value -> global = al_to_phrase al_to_global'
877893

878894
let al_to_table': value -> table' = function
895+
| CaseV ("TABLE", [ tt ]) when !version <= 2 ->
896+
let TableT (_, _, rt) as tt' = al_to_tabletype tt in
897+
let _, ht = rt in
898+
Table (tt', [RefNull ht @@ no_region] @@ no_region)
879899
| CaseV ("TABLE", [ tt; const ]) ->
880900
Table (al_to_tabletype tt, al_to_const const)
881901
| v -> error_value "table" v
@@ -899,18 +919,26 @@ let al_to_segmentmode': value -> segmentmode' = function
899919
let al_to_segmentmode: value -> segmentmode = al_to_phrase al_to_segmentmode'
900920

901921
let al_to_elem': value -> elem' = function
922+
| CaseV ("ELEM", [ offset; indices ]) when !version = 1 ->
923+
let const x = [RefFunc (al_to_idx x) @@ no_region] @@ no_region in
924+
Elem ((Null, FuncHT), al_to_list const indices,
925+
Active (0l @@ no_region, al_to_const offset) @@ no_region)
902926
| CaseV ("ELEM", [ rt; consts; mode ]) ->
903927
Elem (al_to_reftype rt, al_to_list al_to_const consts, al_to_segmentmode mode)
904928
| v -> error_value "elem" v
905929
let al_to_elem: value -> elem = al_to_phrase al_to_elem'
906930

907931
let al_to_data': value -> data' = function
932+
| CaseV ("DATA", [ offset; bytes ]) when !version = 1 ->
933+
Data (al_to_bytes bytes, Active (0l @@ no_region, al_to_const offset) @@ no_region)
908934
| CaseV ("DATA", [ bytes; mode ]) ->
909935
Data (al_to_bytes bytes, al_to_segmentmode mode)
910936
| v -> error_value "data" v
911937
let al_to_data: value -> data = al_to_phrase al_to_data'
912938

913939
let al_to_externtype = function
940+
| CaseV ("FUNC", [CaseV ("->", _) as ft]) when !version <= 2 ->
941+
ExternFuncT (Def (DefT (RecT [SubT (Final, [], al_to_comptype ft)], 0l)))
914942
| CaseV ("FUNC", [typeuse]) -> ExternFuncT (al_to_typeuse typeuse)
915943
| CaseV ("GLOBAL", [globaltype]) -> ExternGlobalT (al_to_globaltype globaltype)
916944
| CaseV ("TABLE", [tabletype]) -> ExternTableT (al_to_tabletype tabletype)
@@ -1973,6 +2001,8 @@ let al_of_data data =
19732001

19742002

19752003
let al_of_externtype = function
2004+
| ExternFuncT (Def dt) when !version <= 2 ->
2005+
CaseV ("FUNC", [al_of_comptype (Types.expand_deftype dt)])
19762006
| ExternFuncT (typeuse) -> CaseV ("FUNC", [al_of_typeuse typeuse])
19772007
| ExternGlobalT (globaltype) -> CaseV ("GLOBAL", [al_of_globaltype globaltype])
19782008
| ExternTableT (tabletype) -> CaseV ("TABLE", [al_of_tabletype tabletype])

‎spectec/src/backend-interpreter/relation.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ let ref_ok =
4444
| vs -> Numerics.error_values "$Ref_ok" vs
4545

4646
let module_ok v =
47-
if !Construct.version <> 3 then failwith "This hardcoded function ($Module_ok) should be only called with test version 3.0";
47+
(* Use Wasm-3 validator for Wasm-1+2 as well. Does not work for negative tests! *)
4848
match v with
4949
| [ m ] ->
5050
(try

0 commit comments

Comments
 (0)