From 7abade274c94fd0ca15cfa173751e25d2c226b89 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 9 Sep 2026 11:04:03 +0200 Subject: [PATCH] [spectec] Backport missing instantiation checks to Wasm 1.0/2.0 specs --- specification/wasm-1.0/0-aux.spectec | 4 +++ specification/wasm-1.0/6-typing.spectec | 8 +++--- specification/wasm-1.0/9-module.spectec | 31 +++++++++++++++++++++ specification/wasm-2.0/0-aux.spectec | 4 +++ specification/wasm-2.0/6-typing.spectec | 8 +++--- specification/wasm-2.0/9-module.spectec | 31 +++++++++++++++++++++ spectec/src/backend-interpreter/relation.ml | 2 ++ 7 files changed, 80 insertions(+), 8 deletions(-) diff --git a/specification/wasm-1.0/0-aux.spectec b/specification/wasm-1.0/0-aux.spectec index d924605e41..2c703f0870 100644 --- a/specification/wasm-1.0/0-aux.spectec +++ b/specification/wasm-1.0/0-aux.spectec @@ -40,3 +40,7 @@ def $list_(syntax X, w) = w def $concat_(syntax X, (X*)*) : X* hint(show $concat(%2)) def $concat_(syntax X, eps) = eps def $concat_(syntax X, (w*) (w'*)*) = w* $concat_(X, (w'*)*) + +def $disjoint_(syntax X, X*) : bool hint(show %2 $disjoint) hint(macro none) +def $disjoint_(syntax X, eps) = true +def $disjoint_(syntax X, w w'*) = ~(w <- w'*) /\ $disjoint_(X, w'*) diff --git a/specification/wasm-1.0/6-typing.spectec b/specification/wasm-1.0/6-typing.spectec index 93af498052..92d91c4777 100644 --- a/specification/wasm-1.0/6-typing.spectec +++ b/specification/wasm-1.0/6-typing.spectec @@ -404,7 +404,7 @@ rule Start_ok: ;; Module im/exports relation Import_ok: context |- import : externtype hint(show "T-import") -relation Export_ok: context |- export : externtype hint(show "T-export") +relation Export_ok: context |- export : name externtype hint(show "T-export") relation Externidx_ok: context |- externidx : externtype hint(show "T-externidx") rule Import_ok: @@ -412,7 +412,7 @@ rule Import_ok: -- Externtype_ok: |- xt : OK rule Export_ok: - C |- EXPORT name externidx : xt + C |- EXPORT name externidx : name xt -- Externidx_ok: C |- externidx : xt @@ -450,11 +450,11 @@ rule Module_ok: -- (Elem_ok: C |- elem : OK)* -- (Data_ok: C |- data : OK)* -- (Start_ok: C |- start : OK)? - -- (Export_ok: C |- export : xt)* + -- (Export_ok: C |- export : nm xt)* ---- -- if |tt*| <= 1 -- if |mt*| <= 1 - ;; -- TODO: disjoint export names + -- if $disjoint_(name, nm*) ---- -- if C = {TYPES ft'*, FUNCS ift* ft*, GLOBALS igt* gt*, TABLES itt* tt*, MEMS imt* mt*} ---- diff --git a/specification/wasm-1.0/9-module.spectec b/specification/wasm-1.0/9-module.spectec index d6edf3fd51..52191e6a30 100644 --- a/specification/wasm-1.0/9-module.spectec +++ b/specification/wasm-1.0/9-module.spectec @@ -1,3 +1,32 @@ +;; +;; External addresses +;; + +relation Externaddr_ok: store |- externaddr : externtype hint(macro "%externaddr") + +rule Externaddr_ok/global: + s |- GLOBAL a : GLOBAL globalinst.TYPE + -- if s.GLOBALS[a] = globalinst + +rule Externaddr_ok/mem: + s |- MEM a : MEM meminst.TYPE + -- if s.MEMS[a] = meminst + +rule Externaddr_ok/table: + s |- TABLE a : TABLE tableinst.TYPE + -- if s.TABLES[a] = tableinst + +rule Externaddr_ok/func: + s |- FUNC a : FUNC funcinst.TYPE + -- if s.FUNCS[a] = funcinst + +rule Externaddr_ok/sub: + s |- externaddr : xt + -- Externaddr_ok: s |- externaddr : xt' + -- Externtype_ok: |- xt : OK + -- Externtype_sub: |- xt' <: xt + + ;; ;; Projections ;; @@ -139,6 +168,8 @@ def $initdata(s, moduleinst, i i'*, (b*) (b'*)*) = s_2 def $instantiate(store, module, externaddr*) : config def $instantiate(s, module, externaddr*) = s_3; f; (CALL x')? + -- Module_ok: |- module : xt_I* -> xt_E* + -- (Externaddr_ok: s |- externaddr : xt_I)* -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export* -- if type* = (TYPE functype)* -- if global* = (GLOBAL globaltype expr_G)* diff --git a/specification/wasm-2.0/0-aux.spectec b/specification/wasm-2.0/0-aux.spectec index 68e9301757..6a8033d388 100644 --- a/specification/wasm-2.0/0-aux.spectec +++ b/specification/wasm-2.0/0-aux.spectec @@ -43,6 +43,10 @@ def $concat_(syntax X, (w*) (w'*)*) = w* $concat_(X, (w'*)*) def $inv_concat_(syntax X, X*) : (X*)* def $inv_concat_ hint(builtin) +def $disjoint_(syntax X, X*) : bool hint(show %2 $disjoint) hint(macro none) +def $disjoint_(syntax X, eps) = true +def $disjoint_(syntax X, w w'*) = ~(w <- w'*) /\ $disjoint_(X, w'*) + ;; [{1, 2}, {a, b, c}] -> {[1, a], [1, b], [1, c], [2, a], [2, b], [2, c]} def $setproduct_(syntax X, (X*)*) : (X*)* hint(show %latex("{\\Large\\times}") %2) diff --git a/specification/wasm-2.0/6-typing.spectec b/specification/wasm-2.0/6-typing.spectec index 20782f74a7..4c77d1cc63 100644 --- a/specification/wasm-2.0/6-typing.spectec +++ b/specification/wasm-2.0/6-typing.spectec @@ -645,7 +645,7 @@ rule Start_ok: ;; Module im/exports relation Import_ok: context |- import : externtype hint(show "T-import") -relation Export_ok: context |- export : externtype hint(show "T-export") +relation Export_ok: context |- export : name externtype hint(show "T-export") relation Externidx_ok: context |- externidx : externtype hint(show "T-externidx") rule Import_ok: @@ -653,7 +653,7 @@ rule Import_ok: -- Externtype_ok: |- xt : OK rule Export_ok: - C |- EXPORT name externidx : xt + C |- EXPORT name externidx : name xt -- Externidx_ok: C |- externidx : xt @@ -693,10 +693,10 @@ rule Module_ok: ---- -- (Func_ok: C |- func : ft)* -- (Start_ok: C |- start : OK)? - -- (Export_ok: C |- export : xt)* + -- (Export_ok: C |- export : nm xt)* ---- -- if |mt*| <= 1 - ;; -- TODO: disjoint export names + -- if $disjoint_(name, nm*) ---- -- if C = {TYPES ft'*, FUNCS ift* ft*, GLOBALS igt* gt*, TABLES itt* tt*, MEMS imt* mt*, ELEMS rt*, DATAS OK^n} ---- diff --git a/specification/wasm-2.0/9-module.spectec b/specification/wasm-2.0/9-module.spectec index e456fc0a17..f05cf7e177 100644 --- a/specification/wasm-2.0/9-module.spectec +++ b/specification/wasm-2.0/9-module.spectec @@ -1,3 +1,32 @@ +;; +;; External addresses +;; + +relation Externaddr_ok: store |- externaddr : externtype hint(macro "%externaddr") + +rule Externaddr_ok/global: + s |- GLOBAL a : GLOBAL globalinst.TYPE + -- if s.GLOBALS[a] = globalinst + +rule Externaddr_ok/mem: + s |- MEM a : MEM meminst.TYPE + -- if s.MEMS[a] = meminst + +rule Externaddr_ok/table: + s |- TABLE a : TABLE tableinst.TYPE + -- if s.TABLES[a] = tableinst + +rule Externaddr_ok/func: + s |- FUNC a : FUNC funcinst.TYPE + -- if s.FUNCS[a] = funcinst + +rule Externaddr_ok/sub: + s |- externaddr : xt + -- Externaddr_ok: s |- externaddr : xt' + -- Externtype_ok: |- xt : OK + -- Externtype_sub: |- xt' <: xt + + ;; ;; Projections ;; @@ -166,6 +195,8 @@ def $rundata(DATA byte* (ACTIVE 0 instr*), i) = def $instantiate(store, module, externaddr*) : config def $instantiate(s, module, externaddr*) = s'; f; instr_E* instr_D* (CALL x)? + -- Module_ok: |- module : xt_I* -> xt_E* + -- (Externaddr_ok: s |- externaddr : xt_I)* -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export* -- if type* = (TYPE functype)* -- if global* = (GLOBAL globaltype expr_G)* diff --git a/spectec/src/backend-interpreter/relation.ml b/spectec/src/backend-interpreter/relation.ml index fe8a5cd32c..b1151ac5cb 100644 --- a/spectec/src/backend-interpreter/relation.ml +++ b/spectec/src/backend-interpreter/relation.ml @@ -44,7 +44,9 @@ let ref_ok = | vs -> Numerics.error_values "$Ref_ok" vs let module_ok v = +(* Use Wasm-3 validator for Wasm-1+2 as well. Does not work for negative tests! if !Construct.version <> 3 then failwith "This hardcoded function ($Module_ok) should be only called with test version 3.0"; +*) match v with | [ m ] -> (try