[spectec] Backport missing instantiation checks to Wasm 1.0/2.0 specs
diff --git a/specification/wasm-1.0/0-aux.spectec b/specification/wasm-1.0/0-aux.spectec index d924605..2c703f0 100644 --- a/specification/wasm-1.0/0-aux.spectec +++ b/specification/wasm-1.0/0-aux.spectec
@@ -40,3 +40,7 @@ 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 93af498..92d91c4 100644 --- a/specification/wasm-1.0/6-typing.spectec +++ b/specification/wasm-1.0/6-typing.spectec
@@ -404,7 +404,7 @@ ;; 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 @@ -- 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 @@ -- (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 d6edf3f..52191e6 100644 --- a/specification/wasm-1.0/9-module.spectec +++ b/specification/wasm-1.0/9-module.spectec
@@ -1,4 +1,33 @@ ;; +;; 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 $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 68e9301..6a8033d 100644 --- a/specification/wasm-2.0/0-aux.spectec +++ b/specification/wasm-2.0/0-aux.spectec
@@ -43,6 +43,10 @@ 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 20782f7..4c77d1c 100644 --- a/specification/wasm-2.0/6-typing.spectec +++ b/specification/wasm-2.0/6-typing.spectec
@@ -645,7 +645,7 @@ ;; 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 @@ -- 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 @@ ---- -- (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 e456fc0..f05cf7e 100644 --- a/specification/wasm-2.0/9-module.spectec +++ b/specification/wasm-2.0/9-module.spectec
@@ -1,4 +1,33 @@ ;; +;; 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 $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 fe8a5cd..b1151ac 100644 --- a/spectec/src/backend-interpreter/relation.ml +++ b/spectec/src/backend-interpreter/relation.ml
@@ -44,7 +44,9 @@ | 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