Skip to content

Commit 212271b

Browse files
Implement zero-dependency Wasm binary parser (#754)
* update `DataDefn` and `ExternDefn`, fix type annotations * add binary parser for numbers * parse modules * add integrations tests and compare legacy and new parser * format * pyupgrade * organize imports * fix `<exports>`: migrate to typed export indices * migrate to the new parser * add `#instrWithPos` support * Set Version: 0.1.157 * fix `elem_init` after instrWithPos * remove unused `BlockMetaData` * fix `limits` address-type flag bytes for memory64 The i64 (memory64/table64) limit encodings are 0x04/0x05 per the Wasm 3.0 grammar; 0x02/0x03 are the shared-memory (threads) flags for i32 and were being misdecoded as i64. Address type is discarded downstream regardless, so this only affects which flag byte is recognized as which type. Adds regression tests covering the i32/i64 limit cases and confirming the shared-memory flags are now rejected instead of misdecoded. * fix custom sections not being consumed parse_custom_section skipped the section id byte but then read_bytes(n, s) used n (the id, always 0) as the length instead of reading the section's size:u32 first. This left the stream misaligned after any custom section, silently dropping every section that followed. Also switch the "no more custom sections" sentinel from falsy bytes to explicit None, since an empty-payload custom section is valid and isn't the same as "not a custom section". Adds a regression test that builds raw bytes with custom sections interleaved between real sections and confirms the type/function/export sections still parse correctly. * add memory.copy and memory.fill opcode parsing 0xFC 10 (memory.copy) and 0xFC 11 (memory.fill) map to the existing aCopy/aFill K constructs. Their memory index operands are parsed and discarded, matching the existing memory.size/memory.grow handling, since the K semantics has a single implicit memory. Adds parametrized unit tests (zero and multi-byte memidx values, plus a trailing sentinel byte) proving the parser consumes exactly the memidx operands rather than a fixed byte count, and exercises both opcodes through the full K interpreter via instrs.wat. * fix binary parser to reject trailing data after module end parse_module never checked that the input stream was fully consumed, so an unrecognized section id or garbage appended after a well-formed module was silently ignored instead of raising a parse error. * remove unused iterate combinator from binary parser Dead code: nothing in the parser calls it, and its broad exception swallow (WasmParseError | IndexError | ValueError) risked masking real bugs if it were ever reused. * raise WasmParseError instead of ValueError on func/code length mismatch zip(function_section, code_section, strict=True) surfaced a bare Python ValueError on mismatch, unlike every other malformed-input path in the parser, which raises WasmParseError. * fix peek_bytes to restore stream position on partial-EOF read reset(pos, s) only ran on the success path, so a short read at EOF (fewer than n bytes remaining but more than zero) left the stream advanced past the bytes it consumed while trying, violating peek's no-side-effects contract. * fix parsing of if instructions without an else branch 'if bt in* end' is a valid encoding that omits the 0x05 else opcode; the parser only handled the explicit-else form and raised 'Unsupported opcode: 0x0b' on the then-branch terminator. * reject non-zero memory indices instead of silently using memory 0 The K semantics models a single memory; multi-memory support is future work. Previously the memory index was parsed and discarded in memarg, memory.size/grow/copy/fill, active data segments, and memory exports, so a valid multi-memory module would silently execute against memory 0. Now memidx raises WasmParseError on any index other than 0. * improve comment clarity in binary parser unit tests Explain the constructed bytecode in TestCustomSections and TestFuncCodeLengthMismatch, state the sentinel-byte contract once at class level instead of four times, explain why the shared-memory limit flags 0x02/0x03 must be rejected, note the intent behind the LEB128 boundary values, and untangle the peek_bytes test comment. * scope the recursion limit to run_module and clean up dead code sys.setrecursionlimit(1500000000) was an import-time side effect inherited from the 2020 py-wasm-era script, and the value effectively disabled Python's recursion guard. The limit is only needed because pyk serializes kore terms recursively (pyk.kore.syntax.Pattern.write) and the depth grows with module size: basic-features.wat needs about 4000, while the default 1000 is enough for everything else. Set 20000 inside run_module, never lowering an externally raised limit. Also remove an assert made dead by check=True and a try/except that re-raised as a bare Exception, hiding the original exception type. * reject unsupported 64-bit addressing and non-funcref table imports The limits parser decoded the memory64/table64 flags (0x04/0x05) and returned the i64 address type, which every caller discarded; a table import's reference type was likewise parsed and dropped since the K ImportDefn sort has no reftype slot. In both cases a valid module using the feature would silently execute with wrong (32-bit / funcref) semantics. The K AST cannot represent either feature, so raise a parse error instead, keeping the spec-correct handling in place as commented-out skeleton for future support. * improve parse error reporting and exception hygiene Magic and version checks no longer rely on assert (stripped under python -O) and report expected vs. actual bytes; invalid UTF-8 in a name raises WasmParseError instead of leaking UnicodeDecodeError; the blocktype error names the unsupported type-index (i33) form; and the 0xFC handler catches WasmParseError instead of Exception so internal errors are not disguised as parse errors. No accept/reject behavior changes. * turn version-bump CI job into a check instead of auto-commit * update uv lock * remove obsolete unit test file `test_wasm2kast.py` --------- Co-authored-by: devops <devops@runtimeverification.com>
1 parent 194cccd commit 212271b

23 files changed

Lines changed: 2438 additions & 1036 deletions

File tree

‎.github/workflows/test-pr.yml‎

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -15,23 +15,19 @@ jobs:
1515
- name: 'Check out code'
1616
uses: actions/checkout@v3
1717
with:
18-
token: ${{ secrets.JENKINS_GITHUB_PAT }}
1918
# fetch-depth 0 means deep clone the repo
2019
fetch-depth: 0
2120
ref: ${{ github.event.pull_request.head.sha }}
22-
- name: 'Configure GitHub user'
23-
run: |
24-
git config user.name devops
25-
git config user.email devops@runtimeverification.com
26-
- name: 'Update version'
21+
- name: 'Check version was bumped'
2722
run: |
2823
og_version=$(git show origin/${GITHUB_BASE_REF}:package/version)
2924
./package/version.sh bump ${og_version}
3025
./package/version.sh sub
31-
new_version=$(cat package/version)
32-
git add --update && git commit --message "Set Version: ${new_version}" || true
33-
- name: 'Push updates'
34-
run: git push origin HEAD:${GITHUB_HEAD_REF}
26+
if ! git diff --quiet; then
27+
echo "::error::Version was not bumped for this PR. Run './package/version.sh bump ${og_version} && ./package/version.sh sub' locally and commit the result."
28+
git diff
29+
exit 1
30+
fi
3531
3632
pykwasm-code-quality-checks:
3733
name: 'Code Quality Checks'

‎package/version‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.156
1+
0.1.157

‎pykwasm/pyproject.toml‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,13 +4,12 @@ build-backend = "hatchling.build"
44

55
[project]
66
name = "pykwasm"
7-
version = "0.1.156"
7+
version = "0.1.157"
88
description = ""
99
readme = "README.md"
1010
requires-python = "~=3.10"
1111
dependencies = [
12-
"kframework>=7.1.329",
13-
"py-wasm@git+https://github.com/runtimeverification/py-wasm.git@0.3.1"
12+
"kframework>=7.1.329"
1413
]
1514

1615
[[project.authors]]
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
from .module import parse_module
Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
from __future__ import annotations
2+
3+
from typing import TYPE_CHECKING
4+
5+
from .integers import u32
6+
from .utils import WasmParseError, reset
7+
8+
if TYPE_CHECKING:
9+
from .utils import A, InputStream, Parser
10+
11+
12+
def sized(p: Parser[A], s: InputStream) -> A:
13+
size = u32(s)
14+
start_pos = s.tell()
15+
res = p(s)
16+
end_pos = s.tell()
17+
if end_pos - start_pos != size:
18+
raise WasmParseError('Size mismatch')
19+
return res
20+
21+
22+
def parse_n(p: Parser[A], n: int, s: InputStream) -> list[A]:
23+
results = []
24+
for _ in range(n):
25+
x = p(s)
26+
results.append(x)
27+
return results
28+
29+
30+
def list_of(p: Parser[A], s: InputStream) -> list[A]:
31+
n = u32(s)
32+
return parse_n(p, n, s)
33+
34+
35+
def either(ps: list[Parser[A]], s: InputStream) -> A:
36+
for p in ps:
37+
pos = s.tell()
38+
try:
39+
return p(s)
40+
except WasmParseError:
41+
reset(pos, s)
42+
continue
43+
raise WasmParseError('None of the alternatives succeeded')
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
from __future__ import annotations
2+
3+
import struct
4+
from typing import TYPE_CHECKING
5+
6+
from .utils import read_bytes
7+
8+
if TYPE_CHECKING:
9+
from .utils import InputStream
10+
11+
12+
def f32(s: InputStream) -> float:
13+
bs = read_bytes(4, s)
14+
f = struct.unpack('<f', bs)[0]
15+
return f
16+
17+
18+
def f64(s: InputStream) -> float:
19+
bs = read_bytes(8, s)
20+
f = struct.unpack('<d', bs)[0]
21+
return f
Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
from __future__ import annotations
2+
3+
from typing import TYPE_CHECKING
4+
5+
import pykwasm.kwasm_ast as wast
6+
7+
from .integers import u32
8+
from .utils import WasmParseError, read_byte
9+
10+
if TYPE_CHECKING:
11+
from pyk.kast.inner import KInner
12+
13+
from .utils import InputStream
14+
15+
16+
def typeidx(s: InputStream) -> int:
17+
return u32(s)
18+
19+
20+
def funcidx(s: InputStream) -> int:
21+
return u32(s)
22+
23+
24+
def tableidx(s: InputStream) -> int:
25+
return u32(s)
26+
27+
28+
# TODO multi-memory support is future work; the K semantics models a single memory,
29+
# so any reference to a memory other than 0 is rejected instead of mis-executing.
30+
def memidx(s: InputStream) -> int:
31+
x = u32(s)
32+
if x != 0:
33+
raise WasmParseError(f'Multi-memory is not supported. Expected memory index 0, got: {x}')
34+
return x
35+
36+
37+
def globalidx(s: InputStream) -> int:
38+
return u32(s)
39+
40+
41+
def tagidx(s: InputStream) -> int:
42+
return u32(s)
43+
44+
45+
def elemidx(s: InputStream) -> int:
46+
return u32(s)
47+
48+
49+
def dataidx(s: InputStream) -> int:
50+
return u32(s)
51+
52+
53+
def localidx(s: InputStream) -> int:
54+
return u32(s)
55+
56+
57+
def labelidx(s: InputStream) -> int:
58+
return u32(s)
59+
60+
61+
def externidx(s: InputStream) -> KInner:
62+
match read_byte(s):
63+
case 0x00:
64+
return wast.externidx_func(funcidx(s))
65+
case 0x01:
66+
return wast.externidx_table(tableidx(s))
67+
case 0x02:
68+
return wast.externidx_memory(memidx(s))
69+
case 0x03:
70+
return wast.externidx_global(globalidx(s))
71+
case 0x04:
72+
return wast.externidx_tag(tagidx(s))
73+
case x:
74+
raise WasmParseError(f'Invalid externidx descriptor: {x}')

0 commit comments

Comments
 (0)