From d78f69bc69a46d5871d53acda104a1975bdb212d Mon Sep 17 00:00:00 2001 From: gtrepta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 9 Jul 2024 19:04:32 -0500 Subject: [PATCH] Support `memory.fill` (#670) * Support memory.fill https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-fill * Set Version: 0.1.78 * Add links to the spec in the memory instructions section --------- Co-authored-by: devops --- package/version | 2 +- pykwasm/pyproject.toml | 2 +- .../pykwasm/kdist/wasm-semantics/wasm-text.md | 1 + .../src/pykwasm/kdist/wasm-semantics/wasm.md | 52 +++++++++++++++++++ pykwasm/src/pykwasm/kwasm_ast.py | 1 + tests/conformance/unparseable.txt | 1 - 6 files changed, 56 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 1f7a170d7..59057fc2c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.77 +0.1.78 diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index 3558850c8..e9e33a9a7 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pykwasm" -version = "0.1.77" +version = "0.1.78" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md index da377db1f..8ab68f908 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md @@ -1141,6 +1141,7 @@ The `align` parameter is for optimization only and is not allowed to influence t rule #t2aInstr<_>(FTYPE:FValType.OP:LoadOp MemArg) => #load(FTYPE, OP, #getOffset(MemArg)) rule #t2aInstr<_>(memory.size) => memory.size rule #t2aInstr<_>(memory.grow) => memory.grow + rule #t2aInstr<_>(memory.fill) => memory.fill syntax Int ::= #getOffset ( MemArg ) [function, total] // ----------------------------------------------------------- diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index 1c90d62da..2d9be26e8 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -94,6 +94,7 @@ The sorts `EmptyStmt` and `EmptyStmts` are administrative so that the empty list | "return" [symbol(aReturn)] | "memory.size" [symbol(aSize)] | "memory.grow" [symbol(aGrow)] + | "memory.fill" [symbol(aFill)] // ----------------------------------- syntax TypeUse ::= TypeDecls @@ -1348,6 +1349,7 @@ The `MemorySpec` production is used to define all ways that a global can specifi A memory can either be specified by giving its type (limits); by specifying a vector of its initial `data`; or by an import and its expected type. The specification can also include export directives. The importing and exporting parts of specifications are dealt with in the respective sections for import and export. +[Memory Instructions](https://webassembly.github.io/spec/core/exec/instructions.html#memory-instructions) ```k syntax MemoryDefn ::= #memory(limits: Limits, metadata: OptionalId) [symbol(aMemoryDefn)] @@ -1384,6 +1386,7 @@ The importing and exporting parts of specifications are dealt with in the respec The assorted store operations take an address of type `i32` and a value. The `storeX` operations first wrap the the value to be stored to the bit wdith `X`. The value is encoded as bytes and stored at the "effective address", which is the address given on the stack plus offset. +[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)] @@ -1436,6 +1439,7 @@ The assorted load operations take an address of type `i32`. The `loadX_sx` operations loads `X` bits from memory, and extend it to the right length for the return value, interpreting the bytes as either signed or unsigned according to `sx`. The value is fetched from the "effective address", which is the address given on the stack plus offset. 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)] @@ -1492,6 +1496,7 @@ Sort `Signedness` is defined in module `BYTES`. ``` The `size` operation returns the size of the memory, measured in pages. +[Memory Size](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-size) ```k rule memory.size => < i32 > SIZE ... @@ -1513,6 +1518,7 @@ Failure to grow is indicated by pushing -1 to the stack. Success is indicated by pushing the previous memory size to the stack. `grow` is non-deterministic and may fail either due to trying to exceed explicit max values, or because the embedder does not have resources available. By setting the `` field in the configuration to `true`, the sematnics ensure memory growth only fails if the memory in question would exceed max bounds. +[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 @@ -1568,6 +1574,52 @@ The maximum of table size is 2^32 bytes. rule #maxTableSize() => 4294967296 ``` +`fill` fills a contiguous section of memory with a value. +When the section specified goes beyond the bounds of the memory region, that causes a trap. +If the section has length 0, nothing happens. +The spec states that this is really a sequence of `i32.store8` instructions, but we use `#setBytesRange` here. +[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 + // --------------------------------------- + rule memory.fill => fillTrap N VAL D ... + < i32 > N : < i32 > VAL : < i32 > D : VALSTACK => VALSTACK + + rule fillTrap N _VAL D => trap ... + CUR + + CUR + 0 |-> ADDR + ... + + + ADDR + SIZE + ... + + requires N +Int D >Int SIZE *Int #pageSize() + + rule fillTrap N VAL D => fill N VAL D ... [owise] + + rule fill 0 _VAL _D => .K ... + + rule fill N VAL D => .K ... + CUR + + CUR + 0 |-> ADDR + ... + + + ADDR + DATA => #setBytesRange(DATA, D, padRightBytes(.Bytes, N, VAL)) + ... + + requires notBool N ==Int 0 +``` + Element Segments ---------------- diff --git a/pykwasm/src/pykwasm/kwasm_ast.py b/pykwasm/src/pykwasm/kwasm_ast.py index 50c82dc86..925a39f8c 100644 --- a/pykwasm/src/pykwasm/kwasm_ast.py +++ b/pykwasm/src/pykwasm/kwasm_ast.py @@ -580,6 +580,7 @@ def I64_LOAD32_S(offset: int) -> KInner: MEMORY_GROW = KApply('aGrow', []) MEMORY_SIZE = KApply('aSize', []) +MEMORY_FILL = KApply('aFill', []) ####################### # Global Instructions # diff --git a/tests/conformance/unparseable.txt b/tests/conformance/unparseable.txt index ddf8d0117..9328bfbf6 100644 --- a/tests/conformance/unparseable.txt +++ b/tests/conformance/unparseable.txt @@ -16,7 +16,6 @@ if.wast imports.wast loop.wast memory_copy.wast -memory_fill.wast memory_init.wast memory.wast select.wast