DSL for module semantics

spectec/spec/1-syntax.watsup

@@ -57,7 +57,7 @@ syntax resulttype hint(desc "result type") =
   valtype*
 
 syntax limits hint(desc "limits") =
-  `[u32 .. u32]
+  `[u32 .. u32?]
 syntax globaltype hint(desc "global type") =
   MUT? valtype
 syntax functype hint(desc "function type") =
@@ -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
 

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:

spectec/spec/4-runtime.watsup

@@ -52,13 +52,26 @@ def $default_(EXTERNREF) = (REF.NULL EXTERNREF) ;; TODO: All reference types sho
 
 ;; Configurations
 
-syntax funcinst hint(desc "function instance") = moduleinst; func
-syntax globalinst hint(desc "global instance") = val
-syntax tableinst hint(desc "table instance") = ref*
-syntax meminst hint(desc "memory instance") = byte*
-syntax eleminst hint(desc "element instance") = ref*
-syntax datainst hint(desc "data instance") = byte*
-syntax exportinst hint(desc "export instance") = EXPORT name externval
+syntax funcinst hint(desc "function instance") =
+  { MODULE moduleinst,
+    CODE func }
+syntax globalinst hint(desc "global instance") =
+  { TYPE globaltype,
+    VALUE val }
+syntax tableinst hint(desc "table instance") =
+  { TYPE tabletype,
+    ELEM ref* }
+syntax meminst hint(desc "memory instance") =
+  { TYPE memtype,
+    DATA byte* }
+syntax eleminst hint(desc "element instance") =
+  { TYPE elemtype,
+    ELEM ref* }
+syntax datainst hint(desc "data instance") =
+  { DATA byte* }
+syntax exportinst hint(desc "export instance") =
+  { NAME name,
+    VALUE externval }
 
 syntax store hint(desc "store") =
   { FUNC funcinst*,
@@ -103,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#`[%])
@@ -123,23 +147,33 @@ def $local((s; f), x) = f.LOCAL[x]
 
 
 def $with_local(state, localidx, val) : state     hint(show %[.LOCAL[%] = %])
-def $with_global(state, globalidx, val) : state   hint(show %[.GLOBAL[%] = %])
-def $with_table(state, tableidx, nat, ref) : state  hint(show %[.TABLE[%][%] = %])
-def $with_tableext(state, tableidx, ref*) : state hint(show %[.TABLE[%] =.. %])
-def $with_mem(state, tableidx, nat, nat, byte*) : state  hint(show %[.MEM[%][% : %] = %])
-def $with_memext(state, tableidx, byte*) : state  hint(show %[.MEM[%] =.. %])
-def $with_elem(state, elemidx, ref*) : state      hint(show %[.ELEM[%] = %])
-def $with_data(state, dataidx, byte*) : state     hint(show %[.DATA[%] = %])
+def $with_global(state, globalidx, val) : state   hint(show %[.GLOBAL[%].VALUE = %])
+def $with_table(state, tableidx, nat, ref) : state  hint(show %[.TABLE[%].ELEM[%] = %])
+def $with_tableinst(state, tableidx, tableinst) : state hint(show %[.TABLE[%] = %])
+def $with_mem(state, memidx, nat, nat, byte*) : state  hint(show %[.MEM[%].DATA[% : %] = %])
+def $with_meminst(state, memidx, meminst) : state  hint(show %[.MEM[%] = %])
+def $with_elem(state, elemidx, ref*) : state      hint(show %[.ELEM[%].ELEM = %])
+def $with_data(state, dataidx, byte*) : state     hint(show %[.DATA[%].DATA = %])
 
 def $with_local((s; f), x, v) = s; f[.LOCAL[x] = v]
-def $with_global((s; f), x, v) = s[.GLOBAL[f.MODULE.GLOBAL[x]] = v]; f
-def $with_table((s; f), x, i, r) = s[.TABLE[f.MODULE.TABLE[x]][i] = r]; f
-def $with_tableext((s; f), x, r*) = s[.TABLE[f.MODULE.TABLE[x]] =.. r*]; f
-def $with_mem((s; f), x, i, j, b*) = s[.MEM[f.MODULE.MEM[x]][i : j] = b*]; f
-def $with_memext((s; f), x, b*) = s[.MEM[f.MODULE.MEM[x]] =.. b*]; f
-def $with_elem((s; f), x, r*) = s[.ELEM[f.MODULE.ELEM[x]] = r*]; f
-def $with_data((s; f), x, b*) = s[.DATA[f.MODULE.DATA[x]] = b*]; f
-
+def $with_global((s; f), x, v) = s[.GLOBAL[f.MODULE.GLOBAL[x]].VALUE = v]; f
+def $with_table((s; f), x, i, r) = s[.TABLE[f.MODULE.TABLE[x]].ELEM[i] = r]; f
+def $with_tableinst((s; f), x, ti) = s[.TABLE[f.MODULE.TABLE[x]] = ti]; f
+def $with_mem((s; f), x, i, j, b*) = s[.MEM[f.MODULE.MEM[x]].DATA[i : j] = b*]; f
+def $with_meminst((s; f), x, mi) = s[.MEM[f.MODULE.MEM[x]] = mi]; f
+def $with_elem((s; f), x, r*) = s[.ELEM[f.MODULE.ELEM[x]].ELEM = r*]; f
+def $with_data((s; f), x, b*) = s[.DATA[f.MODULE.DATA[x]].DATA = b*]; f
+
+def $grow_table(tableinst, nat, ref) : tableinst
+def $grow_memory(meminst, nat) : meminst
+def $grow_table(ti, n, r) = ti'
+  -- if ti = { TYPE `[i .. j?] reftype, ELEM r'* }
+  -- if i' = $(|r'*| + n)
+  -- if ti' = { TYPE `[i' .. j?] reftype, ELEM r'* r^n }
+def $grow_memory(mi, n) = mi'
+  -- if mi = { TYPE (`[i .. j?] I8), DATA b* }
+  -- if i' = $(|b*| / (64 * $Ki) + n)
+  -- if mi' = { TYPE (`[i' .. j?] I8), DATA b* 0^(n * 64 * $Ki) }
 
 ;; Administrative Instructions
 

spectec/spec/6-reduction.watsup

@@ -84,8 +84,8 @@ rule Step_read/call:
 
 rule Step_read/call_indirect-call:
   z; (CONST I32 i) (CALL_INDIRECT x ft)  ~>  (CALL_ADDR a)
-  -- if $table(z, x)[i] = (REF.FUNC_ADDR a)
-  -- if $funcinst(z)[a] = m; FUNC ft' t* instr*
+  -- if $table(z, x).ELEM[i] = (REF.FUNC_ADDR a)
+  -- if $funcinst(z)[a].CODE = FUNC ft' t* instr*
   -- if ft = ft'
 
 rule Step_read/call_indirect-trap:
@@ -94,7 +94,8 @@ rule Step_read/call_indirect-trap:
 
 rule Step_read/call_addr:
   z; val^k (CALL_ADDR a)  ~>  (FRAME_ n `{f} (LABEL_ n `{epsilon} instr*))
-  -- if $funcinst(z)[a] = m; FUNC (t_1^k -> t_2^n) t* instr*
+  -- if $funcinst(z)[a] = {MODULE m, CODE func}
+  -- if func = FUNC (t_1^k -> t_2^n) t* instr*
   -- if f = {LOCAL val^k ($default_(t))*, MODULE m}
 
 
@@ -172,44 +173,47 @@ rule Step_pure/local.tee:
 
 
 rule Step_read/global.get:
-  z; (GLOBAL.GET x)  ~>  $global(z, x)
+  z; (GLOBAL.GET x)  ~>  $global(z, x).VALUE
 
 rule Step/global.set:
   z; val (GLOBAL.SET x)  ~>  $with_global(z, x, val); epsilon
 
 
 rule Step_read/table.get-trap:
   z; (CONST I32 i) (TABLE.GET x)  ~>  TRAP
-  -- if i >= |$table(z, x)|
+  -- if i >= |$table(z, x).ELEM|
 
 rule Step_read/table.get-val:
-  z; (CONST I32 i) (TABLE.GET x)  ~>  $table(z,x)[i]
-  -- if i < |$table(z, x)|
+  z; (CONST I32 i) (TABLE.GET x)  ~>  $table(z,x).ELEM[i]
+  -- if i < |$table(z, x).ELEM|
 
 rule Step/table.set-trap:
   z; (CONST I32 i) ref (TABLE.GET x)  ~>  z; TRAP
-  -- if i >= |$table(z, x)|
+  -- if i >= |$table(z, x).ELEM|
 
 rule Step/table.set-val:
   z; (CONST I32 i) ref (TABLE.GET x)  ~>  $with_table(z, x, i, ref); epsilon
-  -- if i < |$table(z, x)|
+  -- if i < |$table(z, x).ELEM|
 
 
 rule Step_read/table.size:
   z; (TABLE.SIZE x)  ~>  (CONST I32 n)
-  -- if |$table(z, x)| = n  ;; TODO: inline this
+  -- if |$table(z, x).ELEM| = n  ;; TODO: inline this
 
 
 rule Step/table.grow-succeed:
-  z; ref (CONST I32 n) (TABLE.GROW x)  ~>  $with_tableext(z, x, ref^n); (CONST I32 $(|$table(z, x)|))
+  z; ref (CONST I32 n) (TABLE.GROW x)  ~>  $with_tableinst(z, x, ti'); (CONST I32 $(|$table(z, x).ELEM|))
+  -- if $table(z, x) = ti
+  -- if $grow_table(ti, n, ref) = ti'
+  -- Tabletype_ok: |- ti'.TYPE : OK
 
 rule Step/table.grow-fail:
   z; ref (CONST I32 n) (TABLE.GROW x)  ~>  z; (CONST I32 $(-1))
 
 
 rule Step_read/table.fill-trap:
   z; (CONST I32 i) val (CONST I32 n) (TABLE.FILL x)  ~>  TRAP
-  -- if $(i + n) > |$table(z, x)|
+  -- if $(i + n) > |$table(z, x).ELEM|
 
 rule Step_read/table.fill-zero:
   z; (CONST I32 i) val (CONST I32 n) (TABLE.FILL x)  ~>  epsilon
@@ -225,7 +229,7 @@ rule Step_read/table.fill-succ:
 
 rule Step_read/table.copy-trap:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (TABLE.COPY x y)  ~>  TRAP
-  -- if $(i + n) > |$table(z, y)| \/ $(j + n) > |$table(z, x)|
+  -- if $(i + n) > |$table(z, y).ELEM| \/ $(j + n) > |$table(z, x).ELEM|
 
 rule Step_read/table.copy-zero:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (TABLE.COPY x y)  ~>  epsilon
@@ -248,7 +252,7 @@ rule Step_read/table.copy-gt:
 
 rule Step_read/table.init-trap:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (TABLE.INIT x y)  ~>  TRAP
-  -- if $(i + n) > |$elem(z, y)| \/ $(j + n) > |$table(z, x)|
+  -- if $(i + n) > |$elem(z, y).ELEM| \/ $(j + n) > |$table(z, x).ELEM|
 
 rule Step_read/table.init-zero:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (TABLE.INIT x y)  ~>  epsilon
@@ -257,7 +261,7 @@ rule Step_read/table.init-zero:
 
 rule Step_read/table.init-succ:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (TABLE.INIT x y)  ~>
-    (CONST I32 j) $elem(z,y)[i] (TABLE.SET x)
+    (CONST I32 j) $elem(z,y).ELEM[i] (TABLE.SET x)
     (CONST I32 $(j+1)) (CONST I32 $(i+1)) (CONST I32 $(n-1)) (TABLE.INIT x y)
   -- otherwise
 
@@ -268,32 +272,32 @@ rule Step/elem.drop:
 
 rule Step_read/load-num-trap:
   z; (CONST I32 i) (LOAD nt n_A n_O)  ~>  TRAP
-  -- if $(i + n_O + $size(nt)/8 > |$mem(z, 0)|)
+  -- if $(i + n_O + $size(nt)/8 > |$mem(z, 0).DATA|)
 
 rule Step_read/load-num-val:
   z; (CONST I32 i) (LOAD nt n_A n_O)  ~>  (CONST nt c)
-  -- if $bytes_($size(nt), c) = $mem(z, 0)[i + n_O : $size(nt)/8]
+  -- if $bytes_($size(nt), c) = $mem(z, 0).DATA[i + n_O : $size(nt)/8]
 
 rule Step_read/load-pack-trap:
   z; (CONST I32 i) (LOAD nt (n _ sx) n_A n_O)  ~>  TRAP
-  -- if $(i + n_O + n/8 > |$mem(z, 0)|)
+  -- if $(i + n_O + n/8 > |$mem(z, 0).DATA|)
 
 rule Step_read/load-pack-val:
   z; (CONST I32 i) (LOAD nt (n _ sx) n_A n_O)  ~>  (CONST nt $ext(n, $size(nt), sx, c))
-  -- if $bytes_(n, c) = $mem(z, 0)[i + n_O : n/8]
+  -- if $bytes_(n, c) = $mem(z, 0).DATA[i + n_O : n/8]
 
 
 rule Step/store-num-trap:
   z; (CONST I32 i) (CONST nt c) (STORE nt n_A n_O)  ~>  z; TRAP
-  -- if $(i + n_O + $size(nt)/8) > |$mem(z, 0)|
+  -- if $(i + n_O + $size(nt)/8) > |$mem(z, 0).DATA|
 
 rule Step/store-num-val:
   z; (CONST I32 i) (CONST nt c) (STORE nt n_A n_O)  ~>  $with_mem(z, 0, $(i + n_O), $($size(nt)/8), b*); epsilon
   -- if b* = $bytes_($size(nt), c)
 
 rule Step/store-pack-trap:
   z; (CONST I32 i) (CONST nt c) (STORE nt n n_A n_O)  ~>  z; TRAP
-  -- if $(i + n_O + n/8) > |$mem(z, 0)|
+  -- if $(i + n_O + n/8) > |$mem(z, 0).DATA|
 
 rule Step/store-pack-val:
   z; (CONST I32 i) (CONST nt c) (STORE nt n n_A n_O)  ~>  $with_mem(z, 0, $(i + n_O), $(n/8), b*); epsilon
@@ -302,19 +306,22 @@ rule Step/store-pack-val:
 
 rule Step_read/memory.size:
   z; (MEMORY.SIZE)  ~>  (CONST I32 n)
-  -- if $(n * 64 * $Ki) = |$mem(z, 0)|
+  -- if $(n * 64 * $Ki) = |$mem(z, 0).DATA|
 
 
 rule Step/memory.grow-succeed:
-  z; (CONST I32 n) (MEMORY.GROW)  ~>  $with_memext(z, 0, 0^(n * 64 * $Ki)); (CONST I32 $(|$mem(z, 0)| / (64 * $Ki)))
+  z; (CONST I32 n) (MEMORY.GROW)  ~>  $with_meminst(z, 0, mi'); (CONST I32 $(|$mem(z, 0).DATA| / (64 * $Ki)))
+  -- if $mem(z, 0) = mi
+  -- if $grow_memory(mi, n) = mi'
+  -- Memtype_ok: |- mi'.TYPE : OK
 
 rule Step/memory.grow-fail:
   z; (CONST I32 n) (MEMORY.GROW)  ~>  z; (CONST I32 $(-1))
 
 
 rule Step_read/memory.fill-trap:
   z; (CONST I32 i) val (CONST I32 n) (MEMORY.FILL)  ~>  TRAP
-  -- if $(i + n) > |$mem(z, 0)|
+  -- if $(i + n) > |$mem(z, 0).DATA|
 
 rule Step_read/memory.fill-zero:
   z; (CONST I32 i) val (CONST I32 n) (MEMORY.FILL)  ~>  epsilon
@@ -330,7 +337,7 @@ rule Step_read/memory.fill-succ:
 
 rule Step_read/memory.copy-trap:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.COPY)  ~>  TRAP
-  -- if $(i + n) > |$mem(z, 0)| \/ $(j + n) > |$mem(z, 0)|
+  -- if $(i + n) > |$mem(z, 0).DATA| \/ $(j + n) > |$mem(z, 0).DATA|
 
 rule Step_read/memory.copy-zero:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.COPY)  ~>  epsilon
@@ -353,7 +360,7 @@ rule Step_read/memory.copy-gt:
 
 rule Step_read/memory.init-trap:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.INIT x)  ~>  TRAP
-  -- if $(i + n) > |$data(z, x)| \/ $(j + n) > |$mem(z, 0)|
+  -- if $(i + n) > |$data(z, x).DATA| \/ $(j + n) > |$mem(z, 0).DATA|
 
 rule Step_read/memory.init-zero:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.INIT x)  ~>  epsilon
@@ -362,7 +369,7 @@ rule Step_read/memory.init-zero:
 
 rule Step_read/memory.init-succ:
   z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.INIT x)  ~>
-    (CONST I32 j) (CONST I32 $data(z,x)[i]) (STORE I32 8 0 0)
+    (CONST I32 j) (CONST I32 $data(z,x).DATA[i]) (STORE I32 8 0 0)
     (CONST I32 $(j+1)) (CONST I32 $(i+1)) (CONST I32 $(n-1)) (MEMORY.INIT x)
   -- otherwise