Add tests for parsing wasm types

Pi-Squared-Inc · Jan 14, 2025 · 18a6791 · 18a6791
1 parent fa7e39c
commit 18a6791
Show file tree

Hide file tree

Showing 29 changed files with 826 additions and 3 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,5 +1,6 @@
 /.kwasm-logs/
 /tests/*/*-out
+/tmp
 
 *.pdf
 *.sty

diff --git a/Makefile b/Makefile
@@ -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
 
@@ -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
@@ -271,6 +274,31 @@ 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 TODO: Figure out how to depend on this without rerunning the test each time.
+	mkdir -p build/binary-parsing
+	wat2wasm $< -o $@.wasm
+	cat $@.wasm \
+			| xxd -ps \
+			| 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)
+
 ### Conformance Tests
 
 conformance_tests:=$(wildcard tests/wasm-tests/test/core/*.wast)

diff --git a/pykwasm/src/pykwasm/kdist/plugin.py b/pykwasm/src/pykwasm/kdist/plugin.py
@@ -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,
+        },
+    ),
 }
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md
@@ -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
+```
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
@@ -650,7 +650,7 @@ endmodule
 ```
 
 ```k
-module BINARY-PARSER [private]
+module BINARY-PARSER //[private]
   imports BINARY-PARSER-DATA
   imports LIST
   imports STRING
@@ -956,7 +956,7 @@ module BINARY-PARSER [private]
       requires Index +Int lengthBytes(Constant) <=Int lengthBytes(Buffer)
           andBool substrBytes(Buffer, Index, Index +Int lengthBytes(Constant)) ==K Constant
   rule parseConstant(bwi(Buffer:Bytes, Index:Int), Constant:Bytes)
-      => parseError("parseConstant", ListItem(Buffer) ListItem(lengthBytes(Buffer)) ListItem(Index) ListItem(Constant))
+      => parseError("parseConstant", ListItem(lengthBytes(Buffer)) ListItem(Index) ListItem(Constant) ListItem(Buffer))
       [owise]
   rule parseConstant(E:ParseError, _:Bytes) => E
 

diff --git a/tests/binary-parsing/empty-module.wast b/tests/binary-parsing/empty-module.wast
@@ -0,0 +1,2 @@
+(module $mymodule
+)
diff --git a/tests/binary-parsing/empty-module.wast.out b/tests/binary-parsing/empty-module.wast.out
@@ -0,0 +1,65 @@
+<generatedTop>
+  <k>
+    #module (... types: .EmptyStmts , funcs: .EmptyStmts , tables: .EmptyStmts , mems: .EmptyStmts , globals: .EmptyStmts , elem: .EmptyStmts , data: .EmptyStmts , start: .EmptyStmts , importDefns: .EmptyStmts , exports: .EmptyStmts , metadata: #meta (... id:  , funcIds: .Map , filename: .String ) ) ~> .K
+  </k>
+  <wasm>
+    <instrs>
+      .K
+    </instrs>
+    <valstack>
+      .ValStack
+    </valstack>
+    <curFrame>
+      <locals>
+        .List
+      </locals>
+      <curModIdx>
+        .Int
+      </curModIdx>
+    </curFrame>
+    <moduleRegistry>
+      .Map
+    </moduleRegistry>
+    <moduleIds>
+      .Map
+    </moduleIds>
+    <moduleInstances>
+      .ModuleInstCellMap
+    </moduleInstances>
+    <nextModuleIdx>
+      0
+    </nextModuleIdx>
+    <mainStore>
+      <funcs>
+        .FuncDefCellMap
+      </funcs>
+      <nextFuncAddr>
+        0
+      </nextFuncAddr>
+      <tabs>
+        .TabInstCellMap
+      </tabs>
+      <nextTabAddr>
+        0
+      </nextTabAddr>
+      <mems>
+        .List
+      </mems>
+      <globals>
+        .GlobalInstCellMap
+      </globals>
+      <nextGlobAddr>
+        0
+      </nextGlobAddr>
+      <elems>
+        .ElemInstCellMap
+      </elems>
+      <nextElemAddr>
+        0
+      </nextElemAddr>
+    </mainStore>
+    <deterministicMemoryGrowth>
+      true
+    </deterministicMemoryGrowth>
+  </wasm>
+</generatedTop>
diff --git a/tests/binary-parsing/failing b/tests/binary-parsing/failing
@@ -0,0 +1 @@
+tests/binary-parsing/type-param-v128.wast
diff --git a/tests/binary-parsing/type-empty.wast b/tests/binary-parsing/type-empty.wast
@@ -0,0 +1,3 @@
+(module $mymodule
+  (type (;0;) (func))
+)
diff --git a/tests/binary-parsing/type-empty.wast.out b/tests/binary-parsing/type-empty.wast.out
@@ -0,0 +1,65 @@
+<generatedTop>
+  <k>
+    #module (... types: #type (... type: [ .ValTypes ] -> [ .ValTypes ] , metadata:  )  .EmptyStmts , funcs: .EmptyStmts , tables: .EmptyStmts , mems: .EmptyStmts , globals: .EmptyStmts , elem: .EmptyStmts , data: .EmptyStmts , start: .EmptyStmts , importDefns: .EmptyStmts , exports: .EmptyStmts , metadata: #meta (... id:  , funcIds: .Map , filename: .String ) ) ~> .K
+  </k>
+  <wasm>
+    <instrs>
+      .K
+    </instrs>
+    <valstack>
+      .ValStack
+    </valstack>
+    <curFrame>
+      <locals>
+        .List
+      </locals>
+      <curModIdx>
+        .Int
+      </curModIdx>
+    </curFrame>
+    <moduleRegistry>
+      .Map
+    </moduleRegistry>
+    <moduleIds>
+      .Map
+    </moduleIds>
+    <moduleInstances>
+      .ModuleInstCellMap
+    </moduleInstances>
+    <nextModuleIdx>
+      0
+    </nextModuleIdx>
+    <mainStore>
+      <funcs>
+        .FuncDefCellMap
+      </funcs>
+      <nextFuncAddr>
+        0
+      </nextFuncAddr>
+      <tabs>
+        .TabInstCellMap
+      </tabs>
+      <nextTabAddr>
+        0
+      </nextTabAddr>
+      <mems>
+        .List
+      </mems>
+      <globals>
+        .GlobalInstCellMap
+      </globals>
+      <nextGlobAddr>
+        0
+      </nextGlobAddr>
+      <elems>
+        .ElemInstCellMap
+      </elems>
+      <nextElemAddr>
+        0
+      </nextElemAddr>
+    </mainStore>
+    <deterministicMemoryGrowth>
+      true
+    </deterministicMemoryGrowth>
+  </wasm>
+</generatedTop>
diff --git a/tests/binary-parsing/type-param-externref.wast b/tests/binary-parsing/type-param-externref.wast
@@ -0,0 +1,3 @@
+(module $mymodule
+  (type (;0;) (func (param externref)))
+)
diff --git a/tests/binary-parsing/type-param-externref.wast.out b/tests/binary-parsing/type-param-externref.wast.out
@@ -0,0 +1,65 @@
+<generatedTop>
+  <k>
+    #module (... types: #type (... type: [ externref  .ValTypes ] -> [ .ValTypes ] , metadata:  )  .EmptyStmts , funcs: .EmptyStmts , tables: .EmptyStmts , mems: .EmptyStmts , globals: .EmptyStmts , elem: .EmptyStmts , data: .EmptyStmts , start: .EmptyStmts , importDefns: .EmptyStmts , exports: .EmptyStmts , metadata: #meta (... id:  , funcIds: .Map , filename: .String ) ) ~> .K
+  </k>
+  <wasm>
+    <instrs>
+      .K
+    </instrs>
+    <valstack>
+      .ValStack
+    </valstack>
+    <curFrame>
+      <locals>
+        .List
+      </locals>
+      <curModIdx>
+        .Int
+      </curModIdx>
+    </curFrame>
+    <moduleRegistry>
+      .Map
+    </moduleRegistry>
+    <moduleIds>
+      .Map
+    </moduleIds>
+    <moduleInstances>
+      .ModuleInstCellMap
+    </moduleInstances>
+    <nextModuleIdx>
+      0
+    </nextModuleIdx>
+    <mainStore>
+      <funcs>
+        .FuncDefCellMap
+      </funcs>
+      <nextFuncAddr>
+        0
+      </nextFuncAddr>
+      <tabs>
+        .TabInstCellMap
+      </tabs>
+      <nextTabAddr>
+        0
+      </nextTabAddr>
+      <mems>
+        .List
+      </mems>
+      <globals>
+        .GlobalInstCellMap
+      </globals>
+      <nextGlobAddr>
+        0
+      </nextGlobAddr>
+      <elems>
+        .ElemInstCellMap
+      </elems>
+      <nextElemAddr>
+        0
+      </nextElemAddr>
+    </mainStore>
+    <deterministicMemoryGrowth>
+      true
+    </deterministicMemoryGrowth>
+  </wasm>
+</generatedTop>
diff --git a/tests/binary-parsing/type-param-f32.wast b/tests/binary-parsing/type-param-f32.wast
@@ -0,0 +1,3 @@
+(module $mymodule
+  (type (;0;) (func (param f32)))
+)