Parse the code section (#66)

* Refactored Instruction parsing * Lint fixes for the code generator * Cleanup * Cleanup * Update pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/int.md Co-authored-by: Stephen Skeirik <[email protected]> * Fix review comments * Fix mem instruction parsing --------- Co-authored-by: Stephen Skeirik <[email protected]>
Pi-Squared-Inc · Jan 28, 2025 · 0d78257 · 0d78257
1 parent 2e01a7a
commit 0d78257
Show file tree

Hide file tree

Showing 70 changed files with 6,736 additions and 118 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -29,6 +29,8 @@ jobs:
         run: make -C pykwasm cov-unit
       - name: 'Run Rust unit-tests'
         run: make rust-tests
+      - name: 'Generated code did not change'
+        run: make generate-code && git status --porcelain=v1 2>/dev/null
 
   conformance-tests:
     name: 'Conformance Tests'

diff --git a/Makefile b/Makefile
@@ -20,25 +20,30 @@ endif
 pykwasm:
 	$(POETRY) install
 
+.PHONY: generate-code
+generate-code: pykwasm
+	$(POETRY_RUN) binary-parser-gen > pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/instr.md
+
 .PHONY: build build-simple build-prove build-wrc20 build-binary-parser-test
-build: pykwasm
+build: pykwasm generate-code
 	$(KDIST) -v build -j3
 
-build-simple: pykwasm
+build-simple: pykwasm generate-code
 	$(KDIST) -v build wasm-semantics.llvm -j3
 
-build-prove: pykwasm
+build-prove: pykwasm generate-code
 	$(KDIST) -v build wasm-semantics.kwasm-lemmas -j3
 
-build-wrc20: pykwasm
+build-wrc20: pykwasm generate-code
 	$(KDIST) -v build wasm-semantics.wrc20 -j3
 
-build-binary-parser-test: pykwasm
+build-binary-parser-test: pykwasm generate-code
 	$(KDIST) -v build wasm-semantics.binary-parser-test -j3
 
 .PHONY: clean
 clean: pykwasm
 	$(KDIST) clean
+	rm build -rf
 
 
 # Building ULM-integrated Definition

diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
@@ -21,6 +21,7 @@ wasm2kast = "pykwasm.wasm2kast:main"
 kwasm = "pykwasm.scripts.kwasm:main"
 kwasm-convert = "pykwasm.scripts.convert:main"
 kwasm-preprocess = "pykwasm.scripts.preprocessor:main"
+binary-parser-gen = "pykwasm.scripts.binary-parser-gen:main"
 
 [tool.poetry.plugins.kdist]
 wasm-semantics = "pykwasm.kdist.plugin"

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md
@@ -22,11 +22,46 @@ module BINARY-PARSER-TEST
 
     rule parseBinary(B:Bytes) => parseModule(B)
 
+    rule addDefnToModule
+            ( false => true
+            , _D:GlobalDefn
+            , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule(GlobalDefn) branch called." )))
+        [owise]
+    rule addDefnToModule
+            ( false => true
+            , _D:TableDefn
+            , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule(TableDefn) branch called." )))
+        [owise]
+    rule addDefnToModule
+            ( false => true
+            , _D:MemoryDefn
+            , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule(MemoryDefn) branch called." )))
+        [owise]
+    rule addDefnToModule
+            ( false => true
+            , _D:ElemDefn
+            , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule(ElemDefn) branch called." )))
+        [owise]
+    rule addDefnToModule
+            ( false => true
+            , _D:DataDefn
+            , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule(DataDefn) branch called." )))
+        [owise]
+    rule addDefnToModule
+            ( false => true
+            , _D:StartDefn
+            , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule(StartDefn) branch called." )))
+        [owise]
+    rule addDefnToModule
+            ( false => true
+            , _D:ExportDefn
+            , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule(ExportDefn) branch called." )))
+        [owise]
     rule addDefnToModule
             ( false => true
             , _D:Defn
             , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule branch called." )))
-        [owise]
+        [priority(250)]
 
 endmodule
 ```
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
@@ -6,14 +6,29 @@ This file defines a Wasm binary parser based on this
 ```k
 
 requires "binary-parsing/base.md"
+requires "binary-parsing/binary-defn-convert.md"
+requires "binary-parsing/block.md"
+requires "binary-parsing/bytes.md"
+requires "binary-parsing/code.md"
+requires "binary-parsing/code-section.md"
 requires "binary-parsing/constant.md"
 requires "binary-parsing/defn.md"
+requires "binary-parsing/float.md"
+requires "binary-parsing/func-section.md"
+requires "binary-parsing/func-section-entry.md"
 requires "binary-parsing/functype.md"
 requires "binary-parsing/globaltype.md"
+requires "binary-parsing/helpers.md"
+requires "binary-parsing/if.md"
 requires "binary-parsing/import.md"
 requires "binary-parsing/import-section.md"
+requires "binary-parsing/instr.md"
+requires "binary-parsing/instr-list.md"
 requires "binary-parsing/int.md"
 requires "binary-parsing/limits.md"
+requires "binary-parsing/locals.md"
+requires "binary-parsing/loop.md"
+requires "binary-parsing/memarg.md"
 requires "binary-parsing/module.md"
 requires "binary-parsing/name.md"
 requires "binary-parsing/resulttype.md"
@@ -22,6 +37,7 @@ requires "binary-parsing/tags.md"
 requires "binary-parsing/type-section.md"
 requires "binary-parsing/valtype.md"
 
+
 module BINARY-PARSER-SYNTAX
   imports BINARY-PARSER-BASE-SYNTAX
   imports WASM
@@ -33,13 +49,28 @@ endmodule
 module BINARY-PARSER  [private]
   imports BINARY-PARSER-MODULE-SYNTAX
 
+  imports BINARY-PARSER-BINARY-DEFN-CONVERT
+  imports BINARY-PARSER-BLOCK
+  imports BINARY-PARSER-BYTES
+  imports BINARY-PARSER-CODE
+  imports BINARY-PARSER-CODE-SECTION
   imports BINARY-PARSER-CONSTANT
+  imports BINARY-PARSER-FLOAT
+  imports BINARY-PARSER-FUNC-SECTION
+  imports BINARY-PARSER-FUNC-SECTION-ENTRY
   imports BINARY-PARSER-FUNCTYPE
   imports BINARY-PARSER-GLOBALTYPE
+  imports BINARY-PARSER-HELPERS
+  imports BINARY-PARSER-IF
   imports BINARY-PARSER-IMPORT
   imports BINARY-PARSER-IMPORT-SECTION
+  imports BINARY-PARSER-INSTR-LIST
+  imports BINARY-PARSER-INSTR
   imports BINARY-PARSER-INT
   imports BINARY-PARSER-LIMITS
+  imports BINARY-PARSER-LOCALS
+  imports BINARY-PARSER-LOOP
+  imports BINARY-PARSER-MEMARG
   imports BINARY-PARSER-MODULE
   imports BINARY-PARSER-NAME
   imports BINARY-PARSER-RESULTTYPE

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/binary-defn-convert.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/binary-defn-convert.md
@@ -0,0 +1,123 @@
+Convert BinaryDefn to Defn.
+
+```k
+module BINARY-PARSER-BINARY-DEFN-CONVERT-SYNTAX
+  imports BINARY-PARSER-BASE-SYNTAX
+  imports BINARY-PARSER-CODE-SYNTAX
+  imports BINARY-PARSER-DEFN-SYNTAX
+  imports BINARY-PARSER-FUNC-SECTION-ENTRY-SYNTAX
+  imports WASM-DATA-COMMON
+
+  syntax DefnsOrError ::= buildFunctionDefns(Defns, BinaryDefnFunctionTypes, BinaryDefnFunctionBodies)  [function, total]
+
+endmodule
+
+module BINARY-PARSER-BINARY-DEFN-CONVERT  [private]
+  imports BINARY-PARSER-BINARY-DEFN-CONVERT-SYNTAX
+  imports BINARY-PARSER-BLOCK-SYNTAX
+  imports BINARY-PARSER-IF-SYNTAX
+  imports BINARY-PARSER-LOOP-SYNTAX
+  imports BINARY-PARSER-INSTR-LIST-SYNTAX
+  imports WASM
+
+  syntax DefnsOrError ::= #buildFunctionDefns1
+                              ( DefnOrError
+                              , Defns
+                              , BinaryDefnFunctionTypes
+                              , BinaryDefnFunctionBodies
+                              )  [function, total]
+                        | #buildFunctionDefns2(Defn, DefnsOrError)  [function, total]
+  rule buildFunctionDefns(_:Defns, .BinaryDefnFunctionTypes, .BinaryDefnFunctionBodies)
+      => .Defns
+  rule buildFunctionDefns
+          ( Ds:Defns
+          , FT:BinaryDefnFunctionType FTs:BinaryDefnFunctionTypes
+          , FB:BinaryDefnFunctionBody FBs:BinaryDefnFunctionBodies
+          )
+      => #buildFunctionDefns1(buildFunctionDefn(Ds, FT, FB), Ds, FTs, FBs)
+  rule buildFunctionDefns(Ds:Defns, FTs:BinaryDefnFunctionTypes, FBs:BinaryDefnFunctionBodies)
+      => parseError("buildFunctionDefns", ListItem(Ds) ListItem(FTs) ListItem(FBs))
+      [owise]
+  rule #buildFunctionDefns1
+          ( D:Defn
+          , Ds:Defns
+          , FTs:BinaryDefnFunctionTypes
+          , FBs:BinaryDefnFunctionBodies
+          )
+      => #buildFunctionDefns2(D, buildFunctionDefns(Ds, FTs, FBs))
+  rule #buildFunctionDefns1
+          ( E:ParseError
+          , _:Defns
+          , _:BinaryDefnFunctionTypes
+          , _:BinaryDefnFunctionBodies
+          )
+      => E
+  rule #buildFunctionDefns2(D:Defn, Ds:Defns) => D Ds
+  rule #buildFunctionDefns2(_:Defn, E:ParseError) => E
+
+  syntax DefnOrError  ::= buildFunctionDefn
+                              ( Defns
+                              , BinaryDefnFunctionType
+                              , BinaryDefnFunctionBody
+                              )  [function, total]
+                        | #buildFunctionDefn1
+                              ( BinaryDefnFunctionType
+                              , locals: VecType
+                              , InstrsOrError
+                              )  [function, total]
+
+  rule buildFunctionDefn
+          ( Ds:Defns
+          , FT:BinaryDefnFunctionType
+          , binaryDefnFunctionBody(Locals:VecType, Is:BinaryInstrs)
+          )
+      => #buildFunctionDefn1(FT, Locals, binaryInstrsToInstrs(Ds, Is))
+  rule #buildFunctionDefn1(binaryDefnFunctionType(TypeIndex:Int), Locals:VecType, Is:Instrs)
+      => #func(TypeIndex, Locals, Is, #meta(, .Map))
+  rule #buildFunctionDefn1(_:BinaryDefnFunctionType, _Locals:VecType, E:ParseError) => E
+
+  syntax InstrsOrError  ::= binaryInstrsToInstrs(Defns, BinaryInstrs)  [function, total]
+                          | #binaryInstrsToInstrs(InstrOrError, InstrsOrError)  [function, total]
+  rule binaryInstrsToInstrs(_:Defns, .BinaryInstrs) => .Instrs
+  rule binaryInstrsToInstrs(Ds:Defns, I:BinaryInstr Is:BinaryInstrs)
+      => #binaryInstrsToInstrs(binaryInstrToInstr(Ds, I), binaryInstrsToInstrs(Ds, Is))
+  rule #binaryInstrsToInstrs(I:Instr, Is:Instrs) => I Is
+  rule #binaryInstrsToInstrs(E:ParseError, _:InstrsOrError) => E
+  rule #binaryInstrsToInstrs(_:Instr, E:ParseError) => E
+
+  syntax InstrOrError ::= binaryInstrToInstr(Defns, BinaryInstr)  [function, total]
+  rule binaryInstrToInstr(_Ds:Defns, I:Instr) => I
+  rule binaryInstrToInstr(Ds:Defns, B:Block)
+      => resolvedBlockToInstr(resolveBlock(Ds, B))
+  rule binaryInstrToInstr(Ds:Defns, loop(B:Block))
+      => resolvedBlockToLoop(resolveBlock(Ds, B))
+  rule binaryInstrToInstr(Ds:Defns, if(B:Block, Is:BinaryInstrs))
+      => resolvedBlockInstrsToIf(resolveBlock(Ds, B), binaryInstrsToInstrs(Ds, Is))
+
+  syntax VecTypeOrError ::= VecType | ParseError
+
+  syntax ResolvedBlockOrError ::= resolvedBlock(VecType, Instrs) | ParseError
+
+  syntax ResolvedBlockOrError ::= resolveBlock(Defns, Block)  [function, total]
+                                | #resolveBlock(VecTypeOrError, InstrsOrError)  [function, total]
+  rule resolveBlock(Ds:Defns, block(T:BlockType, Is:BinaryInstrs))
+      => #resolveBlock(blockTypeToVecType(T, Ds), binaryInstrsToInstrs(Ds, Is))
+  rule #resolveBlock(T:VecType, Is:Instrs) => resolvedBlock(T, Is)
+  rule #resolveBlock(E:ParseError, _:InstrsOrError) => E
+  rule #resolveBlock(_:VecType, E:ParseError) => E
+
+  syntax InstrOrError ::= resolvedBlockToInstr(ResolvedBlockOrError)  [function, total]
+  rule resolvedBlockToInstr(resolvedBlock(T:VecType, Is:Instrs)) => #block(T, Is, .Int)
+  rule resolvedBlockToInstr(E:ParseError) => E
+
+  syntax InstrOrError ::= resolvedBlockToLoop(ResolvedBlockOrError)  [function, total]
+  rule resolvedBlockToLoop(resolvedBlock(T:VecType, Is:Instrs)) => #loop(T, Is, .Int)
+  rule resolvedBlockToLoop(E:ParseError) => E
+
+  syntax InstrOrError ::= resolvedBlockInstrsToIf(ResolvedBlockOrError, InstrsOrError)  [function, total]
+  rule resolvedBlockInstrsToIf(resolvedBlock(T:VecType, Then:Instrs), Else:Instrs) => #if(T, Then, Else, .Int)
+  rule resolvedBlockInstrsToIf(E:ParseError, _:InstrsOrError) => E
+  rule resolvedBlockInstrsToIf(_:ResolvedBlockOrError, E:ParseError) => E
+      [owise]
+endmodule
+```
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/block.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/block.md
@@ -0,0 +1,66 @@
+Parsing [blocks](https://webassembly.github.io/spec/core/binary/instructions.html#control-instructions),
+i.e., a blocktype + instr list.
+
+```k
+
+module BINARY-PARSER-BLOCK-SYNTAX
+  imports BINARY-PARSER-BASE-SYNTAX
+  imports BINARY-PARSER-INSTR-LIST-SYNTAX
+  imports WASM-COMMON-SYNTAX
+  imports WASM-DATA-COMMON
+
+  syntax BlockType ::= "epsilon" | ValType | Int
+  syntax Block ::= block(BlockType, BinaryInstrs)
+  syntax BinaryInstr ::= Block
+  syntax BlockResult ::= blockResult(Block, endsWithElse: Bool, BytesWithIndex) | ParseError
+
+  syntax BlockResult  ::= parseBlock(BytesWithIndex) [function, total]
+
+  syntax VecTypeOrError ::= VecType | ParseError
+  syntax VecTypeOrError ::= blockTypeToVecType(BlockType, Defns)  [function, total]
+endmodule
+
+module BINARY-PARSER-BLOCK  [private]
+  imports BINARY-PARSER-BLOCK-SYNTAX
+  imports BINARY-PARSER-CONSTANT-SYNTAX
+  imports BINARY-PARSER-INSTR-LIST-SYNTAX
+  imports BINARY-PARSER-INT-SYNTAX
+  imports BINARY-PARSER-TAGS
+  imports BINARY-PARSER-VALTYPE-SYNTAX
+
+  syntax BlockResult  ::= #parseBlock1(BlockTypeResult) [function, total]
+                        | #parseBlock2(BlockType, InstrListResult) [function, total]
+  rule parseBlock(BWI:BytesWithIndex) => #parseBlock1(parseBlockType(BWI))
+  rule #parseBlock1(blockTypeResult(BT:BlockType, BWI:BytesWithIndex))
+      => #parseBlock2(BT, parseInstrList(BWI))
+  rule #parseBlock1(E:ParseError) => E
+  rule #parseBlock2(BT:BlockType, instrListResult(Is:BinaryInstrs, EndsWithElse:Bool, BWI:BytesWithIndex))
+      => blockResult(block(BT, Is), EndsWithElse, BWI)
+  rule #parseBlock2(_:BlockType, E:ParseError) => E
+
+  syntax BlockTypeResult ::= blockTypeResult(BlockType, BytesWithIndex) | ParseError
+
+  syntax BlockTypeResult  ::= parseBlockType(BytesWithIndex)  [function, total]
+                            | #parseBlockType1(BytesWithIndex, BytesWithIndexOrError)  [function, total]
+                            | #parseBlockType2(BytesWithIndex, ValTypeResult)  [function, total]
+                            | #parseBlockType3(IntResult)  [function, total]
+  rule parseBlockType(BWI:BytesWithIndex)
+      => #parseBlockType1(BWI, parseConstant(BWI, TYPE_EMPTY))
+  rule #parseBlockType1(_:BytesWithIndex, BWI:BytesWithIndex)
+      => blockTypeResult(epsilon, BWI:BytesWithIndex)
+  rule #parseBlockType1(BWI:BytesWithIndex, _:ParseError)
+      => #parseBlockType2(BWI, parseValType(BWI))
+  rule #parseBlockType2(_:BytesWithIndex, valTypeResult(VT:ValType, BWI:BytesWithIndex))
+      => blockTypeResult(VT, BWI)
+  rule #parseBlockType2(BWI:BytesWithIndex, _:ParseError)
+      => #parseBlockType3(parseLeb128SInt(BWI))
+  rule #parseBlockType3(intResult(Value:Int, BWI:BytesWithIndex))
+      => blockTypeResult(Value, BWI)
+  rule #parseBlockType3(E:ParseError) => E
+
+  rule blockTypeToVecType(epsilon, _:Defns) => [ .ValTypes ]
+  rule blockTypeToVecType(ValType, _:Defns) => [ ValType .ValTypes ]
+  rule blockTypeToVecType(Index:Int, Ds::Defns) => parseError("blockTypeToVecType: unimplemented", ListItem(Index) ListItem(Ds))
+
+endmodule
+```
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/bytes.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/bytes.md
@@ -0,0 +1,34 @@
+Extract a number of bytes from the buffer.
+
+```k
+module BINARY-PARSER-BYTES-SYNTAX
+  imports BINARY-PARSER-BASE-SYNTAX
+
+  syntax BytesResult ::= bytesResult(Bytes, BytesWithIndex) | ParseError
+  syntax BytesResult ::= parseBytes(BytesWithIndex, Int)  [function, total]
+
+  syntax BytesWithIndexOrError ::= ignoreBytes(BytesWithIndex, Int)  [function, total]
+endmodule
+
+module BINARY-PARSER-BYTES  [private]
+  imports BINARY-PARSER-BYTES-SYNTAX
+
+  rule parseBytes(bwi(Buffer:Bytes, Index:Int), Count:Int)
+      => bytesResult
+            ( substrBytes(Buffer, Index, Index +Int Count)
+            , bwi(Buffer, Index +Int Count)
+            )
+      requires Index +Int Count <=Int lengthBytes(Buffer)
+  rule parseBytes(bwi(Buffer:Bytes, Index:Int), Count:Int)
+      => parseError("parseBytes", ListItem(lengthBytes(Buffer)) ListItem(Index) ListItem(Count) ListItem(Buffer))
+      [owise]
+
+  rule ignoreBytes(BWI:BytesWithIndex, Count:Int)
+      => #ignoreBytes(parseBytes(BWI, Count))
+
+  syntax BytesWithIndexOrError ::= #ignoreBytes(BytesResult)  [function, total]
+  rule #ignoreBytes(bytesResult(_:Bytes, BWI:BytesWithIndex)) => BWI
+  rule #ignoreBytes(E:ParseError) => E
+endmodule
+
+```