diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index 0fae18f1b..58fb5d506 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -15,7 +15,7 @@ python = "^3.10" cytoolz = "^0.12.1" numpy = "^1.24.2" pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.572" } -py-wasm = {url = "https://github.com/runtimeverification/py-wasm/archive/refs/tags/0.1.1.tar.gz"} +py-wasm = {url = "https://github.com/runtimeverification/py-wasm/archive/refs/tags/0.2.0.tar.gz"} [tool.poetry.group.dev.dependencies] autoflake = "*" diff --git a/pykwasm/src/pykwasm/kwasm_ast.py b/pykwasm/src/pykwasm/kwasm_ast.py index 8392fc58e..bbb5896e9 100644 --- a/pykwasm/src/pykwasm/kwasm_ast.py +++ b/pykwasm/src/pykwasm/kwasm_ast.py @@ -225,6 +225,59 @@ def CALL_INDIRECT(type_idx: int) -> KInner: return KApply('aCall_indirect', [KInt(0), type_use]) +########################## +# Reference Instructions # +########################## + + +def REF_FUNC(func_idx: int) -> KInner: + return KApply('aRef.func', [KInt(func_idx)]) + + +REF_IS_NULL: KInner = KApply('aRef.is_null', []) + + +def REF_NULL(t: str) -> KInner: + return KApply('aRef.null', [KApply(t, [])]) + + +########################## +# Table Instructions # +########################## + + +def TABLE_GET(table_idx: int) -> KInner: + return KApply('aTable.get', [KInt(table_idx)]) + + +def TABLE_SET(table_idx: int) -> KInner: + return KApply('aTable.set', [KInt(table_idx)]) + + +def TABLE_INIT(table_idx: int, elem_idx: int) -> KInner: + return KApply('aTable.init', [KInt(table_idx), KInt(elem_idx)]) + + +def ELEM_DROP(elem_idx: int) -> KInner: + return KApply('aElem.drop', [KInt(elem_idx)]) + + +def TABLE_COPY(table_idx1: int, table_idx2: int) -> KInner: + return KApply('aTable.copy', [KInt(table_idx1), KInt(table_idx2)]) + + +def TABLE_GROW(table_idx: int) -> KInner: + return KApply('aTable.grow', [KInt(table_idx)]) + + +def TABLE_SIZE(table_idx: int) -> KInner: + return KApply('aTable.size', [KInt(table_idx)]) + + +def TABLE_FILL(table_idx: int) -> KInner: + return KApply('aTable.fill', [KInt(table_idx)]) + + ########################## # Parametric Instruction # ########################## @@ -596,11 +649,18 @@ def glob(type: KInner, init: KInner, metadata: KInner = EMPTY_ID) -> KInner: return KApply(GLOBAL, [type, init, metadata]) -def elem_mode(table_idx: int, offset: KInner) -> KInner: - # TODO Implement other elem modes +def elem_active(table_idx: int, offset: KInner) -> KInner: return KApply('aElemActive', [KInt(table_idx), offset]) +def elem_declarative() -> KInner: + return KApply('aElemDeclarative', []) + + +def elem_passive() -> KInner: + return KApply('aElemPassive', []) + + def elem(typ: KInner, elem_mode: KInner, init: Iterable[int | None], metadata: KInner = EMPTY_ID) -> KInner: return KApply(ELEM, [typ, refs(init), elem_mode, metadata]) diff --git a/pykwasm/src/pykwasm/wasm2kast.py b/pykwasm/src/pykwasm/wasm2kast.py index 46cd24741..4bd63b843 100644 --- a/pykwasm/src/pykwasm/wasm2kast.py +++ b/pykwasm/src/pykwasm/wasm2kast.py @@ -8,6 +8,7 @@ from typing import IO, Iterable from pyk.kast.inner import KInner +from wasm import instructions from wasm.datatypes import ( DataSegment, ElementSegment, @@ -22,6 +23,7 @@ MemoryType, Module, Mutability, + RefType, StartFunction, Table, TableType, @@ -29,6 +31,8 @@ ValType, addresses, ) +from wasm.datatypes.element_segment import ElemMode, ElemModeActive, ElemModeDeclarative, ElemModePassive +from wasm.instructions import BaseInstruction from wasm.opcodes import BinaryOpcode from wasm.parsers import parse_module @@ -116,10 +120,43 @@ def glob(g: Global): return a.glob(t, init) +def ref_type(t: RefType): + if t is addresses.FunctionAddress: + return a.funcref + return a.externref + + +def elem_mode(m: ElemMode) -> KInner: + if isinstance(m, ElemModeActive): + offset = instrs(m.offset) + return a.elem_active(m.table, offset) + if isinstance(m, ElemModeDeclarative): + return a.elem_declarative() + if isinstance(m, ElemModePassive): + return a.elem_passive() + raise ValueError(f'Unknown ElemMode: {m}') + + +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 + instr = expr[0] + + if isinstance(instr, instructions.RefFunc): + return instr.funcidx + if isinstance(instr, instructions.RefNull): + return None + raise ValueError(f'Invalid reference expression: {expr}') + + return [expr_to_int(e) for e in init] + + def elem(e: ElementSegment): - offset = instrs(e.offset) - elem_mode = a.elem_mode(e.table_idx, offset) - return a.elem(a.funcref, elem_mode, e.init) + typ = ref_type(e.type) + mode = elem_mode(e.mode) + init = elem_init(e.init) + return a.elem(typ, mode, init) def data(d: DataSegment): @@ -173,6 +210,7 @@ def instrs(iis): def instr(i): B = BinaryOpcode global block_id + # TODO rewrite 'i.opcode == _' conditions as isinstance for better type-checking if i.opcode == B.BLOCK: cur_block_id = block_id block_id += 1 @@ -278,6 +316,31 @@ def instr(i): return a.SET_LOCAL(i.local_idx) if i.opcode == B.TEE_LOCAL: return a.TEE_LOCAL(i.local_idx) + if isinstance(i, instructions.RefFunc): + return a.REF_FUNC(i.funcidx) + if isinstance(i, instructions.RefNull): + if i.reftype is addresses.FunctionAddress: + return a.REF_NULL('func') + if i.reftype is addresses.ExternAddress: + return a.REF_NULL('extern') + raise ValueError(f'Unknown heap type: {i}, {i.reftype}') + if isinstance(i, instructions.TableGet): + return a.TABLE_GET(i.tableidx) + if isinstance(i, instructions.TableSet): + return a.TABLE_SET(i.tableidx) + if isinstance(i, instructions.TableInit): + return a.TABLE_INIT(i.tableidx, i.elemidx) + if isinstance(i, instructions.ElemDrop): + return a.ELEM_DROP(i.elemidx) + if isinstance(i, instructions.TableCopy): + return a.TABLE_COPY(i.tableidx1, i.tableidx2) + if isinstance(i, instructions.TableGrow): + return a.TABLE_GROW(i.tableidx) + if isinstance(i, instructions.TableSize): + return a.TABLE_SIZE(i.tableidx) + if isinstance(i, instructions.TableFill): + return a.TABLE_FILL(i.tableidx) + # Catch all for operations without direct arguments. return eval('a.' + i.opcode.name) @@ -296,6 +359,11 @@ def val_type(t: ValType): return a.f32 if t == ValType.f64: return a.f64 + if t == ValType.externref: + return a.externref + if t == ValType.funcref: + return a.funcref + raise ValueError(f'Unknown value type: {t}') def vec_type(ts: Iterable[ValType]): diff --git a/pykwasm/src/tests/integration/binary/instrs.wat b/pykwasm/src/tests/integration/binary/instrs.wat index 22aebf8ab..b719c8318 100644 --- a/pykwasm/src/tests/integration/binary/instrs.wat +++ b/pykwasm/src/tests/integration/binary/instrs.wat @@ -1,8 +1,11 @@ (module (memory 0) (table 100 funcref) + (elem func $f) (global (mut i32) (i32.const 0)) (func (param i32 i64) (local f64)) + (func $f) + (global funcref (ref.func $f)) (func (local i32) ;; `unreachable` and `drop` are inserted as needed to ;; ensure correct typing. @@ -171,6 +174,25 @@ call 0 call_indirect (type 0) ;; -- + + ;; Reference Instrs + ref.is_null drop + ref.null extern drop + ref.null func drop + ref.func $f drop + ;; -- + + ;; Table Instrs + table.get 0 drop + table.set 0 drop + table.init 0 0 drop + elem.drop 0 drop + table.copy 0 0 drop + table.grow 0 drop + table.size 0 drop + table.fill 0 drop + ;; -- + unreachable ) diff --git a/pykwasm/src/tests/integration/binary/spec_elem_0.wat b/pykwasm/src/tests/integration/binary/spec_elem_0.wat new file mode 100644 index 000000000..c3a452668 --- /dev/null +++ b/pykwasm/src/tests/integration/binary/spec_elem_0.wat @@ -0,0 +1,75 @@ +;; Syntax +(module + (table $t 10 funcref) + (func $f) + (func $g) + + ;; Passive + (elem funcref) + (elem funcref (ref.func $f) (item ref.func $f) (item (ref.null func)) (ref.func $g)) + (elem func) + (elem func $f $f $g $g) + + (elem $p1 funcref) + (elem $p2 funcref (ref.func $f) (ref.func $f) (ref.null func) (ref.func $g)) + (elem $p3 func) + (elem $p4 func $f $f $g $g) + + ;; Active + (elem (table $t) (i32.const 0) funcref) + (elem (table $t) (i32.const 0) funcref (ref.func $f) (ref.null func)) + (elem (table $t) (i32.const 0) func) + (elem (table $t) (i32.const 0) func $f $g) + (elem (table $t) (offset (i32.const 0)) funcref) + (elem (table $t) (offset (i32.const 0)) func $f $g) + (elem (table 0) (i32.const 0) func) + (elem (table 0x0) (i32.const 0) func $f $f) + (elem (table 0x000) (offset (i32.const 0)) func) + (elem (table 0) (offset (i32.const 0)) func $f $f) + (elem (table $t) (i32.const 0) func) + (elem (table $t) (i32.const 0) func $f $f) + (elem (table $t) (offset (i32.const 0)) func) + (elem (table $t) (offset (i32.const 0)) func $f $f) + (elem (offset (i32.const 0))) + (elem (offset (i32.const 0)) funcref (ref.func $f) (ref.null func)) + (elem (offset (i32.const 0)) func $f $f) + (elem (offset (i32.const 0)) $f $f) + (elem (i32.const 0)) + (elem (i32.const 0) funcref (ref.func $f) (ref.null func)) + (elem (i32.const 0) func $f $f) + (elem (i32.const 0) $f $f) + + (elem $a1 (table $t) (i32.const 0) funcref) + (elem $a2 (table $t) (i32.const 0) funcref (ref.func $f) (ref.null func)) + (elem $a3 (table $t) (i32.const 0) func) + (elem $a4 (table $t) (i32.const 0) func $f $g) + (elem $a9 (table $t) (offset (i32.const 0)) funcref) + (elem $a10 (table $t) (offset (i32.const 0)) func $f $g) + (elem $a11 (table 0) (i32.const 0) func) + (elem $a12 (table 0x0) (i32.const 0) func $f $f) + (elem $a13 (table 0x000) (offset (i32.const 0)) func) + (elem $a14 (table 0) (offset (i32.const 0)) func $f $f) + (elem $a15 (table $t) (i32.const 0) func) + (elem $a16 (table $t) (i32.const 0) func $f $f) + (elem $a17 (table $t) (offset (i32.const 0)) func) + (elem $a18 (table $t) (offset (i32.const 0)) func $f $f) + (elem $a19 (offset (i32.const 0))) + (elem $a20 (offset (i32.const 0)) funcref (ref.func $f) (ref.null func)) + (elem $a21 (offset (i32.const 0)) func $f $f) + (elem $a22 (offset (i32.const 0)) $f $f) + (elem $a23 (i32.const 0)) + (elem $a24 (i32.const 0) funcref (ref.func $f) (ref.null func)) + (elem $a25 (i32.const 0) func $f $f) + (elem $a26 (i32.const 0) $f $f) + + ;; Declarative + (elem declare funcref) + (elem declare funcref (ref.func $f) (ref.func $f) (ref.null func) (ref.func $g)) + (elem declare func) + (elem declare func $f $f $g $g) + + (elem $d1 declare funcref) + (elem $d2 declare funcref (ref.func $f) (ref.func $f) (ref.null func) (ref.func $g)) + (elem $d3 declare func) + (elem $d4 declare func $f $f $g $g) +) \ No newline at end of file diff --git a/pykwasm/src/tests/integration/binary/spec_elem_1.wat b/pykwasm/src/tests/integration/binary/spec_elem_1.wat new file mode 100644 index 000000000..285d430b8 --- /dev/null +++ b/pykwasm/src/tests/integration/binary/spec_elem_1.wat @@ -0,0 +1,14 @@ +(module + (type $out-i32 (func (result i32))) + (table 10 funcref) + (elem (i32.const 7) $const-i32-a) + (elem (i32.const 9) $const-i32-b) + (func $const-i32-a (type $out-i32) (i32.const 65)) + (func $const-i32-b (type $out-i32) (i32.const 66)) + (func (export "call-7") (type $out-i32) + (call_indirect (type $out-i32) (i32.const 7)) + ) + (func (export "call-9") (type $out-i32) + (call_indirect (type $out-i32) (i32.const 9)) + ) +) \ No newline at end of file diff --git a/pykwasm/src/tests/integration/binary/spec_elem_2.wat b/pykwasm/src/tests/integration/binary/spec_elem_2.wat new file mode 100644 index 000000000..5a4a74663 --- /dev/null +++ b/pykwasm/src/tests/integration/binary/spec_elem_2.wat @@ -0,0 +1,17 @@ +(module $module1 + (type $out-i32 (func (result i32))) + (table (export "shared-table") 10 funcref) + (elem (i32.const 8) $const-i32-a) + (elem (i32.const 9) $const-i32-b) + (func $const-i32-a (type $out-i32) (i32.const 65)) + (func $const-i32-b (type $out-i32) (i32.const 66)) + (func (export "call-7") (type $out-i32) + (call_indirect (type $out-i32) (i32.const 7)) + ) + (func (export "call-8") (type $out-i32) + (call_indirect (type $out-i32) (i32.const 8)) + ) + (func (export "call-9") (type $out-i32) + (call_indirect (type $out-i32) (i32.const 9)) + ) +) \ No newline at end of file diff --git a/wasm.md b/wasm.md index 2121d4b6d..de065ab58 100644 --- a/wasm.md +++ b/wasm.md @@ -78,7 +78,7 @@ The sorts `EmptyStmt` and `EmptyStmts` are administrative so that the empty list ```k syntax PlainInstr ::= IValType "." "const" WasmInt [klabel(aIConst), symbol] | FValType "." "const" Number [klabel(aFConst), symbol] - | "ref.null" HeapType [klabel(aRefNull), symbol] + | "ref.null" HeapType [klabel(aRef.null), symbol] | IValType "." IUnOp [klabel(aIUnOp), symbol] | FValType "." FUnOp [klabel(aFUnOp), symbol] | IValType "." ExtendS [klabel(aExtendS), symbol] // TODO this is more permissive than the official spec as it allows 'i32.extend32_s'