From 4fdefcec698ee62f3f44edf18ee775bd1e8c6330 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Wed, 18 Mar 2026 11:46:17 +0200 Subject: [PATCH 1/3] wasm.md: add new HelperInstr sort --- .../src/pykwasm/kdist/wasm-semantics/wasm.md | 152 +++++++++--------- 1 file changed, 78 insertions(+), 74 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index 9ae1404df..f399d3956 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -165,10 +165,13 @@ Internal Syntax module WASM-INTERNAL-SYNTAX imports WASM-DATA-INTERNAL-SYNTAX - syntax Instr ::= "init_local" Int Val - | "init_locals" ValStack - | "#init_locals" Int ValStack - // -------------------------------------------- + syntax Instr ::= HelperInstr + // ---------------------------- + + syntax HelperInstr ::= "init_local" Int Val + | "init_locals" ValStack + | "#init_locals" Int ValStack + // -------------------------------------------------- syntax Int ::= #pageSize() [function, total] syntax Int ::= #maxMemorySize() [function, total] @@ -492,8 +495,8 @@ It simply executes the block then records a label with an empty continuation. syntax BlockMetaData ::= OptionalInt // ------------------------------------ - syntax Instr ::= #block(VecType, Instrs, BlockMetaData) [symbol(aBlock)] - // -------------------------------------------------------------------------------- + syntax HelperInstr ::= #block(VecType, Instrs, BlockMetaData) [symbol(aBlock)] + // ------------------------------------------------------------------------------ rule #block(VECTYP, IS, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... VALSTACK => .ValStack ``` @@ -504,16 +507,16 @@ Upon reaching it, the label itself is executed. Note that, unlike in the WebAssembly specification document, we do not need the special "context" operator here because the value and instruction stacks are separate. ```k - syntax Instr ::= #br( Int ) [symbol(aBr)] - // ------------------------------------------------- + syntax HelperInstr ::= #br( Int ) [symbol(aBr)] + // ----------------------------------------------- rule #br(_IDX) ~> (_S:Stmt => .K) ... rule #br(0 ) ~> label [ TYPES ] { IS } VALSTACK' => sequenceInstrs(IS) ... VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' rule #br(N:Int) ~> _L:Label => #br(N -Int 1) ... requires N >Int 0 - syntax Instr ::= "#br_if" "(" Int ")" [symbol(aBr_if)] - // -------------------------------------------------------------- + syntax HelperInstr ::= "#br_if" "(" Int ")" [symbol(aBr_if)] + // ------------------------------------------------------------ rule #br_if(IDX) => #br(IDX) ... VAL : VALSTACK => VALSTACK requires VAL =/=Int 0 @@ -521,8 +524,8 @@ Note that, unlike in the WebAssembly specification document, we do not need the VAL : VALSTACK => VALSTACK requires VAL ==Int 0 - syntax Instr ::= "#br_table" "(" Ints ")" [symbol(aBr_table)] - // --------------------------------------------------------------------- + syntax HelperInstr ::= "#br_table" "(" Ints ")" [symbol(aBr_table)] + // ------------------------------------------------------------------- rule #br_table(ES) => #br(#getInts(ES, minInt(VAL, #lenInts(ES) -Int 1))) ... VAL : VALSTACK => VALSTACK requires 0 <=Int VAL @@ -536,8 +539,8 @@ Note that, unlike in the WebAssembly specification document, we do not need the Finally, we have the conditional and loop instructions. ```k - syntax Instr ::= #if( VecType, then : Instrs, else : Instrs, blockInfo: BlockMetaData) [symbol(aIf)] - // ------------------------------------------------------------------------------------------------------------ + syntax HelperInstr ::= #if( VecType, then : Instrs, else : Instrs, blockInfo: BlockMetaData) [symbol(aIf)] + // ---------------------------------------------------------------------------------------------------------- rule #if(VECTYP, IS, _, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... < i32 > VAL : VALSTACK => VALSTACK requires VAL =/=Int 0 @@ -546,8 +549,8 @@ Finally, we have the conditional and loop instructions. < i32 > VAL : VALSTACK => VALSTACK requires VAL ==Int 0 - syntax Instr ::= #loop(VecType, Instrs, BlockMetaData) [symbol(aLoop)] - // ------------------------------------------------------------------------------ + syntax HelperInstr ::= #loop(VecType, Instrs, BlockMetaData) [symbol(aLoop)] + // ---------------------------------------------------------------------------- rule #loop(VECTYP, IS, BLOCKMETA) => sequenceInstrs(IS) ~> label VECTYP { #loop(VECTYP, IS, BLOCKMETA) } VALSTACK ... VALSTACK => .ValStack ``` @@ -576,10 +579,10 @@ The various `init_local` variants assist in setting up the `locals` cell. The `*_local` instructions are defined here. ```k - syntax Instr ::= "#local.get" "(" Int ")" [symbol(aLocal.get)] - | "#local.set" "(" Int ")" [symbol(aLocal.set)] - | "#local.tee" "(" Int ")" [symbol(aLocal.tee)] - // ---------------------------------------------------------------------- + syntax HelperInstr ::= "#local.get" "(" Int ")" [symbol(aLocal.get)] + | "#local.set" "(" Int ")" [symbol(aLocal.set)] + | "#local.tee" "(" Int ")" [symbol(aLocal.tee)] + // -------------------------------------------------------------------- rule #local.get(I) => .K ... VALSTACK => VALUE : VALSTACK ... I |-> VALUE ... @@ -644,9 +647,9 @@ The importing and exporting parts of specifications are dealt with in the respec The `get` and `set` instructions read and write globals. ```k - syntax Instr ::= "#global.get" "(" Int ")" [symbol(aGlobal.get)] - | "#global.set" "(" Int ")" [symbol(aGlobal.set)] - // ------------------------------------------------------------------------ + syntax HelperInstr ::= "#global.get" "(" Int ")" [symbol(aGlobal.get)] + | "#global.set" "(" Int ")" [symbol(aGlobal.set)] + // ---------------------------------------------------------------------- rule #global.get(IDX) => .K ... VALSTACK => VALUE : VALSTACK CUR @@ -685,15 +688,15 @@ The `get` and `set` instructions read and write globals. - [Execution](https://webassembly.github.io/spec/core/exec/instructions.html#table-instructions) ```k - syntax Instr ::= "#table.get" "(" Int ")" [symbol(aTable.get)] - | "#table.set" "(" Int ")" [symbol(aTable.set)] - | "#table.size" "(" Int ")" [symbol(aTable.size)] - | "#table.grow" "(" Int ")" [symbol(aTable.grow)] - | "#table.fill" "(" Int ")" [symbol(aTable.fill)] - | "#table.copy" "(" Int "," Int ")" [symbol(aTable.copy)] - | "#table.init" "(" Int "," Int ")" [symbol(aTable.init)] - | "#elem.drop" "(" Int ")" [symbol(aElem.drop)] - // --------------------------------------------------------------------------------- + syntax HelperInstr ::= "#table.get" "(" Int ")" [symbol(aTable.get)] + | "#table.set" "(" Int ")" [symbol(aTable.set)] + | "#table.size" "(" Int ")" [symbol(aTable.size)] + | "#table.grow" "(" Int ")" [symbol(aTable.grow)] + | "#table.fill" "(" Int ")" [symbol(aTable.fill)] + | "#table.copy" "(" Int "," Int ")" [symbol(aTable.copy)] + | "#table.init" "(" Int "," Int ")" [symbol(aTable.init)] + | "#elem.drop" "(" Int ")" [symbol(aElem.drop)] + // ------------------------------------------------------------------------------ ``` #### `table.get` @@ -709,7 +712,8 @@ The `get` and `set` instructions read and write globals. ... - syntax Instr ::= #tableGet( addr: Int, index: Int) + syntax HelperInstr ::= #tableGet( addr: Int, index: Int) + // -------------------------------------------------------- rule [tableGet]: #tableGet( TADDR, I) => getRefOrNull(TDATA, I) ... @@ -734,8 +738,8 @@ The `get` and `set` instructions read and write globals. #### `table.set` ```k - syntax Instr ::= #tableSet( addr: Int , val: RefVal , idx: Int ) - // ----------------------------------------- + syntax HelperInstr ::= #tableSet( addr: Int , val: RefVal , idx: Int ) + // ---------------------------------------------------------------------- rule [table.set]: #table.set( TID ) => #tableSet(TADDR, VAL, I) ... @@ -851,8 +855,8 @@ The `get` and `set` instructions read and write globals. ... - syntax Instr ::= #tableFill(Int, Int, RefVal, Int) - // ------------------------------------------------------ + syntax HelperInstr ::= #tableFill(Int, Int, RefVal, Int) + // -------------------------------------------------------- rule [tableFill-zero]: #tableFill(_, 0, _, _) => .K ... @@ -900,8 +904,8 @@ The `get` and `set` instructions read and write globals. ... - syntax Instr ::= #tableCopy(tix: Int, tiy: Int, n: Int, s: Int, d: Int) - // ----------------------------------------------------------------------- + syntax HelperInstr ::= #tableCopy(tix: Int, tiy: Int, n: Int, s: Int, d: Int) + // ----------------------------------------------------------------------------- rule [tableCopy-zero]: #tableCopy(_, _, 0, _, _) => .K ... @@ -956,8 +960,8 @@ The `get` and `set` instructions read and write globals. ... - syntax Instr ::= #tableInit(tidx: Int, n: Int, d: Int, es: ListRef) - // ---------------------------------------------------- + syntax HelperInstr ::= #tableInit(tidx: Int, n: Int, d: Int, es: ListRef) + // ------------------------------------------------------------------------- rule [tableInit-done]: #tableInit(_, 0, _, _) => .K ... @@ -994,8 +998,8 @@ The `get` and `set` instructions read and write globals. #### Misc ```k - syntax Instr ::= #tableCheckSizeGTE(addr: Int, n: Int) - // ------------------------------------------------------- + syntax HelperInstr ::= #tableCheckSizeGTE(addr: Int, n: Int) + // ------------------------------------------------------------ rule [tableCheckSizeGTE-pass]: #tableCheckSizeGTE(ADDR, N) => .K ... @@ -1010,8 +1014,8 @@ The `get` and `set` instructions read and write globals. [owise] - syntax Instr ::= #elemCheckSizeGTE(addr: Int, n: Int) - // ------------------------------------------------------- + syntax HelperInstr ::= #elemCheckSizeGTE(addr: Int, n: Int) + // ----------------------------------------------------------- rule [elemCheckSizeGTE-pass]: #elemCheckSizeGTE(ADDR, N) => .K ... @@ -1032,9 +1036,9 @@ The `get` and `set` instructions read and write globals. - [Execution](https://webassembly.github.io/spec/core/exec/instructions.html#reference-instructions) ```k - syntax Instr ::= "#ref.is_null" [symbol(aRef.is_null)] - | "#ref.func" "(" Int ")" [symbol(aRef.func)] - // ------------------------------------------------------------------------ + syntax HelperInstr ::= "#ref.is_null" [symbol(aRef.is_null)] + | "#ref.func" "(" Int ")" [symbol(aRef.func)] + // ------------------------------------------------------------------ rule [ref.null.func]: ref.null func => null ... @@ -1230,8 +1234,8 @@ The `#take` function will return the parameter stack in the reversed order, then `call funcidx` and `call_indirect tableidx typeuse` are 2 control instructions that invoke a function in the current frame. ```k - syntax Instr ::= #call(Int) [symbol(aCall)] - // --------------------------------------------------- + syntax HelperInstr ::= #call(Int) [symbol(aCall)] + // ------------------------------------------------- rule #call(IDX) => ( invoke FUNCADDRS {{ IDX }} orDefault 0 ) ... CUR @@ -1243,8 +1247,8 @@ The `#take` function will return the parameter stack in the reversed order, then ``` ```k - syntax Instr ::= "#call_indirect" "(" Int "," TypeUse ")" [symbol(aCall_indirect)] - // ------------------------------------------------------------------------------ + syntax HelperInstr ::= "#call_indirect" "(" Int "," TypeUse ")" [symbol(aCall_indirect)] + // ---------------------------------------------------------------------------------------- ``` TODO: This is kept for compatibility with the text format. @@ -1276,8 +1280,8 @@ The types need to be inserted at the definitions level, if a previously undeclar - syntax Instr ::= #callIndirect(RefVal, FuncType) - // ------------------------------------------ + syntax HelperInstr ::= #callIndirect(RefVal, FuncType) + // ------------------------------------------------------ rule [callIndirect-invoke]: #callIndirect( FADDR, ETYPE) => ( invoke FADDR ) ... @@ -1406,12 +1410,12 @@ The value is encoded as bytes and stored at the "effective address", which is th [Store Instructions](https://webassembly.github.io/spec/core/exec/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-xref-syntax-instructions-syntax-memarg-mathit-memarg-and-t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-n-xref-syntax-instructions-syntax-memarg-mathit-memarg) ```k - syntax Instr ::= #store(ValType, StoreOp, offset : Int) [symbol(aStore)] - | IValType "." StoreOp Int Int - // | FValType "." StoreOp Int Float - | "store" "{" IWidth Int Number "}" - | "store" "{" IWidth Int Number Int "}" - // ----------------------------------------------- + syntax HelperInstr ::= #store(ValType, StoreOp, offset : Int) [symbol(aStore)] + | IValType "." StoreOp Int Int + // | FValType "." StoreOp Int Float + | "store" "{" IWidth Int Number "}" + | "store" "{" IWidth Int Number Int "}" + // ------------------------------------------------------------ rule #store(ITYPE:IValType, SOP, OFFSET) => ITYPE . SOP (IDX +Int OFFSET) VAL ... < ITYPE > VAL : < i32 > IDX : VALSTACK => VALSTACK @@ -1459,12 +1463,12 @@ Sort `Signedness` is defined in module `BYTES`. [Load Instructions](https://webassembly.github.io/spec/core/exec/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-xref-syntax-instructions-syntax-memarg-mathit-memarg-and-t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg) ```k - syntax Instr ::= #load(ValType, LoadOp, offset : Int) [symbol(aLoad)] - | "load" "{" IValType IWidth Int Signedness"}" - | "load" "{" IValType IWidth Int Signedness Int"}" - | "load" "{" IValType IWidth Int Signedness SparseBytes"}" - | IValType "." LoadOp Int - // ---------------------------------------- + syntax HelperInstr ::= #load(ValType, LoadOp, offset : Int) [symbol(aLoad)] + | "load" "{" IValType IWidth Int Signedness"}" + | "load" "{" IValType IWidth Int Signedness Int"}" + | "load" "{" IValType IWidth Int Signedness SparseBytes"}" + | IValType "." LoadOp Int + // ---------------------------------------------- rule #load(ITYPE:IValType, LOP, OFFSET) => ITYPE . LOP (IDX +Int OFFSET) ... < i32 > IDX : VALSTACK => VALSTACK @@ -1538,8 +1542,8 @@ By setting the `` field in the configuration to `true [Memory Grow](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-grow) ```k - syntax Instr ::= "grow" Int - // --------------------------- + syntax HelperInstr ::= "grow" Int + // --------------------------------- rule memory.grow => grow N ... < i32 > N : VALSTACK => VALSTACK @@ -1598,9 +1602,9 @@ The spec states that this is really a sequence of `i32.store8` instructions, but [Memory Fill](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-fill) ```k - syntax Instr ::= "fillTrap" Int Int Int - | "fill" Int Int Int - // --------------------------------------- + syntax HelperInstr ::= "fillTrap" Int Int Int + | "fill" Int Int Int + // --------------------------------------------- rule memory.fill => fillTrap N VAL D ... < i32 > N : < i32 > VAL : < i32 > D : VALSTACK => VALSTACK @@ -1644,9 +1648,9 @@ performing a series of load and store operations as stated in the spec. [Memory Copy](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-copy) ```k - syntax Instr ::= "copyTrap" Int Int Int - | "copy" Int Int Int - // --------------------------------------- + syntax HelperInstr ::= "copyTrap" Int Int Int + | "copy" Int Int Int + // ----------------------------------------- rule memory.copy => copyTrap N S D ... < i32 > N : < i32 > S : < i32 > D : VALSTACK => VALSTACK From 7dbad5256f481da5c5a44322aa1e11dd982ab85c Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 18 Mar 2026 09:51:43 +0000 Subject: [PATCH 2/3] Set Version: 0.1.147 --- package/version | 2 +- pykwasm/pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 22a9c16f5..03bb3b2a8 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.146 +0.1.147 diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index a5086deed..1303e33b6 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "pykwasm" -version = "0.1.146" +version = "0.1.147" description = "" readme = "README.md" requires-python = "~=3.10" From d90e8e662339ad1f09d3f1c172cf956e00420d84 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20V=C4=83caru?= <16517508+anvacaru@users.noreply.github.com> Date: Mon, 23 Mar 2026 15:23:58 +0200 Subject: [PATCH 3/3] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Burak Bilge Yalçınkaya --- .../src/pykwasm/kdist/wasm-semantics/wasm.md | 78 +++++++++---------- 1 file changed, 39 insertions(+), 39 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index f399d3956..8470abaff 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -495,8 +495,8 @@ It simply executes the block then records a label with an empty continuation. syntax BlockMetaData ::= OptionalInt // ------------------------------------ - syntax HelperInstr ::= #block(VecType, Instrs, BlockMetaData) [symbol(aBlock)] - // ------------------------------------------------------------------------------ + syntax Instr ::= #block(VecType, Instrs, BlockMetaData) [symbol(aBlock)] + // ------------------------------------------------------------------------ rule #block(VECTYP, IS, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... VALSTACK => .ValStack ``` @@ -507,16 +507,16 @@ Upon reaching it, the label itself is executed. Note that, unlike in the WebAssembly specification document, we do not need the special "context" operator here because the value and instruction stacks are separate. ```k - syntax HelperInstr ::= #br( Int ) [symbol(aBr)] - // ----------------------------------------------- + syntax Instr ::= #br( Int ) [symbol(aBr)] + // ----------------------------------------- rule #br(_IDX) ~> (_S:Stmt => .K) ... rule #br(0 ) ~> label [ TYPES ] { IS } VALSTACK' => sequenceInstrs(IS) ... VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' rule #br(N:Int) ~> _L:Label => #br(N -Int 1) ... requires N >Int 0 - syntax HelperInstr ::= "#br_if" "(" Int ")" [symbol(aBr_if)] - // ------------------------------------------------------------ + syntax Instr ::= "#br_if" "(" Int ")" [symbol(aBr_if)] + // ------------------------------------------------------ rule #br_if(IDX) => #br(IDX) ... VAL : VALSTACK => VALSTACK requires VAL =/=Int 0 @@ -524,8 +524,8 @@ Note that, unlike in the WebAssembly specification document, we do not need the VAL : VALSTACK => VALSTACK requires VAL ==Int 0 - syntax HelperInstr ::= "#br_table" "(" Ints ")" [symbol(aBr_table)] - // ------------------------------------------------------------------- + syntax Instr ::= "#br_table" "(" Ints ")" [symbol(aBr_table)] + // ------------------------------------------------------------- rule #br_table(ES) => #br(#getInts(ES, minInt(VAL, #lenInts(ES) -Int 1))) ... VAL : VALSTACK => VALSTACK requires 0 <=Int VAL @@ -539,8 +539,8 @@ Note that, unlike in the WebAssembly specification document, we do not need the Finally, we have the conditional and loop instructions. ```k - syntax HelperInstr ::= #if( VecType, then : Instrs, else : Instrs, blockInfo: BlockMetaData) [symbol(aIf)] - // ---------------------------------------------------------------------------------------------------------- + syntax Instr ::= #if( VecType, then : Instrs, else : Instrs, blockInfo: BlockMetaData) [symbol(aIf)] + // ---------------------------------------------------------------------------------------------------- rule #if(VECTYP, IS, _, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... < i32 > VAL : VALSTACK => VALSTACK requires VAL =/=Int 0 @@ -549,8 +549,8 @@ Finally, we have the conditional and loop instructions. < i32 > VAL : VALSTACK => VALSTACK requires VAL ==Int 0 - syntax HelperInstr ::= #loop(VecType, Instrs, BlockMetaData) [symbol(aLoop)] - // ---------------------------------------------------------------------------- + syntax Instr ::= #loop(VecType, Instrs, BlockMetaData) [symbol(aLoop)] + // ---------------------------------------------------------------------- rule #loop(VECTYP, IS, BLOCKMETA) => sequenceInstrs(IS) ~> label VECTYP { #loop(VECTYP, IS, BLOCKMETA) } VALSTACK ... VALSTACK => .ValStack ``` @@ -579,10 +579,10 @@ The various `init_local` variants assist in setting up the `locals` cell. The `*_local` instructions are defined here. ```k - syntax HelperInstr ::= "#local.get" "(" Int ")" [symbol(aLocal.get)] - | "#local.set" "(" Int ")" [symbol(aLocal.set)] - | "#local.tee" "(" Int ")" [symbol(aLocal.tee)] - // -------------------------------------------------------------------- + syntax Instr ::= "#local.get" "(" Int ")" [symbol(aLocal.get)] + | "#local.set" "(" Int ")" [symbol(aLocal.set)] + | "#local.tee" "(" Int ")" [symbol(aLocal.tee)] + // -------------------------------------------------------------- rule #local.get(I) => .K ... VALSTACK => VALUE : VALSTACK ... I |-> VALUE ... @@ -647,9 +647,9 @@ The importing and exporting parts of specifications are dealt with in the respec The `get` and `set` instructions read and write globals. ```k - syntax HelperInstr ::= "#global.get" "(" Int ")" [symbol(aGlobal.get)] - | "#global.set" "(" Int ")" [symbol(aGlobal.set)] - // ---------------------------------------------------------------------- + syntax Instr ::= "#global.get" "(" Int ")" [symbol(aGlobal.get)] + | "#global.set" "(" Int ")" [symbol(aGlobal.set)] + // ---------------------------------------------------------------- rule #global.get(IDX) => .K ... VALSTACK => VALUE : VALSTACK CUR @@ -688,15 +688,15 @@ The `get` and `set` instructions read and write globals. - [Execution](https://webassembly.github.io/spec/core/exec/instructions.html#table-instructions) ```k - syntax HelperInstr ::= "#table.get" "(" Int ")" [symbol(aTable.get)] - | "#table.set" "(" Int ")" [symbol(aTable.set)] - | "#table.size" "(" Int ")" [symbol(aTable.size)] - | "#table.grow" "(" Int ")" [symbol(aTable.grow)] - | "#table.fill" "(" Int ")" [symbol(aTable.fill)] - | "#table.copy" "(" Int "," Int ")" [symbol(aTable.copy)] - | "#table.init" "(" Int "," Int ")" [symbol(aTable.init)] - | "#elem.drop" "(" Int ")" [symbol(aElem.drop)] - // ------------------------------------------------------------------------------ + syntax Instr ::= "#table.get" "(" Int ")" [symbol(aTable.get)] + | "#table.set" "(" Int ")" [symbol(aTable.set)] + | "#table.size" "(" Int ")" [symbol(aTable.size)] + | "#table.grow" "(" Int ")" [symbol(aTable.grow)] + | "#table.fill" "(" Int ")" [symbol(aTable.fill)] + | "#table.copy" "(" Int "," Int ")" [symbol(aTable.copy)] + | "#table.init" "(" Int "," Int ")" [symbol(aTable.init)] + | "#elem.drop" "(" Int ")" [symbol(aElem.drop)] + // ------------------------------------------------------------------------ ``` #### `table.get` @@ -1036,9 +1036,9 @@ The `get` and `set` instructions read and write globals. - [Execution](https://webassembly.github.io/spec/core/exec/instructions.html#reference-instructions) ```k - syntax HelperInstr ::= "#ref.is_null" [symbol(aRef.is_null)] - | "#ref.func" "(" Int ")" [symbol(aRef.func)] - // ------------------------------------------------------------------ + syntax Instr ::= "#ref.is_null" [symbol(aRef.is_null)] + | "#ref.func" "(" Int ")" [symbol(aRef.func)] + // ---------------------------------------------------------------- rule [ref.null.func]: ref.null func => null ... @@ -1234,8 +1234,8 @@ The `#take` function will return the parameter stack in the reversed order, then `call funcidx` and `call_indirect tableidx typeuse` are 2 control instructions that invoke a function in the current frame. ```k - syntax HelperInstr ::= #call(Int) [symbol(aCall)] - // ------------------------------------------------- + syntax Instr ::= #call(Int) [symbol(aCall)] + // ----------------------------------------------- rule #call(IDX) => ( invoke FUNCADDRS {{ IDX }} orDefault 0 ) ... CUR @@ -1247,8 +1247,8 @@ The `#take` function will return the parameter stack in the reversed order, then ``` ```k - syntax HelperInstr ::= "#call_indirect" "(" Int "," TypeUse ")" [symbol(aCall_indirect)] - // ---------------------------------------------------------------------------------------- + syntax Instr ::= "#call_indirect" "(" Int "," TypeUse ")" [symbol(aCall_indirect)] + // -------------------------------------------------------------------------------------- ``` TODO: This is kept for compatibility with the text format. @@ -1410,8 +1410,8 @@ The value is encoded as bytes and stored at the "effective address", which is th [Store Instructions](https://webassembly.github.io/spec/core/exec/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-xref-syntax-instructions-syntax-memarg-mathit-memarg-and-t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-n-xref-syntax-instructions-syntax-memarg-mathit-memarg) ```k - syntax HelperInstr ::= #store(ValType, StoreOp, offset : Int) [symbol(aStore)] - | IValType "." StoreOp Int Int + syntax Instr ::= #store(ValType, StoreOp, offset : Int) [symbol(aStore)] + syntax HelperInstr ::= IValType "." StoreOp Int Int // | FValType "." StoreOp Int Float | "store" "{" IWidth Int Number "}" | "store" "{" IWidth Int Number Int "}" @@ -1463,8 +1463,8 @@ Sort `Signedness` is defined in module `BYTES`. [Load Instructions](https://webassembly.github.io/spec/core/exec/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-xref-syntax-instructions-syntax-memarg-mathit-memarg-and-t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg) ```k - syntax HelperInstr ::= #load(ValType, LoadOp, offset : Int) [symbol(aLoad)] - | "load" "{" IValType IWidth Int Signedness"}" + syntax Instr ::= #load(ValType, LoadOp, offset : Int) [symbol(aLoad)] + syntax HelperInstr ::= "load" "{" IValType IWidth Int Signedness"}" | "load" "{" IValType IWidth Int Signedness Int"}" | "load" "{" IValType IWidth Int Signedness SparseBytes"}" | IValType "." LoadOp Int