Add algorithmic backend

spectec/README.md

@@ -233,21 +233,18 @@ Then, Sphinx builds the `rst` files into desired formats such as pdf or html.
 
 ## Running Interpreter Backend (WIP)
 
-The interpreter backend can be found in the [`al`](https://github.com/Wasm-DSL/spectec/tree/al) branch at the moment. It currently passes all tests in the official WebAssembly test suite.
+The interpreter backend can be found in the [`al`](https://github.com/Wasm-DSL/spectec/tree/al) branch at the moment.
 
-To run our interpreter backend against all of the official test suite,
+To run a wast file,
 ```
 $ git checkout al
 $ make
-$ ./watsup spec/* --animate --sideconditions --interpreter
+$ ./watsup spec/* --animate --sideconditions --interpreter test-interpreter/sample.wast
 ```
 
-You may also run custom Wasm programs on our interpreter backend.
-
-This feature is yet under construction, as our interpreter accepts `wast` format programs only.
-For convenience, modify [test-interpreter/sample.wast](https://github.com/Wasm-DSL/spectec/blob/al/spectec/test-interpreter/sample.wast) as you like and run,
+You may also run all wast files in the directory.
 ```
 $ git checkout al
 $ make
-$ ./watsup spec/* --animate --sideconditions --interpreter --test-interpreter test-interpreter/sample
+$ ./watsup spec/* --animate --sideconditions --interpreter ../test/core
 ```

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

@@ -21,6 +21,7 @@ syntax uN(N) hint(desc "unsigned integer") = 0 | ... | 2^N-1
 syntax sN(N) hint(desc "signed integer") = -2^(N-1) | ... | -1 | 0 | +1 | ... | 2^(N-1)-1
 syntax iN(N) hint(desc "integer") = uN(N)
 
+syntax u8 = uN(8)
 syntax u31 = uN(31)
 syntax u32 = uN(32)
 syntax u64 = uN(64)
@@ -68,6 +69,7 @@ syntax f64 = fN(64)
 ;;
 
 syntax idx hint(desc "index") = u32
+syntax laneidx hint(desc "index") = u8
 
 syntax typeidx hint(desc "type index") = idx
 syntax funcidx hint(desc "function index") = idx
@@ -92,6 +94,7 @@ var x33 : s33 hint(show x)
 ;; Value types
 
 syntax nul = NULL?
+syntax zero = ZERO?
 
 syntax numtype hint(desc "number type") =
   | I32 | I64 | F32 | F64
@@ -250,9 +253,71 @@ var testop : testop_numtype
 var relop : relop_numtype
 
 
-syntax memop hint(desc "memory operator") = {ALIGN u32, OFFSET u32}
+syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}
 
-var mo : memop
+var marg : memarg
+
+syntax lanetype hint(desc "lane type") =
+  | packedtype | numtype
+syntax lanesize hint(desc "lane size") = nat
+
+var lnt : lanetype
+var lns : lanesize
+syntax shape hint(desc "shape") = lanetype X lanesize
+
+var psl : nat
+var psr : nat
+
+syntax packshape =
+  | PACKSHAPE nat nat
+
+var psh : packshape
+
+syntax half = | LOW | HIGH
+var hf : half
+
+var sh : shape
+
+syntax unopVVXX = | NOT
+syntax binopVVXX = | AND | ANDNOT | OR | XOR
+syntax ternopVVXX = | BITSELECT
+syntax testopVVXX = | ANY_TRUE
+syntax testopVIXX = | ALL_TRUE
+syntax relopVIXX = | EQ | NE | LT sx | GT sx | LE sx | GE sx
+syntax relopVFXX = | EQ | NE | LT | GT | LE | GE
+syntax unopVIXX = | ABS | NEG
+syntax binopVIXX = | ADD | SUB | SWIZZLE
+syntax minmaxopVIXX = | MIN sx | MAX sx
+syntax satbinopVIXX = | ADD_SAT sx | SUB_SAT sx
+syntax shiftopVIXX = | SHL | SHR sx
+syntax unopVFXX = | ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST
+syntax binopVFXX = | ADD | SUB | MUL | DIV | MIN | MAX | PMIN | PMAX
+
+
+syntax unop_vvectype = | _VV unopVVXX
+syntax binop_vvectype = | _VV binopVVXX
+syntax ternop_vvectype = | _VV ternopVVXX
+syntax testop_vvectype = | _VV testopVVXX
+
+syntax shiftop_vectype = | _VI shiftopVIXX
+syntax unop_vectype = | _VI unopVIXX | _VF unopVFXX | POPCNT
+syntax binop_vectype = | _VI binopVIXX minmaxopVIXX satbinopVIXX | _VF binopVFXX | MUL | AVGR_U | Q15MULR_SAT_S
+syntax testop_vectype = | _VI testopVIXX
+syntax relop_vectype = | _VI relopVIXX | _VF relopVFXX
+syntax cvtop_vectype = | EXTEND | TRUNC_SAT | CONVERT | DEMOTE | PROMOTE
+
+
+var vvunop : unop_vvectype
+var vvbinop : binop_vvectype
+var vvternop : ternop_vvectype
+var vvtestop : testop_vvectype
+
+var vishiftop : shiftop_vectype
+var vunop : unop_vectype
+var vbinop : binop_vectype
+var vtestop : testop_vectype
+var vrelop : relop_vectype
+var vcvtop : cvtop_vectype
 
 
 ;;
@@ -262,7 +327,8 @@ var mo : memop
 ;; TODO: do c(numtype)?
 syntax c = nat
 syntax c_numtype = nat  ;; TODO
-syntax c_vectype = nat  ;; TODO
+syntax c_vectype = byte*;; TODO
+var cv : c_vectype
 
 syntax blocktype hint(desc "block type") =
   | _RESULT valtype?
@@ -304,6 +370,30 @@ syntax instr/numeric hint(desc "numeric instruction") = ...
   | CVTOP numtype cvtop numtype sx?  hint(show %.%#_#%#_#%)
   | ...
 
+syntax instr/vector hint(desc "vector instruction") = ...
+  | VVCONST vectype c_vectype                                        hint(show %.CONST %)
+  | VVUNOP vectype unop_vvectype                                     hint(show %.%)
+  | VVBINOP vectype binop_vvectype                                   hint(show %.%)
+  | VVTERNOP vectype ternop_vvectype                                 hint(show %.%)
+  | VVTESTOP vectype testop_vvectype                                 hint(show %.%)
+  | SWIZZLE shape
+  | SHUFFLE shape laneidx*
+  | SPLAT shape                                                     hint(show %.SPLAT)
+  | EXTRACT_LANE shape sx? laneidx                                  hint(show %.EXTRACT#_#LANE#_#% %)
+  | REPLACE_LANE shape laneidx                                      hint(show %.REPLACE#_#LANE %)
+  | VUNOP shape unop_vectype
+  | VBINOP shape binop_vectype
+  | VRELOP shape relop_vectype
+  | VISHIFTOP shape shiftop_vectype
+  | ALL_TRUE shape                                                  hint(show %.ALL_TRUE)
+  | BITMASK shape
+  | NARROW shape shape sx
+  | VCVTOP shape cvtop_vectype half? shape sx? zero
+  | EXTMUL_HALF shape half shape sx
+  | DOT shape shape sx
+  | EXTADD_PAIRWISE shape shape sx
+  | ...
+
 syntax instr/reference hint(desc "reference instruction") = ...
   | REF.NULL heaptype
   | REF.I31
@@ -359,15 +449,22 @@ syntax instr/table hint(desc "table instruction") = ...
   | ELEM.DROP elemidx
   | ...
 
+syntax vloadop =
+  | LOAD memarg | SHAPE packshape sx memarg | SPLAT nat memarg | ZERO nat memarg
+
 syntax instr/memory hint(desc "memory instruction") = ...
   | MEMORY.SIZE memidx
   | MEMORY.GROW memidx
   | MEMORY.FILL memidx
   | MEMORY.COPY memidx memidx
   | MEMORY.INIT memidx dataidx
   | DATA.DROP dataidx
-  | LOAD numtype (n _ sx)? memidx memop  hint(show %.LOAD % %)  hint(show %.LOAD#% % %)
-  | STORE numtype n? memidx memop        hint(show %.STORE % %) hint(show %.STORE#% % %)
+  | LOAD numtype (n _ sx)? memidx memarg  hint(show %.LOAD % %)  hint(show %.LOAD#% % %)
+  | STORE numtype n? memidx memarg        hint(show %.STORE % %) hint(show %.STORE#% % %)
+  | VLOAD vloadop memidx
+  | VLOAD_LANE n memidx memarg laneidx
+  | VSTORE memidx memarg
+  | VSTORE_LANE n memidx memarg laneidx
 
 syntax expr hint(desc "expression") =
   instr*

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

@@ -246,5 +246,5 @@ def $memsxt(externtype et*) = $memsxt(et*)  -- otherwise
 
 ;; Shorthands for Instructions
 
-def $memop0 : memop  hint(show )
-def $memop0 = {ALIGN 0, OFFSET 0}
+def $memarg0 : memarg  hint(show )
+def $memarg0 = {ALIGN 0, OFFSET 0}

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

@@ -28,13 +28,52 @@ def $cvtop(cvtop, numtype, numtype, sx?, c) : c_numtype* hint(show %#$_((%,%))^(
 def $wrap(nat, nat, c) : nat                             hint(show $wrap_((%,%))#((%)))
 def $ext(nat, nat, sx, c) : c_numtype                    hint(show $ext_((%,%))^(%)#((%)))
 
+def $ext128(nat, c) : c_vectype ;; TODO
+
 def $ibytes(N, iN(N)) : byte*         hint(show $bytes_(i#%,%))
 def $fbytes(N, fN(N)) : byte*         hint(show $bytes_(f#%,%))
 def $ntbytes(numtype, c) : byte*      hint(show $bytes_(%,%))
+def $vtbytes(vectype, c_vectype) : byte*   hint(show $bytes_(%,%))
 def $ztbytes(storagetype, c) : byte*  hint(show $bytes_(%,%))
 
 def $invibytes(N, byte*) : iN(N)
 def $invfbytes(N, byte*) : fN(N)
 
 def $invibytes(N, b*) = n  -- if $ibytes(N, n) = b*
 def $invfbytes(N, b*) = p  -- if $fbytes(N, p) = b*
+
+def $ine_128(c_vectype, c_vectype) : nat
+def $imul(N, c, c) : c_numtype
+def $iadd(N, c, c) : c_numtype
+def $lanes(shape, c_vectype) : nat*
+def $narrow(nat, nat, sx, nat) : nat
+def $ibits(nat, nat) : nat*
+def $ilt_s(nat, nat, nat) : nat
+
+def $vzero : c_vectype ;; TODO
+
+def $unpacked(shape) : numtype
+def $unpacked(pt X lns) = I32
+def $unpacked(nt X lns) = nt
+
+def $dim(shape) : lanesize
+def $dim(lnt X lns) = lns
+
+def $halfop(half, nat, nat) : nat
+def $halfop(LOW, i, j) = i
+def $halfop(HIGH, i, j) = j
+
+def $ishape(nat) : lanetype
+def $ishape(8) = I8
+def $ishape(16) = I16
+def $ishape(32) = I32
+def $ishape(64) = I64
+
+def $vvunop(unop_vvectype, vectype, c_vectype) : c_vectype                           hint(show %#_%#((%)))
+def $vvbinop(binop_vvectype, vectype, c_vectype, c_vectype) : c_vectype              hint(show %#_%#(%, %))
+def $vvternop(ternop_vvectype, vectype, c_vectype, c_vectype, c_vectype) : c_vectype hint(show %#_%#(%, %, %))
+def $vunop(unop_vectype, shape, c_vectype) : c_vectype
+def $vbinop(binop_vectype, shape, c_vectype, c_vectype) : c_vectype*
+def $vrelop(relop_vectype, shape, nat, nat) : nat
+def $vishiftop(shiftop_vectype, lanetype, nat, nat) : nat                            hint(show %#_%#(%, %))
+def $vcvtop(cvtop_vectype, nat, nat, sx?, nat) : nat                                 hint(show %#_%#(%, %, %))

spectec/spec/wasm-3.0/4-runtime.watsup

@@ -31,7 +31,9 @@ var aa : arrayaddr
 ;; Basic values
 
 syntax num hint(desc "number") =
-  | CONST numtype c_numtype
+  | CONST numtype c_numtype        hint(show %.CONST %)
+syntax vec hint(desc "vector") =
+  | VVCONST vectype c_vectype      hint(show %.CONST %)
 syntax addrref hint(desc "address reference") =
   | REF.I31_NUM u31                hint(show REF.I31 %)
   | REF.STRUCT_ADDR structaddr     hint(show REF.STRUCT %)
@@ -43,7 +45,7 @@ syntax ref hint(desc "reference") =
   | addrref
   | REF.NULL heaptype
 syntax val hint(desc "value") =
-  | num | ref
+  | num | vec | ref
 
 syntax result hint(desc "result") =
   | _VALS val* | TRAP

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

@@ -22,6 +22,7 @@ def $default(I32) = (CONST I32 0)
 def $default(I64) = (CONST I64 0)
 def $default(F32) = (CONST F32 0)
 def $default(F64) = (CONST F64 0)
+def $default(V128) = (VVCONST V128 0x00^128)
 def $default(REF NULL ht) = (REF.NULL ht)
 def $default(REF eps ht) = eps
 
@@ -128,8 +129,8 @@ def $with_mem(state, memidx, nat, nat, byte*) : state       hint(show %[.MEM[%].
 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[i] = %])
-def $with_array(state, arrayaddr, nat, fieldval) : state    hint(show %[.STRUCT[%].FIELD[i] = %])
+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_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