Merge pull request #88 from Wasm-DSL/exec

Replace more execution; fix array.new/init_data rules

spectec/spec/wasm-1.0/3-numerics.watsup

@@ -15,13 +15,13 @@ def $invsigned(N, ii) = j       -- if $signed(N, j) = ii
 ;; TODO
 
 def $unop(valtype, unop_(valtype), val_(valtype)) : val_(valtype)*
-    hint(show %2#_%1#((%3)))
+    hint(show %2#$_(%1)#((%3)))
 def $binop(valtype, binop_(valtype), val_(valtype), val_(valtype)) : val_(valtype)*
-    hint(show %2#_%1#(%3, %4))
+    hint(show %2#$_(%1)#(%3, %4))
 def $testop(valtype, testop_(valtype), val_(valtype)) : val_(I32)
-    hint(show %2#_%1#((%3)))
+    hint(show %2#$_(%1)#((%3)))
 def $relop(valtype, relop_(valtype), val_(valtype), val_(valtype)) : val_(I32)
-    hint(show %2#_%1#(%3, %4))
+    hint(show %2#$_(%1)#(%3, %4))
 def $cvtop(valtype_1, valtype_2, cvtop, sx?, val_(valtype_1)) : val_(valtype_2)*
     hint(show %3#$_((%1,%2))^(%4)#((%5)))
 

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

@@ -65,12 +65,12 @@ def $tableinst((s; f)) = s.TABLE
 def $meminst((s; f)) = s.MEM
 def $moduleinst((s; f)) = f.MODULE
 
-def $type(state, typeidx) : functype        hint(show %.TYPE`[%])
-def $func(state, funcidx) : funcinst        hint(show %.FUNC#`[%])
-def $global(state, globalidx) : globalinst  hint(show %.GLOBAL#`[%])
-def $table(state, tableidx) : tableinst     hint(show %.TABLE#`[%])
-def $mem(state, memidx) : meminst           hint(show %.MEM#`[%])
-def $local(state, localidx) : val           hint(show %.LOCAL#`[%])
+def $type(state, typeidx) : functype        hint(show %.TYPE[%])
+def $func(state, funcidx) : funcinst        hint(show %.FUNC[%])
+def $global(state, globalidx) : globalinst  hint(show %.GLOBAL[%])
+def $table(state, tableidx) : tableinst     hint(show %.TABLE[%])
+def $mem(state, memidx) : meminst           hint(show %.MEM[%])
+def $local(state, localidx) : val           hint(show %.LOCAL[%])
 
 def $type((s; f), x) = f.MODULE.TYPE[x]
 def $func((s; f), x) = s.FUNC[f.MODULE.FUNC[x]]

spectec/spec/wasm-2.0/1-syntax.watsup

@@ -126,6 +126,9 @@ syntax numtype hint(desc "number type") =
 syntax vectype hint(desc "vector type") =
   | V128
 
+syntax consttype hint(desc "literal type") =
+  | numtype | vectype
+
 syntax reftype hint(desc "reference type") =
   | FUNCREF | EXTERNREF
 
@@ -147,7 +150,7 @@ syntax packtype hint(desc "packed type") = I8 | I16
 syntax lanetype hint(desc "lane type") = numtype | packtype
 
 syntax pnn hint(show I#n) = I8 | I16
-syntax lnn hint(show I#n) = numtype | pnn
+syntax lnn hint(show I#n) = inn | fnn | pnn
 syntax imm hint(show I#n) = inn | pnn
 
 

spectec/spec/wasm-2.0/3-numerics.watsup

@@ -20,13 +20,13 @@ def $invsigned(N, i) = j        -- if $signed(N, j) = i
 ;; TODO
 
 def $unop(numtype, unop_(numtype), num_(numtype)) : num_(numtype)*
-    hint(show %2#_%1#((%3)))
+    hint(show %2#$_(%1)#((%3)))
 def $binop(numtype, binop_(numtype), num_(numtype), num_(numtype)) : num_(numtype)*
-    hint(show %2#_%1#(%3, %4))
+    hint(show %2#$_(%1)#(%3, %4))
 def $testop(numtype, testop_(numtype), num_(numtype)) : num_(I32)
-    hint(show %2#_%1#((%3)))
+    hint(show %2#$_(%1)#((%3)))
 def $relop(numtype, relop_(numtype), num_(numtype), num_(numtype)) : num_(I32)
-    hint(show %2#_%1#(%3, %4))
+    hint(show %2#$_(%1)#(%3, %4))
 def $cvtop(numtype_1, numtype_2, cvtop, sx?, num_(numtype_1)) : num_(numtype_2)*
     hint(show %3#$_((%1,%2))^(%4)#((%5)))
 

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

@@ -71,14 +71,14 @@ def $eleminst((s; f)) = s.ELEM
 def $datainst((s; f)) = s.DATA
 def $moduleinst((s; f)) = f.MODULE
 
-def $type(state, typeidx) : functype        hint(show %.TYPE`[%])
-def $func(state, funcidx) : funcinst        hint(show %.FUNC#`[%])
-def $global(state, globalidx) : globalinst  hint(show %.GLOBAL#`[%])
-def $table(state, tableidx) : tableinst     hint(show %.TABLE#`[%])
-def $mem(state, memidx) : meminst           hint(show %.MEM#`[%])
-def $elem(state, tableidx) : eleminst       hint(show %.ELEM#`[%])
-def $data(state, dataidx) : datainst        hint(show %.DATA#`[%])
-def $local(state, localidx) : val           hint(show %.LOCAL#`[%])
+def $type(state, typeidx) : functype        hint(show %.TYPE[%])
+def $func(state, funcidx) : funcinst        hint(show %.FUNC[%])
+def $global(state, globalidx) : globalinst  hint(show %.GLOBAL[%])
+def $table(state, tableidx) : tableinst     hint(show %.TABLE[%])
+def $mem(state, memidx) : meminst           hint(show %.MEM[%])
+def $elem(state, tableidx) : eleminst       hint(show %.ELEM[%])
+def $data(state, dataidx) : datainst        hint(show %.DATA[%])
+def $local(state, localidx) : val           hint(show %.LOCAL[%])
 
 def $type((s; f), x) = f.MODULE.TYPE[x]
 def $func((s; f), x) = s.FUNC[f.MODULE.FUNC[x]]

spectec/spec/wasm-2.0/8-reduction.watsup

@@ -190,11 +190,11 @@ rule Step_read/ref.func:
 
 
 rule Step_pure/ref.is_null-true:
-  val REF.IS_NULL  ~>  (CONST I32 1)
-  -- if val = (REF.NULL rt)
+  ref REF.IS_NULL  ~>  (CONST I32 1)
+  -- if ref = (REF.NULL rt)
 
 rule Step_pure/ref.is_null-false:
-  val REF.IS_NULL  ~>  (CONST I32 0)
+  ref REF.IS_NULL  ~>  (CONST I32 0)
   -- otherwise
 
 

spectec/spec/wasm-3.0/1-syntax.watsup

@@ -129,6 +129,9 @@ syntax numtype hint(desc "number type") =
 syntax vectype hint(desc "vector type") =
   | V128
 
+syntax consttype hint(desc "literal type") =
+  | numtype | vectype
+
 syntax absheaptype/syn hint(desc "abstract heap type") =
   | ANY | EQ | I31 | STRUCT | ARRAY | NONE
   | FUNC | NOFUNC
@@ -163,7 +166,7 @@ syntax lanetype hint(desc "lane type") = numtype | packtype
 syntax storagetype hint(desc "storage type") = valtype | packtype
 
 syntax pnn hint(show I#n) = I8 | I16
-syntax lnn hint(show I#n) = numtype | pnn
+syntax lnn hint(show I#n) = inn | fnn | pnn
 syntax imm hint(show I#n) = inn | pnn
 
 
@@ -276,6 +279,7 @@ syntax lane_(imm) = iN($lsize(imm))  ;; HACK
 
 syntax vec_(vnn) = vN($vsize(vnn))
 
+;; TODO: Rename? bval? storageval\ref?
 syntax zval_(storagetype)
 syntax zval_(numtype) = num_(numtype)
 syntax zval_(vectype) = vec_(vectype)

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

@@ -88,21 +88,21 @@ def $nunpack(packtype) = I32
 def $vunpack(storagetype) : vectype  hint(show $unpack(%)) hint(partial)
 def $vunpack(vectype) = vectype
 
-def $cunpack(storagetype) : cnn  hint(show $unpack(%)) hint(partial)
-def $cunpack(vt) = vt
-def $cunpack(nt) = nt
-def $cunpack(pt) = I32
+def $cunpack(storagetype) : consttype  hint(show $unpack(%)) hint(partial)
+def $cunpack(consttype) = consttype
+def $cunpack(packtype) = I32
+def $cunpack(lanetype) = $lunpack(lanetype)  ;; HACK
 
-def $sxfield(storagetype) : sx?  hint(show $sx(%))
-def $sxfield(valtype) = eps
-def $sxfield(packtype) = S
+def $sx(storagetype) : sx?  hint(show $sx(%))
+def $sx(consttype) = eps
+def $sx(packtype) = S
 
 
 ;; Const
 
-def $const(cnn, zval_(cnn)): instr  hint(show %.CONST %)
-def $const(vt, c) = (VCONST vt c)
-def $const(nt, c) = (CONST nt c)
+def $const(consttype, zval_(consttype)): instr  hint(show %.CONST %)
+def $const(numtype, c) = (CONST numtype c)
+def $const(vectype, c) = (VCONST vectype c)
 
 
 ;; Shapes

spectec/spec/wasm-3.0/3-numerics.watsup

@@ -22,11 +22,11 @@ def $invsigned(N, i) = j        -- if $signed(N, j) = i
 def $unop(numtype, unop_(numtype), num_(numtype)) : num_(numtype)*
     hint(show %2#$_(%1)#((%3)))
 def $binop(numtype, binop_(numtype), num_(numtype), num_(numtype)) : num_(numtype)*
-    hint(show %2#_%1#(%3, %4))
+    hint(show %2#$_(%1)#(%3, %4))
 def $testop(numtype, testop_(numtype), num_(numtype)) : num_(I32)
-    hint(show %2#_%1#((%3)))
+    hint(show %2#$_(%1)#((%3)))
 def $relop(numtype, relop_(numtype), num_(numtype), num_(numtype)) : num_(I32)
-    hint(show %2#_%1#(%3, %4))
+    hint(show %2#$_(%1)#(%3, %4))
 def $cvtop(numtype_1, numtype_2, cvtop, sx?, num_(numtype_1)) : num_(numtype_2)*
     hint(show %3#$_((%1,%2))^(%4)#((%5)))
 
@@ -187,6 +187,10 @@ def $unpacknum(lanetype, lane_(lanetype)) : num_($lunpack(lanetype))
 def $unpacknum(numtype, c) = c
 def $unpacknum(packtype, c) = $ext($psize(packtype), $size($lunpack(packtype)), U, c)
 
+def $packconst(storagetype, zval_($cunpack(storagetype))) : zval_(storagetype)
+def $packconst(consttype, c) = c
+def $packconst(packtype, c) = $packnum(packtype, c)
+
 
 ;; Vectors
 

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

@@ -29,14 +29,14 @@ def $default_(REF eps ht) = eps
 
 ;; Packed fields
 
-def $packval(storagetype, val) : fieldval         hint(show $pack_(%,%))
-def $unpackval(storagetype, sx?, fieldval) : val  hint(show $unpack_(%)^(%)#((%)))
+def $packfield(storagetype, val) : fieldval         hint(show $pack_(%,%))
+def $unpackfield(storagetype, sx?, fieldval) : val  hint(show $unpack_(%)^(%)#((%)))
 
-def $packval(t, val) = val
-def $packval(pt, CONST I32 i) = PACK pt $wrap(32, $psize(pt), i)
+def $packfield(t, val) = val
+def $packfield(pt, CONST I32 i) = PACK pt $wrap(32, $psize(pt), i)
 
-def $unpackval(t, eps, val) = val
-def $unpackval(pt, sx, PACK pt i) = CONST I32 $ext($psize(pt), 32, sx, i)
+def $unpackfield(t, eps, val) = val
+def $unpackfield(pt, sx, PACK pt i) = CONST I32 $ext($psize(pt), 32, sx, i)
 
 
 ;; Projections
@@ -99,14 +99,14 @@ def $structinst((s; f)) = s.STRUCT
 def $arrayinst((s; f)) = s.ARRAY
 def $moduleinst((s; f)) = f.MODULE
 
-def $type(state, typeidx) : deftype         hint(show %.TYPE`[%])
-def $func(state, funcidx) : funcinst        hint(show %.FUNC#`[%])
-def $global(state, globalidx) : globalinst  hint(show %.GLOBAL#`[%])
-def $table(state, tableidx) : tableinst     hint(show %.TABLE#`[%])
-def $mem(state, memidx) : meminst           hint(show %.MEM#`[%])
-def $elem(state, tableidx) : eleminst       hint(show %.ELEM#`[%])
-def $data(state, dataidx) : datainst        hint(show %.DATA#`[%])
-def $local(state, localidx) : val?          hint(show %.LOCAL#`[%])
+def $type(state, typeidx) : deftype         hint(show %.TYPE[%])
+def $func(state, funcidx) : funcinst        hint(show %.FUNC[%])
+def $global(state, globalidx) : globalinst  hint(show %.GLOBAL[%])
+def $table(state, tableidx) : tableinst     hint(show %.TABLE[%])
+def $mem(state, memidx) : meminst           hint(show %.MEM[%])
+def $elem(state, tableidx) : eleminst       hint(show %.ELEM[%])
+def $data(state, dataidx) : datainst        hint(show %.DATA[%])
+def $local(state, localidx) : val?          hint(show %.LOCAL[%])
 
 def $type((s; f), x) = f.MODULE.TYPE[x]
 def $func((s; f), x) = s.FUNC[f.MODULE.FUNC[x]]
@@ -129,7 +129,7 @@ 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_struct(state, structaddr, nat, fieldval) : state  hint(show %[.STRUCT[%].FIELD[%] = %])
-def $with_array(state, arrayaddr, nat, fieldval) : state    hint(show %[.STRUCT[%].FIELD[%] = %])
+def $with_array(state, arrayaddr, nat, fieldval) : state    hint(show %[.ARRAY[%].FIELD[%] = %])
 
 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]].VALUE = v]; f