specification/wasm-1.0/A-binary.spectec

;;
;; Auxiliaries
;;

;; Vectors

grammar Blist(grammar BX : el) : el* =
  | n:Bu32 (el:BX)^n => el^n



;;
;; Values
;;

;; Numbers

grammar Bbyte : byte = 0x00 | ... | 0xFF

grammar BuN(N) : uN(N) hint(show Bu#%) =
  | n:Bbyte                 => n                       -- if $(n < 2^7 /\ n < 2^N)
  | n:Bbyte m:BuN(($(N-7))) => $(2^7 * m + (n - 2^7))  -- if $(n >= 2^7 /\ N > 7)

grammar BsN(N) : sN(N) hint(show Bs#%) =
  | n:Bbyte                 => n                       -- if $(n < 2^6 /\ n < 2^(N-1))
  | n:Bbyte                 => $(n - 2^7)              -- if $(2^6 <= n < 2^7 /\ n >= 2^7 - 2^(N-1))
  | n:Bbyte i:BsN(($(N-7))) => $(2^7 * i + (n - 2^7))  -- if $(n >= 2^7 /\ N > 7)

grammar BiN(N) : iN(N) hint(show Bi#%) =
  | i:BsN(N)                => $inv_signed_(N, i)


grammar BfN(N) : fN(N) hint(show Bf#%) =
  | b*:Bbyte^(N/8)  => $inv_fbytes_(N, b*)


grammar Bu32 : u32 = BuN(32)
grammar Bu64 : u64 = BuN(64)

grammar Bi32 : i32 = BiN(32)
grammar Bi64 : i64 = BiN(64)

grammar Bf32 : f32 = BfN(32)
grammar Bf64 : f64 = BfN(64)


;; Names

var ch : char

;; def $utf8(char*) : byte*
def $utf8(ch) = b  -- if ch < U+0080 /\ ch = b
def $utf8(ch) = b_1 b_2  -- if U+0080 <= ch < U+0800 /\ ch = $(2^6*(b_1 - 0xC0) + (b_2 - 0x80))
def $utf8(ch) = b_1 b_2 b_3  -- if (U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000) /\ ch = $(2^12*(b_1 - 0xE0) + 2^6*(b_2 - 0x80) + (b_3 - 0x80))
def $utf8(ch) = b_1 b_2 b_3 b_4  -- if (U+10000 <= ch < U+11000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80))
def $utf8(ch*) = $concat_(byte, $utf8(ch)*)

grammar Bname : name =
  | b*:Blist(Bbyte) => name  -- if $utf8(name) = b*


;; Indices

grammar Btypeidx : typeidx = x:Bu32 => x
grammar Bfuncidx : funcidx = x:Bu32 => x
grammar Bglobalidx : globalidx = x:Bu32 => x
grammar Btableidx : tableidx = x:Bu32 => x
grammar Bmemidx : memidx = x:Bu32 => x
grammar Blocalidx : localidx = x:Bu32 => x
grammar Blabelidx : labelidx = x:Bu32 => x

grammar Bexternidx : externidx =
  | 0x00 x:Bfuncidx => FUNC x
  | 0x01 x:Btableidx => TABLE x
  | 0x02 x:Bmemidx => MEM x
  | 0x03 x:Bglobalidx => GLOBAL x


;;
;; Types
;;

;; Value types

grammar Bvaltype : valtype =
  | 0x7F => I32
  | 0x7E => I64
  | 0x7D => F32
  | 0x7C => F64


grammar Bresulttype : valtype* =
  | t*:Blist(Bvaltype) => t*


;; Type definitions

grammar Bfunctype : functype =
  | 0x60 t_1*:Bresulttype t_2*:Bresulttype => t_1* -> t_2*


;; External types

grammar Bmut : mut =
  | 0x00 => eps
  | 0x01 => MUT

grammar Blimits : limits =
  | 0x00 n:Bu32 => `[n .. eps]
  | 0x01 n:Bu32 m:Bu32 => `[n .. m]

grammar Bglobaltype : globaltype =
  | t:Bvaltype mut:Bmut => mut t

grammar Btabletype : tabletype =
  | 0x70 lim:Blimits => lim

grammar Bmemtype : memtype =
  | lim:Blimits => lim


grammar Bexterntype : externtype =
  | 0x00 ft:Bfunctype => FUNC ft  ;; TODO: typeidx
  | 0x01 tt:Btabletype => TABLE tt
  | 0x02 mt:Bmemtype => MEM mt
  | 0x03 gt:Bglobaltype => GLOBAL gt


;;
;; Instructions
;;

;; Block types

grammar Bblocktype : blocktype =
  | 0x40 => eps
  | t:Bvaltype => t


;; Control instructions

grammar Binstr/control : instr =
  | 0x00 => UNREACHABLE
  | 0x01 => NOP
  | 0x02 bt:Bblocktype (in:Binstr)* 0x0B => BLOCK bt in*
  | 0x03 bt:Bblocktype (in:Binstr)* 0x0B => LOOP bt in*
  | 0x04 bt:Bblocktype (in:Binstr)* 0x0B => IF bt in* ELSE eps
  | 0x04 bt:Bblocktype (in_1:Binstr)* 0x05 (in_2:Binstr)* 0x0B => IF bt in_1* ELSE in_2*
  | 0x0C l:Blabelidx => BR l
  | 0x0D l:Blabelidx => BR_IF l
  | 0x0E l*:Blist(Blabelidx) l_N:Blabelidx => BR_TABLE l* l_N
  | 0x0F => RETURN
  | 0x10 x:Bfuncidx => CALL x
  | 0x11 x:Btypeidx 0x00 => CALL_INDIRECT x
  | ...


;; Parametric instructions

grammar Binstr/parametric : instr = ...
  | 0x1A => DROP
  | 0x1B => SELECT
  | ...


;; Variable instructions

grammar Binstr/variable : instr = ...
  | 0x20 x:Blocalidx => LOCAL.GET x
  | 0x21 x:Blocalidx => LOCAL.SET x
  | 0x22 x:Blocalidx => LOCAL.TEE x
  | 0x23 x:Bglobalidx => GLOBAL.GET x
  | 0x24 x:Bglobalidx => GLOBAL.SET x
  | ...


;; Memory instructions

grammar Bmemarg : memarg =
  | n:Bu32 m:Bu32 => {ALIGN n, OFFSET m}

grammar Binstr/memory : instr = ...
  | 0x28 ao:Bmemarg => LOAD I32 ao
  | 0x29 ao:Bmemarg => LOAD I64 ao
  | 0x2A ao:Bmemarg => LOAD F32 ao
  | 0x2B ao:Bmemarg => LOAD F64 ao
  | 0x2C ao:Bmemarg => LOAD I32 (8 _ S) ao
  | 0x2D ao:Bmemarg => LOAD I32 (8 _ U) ao
  | 0x2E ao:Bmemarg => LOAD I32 (16 _ S) ao
  | 0x2F ao:Bmemarg => LOAD I32 (16 _ U) ao
  | 0x30 ao:Bmemarg => LOAD I64 (8 _ S) ao
  | 0x31 ao:Bmemarg => LOAD I64 (8 _ U) ao
  | 0x32 ao:Bmemarg => LOAD I64 (16 _ S) ao
  | 0x33 ao:Bmemarg => LOAD I64 (16 _ U) ao
  | 0x34 ao:Bmemarg => LOAD I64 (32 _ S) ao
  | 0x35 ao:Bmemarg => LOAD I64 (32 _ U) ao
  | 0x36 ao:Bmemarg => STORE I32 ao
  | 0x37 ao:Bmemarg => STORE I64 ao
  | 0x38 ao:Bmemarg => STORE F32 ao
  | 0x39 ao:Bmemarg => STORE F64 ao
  | 0x3A ao:Bmemarg => STORE I32 8 ao
  | 0x3B ao:Bmemarg => STORE I32 16 ao
  | 0x3C ao:Bmemarg => STORE I64 8 ao
  | 0x3D ao:Bmemarg => STORE I64 16 ao
  | 0x3E ao:Bmemarg => STORE I64 32 ao
  | 0x3F 0x00 => MEMORY.SIZE
  | 0x40 0x00 => MEMORY.GROW
  | ...



;; Numeric instructions

grammar Binstr/numeric-const : instr = ...
  | 0x41 i:Bi32 => CONST I32 i
  | 0x42 i:Bi64 => CONST I64 i
  | 0x43 p:Bf32 => CONST F32 p
  | 0x44 p:Bf64 => CONST F64 p
  | ...

grammar Binstr/numeric-test-i32 : instr = ...
  | 0x45 => TESTOP I32 EQZ
  | ...

grammar Binstr/numeric-rel-i32 : instr = ...
  | 0x46 => RELOP I32 EQ
  | 0x47 => RELOP I32 NE
  | 0x48 => RELOP I32 (LT S)
  | 0x49 => RELOP I32 (LT U)
  | 0x4A => RELOP I32 (GT S)
  | 0x4B => RELOP I32 (GT U)
  | 0x4C => RELOP I32 (LE S)
  | 0x4D => RELOP I32 (LE U)
  | 0x4E => RELOP I32 (GE S)
  | 0x4F => RELOP I32 (GE U)
  | ...

grammar Binstr/numeric-test-i64 : instr = ...
  | 0x50 => TESTOP I64 EQZ
  | ...

grammar Binstr/numeric-rel-i64 : instr = ...
  | 0x51 => RELOP I64 EQ
  | 0x52 => RELOP I64 NE
  | 0x53 => RELOP I64 (LT S)
  | 0x54 => RELOP I64 (LT U)
  | 0x55 => RELOP I64 (GT S)
  | 0x56 => RELOP I64 (GT U)
  | 0x57 => RELOP I64 (LE S)
  | 0x58 => RELOP I64 (LE U)
  | 0x59 => RELOP I64 (GE S)
  | 0x5A => RELOP I64 (GE U)
  | ...

grammar Binstr/numeric-rel-f32 : instr = ...
  | 0x5B => RELOP F32 EQ
  | 0x5C => RELOP F32 NE
  | 0x5D => RELOP F32 LT
  | 0x5E => RELOP F32 GT
  | 0x5F => RELOP F32 LE
  | 0x60 => RELOP F32 GE
  | ...

grammar Binstr/numeric-rel-f64 : instr = ...
  | 0x61 => RELOP F64 EQ
  | 0x62 => RELOP F64 NE
  | 0x63 => RELOP F64 LT
  | 0x64 => RELOP F64 GT
  | 0x65 => RELOP F64 LE
  | 0x66 => RELOP F64 GE
  | ...

grammar Binstr/numeric-un-i32 : instr = ...
  | 0x67 => UNOP I32 CLZ
  | 0x68 => UNOP I32 CTZ
  | 0x69 => UNOP I32 POPCNT
  | ...

grammar Binstr/numeric-bin-i32 : instr = ...
  | 0x6A => BINOP I32 ADD
  | 0x6B => BINOP I32 SUB
  | 0x6C => BINOP I32 MUL
  | 0x6D => BINOP I32 (DIV S)
  | 0x6E => BINOP I32 (DIV U)
  | 0x6F => BINOP I32 (REM S)
  | 0x70 => BINOP I32 (REM U)
  | 0x71 => BINOP I32 AND
  | 0x72 => BINOP I32 OR
  | 0x73 => BINOP I32 XOR
  | 0x74 => BINOP I32 SHL
  | 0x75 => BINOP I32 (SHR S)
  | 0x76 => BINOP I32 (SHR U)
  | 0x77 => BINOP I32 ROTL
  | 0x78 => BINOP I32 ROTR
  | ...

grammar Binstr/numeric-un-i64 : instr = ...
  | 0x79 => UNOP I64 CLZ
  | 0x7A => UNOP I64 CTZ
  | 0x7B => UNOP I64 POPCNT
  | ...

grammar Binstr/numeric-bin-i64 : instr = ...
  | 0x7C => BINOP I64 ADD
  | 0x7D => BINOP I64 SUB
  | 0x7E => BINOP I64 MUL
  | 0x7F => BINOP I64 (DIV S)
  | 0x80 => BINOP I64 (DIV U)
  | 0x81 => BINOP I64 (REM S)
  | 0x82 => BINOP I64 (REM U)
  | 0x83 => BINOP I64 AND
  | 0x84 => BINOP I64 OR
  | 0x85 => BINOP I64 XOR
  | 0x86 => BINOP I64 SHL
  | 0x87 => BINOP I64 (SHR S)
  | 0x88 => BINOP I64 (SHR U)
  | 0x89 => BINOP I64 ROTL
  | 0x8A => BINOP I64 ROTR
  | ...

grammar Binstr/numeric-un-f32 : instr = ...
  | 0x8B => UNOP F32 ABS
  | 0x8C => UNOP F32 NEG
  | 0x8D => UNOP F32 CEIL
  | 0x8E => UNOP F32 FLOOR
  | 0x8F => UNOP F32 TRUNC
  | 0x90 => UNOP F32 NEAREST
  | 0x91 => UNOP F32 SQRT
  | ...

grammar Binstr/numeric-bin-f32 : instr = ...
  | 0x92 => BINOP F32 ADD
  | 0x93 => BINOP F32 SUB
  | 0x94 => BINOP F32 MUL
  | 0x95 => BINOP F32 DIV
  | 0x96 => BINOP F32 MIN
  | 0x97 => BINOP F32 MAX
  | 0x98 => BINOP F32 COPYSIGN
  | ...

grammar Binstr/numeric-un-f64 : instr = ...
  | 0x99 => UNOP F64 ABS
  | 0x9A => UNOP F64 NEG
  | 0x9B => UNOP F64 CEIL
  | 0x9C => UNOP F64 FLOOR
  | 0x9D => UNOP F64 TRUNC
  | 0x9E => UNOP F64 NEAREST
  | 0x9F => UNOP F64 SQRT
  | ...

grammar Binstr/numeric-bin-f64 : instr = ...
  | 0xA0 => BINOP F64 ADD
  | 0xA1 => BINOP F64 SUB
  | 0xA2 => BINOP F64 MUL
  | 0xA3 => BINOP F64 DIV
  | 0xA4 => BINOP F64 MIN
  | 0xA5 => BINOP F64 MAX
  | 0xA6 => BINOP F64 COPYSIGN
  | ...

grammar Binstr/numeric-cvt : instr = ...
  | 0xA7 => CVTOP I32 I64 WRAP
  | 0xA8 => CVTOP I32 F32 (TRUNC S)
  | 0xA9 => CVTOP I32 F32 (TRUNC U)
  | 0xAA => CVTOP I32 F64 (TRUNC S)
  | 0xAB => CVTOP I32 F64 (TRUNC U)
  | 0xAC => CVTOP I64 I32 (EXTEND S)
  | 0xAD => CVTOP I64 I32 (EXTEND U)
  | 0xAE => CVTOP I64 F32 (TRUNC S)
  | 0xAF => CVTOP I64 F32 (TRUNC U)
  | 0xB0 => CVTOP I64 F64 (TRUNC S)
  | 0xB1 => CVTOP I64 F64 (TRUNC U)
  | 0xB2 => CVTOP F32 I32 (CONVERT S)
  | 0xB3 => CVTOP F32 I32 (CONVERT U)
  | 0xB4 => CVTOP F32 I64 (CONVERT S)
  | 0xB5 => CVTOP F32 I64 (CONVERT U)
  | 0xB6 => CVTOP F32 F64 DEMOTE
  | 0xB7 => CVTOP F64 I32 (CONVERT S)
  | 0xB8 => CVTOP F64 I32 (CONVERT U)
  | 0xB9 => CVTOP F64 I64 (CONVERT S)
  | 0xBA => CVTOP F64 I64 (CONVERT U)
  | 0xBB => CVTOP F32 F64 PROMOTE
  | 0xBC => CVTOP I32 F32 REINTERPRET
  | 0xBD => CVTOP I64 F64 REINTERPRET
  | 0xBE => CVTOP F32 I32 REINTERPRET
  | 0xBF => CVTOP F64 I64 REINTERPRET


;; Expressions

grammar Bexpr : expr =
  | (in:Binstr)* 0x0B => in*



;;
;; Modules
;;

;; Sections

var len : nat

grammar Bsection_(N, grammar BX : en*) : en*  hint(desc "section") =
  | N:Bbyte len:Bu32 en*:BX => en*  -- if len = ||BX||
  | eps => eps


;; Custom sections

grammar Bcustom : ()* hint(desc "custom data") =
  | Bname Bbyte* => ()

grammar Bcustomsec : () hint(desc "custom section") =
  | Bsection_(0, Bcustom) => ()


;; Type section

grammar Btype : type =
  | ft:Bfunctype => TYPE ft

grammar Btypesec : type* hint(desc "type section") =
  | ty*:Bsection_(1, Blist(Btype)) => ty*


;; Import section

grammar Bimport : import =
  | nm_1:Bname nm_2:Bname xt:Bexterntype => IMPORT nm_1 nm_2 xt

grammar Bimportsec : import* hint(desc "import section") =
  | im*:Bsection_(2, Blist(Bimport)) => im*


;; Function section

grammar Bfuncsec : typeidx* hint(desc "function section") =
  | x*:Bsection_(3, Blist(Btypeidx)) => x*


;; Table section

grammar Btable : table =
  | tt:Btabletype => TABLE tt

grammar Btablesec : table* hint(desc "table section") =
  | tab*:Bsection_(4, Blist(Btable)) => tab*


;; Memory section

grammar Bmem : mem =
  | mt:Bmemtype => MEMORY mt

grammar Bmemsec : mem* hint(desc "memory section") =
  | mem*:Bsection_(5, Blist(Bmem)) => mem*


;; Global section

grammar Bglobal : global =
  | gt:Bglobaltype e:Bexpr => GLOBAL gt e

grammar Bglobalsec : global* hint(desc "global section") =
  | glob*:Bsection_(6, Blist(Bglobal)) => glob*


;; Export section

grammar Bexport : export =
  | nm:Bname xx:Bexternidx => EXPORT nm xx

grammar Bexportsec : export* hint(desc "export section") =
  | ex*:Bsection_(7, Blist(Bexport)) => ex*


;; Start section

grammar Bstart : start* =
  | x:Bfuncidx => (START x)

syntax startopt hint(show start?) = start*  ;; HACK

grammar Bstartsec : start? hint(desc "start section") =
  | startopt:Bsection_(8, Bstart) => $opt_(start, startopt)


;; Element section

grammar Belem : elem =
  | 0x00 e:Bexpr x*:Blist(Bfuncidx) => ELEM e x*

grammar Belemsec : elem* hint(desc "element section") =
  | elem*:Bsection_(9, Blist(Belem)) => elem*


;; Code section

syntax code = (local*, expr)

grammar Blocals : local* hint(desc "local") =
  | n:Bu32 t:Bvaltype => (LOCAL t)^n

grammar Bfunc : code =
  | local**:Blist(Blocals) expr:Bexpr => ($concat_(local, local**), expr)

grammar Bcode : code =
  | len:Bu32 code:Bfunc => code  -- if len = ||Bfunc||

grammar Bcodesec : code* hint(desc "code section") =
  | code*:Bsection_(10, Blist(Bcode)) => code*


;; Data section

grammar Bdata : data =
  | 0x00 e:Bexpr b*:Blist(Bbyte) => DATA e b*

grammar Bdatasec : data* hint(desc "data section") =
  | data*:Bsection_(11, Blist(Bdata)) => data*


;; Modules

grammar Bmodule : module =
  | 0x00 0x61 0x73 0x6D 1:Bu32
    Bcustomsec* type*:Btypesec
    Bcustomsec* import*:Bimportsec
    Bcustomsec* typeidx*:Bfuncsec
    Bcustomsec* table*:Btablesec
    Bcustomsec* mem*:Bmemsec
    Bcustomsec* global*:Bglobalsec
    Bcustomsec* export*:Bexportsec
    Bcustomsec* start?:Bstartsec
    Bcustomsec* elem*:Belemsec
    Bcustomsec* (local*, expr)*:Bcodesec
    Bcustomsec* data*:Bdatasec
    Bcustomsec* =>
      MODULE type* import* func* global* table* mem* elem* data* start? export*
    -- (if func = FUNC typeidx local* expr)*