Skip to content

Commit

Permalink
Parse modules + type sections (#59)
Browse files Browse the repository at this point in the history
* Module parsing

* Parse types

* Add tests for parsing wasm types

* Makefile fixes

* Run binary parsing tests on github

* Some documentation
  • Loading branch information
virgil-serbanuta authored Jan 16, 2025
1 parent 7f0a0dd commit 3715249
Show file tree
Hide file tree
Showing 31 changed files with 1,195 additions and 22 deletions.
3 changes: 2 additions & 1 deletion .github/actions/with-docker/Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,8 @@ RUN apt-get update \
pandoc \
python3 \
python3-pip \
wabt
wabt \
xxd

ARG USER_ID=1000
ARG GROUP_ID=1000
Expand Down
2 changes: 2 additions & 0 deletions .github/workflows/test-pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,8 @@ jobs:
run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 test-conformance-supported
- name: 'Run conformance tests: parse'
run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make test-conformance-parse
- name: 'Run conformance tests: binary parse'
run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make test-binary-parsing
- name: 'Tear down Docker'
if: always()
run: |
Expand Down
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
/.kwasm-logs/
/tests/*/*-out
/tmp

*.pdf
*.sty
Expand Down
33 changes: 32 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ endif
pykwasm:
$(POETRY) install

.PHONY: build build-simple build-prove build-wrc20
.PHONY: build build-simple build-prove build-wrc20 build-binary-parser-test
build: pykwasm
$(KDIST) -v build -j3

Expand All @@ -33,6 +33,9 @@ build-prove: pykwasm
build-wrc20: pykwasm
$(KDIST) -v build wasm-semantics.wrc20 -j3

build-binary-parser-test: pykwasm
$(KDIST) -v build wasm-semantics.binary-parser-test -j3

.PHONY: clean
clean: pykwasm
$(KDIST) clean
Expand Down Expand Up @@ -271,6 +274,34 @@ simple_tests_passing := $(filter-out $(simple_tests_failing), $(simple_tests))

test-simple: $(simple_tests_passing:=.run)

### Parsing Tests

build/binary-parsing/%.bprun: tests/binary-parsing/% build-binary-parser-test
mkdir -p build/binary-parsing
wat2wasm $< -o $@.wasm
cat $@.wasm \
| xxd -ps \
| tr -d '\n' \
| sed 's/\(..\)/\\x\1/g' \
| sed 's/^\(.*\)/\\dv{SortBytes{}}("\1")/' \
> $@.kore
krun \
--parser cat \
$@.kore \
--definition $(shell $(KDIST) which wasm-semantics.binary-parser-test) \
> $@-out
$(CHECK) $@-out $<.out
touch $@

binary_parsing_tests := $(wildcard tests/binary-parsing/*.wast)
binary_parsing_failing := $(shell cat tests/binary-parsing/failing)
binary_parsing_passing := $(filter-out $(binary_parsing_failing), $(binary_parsing_tests))
binary_parsing_results := $(patsubst tests/binary-parsing/%, build/binary-parsing/%.bprun, $(binary_parsing_passing))

test-binary-parsing: $(binary_parsing_results)

.PHONY: test-binary-parsing

### Conformance Tests

conformance_tests:=$(wildcard tests/wasm-tests/test/core/*.wast)
Expand Down
10 changes: 10 additions & 0 deletions pykwasm/src/pykwasm/kdist/plugin.py
Original file line number Diff line number Diff line change
Expand Up @@ -137,4 +137,14 @@ def ulm_wasm_args(src_dir: Path, ulm_test: bool = False) -> dict[str, Any]:
'ulm-wasm-test': KompileTarget(
lambda src_dir: ulm_wasm_args(src_dir, ulm_test=True),
),
'binary-parser-test': KompileTarget(
lambda src_dir: {
'backend': PykBackend.LLVM,
'main_file': src_dir / 'wasm-semantics/binary-parser-test.md',
'main_module': 'BINARY-PARSER-TEST',
'syntax_module': 'BINARY-PARSER-TEST-SYNTAX',
'md_selector': 'k',
'warnings_to_errors': True,
},
),
}
32 changes: 32 additions & 0 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
```k
requires "binary-parser.md"
requires "wasm.md"
module BINARY-PARSER-TEST-SYNTAX
endmodule
module BINARY-PARSER-TEST
imports BINARY-PARSER-TEST-SYNTAX
imports BINARY-PARSER
syntax KItem ::= parseBinary(Bytes)
configuration
<k> parseBinary($PGM) </k>
<wasm/>
rule parseBinary(B:Bytes) => parseModule(B)
rule addDefnToModule
( false => true
, _D:Defn
, #module(... metadata: _ => #meta (... id: , funcIds: .Map , filename: "error: test addDefnToModule branch called." )))
[owise]
rule parseSection(U:UnparsedSection)
=> parseError("parseSection test default", ListItem(U))
[owise]
endmodule
```
Loading

0 comments on commit 3715249

Please sign in to comment.