From d908cd0eddf401b489982722af2827dd43e7b294 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 3 Apr 2026 23:14:52 +0300 Subject: [PATCH 1/6] [TEMPORARY] set py-wasm branch --- pykwasm/pyproject.toml | 2 +- pykwasm/uv.lock | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index 2cd96eee5..025f64986 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -10,7 +10,7 @@ readme = "README.md" requires-python = "~=3.10" dependencies = [ "kframework>=7.1.313", - "py-wasm@git+https://github.com/runtimeverification/py-wasm.git@0.2.1" + "py-wasm@git+https://github.com/runtimeverification/py-wasm.git@bytecode-location" ] [[project.authors]] diff --git a/pykwasm/uv.lock b/pykwasm/uv.lock index ece16d297..6d5239062 100644 --- a/pykwasm/uv.lock +++ b/pykwasm/uv.lock @@ -1,5 +1,5 @@ version = 1 -revision = 3 +revision = 2 requires-python = ">=3.10, <4" resolution-markers = [ "python_full_version >= '3.11'", @@ -432,7 +432,7 @@ name = "exceptiongroup" version = "1.3.1" source = { registry = "https://pypi.org/simple" } dependencies = [ - { name = "typing-extensions", marker = "python_full_version < '3.13'" }, + { name = "typing-extensions", marker = "python_full_version < '3.11'" }, ] sdist = { url = "https://files.pythonhosted.org/packages/50/79/66800aadf48771f6b62f7eb014e352e5d06856655206165d775e675a02c9/exceptiongroup-1.3.1.tar.gz", hash = "sha256:8b412432c6055b0b7d14c310000ae93352ed6754f70fa8f7c34141f91c4e3219", size = 30371, upload-time = "2025-11-21T23:01:54.787Z" } wheels = [ @@ -1009,7 +1009,7 @@ wheels = [ [[package]] name = "py-wasm" version = "0.2.0" -source = { git = "https://github.com/runtimeverification/py-wasm.git?rev=0.2.1#e5fb6ed5b1aebf1c0d67087397b3c1240ff412da" } +source = { git = "https://github.com/runtimeverification/py-wasm.git?rev=bytecode-location#694d3af05a39beae5edd837a431e64fd9f69d5f0" } dependencies = [ { name = "cytoolz", marker = "implementation_name == 'cpython'" }, { name = "mypy-extensions" }, @@ -1055,7 +1055,7 @@ wheels = [ [[package]] name = "pykwasm" -version = "0.1.146" +version = "0.1.148" source = { editable = "." } dependencies = [ { name = "kframework" }, @@ -1084,7 +1084,7 @@ dev = [ [package.metadata] requires-dist = [ { name = "kframework", specifier = ">=7.1.313" }, - { name = "py-wasm", git = "https://github.com/runtimeverification/py-wasm.git?rev=0.2.1" }, + { name = "py-wasm", git = "https://github.com/runtimeverification/py-wasm.git?rev=bytecode-location" }, ] [package.metadata.requires-dev] From 2320fb6d79fd35a556f14d18814998804a0b150a Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 3 Apr 2026 23:15:10 +0300 Subject: [PATCH 2/6] implement semantics --- pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index 8470abaff..d56d74df5 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -332,6 +332,20 @@ Instructions rule sequenceInstrs(I IS ) => I ~> sequenceInstrs(IS) ``` +### Position-annotated instruction + +Helper wrapper to attach source position metadata to instructions for tracing/debugging. +`posStart` and `posEnd` represent the byte/code offsets of the instruction in the original Wasm bytecode file. + +This constructor has no semantic effect and its execution simply unwraps the annotated instruction. +The wrapper exists only for the tracing and must not interfere with semantics. + +```k + syntax Instr ::= #instrWithPos(inner: Instr, posStart: Int, posEnd: Int) [symbol(aInstrWithPos)] + // --------------------------------------------------------------------------- + rule #instrWithPos(I, _, _) => I ... +``` + ### Traps `trap` is the error mechanism of Wasm. From 80eb95f68c661f7cf7cd8ceceb2c93952492d79c Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Fri, 3 Apr 2026 23:15:23 +0300 Subject: [PATCH 3/6] implement binary-parser --- pykwasm/src/pykwasm/kwasm_ast.py | 5 +++++ pykwasm/src/pykwasm/wasm2kast.py | 9 ++++++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/pykwasm/src/pykwasm/kwasm_ast.py b/pykwasm/src/pykwasm/kwasm_ast.py index a818e0a35..27a2b7704 100644 --- a/pykwasm/src/pykwasm/kwasm_ast.py +++ b/pykwasm/src/pykwasm/kwasm_ast.py @@ -189,6 +189,11 @@ def global_type(mut: KInner, valtype: KInner) -> KInner: # Instrs # ########## + +def INSTR_WITH_POS(instruction: KInner, start: int, end: int) -> KInner: + return KApply('aInstrWithPos', [instruction, KInt(start), KInt(end)]) + + ######################## # Control Instructions # ######################## diff --git a/pykwasm/src/pykwasm/wasm2kast.py b/pykwasm/src/pykwasm/wasm2kast.py index 91cea1ff6..fa73d303e 100644 --- a/pykwasm/src/pykwasm/wasm2kast.py +++ b/pykwasm/src/pykwasm/wasm2kast.py @@ -12,6 +12,7 @@ from wasm import instructions from wasm.datatypes import GlobalType, MemoryType, Mutability, TableType, TypeIdx, ValType, addresses from wasm.datatypes.element_segment import ElemModeActive, ElemModeDeclarative, ElemModePassive +from wasm.instructions import InstructionWithPos from wasm.opcodes import BinaryOpcode from wasm.parsers import parse_module @@ -141,9 +142,12 @@ def elem_mode(m: ElemMode) -> KInner: def elem_init(init: tuple[Iterable[BaseInstruction], ...]) -> Iterable[int | None]: def expr_to_int(expr: Iterable[BaseInstruction]) -> int | None: # 'expr' must be a constant expression consisting of a reference instruction - assert len(expr) == 1 or len(expr) == 2 and isinstance(expr[1], instructions.End), expr + assert len(expr) == 1 or len(expr) == 2 and expr[1].opcode == BinaryOpcode.END, expr instr = expr[0] + if isinstance(instr, InstructionWithPos): + instr = instr.instruction + if isinstance(instr, instructions.RefFunc): return instr.funcidx if isinstance(instr, instructions.RefNull): @@ -212,6 +216,9 @@ def instr(i): B = BinaryOpcode global block_id # TODO rewrite 'i.opcode == _' conditions as isinstance for better type-checking + if isinstance(i, InstructionWithPos): + inner = instr(i.instruction) + return a.INSTR_WITH_POS(inner, i.pos[0], i.pos[1]) if i.opcode == B.BLOCK: cur_block_id = block_id block_id += 1 From f0a0cf4846d4f68cc4aac2a0b5ff0f634d681dd7 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 3 Apr 2026 20:24:52 +0000 Subject: [PATCH 4/6] Set Version: 0.1.149 --- package/version | 2 +- pykwasm/pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 3a28972df..010fbfb88 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.148 +0.1.149 diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index 025f64986..a730836ec 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "pykwasm" -version = "0.1.148" +version = "0.1.149" description = "" readme = "README.md" requires-python = "~=3.10" From 24d492cfbe44993bf0585e70668f82f93dc21e1c Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 8 Apr 2026 16:16:41 +0300 Subject: [PATCH 5/6] set py-wasm version --- pykwasm/pyproject.toml | 2 +- pykwasm/uv.lock | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index a730836ec..6888c3279 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -10,7 +10,7 @@ readme = "README.md" requires-python = "~=3.10" dependencies = [ "kframework>=7.1.313", - "py-wasm@git+https://github.com/runtimeverification/py-wasm.git@bytecode-location" + "py-wasm@git+https://github.com/runtimeverification/py-wasm.git@0.3.0" ] [[project.authors]] diff --git a/pykwasm/uv.lock b/pykwasm/uv.lock index 6d5239062..b57cd4586 100644 --- a/pykwasm/uv.lock +++ b/pykwasm/uv.lock @@ -1008,8 +1008,8 @@ wheels = [ [[package]] name = "py-wasm" -version = "0.2.0" -source = { git = "https://github.com/runtimeverification/py-wasm.git?rev=bytecode-location#694d3af05a39beae5edd837a431e64fd9f69d5f0" } +version = "0.3.0" +source = { git = "https://github.com/runtimeverification/py-wasm.git?rev=0.3.0#07677b120f40b86d5b7839e2dde42889967dcfce" } dependencies = [ { name = "cytoolz", marker = "implementation_name == 'cpython'" }, { name = "mypy-extensions" }, @@ -1084,7 +1084,7 @@ dev = [ [package.metadata] requires-dist = [ { name = "kframework", specifier = ">=7.1.313" }, - { name = "py-wasm", git = "https://github.com/runtimeverification/py-wasm.git?rev=bytecode-location" }, + { name = "py-wasm", git = "https://github.com/runtimeverification/py-wasm.git?rev=0.3.0" }, ] [package.metadata.requires-dev] From 1aaae4467254c57f3547f359c09249102992073f Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 8 Apr 2026 16:17:13 +0300 Subject: [PATCH 6/6] use (offset, length) --- pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md | 7 ++++--- pykwasm/src/pykwasm/wasm2kast.py | 2 +- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index d56d74df5..78f192f75 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -335,13 +335,14 @@ Instructions ### Position-annotated instruction Helper wrapper to attach source position metadata to instructions for tracing/debugging. -`posStart` and `posEnd` represent the byte/code offsets of the instruction in the original Wasm bytecode file. +`offset` is **0-based** and indicates the starting byte position of the instruction in the original Wasm bytecode. +`length` is the number of bytes the instruction spans. This constructor has no semantic effect and its execution simply unwraps the annotated instruction. -The wrapper exists only for the tracing and must not interfere with semantics. +The wrapper exists only for tracing and must not interfere with semantics. ```k - syntax Instr ::= #instrWithPos(inner: Instr, posStart: Int, posEnd: Int) [symbol(aInstrWithPos)] + syntax Instr ::= #instrWithPos(inner: Instr, offset: Int, length: Int) [symbol(aInstrWithPos)] // --------------------------------------------------------------------------- rule #instrWithPos(I, _, _) => I ... ``` diff --git a/pykwasm/src/pykwasm/wasm2kast.py b/pykwasm/src/pykwasm/wasm2kast.py index fa73d303e..55ea382f5 100644 --- a/pykwasm/src/pykwasm/wasm2kast.py +++ b/pykwasm/src/pykwasm/wasm2kast.py @@ -218,7 +218,7 @@ def instr(i): # TODO rewrite 'i.opcode == _' conditions as isinstance for better type-checking if isinstance(i, InstructionWithPos): inner = instr(i.instruction) - return a.INSTR_WITH_POS(inner, i.pos[0], i.pos[1]) + return a.INSTR_WITH_POS(inner, i.offset, i.length) if i.opcode == B.BLOCK: cur_block_id = block_id block_id += 1