Annotate Wasm AST nodes (Instrs) with bytecode position metadata for tracing/debugging

package/version

@@ -1 +1 @@
-0.1.148
+0.1.149

pykwasm/pyproject.toml

@@ -4,13 +4,13 @@ build-backend = "hatchling.build"
 
 [project]
 name = "pykwasm"
-version = "0.1.148"
+version = "0.1.149"
 description = ""
 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@0.3.0"
 ]
 
 [[project.authors]]

pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md

@@ -332,6 +332,21 @@ Instructions
     rule sequenceInstrs(I IS   ) => I ~> sequenceInstrs(IS)
 ```
 
+### Position-annotated instruction
+
+Helper wrapper to attach source position metadata to instructions for tracing/debugging.
+`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 tracing and must not interfere with semantics.
+
+```k
+    syntax Instr ::= #instrWithPos(inner: Instr, offset: Int, length: Int)     [symbol(aInstrWithPos)]
+ // ---------------------------------------------------------------------------
+    rule <instrs> #instrWithPos(I, _, _) => I ... </instrs>
+```
+
 ### Traps
 
 `trap` is the error mechanism of Wasm.

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 #
 ########################

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.offset, i.length)
     if i.opcode == B.BLOCK:
         cur_block_id = block_id
         block_id += 1