Merge pull request #126 from Wasm-DSL/fix-conditions

Fix closing of types; fix rendering of nul

.github/workflows/ci-spec.yml

@@ -43,7 +43,7 @@ jobs:
       #- name: Run Bikeshed
       #  run: cd document/core && opam exec make bikeshed
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: core-rendered
           path: document/core/_build/html
@@ -58,7 +58,7 @@ jobs:
       - name: Run Bikeshed
         run: bikeshed spec "document/js-api/index.bs" "document/js-api/index.html"
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: js-api-rendered
           path: document/js-api/index.html
@@ -73,7 +73,7 @@ jobs:
       - name: Run Bikeshed
         run: bikeshed spec "document/web-api/index.bs" "document/web-api/index.html"
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: web-api-rendered
           path: document/web-api/index.html
@@ -93,7 +93,7 @@ jobs:
       - name: Build main spec
         run: cd document/metadata/code && make main
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: code-metadata-rendered
           path: document/metadata/code/_build/html
@@ -112,7 +112,7 @@ jobs:
       - name: Build main spec
         run: cd document/legacy/exceptions/core && make main
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: legacy-exceptions-core-rendered
           path: document/legacy/exceptions/core/_build/html
@@ -127,7 +127,7 @@ jobs:
       - name: Run Bikeshed
         run: bikeshed spec "document/legacy/exceptions/js-api/index.bs" "document/legacy/exceptions/js-api/index.html"
       - name: Upload artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: legacy-exceptions-js-api-rendered
           path: document/legacy/exceptions/js-api/index.html
@@ -141,32 +141,32 @@ jobs:
       - name: Create output directory
         run: mkdir _output && cp document/index.html _output/index.html
       - name: Download core spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: core-rendered
           path: _output/core
       - name: Download JS API spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: js-api-rendered
           path: _output/js-api
       - name: Download Web API spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: web-api-rendered
           path: _output/web-api
       - name: Download code metadata spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: code-metadata-rendered
           path: _output/metadata/code
       - name: Download legacy exceptions core spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: legacy-exceptions-core-rendered
           path: _output/legacy/exceptions/core
       - name: Download legacy exceptions JS API spec artifact
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: legacy-exceptions-js-api-rendered
           path: _output/legacy/exceptions/js-api

spectec/spec/wasm-3.0/2-syntax-aux.watsup

@@ -611,11 +611,17 @@ def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, t
 def $subst_all_valtype(valtype, heaptype*) : valtype  hint(show %#`[:=%]) hint(macro "%subst")
 def $subst_all_reftype(reftype, heaptype*) : reftype  hint(show %#`[:=%]) hint(macro "%subst")
 def $subst_all_deftype(deftype, heaptype*) : deftype  hint(show %#`[:=%]) hint(macro "%subst")
+def $subst_all_globaltype(globaltype, heaptype*) : globaltype  hint(show %#`[:=%]) hint(macro "%subst")
+def $subst_all_tabletype(tabletype, heaptype*) : tabletype  hint(show %#`[:=%]) hint(macro "%subst")
+def $subst_all_memtype(memtype, heaptype*) : memtype  hint(show %#`[:=%]) hint(macro "%subst")
 def $subst_all_moduletype(moduletype, heaptype*) : moduletype  hint(show %#`[:=%]) hint(macro "%subst")
 
 def $subst_all_valtype(t, tu^n) = $subst_valtype(t, (_IDX i)^(i<n), tu^n)
 def $subst_all_reftype(rt, tu^n) = $subst_reftype(rt, (_IDX i)^(i<n), tu^n)
 def $subst_all_deftype(dt, tu^n) = $subst_deftype(dt, (_IDX i)^(i<n), tu^n)
+def $subst_all_globaltype(gt, tu^n) = $subst_globaltype(gt, (_IDX i)^(i<n), tu^n)
+def $subst_all_tabletype(tt, tu^n) = $subst_tabletype(tt, (_IDX i)^(i<n), tu^n)
+def $subst_all_memtype(mt, tu^n) = $subst_memtype(mt, (_IDX i)^(i<n), tu^n)
 def $subst_all_moduletype(mmt, tu^n) = $subst_moduletype(mmt, (_IDX i)^(i<n), tu^n)
 
 def $subst_all_deftypes(deftype*, heaptype*) : deftype*  hint(show %#`[:=%]) hint(macro "%subst")

spectec/spec/wasm-3.0/5-runtime-aux.watsup

@@ -6,12 +6,21 @@
 
 def $inst_valtype(moduleinst, valtype) : valtype  hint(show $inst_(%,%)) hint(macro "insttype")
 def $inst_reftype(moduleinst, reftype) : reftype  hint(show $inst_(%,%)) hint(macro "insttype")
+def $inst_globaltype(moduleinst, globaltype) : globaltype  hint(show $inst_(%,%)) hint(macro "insttype")
+def $inst_tabletype(moduleinst, tabletype) : tabletype  hint(show $inst_(%,%)) hint(macro "insttype")
+def $inst_memtype(moduleinst, memtype) : memtype  hint(show $inst_(%,%)) hint(macro "insttype")
 
 ;; TODO(3, rossberg): make inlining moduleinst.TYPES work
 def $inst_valtype(moduleinst, t) = $subst_all_valtype(t, dt*)
   -- if dt* = moduleinst.TYPES
 def $inst_reftype(moduleinst, rt) = $subst_all_reftype(rt, dt*)
   -- if dt* = moduleinst.TYPES
+def $inst_globaltype(moduleinst, gt) = $subst_all_globaltype(gt, dt*)
+  -- if dt* = moduleinst.TYPES
+def $inst_tabletype(moduleinst, tt) = $subst_all_tabletype(tt, dt*)
+  -- if dt* = moduleinst.TYPES
+def $inst_memtype(moduleinst, mt) = $subst_all_memtype(mt, dt*)
+  -- if dt* = moduleinst.TYPES
 
 
 ;;

spectec/spec/wasm-3.0/6-typing.watsup

@@ -914,10 +914,12 @@ rule Instr_ok/array.init_data:
 ;; External reference instructions
 
 rule Instr_ok/extern.convert_any:
-  C |- EXTERN.CONVERT_ANY : (REF nul ANY) -> (REF nul EXTERN)
+  C |- EXTERN.CONVERT_ANY : (REF nul1 ANY) -> (REF nul2 EXTERN)
+  -- if nul1 = nul2
 
 rule Instr_ok/any.convert_extern:
-  C |- ANY.CONVERT_EXTERN : (REF nul EXTERN) -> (REF nul ANY)
+  C |- ANY.CONVERT_EXTERN : (REF nul1 EXTERN) -> (REF nul2 ANY)
+  -- if nul1 = nul2
 
 
 ;; Vector instructions

spectec/spec/wasm-3.0/9-module.watsup

@@ -57,9 +57,9 @@ def $allocmems(s, memtype memtype'*) = (s_2, ma ma'*)
   -- if (s_2, ma'*) = $allocmems(s_1, memtype'*)
 
 def $alloctag(store, tagtype) : (store, tagaddr)
-def $alloctag(s, at) = (s ++ {TAGS taginst}, |s.TAGS|)
+def $alloctag(s, tagtype) = (s ++ {TAGS taginst}, |s.TAGS|)
   ---- ----
-  -- if taginst = { TYPE at }
+  -- if taginst = { TYPE tagtype }
 
 def $alloctags(store, tagtype*) : (store, tagaddr*) hint(show $alloctag*#((%,%)))
 def $alloctags(s, eps) = (s, eps)
@@ -128,12 +128,13 @@ def $allocmodule(s, module, externaddr*, val_G*, ref_T*, (ref_E*)*) = (s_7, modu
   -- if ea* = ($(|s.ELEMS|+i_E))^(i_E<|elem*|)
   -- if da* = ($(|s.DATAS|+i_D))^(i_D<|data*|)
   -- if dt* = $alloctypes(type*)
+  ;; TODO(2, rossberg): use $inst_type(_, moduleinst) instead of $subst_all_type(_, dt*) below
   -- if (s_1, fa*) = $allocfuncs(s, dt*[x]*, (FUNC x local* expr_F)*, moduleinst^(|func*|))
-  -- if (s_2, ga*) = $allocglobals(s_1, globaltype*, val_G*)
-  -- if (s_3, ta*) = $alloctables(s_2, tabletype*, ref_T*)
-  -- if (s_4, ma*) = $allocmems(s_3, memtype*)
+  -- if (s_2, ga*) = $allocglobals(s_1, $subst_all_globaltype(globaltype, dt*)*, val_G*)
+  -- if (s_3, ta*) = $alloctables(s_2, $subst_all_tabletype(tabletype, dt*)*, ref_T*)
+  -- if (s_4, ma*) = $allocmems(s_3, $subst_all_memtype(memtype, dt*)*)
   -- if (s_5, aa*) = $alloctags(s_4, dt*[y]*)
-  -- if (s_6, ea*) = $allocelems(s_5, elemtype*, (ref_E*)*)
+  -- if (s_6, ea*) = $allocelems(s_5, $subst_all_reftype(elemtype, dt*)*, (ref_E*)*)
   -- if (s_7, da*) = $allocdatas(s_6, OK^(|data*|), (byte*)*)
   ;; TODO(2, rossberg): use moduleinst here and remove hack above
   -- if xi* = $allocexports({FUNCS fa_I* fa*, GLOBALS ga_I* ga*, TABLES ta_I* ta*, MEMS ma_I* ma*, TAGS aa_I* aa*}, export*)