Skip to content

Add new HelperInstr sort #748

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
automergerpr-permission-manager merged 3 commits into from
Mar 23, 2026
Merged

Add new HelperInstr sort #748

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4fdefce
wasm.md: add new HelperInstr sort
anvacaru Mar 18, 2026
7dbad52
Set Version: 0.1.147
rv-auditor Mar 18, 2026
d90e8e6
Apply suggestions from code review
anvacaru Mar 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.146
0.1.147
2 changes: 1 addition & 1 deletion pykwasm/pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
152 changes: 78 additions & 74 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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)]
// ------------------------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
rule <instrs> #block(VECTYP, IS, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... </instrs>
<valstack> VALSTACK => .ValStack </valstack>
```
Expand All @@ -504,25 +507,25 @@ 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)]
// -----------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
rule <instrs> #br(_IDX) ~> (_S:Stmt => .K) ... </instrs>
rule <instrs> #br(0 ) ~> label [ TYPES ] { IS } VALSTACK' => sequenceInstrs(IS) ... </instrs>
<valstack> VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' </valstack>
rule <instrs> #br(N:Int) ~> _L:Label => #br(N -Int 1) ... </instrs>
requires N >Int 0

syntax Instr ::= "#br_if" "(" Int ")" [symbol(aBr_if)]
// --------------------------------------------------------------
syntax HelperInstr ::= "#br_if" "(" Int ")" [symbol(aBr_if)]
// ------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
rule <instrs> #br_if(IDX) => #br(IDX) ... </instrs>
<valstack> <i32> VAL : VALSTACK => VALSTACK </valstack>
requires VAL =/=Int 0
rule <instrs> #br_if(_IDX) => .K ... </instrs>
<valstack> <i32> VAL : VALSTACK => VALSTACK </valstack>
requires VAL ==Int 0

syntax Instr ::= "#br_table" "(" Ints ")" [symbol(aBr_table)]
// ---------------------------------------------------------------------
syntax HelperInstr ::= "#br_table" "(" Ints ")" [symbol(aBr_table)]
// -------------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
rule <instrs> #br_table(ES) => #br(#getInts(ES, minInt(VAL, #lenInts(ES) -Int 1))) ... </instrs>
<valstack> <i32> VAL : VALSTACK => VALSTACK </valstack>
requires 0 <=Int VAL
Expand All @@ -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)]
// ----------------------------------------------------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
rule <instrs> #if(VECTYP, IS, _, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... </instrs>
<valstack> < i32 > VAL : VALSTACK => VALSTACK </valstack>
requires VAL =/=Int 0
Expand All @@ -546,8 +549,8 @@ Finally, we have the conditional and loop instructions.
<valstack> < i32 > VAL : VALSTACK => VALSTACK </valstack>
requires VAL ==Int 0

syntax Instr ::= #loop(VecType, Instrs, BlockMetaData) [symbol(aLoop)]
// ------------------------------------------------------------------------------
syntax HelperInstr ::= #loop(VecType, Instrs, BlockMetaData) [symbol(aLoop)]
// ----------------------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
rule <instrs> #loop(VECTYP, IS, BLOCKMETA) => sequenceInstrs(IS) ~> label VECTYP { #loop(VECTYP, IS, BLOCKMETA) } VALSTACK ... </instrs>
<valstack> VALSTACK => .ValStack </valstack>
```
Expand Down Expand Up @@ -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)]
// --------------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
rule <instrs> #local.get(I) => .K ... </instrs>
<valstack> VALSTACK => VALUE : VALSTACK </valstack>
<locals> ... I |-> VALUE ... </locals>
Expand Down Expand Up @@ -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)]
// ----------------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
rule <instrs> #global.get(IDX) => .K ... </instrs>
<valstack> VALSTACK => VALUE : VALSTACK </valstack>
<curModIdx> CUR </curModIdx>
Expand Down Expand Up @@ -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)]
// ------------------------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
```

#### `table.get`
Expand All @@ -709,7 +712,8 @@ The `get` and `set` instructions read and write globals.
...
</moduleInst>

syntax Instr ::= #tableGet( addr: Int, index: Int)
syntax HelperInstr ::= #tableGet( addr: Int, index: Int)
// --------------------------------------------------------
rule [tableGet]:
<instrs> #tableGet( TADDR, I) => getRefOrNull(TDATA, I) ... </instrs>
<tabInst>
Expand All @@ -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]:
<instrs> #table.set( TID )
=> #tableSet(TADDR, VAL, I) ...
Expand Down Expand Up @@ -851,8 +855,8 @@ The `get` and `set` instructions read and write globals.
...
</moduleInst>

syntax Instr ::= #tableFill(Int, Int, RefVal, Int)
// ------------------------------------------------------
syntax HelperInstr ::= #tableFill(Int, Int, RefVal, Int)
// --------------------------------------------------------
rule [tableFill-zero]:
<instrs> #tableFill(_, 0, _, _) => .K ... </instrs>

Expand Down Expand Up @@ -900,8 +904,8 @@ The `get` and `set` instructions read and write globals.
...
</moduleInst>

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]:
<instrs> #tableCopy(_, _, 0, _, _) => .K ... </instrs>

Expand Down Expand Up @@ -956,8 +960,8 @@ The `get` and `set` instructions read and write globals.
...
</elemInst>

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]:
<instrs> #tableInit(_, 0, _, _) => .K ... </instrs>

Expand Down Expand Up @@ -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]:
<instrs> #tableCheckSizeGTE(ADDR, N) => .K ... </instrs>
<tabInst>
Expand All @@ -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]:
<instrs> #elemCheckSizeGTE(ADDR, N) => .K ... </instrs>
<elemInst>
Expand All @@ -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)]
// ------------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated

rule [ref.null.func]:
<instrs> ref.null func => <funcref> null ... </instrs>
Expand Down Expand Up @@ -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)]
// -------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
rule <instrs> #call(IDX) => ( invoke FUNCADDRS {{ IDX }} orDefault 0 ) ... </instrs>
<curModIdx> CUR </curModIdx>
<moduleInst>
Expand All @@ -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)]
// ----------------------------------------------------------------------------------------
Comment thread
anvacaru marked this conversation as resolved.
Outdated
```

TODO: This is kept for compatibility with the text format.
Expand Down Expand Up @@ -1276,8 +1280,8 @@ The types need to be inserted at the definitions level, if a previously undeclar
</tabInst>


syntax Instr ::= #callIndirect(RefVal, FuncType)
// ------------------------------------------
syntax HelperInstr ::= #callIndirect(RefVal, FuncType)
// ------------------------------------------------------
rule [callIndirect-invoke]:
<instrs> #callIndirect(<funcref> FADDR, ETYPE)
=> ( invoke FADDR ) ...
Expand Down Expand Up @@ -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
Comment thread
anvacaru marked this conversation as resolved.
Outdated
// | FValType "." StoreOp Int Float
| "store" "{" IWidth Int Number "}"
| "store" "{" IWidth Int Number Int "}"
// ------------------------------------------------------------
rule <instrs> #store(ITYPE:IValType, SOP, OFFSET) => ITYPE . SOP (IDX +Int OFFSET) VAL ... </instrs>
<valstack> < ITYPE > VAL : < i32 > IDX : VALSTACK => VALSTACK </valstack>

Expand Down Expand Up @@ -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"}"
Comment thread
anvacaru marked this conversation as resolved.
Outdated
| "load" "{" IValType IWidth Int Signedness Int"}"
| "load" "{" IValType IWidth Int Signedness SparseBytes"}"
| IValType "." LoadOp Int
// ----------------------------------------------
rule <instrs> #load(ITYPE:IValType, LOP, OFFSET) => ITYPE . LOP (IDX +Int OFFSET) ... </instrs>
<valstack> < i32 > IDX : VALSTACK => VALSTACK </valstack>

Expand Down Expand Up @@ -1538,8 +1542,8 @@ By setting the `<deterministicMemoryGrowth>` 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 <instrs> memory.grow => grow N ... </instrs>
<valstack> < i32 > N : VALSTACK => VALSTACK </valstack>

Expand Down Expand Up @@ -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 <instrs> memory.fill => fillTrap N VAL D ... </instrs>
<valstack> < i32 > N : < i32 > VAL : < i32 > D : VALSTACK => VALSTACK </valstack>

Expand Down Expand Up @@ -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 <instrs> memory.copy => copyTrap N S D ... </instrs>
<valstack> < i32 > N : < i32 > S : < i32 > D : VALSTACK => VALSTACK </valstack>

Expand Down
Loading