DSL for module semantics (#32)

Co-authored-by: Wonho Shin <[email protected]> Co-authored-by: Andreas Rossberg <[email protected]> Co-authored-by: DJ <[email protected]>
Wasm-DSL · Jul 26, 2023 · 056aebe · 056aebe
1 parent 7de8a3a
commit 056aebe
Show file tree

Hide file tree

Showing 25 changed files with 3,265 additions and 394 deletions.
diff --git a/spectec/spec/1-syntax.watsup b/spectec/spec/1-syntax.watsup
@@ -198,7 +198,7 @@ syntax mem hint(desc "memory") =
 syntax elem hint(desc "table segment") =
   ELEM reftype expr* elemmode?
 syntax data hint(desc "memory segment") =
-  DATA (byte*)* datamode?
+  DATA byte* datamode?
 syntax start hint(desc "start function") =
   START funcidx
 

diff --git a/spectec/spec/3-typing.watsup b/spectec/spec/3-typing.watsup
@@ -431,7 +431,7 @@ rule Elem_ok:
   -- (Elemmode_ok: C |- elemmode : rt)?
 
 rule Data_ok:
-  C |- DATA (b*)* datamode? : OK
+  C |- DATA b* datamode? : OK
   -- (Datamode_ok: C |- datamode : OK)?
 
 rule Elemmode_ok/active:

diff --git a/spectec/spec/4-runtime.watsup b/spectec/spec/4-runtime.watsup
@@ -116,7 +116,18 @@ def $funcaddr(state) : funcaddr*  hint(show %.MODULE.FUNC)
 def $funcaddr((s; f)) = f.MODULE.FUNC
 
 def $funcinst(state) : funcinst*  hint(show %.FUNC)
+def $globalinst(state) : globalinst*  hint(show %.GLOBAL)
+def $tableinst(state) : tableinst*  hint(show %.TABLE)
+def $meminst(state) : meminst*  hint(show %.MEM)
+def $eleminst(state) : eleminst*  hint(show %.ELEM)
+def $datainst(state) : datainst*  hint(show %.DATA)
+
 def $funcinst((s; f)) = s.FUNC
+def $globalinst((s; f)) = s.GLOBAL
+def $tableinst((s; f)) = s.TABLE
+def $meminst((s; f)) = s.MEM
+def $eleminst((s; f)) = s.ELEM
+def $datainst((s; f)) = s.DATA
 
 def $func(state, funcidx) : funcinst        hint(show %.FUNC#`[%])
 def $global(state, globalidx) : globalinst  hint(show %.GLOBAL#`[%])

diff --git a/spectec/spec/7-module.watsup b/spectec/spec/7-module.watsup
@@ -0,0 +1,196 @@
+;; Allocation
+
+
+def $funcs(externval*) : funcaddr*
+def $funcs(epsilon) = epsilon
+def $funcs((FUNC fa) externval'*) = fa $funcs(externval'*)
+def $funcs(externval externval'*) = $funcs(externval'*)
+  -- otherwise
+
+def $globals(externval*) : globaladdr*
+def $globals(epsilon) = epsilon
+def $globals((GLOBAL ga) externval'*) = ga $globals(externval'*)
+def $globals(externval externval'*) = $globals(externval'*)
+  -- otherwise
+
+def $tables(externval*) : tableaddr*
+def $tables(epsilon) = epsilon
+def $tables((TABLE ta) externval'*) = ta $tables(externval'*)
+def $tables(externval externval'*) = $tables(externval'*)
+  -- otherwise
+
+def $mems(externval*) : memaddr*
+def $mems(epsilon) = epsilon
+def $mems((MEM ma) externval'*) = ma $mems(externval'*)
+def $mems(externval externval'*) = $mems(externval'*)
+  -- otherwise
+
+
+def $instexport(funcaddr*, globaladdr*, tableaddr*, memaddr*, export) : exportinst
+def $instexport(fa*, ga*, ta*, ma*, EXPORT name (FUNC x)) = { NAME name, VALUE (FUNC fa*[x]) }
+def $instexport(fa*, ga*, ta*, ma*, EXPORT name (GLOBAL x)) = { NAME name, VALUE (GLOBAL ga*[x]) }
+def $instexport(fa*, ga*, ta*, ma*, EXPORT name (TABLE x)) = { NAME name, VALUE (TABLE ta*[x]) }
+def $instexport(fa*, ga*, ta*, ma*, EXPORT name (MEM x)) = { NAME name, VALUE (MEM ma*[x]) }
+
+
+def $allocfunc(store, moduleinst, func) : (store, funcaddr)
+def $allocfunc(s, m, func) = (s[.FUNC =.. fi], |s.FUNC|)
+  -- if fi = { MODULE m, CODE func }
+
+def $allocfuncs(store, moduleinst, func*) : (store, funcaddr*)
+def $allocfuncs(s, m, epsilon) = (s, epsilon)
+def $allocfuncs(s, m, func func'*) = (s_2, fa fa'*)
+  -- if (s_1, fa) = $allocfunc(s, m, func)
+  -- if (s_2, fa'*) = $allocfuncs(s_1, m, func'*)
+
+def $allocglobal(store, globaltype, val) : (store, globaladdr)
+def $allocglobal(s, globaltype, val) = (s[.GLOBAL =.. gi], |s.GLOBAL|)
+  -- if gi = { TYPE globaltype, VALUE val }
+
+def $allocglobals(store, globaltype*, val*) : (store, globaladdr*)
+def $allocglobals(s, epsilon, epsilon) = (s, epsilon)
+def $allocglobals(s, globaltype globaltype'*, val val'*) = (s_2, ga ga'*)
+  -- if (s_1, ga) = $allocglobal(s, globaltype, val)
+  -- if (s_2, ga'*) = $allocglobals(s_1, globaltype'*, val'*)
+
+def $alloctable(store, tabletype) : (store, tableaddr)
+def $alloctable(s, `[i .. j] rt) = (s[.TABLE =.. ti], |s.TABLE|)
+  -- if ti = { TYPE (`[i .. j] rt), ELEM (REF.NULL rt)^i }
+
+def $alloctables(store, tabletype*) : (store, tableaddr*)
+def $alloctables(s, epsilon) = (s, epsilon)
+def $alloctables(s, tabletype tabletype'*) = (s_2, ta ta'*)
+  -- if (s_1, ta) = $alloctable(s, tabletype)
+  -- if (s_2, ta'*) = $alloctables(s_1, tabletype'*)
+
+def $allocmem(store, memtype) : (store, memaddr)
+def $allocmem(s, `[i .. j] I8) = (s[.MEM =.. mi], |s.MEM|)
+  -- if mi = { TYPE (`[i .. j] I8), DATA 0^(i * 64 * $Ki()) }
+
+def $allocmems(store, memtype*) : (store, memaddr*)
+def $allocmems(s, epsilon) = (s, epsilon)
+def $allocmems(s, memtype memtype'*) = (s_2, ma ma'*)
+  -- if (s_1, ma) = $allocmem(s, memtype)
+  -- if (s_2, ma'*) = $allocmems(s_1, memtype'*)
+
+def $allocelem(store, reftype, ref*) : (store, elemaddr)
+def $allocelem(s, rt, ref*) = (s[.ELEM =.. ei], |s.ELEM|)
+  -- if ei = { TYPE rt, ELEM ref* }
+
+def $allocelems(store, reftype*, (ref*)*) : (store, elemaddr*)
+def $allocelems(s, epsilon, epsilon) = (s, epsilon)
+def $allocelems(s, rt rt'*, ref* ref'**) = (s_2, ea ea'*)
+  -- if (s_1, ea) = $allocelem(s, rt, ref*)
+  -- if (s_2, ea'*) = $allocelems(s_2, rt'*, ref'**)
+
+def $allocdata(store, byte*) : (store, dataaddr)
+def $allocdata(s, byte*) = (s[.DATA =.. di], |s.DATA|)
+  -- if di = { DATA byte* }
+
+def $allocdatas(store, byte**) : (store, dataaddr*)
+def $allocdatas(s, epsilon) = (s, epsilon)
+def $allocdatas(s, byte* byte'**) = (s_2, da da'*)
+  -- if (s_1, da) = $allocdata(s, byte*)
+  -- if (s_2, da'*) = $allocdatas(s_1, byte'**)
+
+
+def $allocmodule(store, module, externval*, val*, (ref*)*) : (store, moduleinst)
+def $allocmodule(s, module, externval*, val*, (ref*)*) = (s_6, m)
+  -- if module =
+    MODULE
+      import*
+      func^n_func
+      (GLOBAL globaltype expr_1)^n_global
+      (TABLE tabletype)^n_table
+      (MEMORY memtype)^n_mem
+      (ELEM rt expr_2* elemmode?)^n_elem
+      (DATA byte* datamode?)^n_data
+      start?
+      export*
+  -- if fa_ex* = $funcs(externval*)
+  -- if ga_ex* = $globals(externval*)
+  -- if ta_ex* = $tables(externval*)
+  -- if ma_ex* = $mems(externval*)
+  -- if fa* = $(|s.FUNC|+i_func)^(i_func<n_func)
+  -- if ga* = $(|s.GLOBAL|+i_global)^(i_global<n_global)
+  -- if ta* = $(|s.TABLE|+i_table)^(i_table<n_table)
+  -- if ma* = $(|s.MEM|+i_mem)^(i_mem<n_mem)
+  -- if ea* = $(|s.ELEM|+i_elem)^(i_elem<n_elem)
+  -- if da* = $(|s.DATA|+i_data)^(i_data<n_data)
+  -- if xi* = $instexport(fa_ex* fa*, ga_ex* ga*, ta_ex* ta*, ma_ex* ma*, export)*
+  -- if m = {
+      FUNC fa_ex* fa*,
+      GLOBAL ga_ex* ga*,
+      TABLE ta_ex* ta*,
+      MEM ma_ex* ma*,
+      ELEM ea*,
+      DATA da*,
+      EXPORT xi*
+    }
+  -- if (s_1, fa*) = $allocfuncs(s, m, func^n_func)
+  -- if (s_2, ga*) = $allocglobals(s_1, globaltype^n_global, val*)
+  -- if (s_3, ta*) = $alloctables(s_2, tabletype^n_table)
+  -- if (s_4, ma*) = $allocmems(s_3, memtype^n_mem)
+  -- if (s_5, ea*) = $allocelems(s_4, rt^n_elem, (ref*)*)
+  -- if (s_6, da*) = $allocdatas(s_5, (byte*)^n_data)
+
+
+def $runelem(elem, idx) : instr*
+def $runelem(ELEM reftype expr*, i) = epsilon
+def $runelem(ELEM reftype expr* (DECLARE), i) = (ELEM.DROP i)
+def $runelem(ELEM reftype expr* (TABLE x instr*), i) =
+  instr* (CONST I32 0) (CONST I32 n) (TABLE.INIT x i) (ELEM.DROP i)
+  -- if n = |expr*|
+
+def $rundata(data, idx) : instr*
+def $rundata(DATA byte*, i) = epsilon
+def $rundata(DATA byte* (MEMORY 0 instr*), i) =
+  instr* (CONST I32 0) (CONST I32 n) (MEMORY.INIT i) (DATA.DROP i)
+  -- if n = |byte*|
+
+
+def $concat_instr(instr**) : instr*
+def $concat_instr(epsilon) = epsilon
+def $concat_instr(instr* instr'**) = instr* $concat_instr(instr'**)
+
+
+def $instantiation(store, module, externval*) : config
+def $instantiation(s, module, externval*) = s'; f; instr_elem* instr_data* (CALL x)?
+  -- if module = MODULE import* func* global* table* mem* elem* data* start? export*
+  -- if m_init = {
+      FUNC $funcs(externval*),
+      GLOBAL $globals(externval*),
+      TABLE epsilon,
+      MEM epsilon,
+      ELEM epsilon,
+      DATA epsilon,
+      EXPORT epsilon
+    }
+  -- if f_init = { LOCAL epsilon, MODULE m_init }
+  -- if global* = (GLOBAL globaltype instr_1*)*
+  -- (Step_read : s; f_init; instr_1* ~> val)*
+  -- if elem* = (ELEM reftype (instr_2*)* elemmode?)*
+  -- (Step_read : s; f_init; instr_2* ~> ref)**
+  -- if (s', m) = $allocmodule(s, module, externval*, val*, (ref*)*)
+  -- if f = { LOCAL epsilon, MODULE m }
+  -- if n_elem = |elem*|
+  -- if instr_elem* = $concat_instr($runelem(elem*[i], i)^(i<n_elem))
+  -- if n_data = |data*|
+  -- if instr_data* = $concat_instr($rundata(data*[j], j)^(j<n_data))
+  -- if start? = (START x)?
+
+
+def $invocation(store, funcaddr, val*) : config
+def $invocation(s, fa, val^n) = s; f; val^n (CALL_ADDR fa)
+  -- if m = {
+      FUNC epsilon,
+      GLOBAL epsilon,
+      TABLE epsilon,
+      MEM epsilon,
+      ELEM epsilon,
+      DATA epsilon,
+      EXPORT epsilon
+    }
+  -- if f = { LOCAL epsilon, MODULE m }
+  -- if $funcinst((s; f))[fa].CODE = FUNC functype valtype* expr
+  -- if functype = valtype_param^n -> valtype_res^k
diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
@@ -327,7 +327,7 @@ exception Arity_mismatch
 let rec expand_iter args iter =
   match iter with
   | Opt | List | List1 -> iter
-  | ListN e -> ListN (expand_exp args e)
+  | ListN (e, id_opt) -> ListN (expand_exp args e, id_opt)
 
 and expand_exp args e = expand_exp' args e.it $ e.at
 and expand_exp' args e' =
@@ -441,7 +441,10 @@ and render_iter env = function
   | Opt -> "^?"
   | List -> "^\\ast"
   | List1 -> "^{+}"
-  | ListN {it = ParenE (e, _); _} | ListN e -> "^{" ^ render_exp env e ^ "}"
+  | ListN ({it = ParenE (e, _); _}, None) | ListN (e, None) ->
+    "^{" ^ render_exp env e ^ "}"
+  | ListN (e, Some id) ->
+    "^(" ^ id.it ^ "<" ^ render_exp env e ^ ")"
 
 
 (* Types *)
@@ -684,25 +687,16 @@ let render_ruledef env d =
     render_rule_deco env " \\, " id1 id2 ""
   | _ -> failwith "render_ruledef"
 
-let render_red_conditions env = function
+let render_conditions env tabs = function
   | [] -> " & "
   | [Elem {it = ElsePr; _}] -> " &\\quad\n  " ^ word "otherwise"
   | (Elem {it = ElsePr; _})::prems ->
     " &\\quad\n  " ^ word "otherwise, if" ^ "~" ^
-    concat_map_nl " \\\\\n &&&&\\quad {\\land}~" "" (render_prem env) prems
+    concat_map_nl (" \\\\\n " ^ tabs ^ "\\quad {\\land}~") "" (render_prem env) prems
   | prems ->
     " &\\quad\n  " ^ word "if" ^ "~" ^
-    concat_map_nl " \\\\\n &&&&\\quad {\\land}~" "" (render_prem env) prems
+    concat_map_nl (" \\\\\n " ^ tabs ^ "\\quad {\\land}~") "" (render_prem env) prems
 
-let render_func_conditions env = function
-  | [] -> " & "
-  | [Elem {it = ElsePr; _}] -> " &\\quad\n  " ^ word "otherwise"
-  | (Elem {it = ElsePr; _})::prems ->
-    " &\\quad\n  " ^ word "otherwise, if" ^ "~" ^
-    concat_map_nl " \\\\\n &&&\\quad {\\land}~" "" (render_prem env) prems
-  | prems ->
-    " &\\quad\n  " ^ word "if" ^ "~" ^
-    concat_map_nl " \\\\\n &&&\\quad {\\land}~" "" (render_prem env) prems
 
 let render_reddef env d =
   match d.it with
@@ -714,14 +708,14 @@ let render_reddef env d =
     in
     render_rule_deco env "" id1 id2 " \\quad " ^ "& " ^
       render_exp env e1 ^ " &" ^ render_atom env SqArrow ^ "& " ^
-        render_exp env e2 ^ render_red_conditions env prems
+        render_exp env e2 ^ render_conditions env "&&&&" prems
   | _ -> failwith "render_reddef"
 
 let render_funcdef env d =
   match d.it with
   | DefD (id1, e1, e2, prems) ->
     render_exp env (CallE (id1, e1) $ d.at) ^ " &=& " ^
-      render_exp env e2 ^ render_func_conditions env prems
+      render_exp env e2 ^ render_conditions env "&&&" prems
   | _ -> failwith "render_funcdef"
 
 let rec render_sep_defs ?(sep = " \\\\\n") ?(br = " \\\\[0.8ex]\n") f = function

diff --git a/spectec/src/el/ast.ml b/spectec/src/el/ast.ml
@@ -44,7 +44,7 @@ type iter =
   | Opt                          (* `?` *)
   | List                         (* `*` *)
   | List1                        (* `+` *)
-  | ListN of exp                 (* `^` exp *)
+  | ListN of exp * id option     (* `^` exp *)
 
 
 (* Types *)

diff --git a/spectec/src/el/eq.ml b/spectec/src/el/eq.ml
@@ -20,7 +20,9 @@ let eq_nl_list eq_x xs1 xs2 = eq_list (eq_nl_elem eq_x) xs1 xs2
 let rec eq_iter iter1 iter2 =
   iter1 = iter2 ||
   match iter1, iter2 with
-  | ListN e1, ListN e2 -> eq_exp e1 e2
+  | ListN (e1, None), ListN (e2, None) -> eq_exp e1 e2
+  | ListN (e1, Some id1), ListN (e2, Some id2) ->
+    eq_exp e1 e2 && id1.it = id2.it
   | _, _ -> false
 
 

diff --git a/spectec/src/el/free.ml b/spectec/src/el/free.ml
@@ -18,6 +18,7 @@ let union sets1 sets2 =
     defid = Set.union sets1.defid sets2.defid;
   }
 
+let free_opt free_x xo = Option.(value (map free_x xo) ~default:empty)
 let free_list free_x xs = List.(fold_left union empty (map free_x xs))
 
 let free_nl_elem free_x = function Nl -> empty | Elem x -> free_x x
@@ -37,7 +38,7 @@ let free_defid id = {empty with defid = Set.singleton id.it}
 let rec free_iter iter =
   match iter with
   | Opt | List | List1 -> empty
-  | ListN e -> free_exp e
+  | ListN (e, id_opt) -> union (free_exp e) (free_opt free_varid id_opt)
 
 
 (* Types *)

diff --git a/spectec/src/el/print.ml b/spectec/src/el/print.ml
@@ -70,7 +70,8 @@ let rec string_of_iter iter =
   | Opt -> "?"
   | List -> "*"
   | List1 -> "+"
-  | ListN e -> "^" ^ string_of_exp e
+  | ListN (e, None) -> "^" ^ string_of_exp e
+  | ListN (e, Some id) -> "^(" ^ id.it ^ "<" ^ string_of_exp e ^ ")"
 
 
 (* Types *)

diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml
@@ -336,7 +336,13 @@ let rec elab_iter env iter : Il.iter =
   | Opt -> Il.Opt
   | List -> Il.List
   | List1 -> Il.List1
-  | ListN e -> Il.ListN (elab_exp env e (NatT $ e.at))
+  | ListN (e, id_opt) ->
+    Option.iter (fun id ->
+      let t = find "variable" env.vars (prefix_id id) in
+      if not (equiv_typ env t (NatT $ id.at)) then
+        error_typ e.at "iteration index" (NatT $ id.at)
+    ) id_opt;
+    Il.ListN (elab_exp env e (NatT $ e.at), id_opt)
 
 
 (* Types *)
@@ -762,7 +768,7 @@ and elab_exp_notation' env e t : Il.exp list =
   | (EpsE | SeqE _), IterT (t1, iter) ->
     [elab_exp_notation_iter env (unseq_exp e) (t1, iter) t e.at]
   | IterE (e1, iter1), IterT (t1, iter) ->
-    if (iter = Opt) <> (iter1 = Opt) then
+    if (iter = Opt) && (iter1 <> Opt) then
       error_typ e.at "iteration expression" t;
     let es1' = elab_exp_notation' env e1 t1 in
     let iter1' = elab_iter env iter1 in