specification/wasm-3.0/5.4-binary.modules.spectec

;;
;; Binary Format of 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 =
  | qt:Brectype => TYPE qt

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 (REF.NULL ht)  -- if tt = at lim (REF NULL? ht)
  | 0x40 0x00 tt:Btabletype e:Bexpr => TABLE tt e

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 Belemkind : reftype hint(desc "element kind") =
  | 0x00 => REF NULL FUNC

grammar Belem : elem =
  | 0:Bu32 e_o:Bexpr y*:Blist(Bfuncidx) =>
      ELEM (REF FUNC) (REF.FUNC y)* (ACTIVE 0 e_o)
  | 1:Bu32 rt:Belemkind y*:Blist(Bfuncidx) =>
      ELEM rt (REF.FUNC y)* PASSIVE
  | 2:Bu32 x:Btableidx e:Bexpr rt:Belemkind y*:Blist(Bfuncidx) =>
      ELEM rt (REF.FUNC y)* (ACTIVE x e)
  | 3:Bu32 rt:Belemkind y*:Blist(Bfuncidx) =>
      ELEM rt (REF.FUNC y)* DECLARE
  | 4:Bu32 e_O:Bexpr e*:Blist(Bexpr) =>
      ELEM (REF NULL FUNC) e* (ACTIVE 0 e_O)
  | 5:Bu32 rt:Breftype e*:Blist(Bexpr) =>
      ELEM rt e* PASSIVE
  | 6:Bu32 x:Btableidx e_O:Bexpr e*:Blist(Bexpr) =>
      ELEM (REF NULL FUNC) e* (ACTIVE x e_O)
  | 7:Bu32 rt:Breftype e*:Blist(Bexpr) =>
      ELEM rt e* DECLARE

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


;; Code section

syntax code hint(macro none) = (local*, expr)

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

grammar Bfunc : code =
  | loc**:Blist(Blocals) e:Bexpr => ($concat_(local, loc**), e)
    -- if $(|$concat_(local, loc**)| < 2^32)

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 =
  | 0:Bu32 e:Bexpr b*:Blist(Bbyte) => DATA b* (ACTIVE 0 e)
  | 1:Bu32 b*:Blist(Bbyte) => DATA b* PASSIVE
  | 2:Bu32 x:Bmemidx e:Bexpr b*:Blist(Bbyte) => DATA b* (ACTIVE x e)

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


;; Data count section

grammar Bdatacnt : u32* hint(desc "data count") =
  | n:Bu32 => n

syntax nopt hint(show n?) = u32*  ;; HACK

grammar Bdatacntsec : u32? hint(desc "data count section") =
  | nopt:Bsection_(12, Bdatacnt) => $opt_(u32, nopt)


;; Tag section

grammar Btag : tag =
  | jt:Btagtype => TAG jt

grammar Btagsec : tag* hint(desc "tag section") =
  | tag*:Bsection_(13, Blist(Btag)) => tag*


;; Modules

grammar Bmagic : () = 0x00 0x61 0x73 0x6D => ()
grammar Bversion : () = 0x01 0x00 0x00 0x00 => ()
grammar Bmodule : module =
  | Bmagic Bversion
    Bcustomsec* type*:Btypesec
    Bcustomsec* import*:Bimportsec
    Bcustomsec* typeidx*:Bfuncsec
    Bcustomsec* table*:Btablesec
    Bcustomsec* mem*:Bmemsec
    Bcustomsec* tag*:Btagsec
    Bcustomsec* global*:Bglobalsec
    Bcustomsec* export*:Bexportsec
    Bcustomsec* start?:Bstartsec
    Bcustomsec* elem*:Belemsec
    Bcustomsec* n?:Bdatacntsec
    Bcustomsec* (local*, expr)*:Bcodesec
    Bcustomsec* data*:Bdatasec
    Bcustomsec* =>
      MODULE type* import* tag* global* mem* table* func* data* elem* start? export*
    ----
    -- (if n = |data*|)?
    -- if (n? =/= eps \/ $dataidx_funcs(func*) = eps)
    -- (if func = FUNC typeidx local* expr)*