Parse the raw binary wasm code for ULM (#68)

* Parse the raw binary wasm code for ULM * Cleanup * Explain that parsing errors are not cleared from the k cell
Pi-Squared-Inc · Jan 30, 2025 · 089a630 · 089a630
1 parent 0bcb309
commit 089a630
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 34 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -109,8 +109,6 @@ jobs:
         run: docker exec -u user kwasm-ci-erc20-${GITHUB_SHA} poetry -C pykwasm install
       - name: 'Build ulm-wasm'
         run: docker exec -u user kwasm-ci-erc20-${GITHUB_SHA} bash -c "CXX=clang++-16 make ulm-wasm"
-      - name: 'Build ulm-contract-compiler'
-        run: docker exec -u user kwasm-ci-erc20-${GITHUB_SHA} bash -c "CXX=clang++-16 make ulm-contract-compiler"
       - name: 'Build ulm-build'
         run: docker exec -u user kwasm-ci-erc20-${GITHUB_SHA} bash -c "CXX=clang++-16 make ulm-build"
       - name: 'Build erc20-bin'

diff --git a/Makefile b/Makefile
@@ -63,8 +63,6 @@ ULM_WASM_TARGET=$(ULM_LIB_DIR)/$(ULM_WASM_LIB)
 ULM_WASM_MAIN=$(ULM_WASM_SRC_DIR)/ulm-wasm.md
 ULM_WASM_SRC=$(wildcard $(ULM_WASM_SRC_DIR)/*.md $(ULM_WASM_SRC_DIR)/data/*.k)
 
-ULM_WASM_COMPILER_TARGET=$(ULM_BUILD_DIR)/ulm-contract-compiler
-
 ## Depedencies
 
 ULM_KRYPTO_DIR=$(ULM_DEP_DIR)/plugin
@@ -186,27 +184,9 @@ ulm-wasm: $(ULM_WASM_TARGET)
 $(ULM_WASM_TARGET): $(ULM_KRYPTO_TARGET) $(ULM_HOOKS_TARGET) $(ULM_WASM_SRC) pykwasm
 	$(KDIST) -v build wasm-semantics.$(ULM_WASM_TARGET_NAME) -j3
 	$(eval ULM_WASM_DIR := $(shell $(KDIST) which wasm-semantics.$(ULM_WASM_TARGET_NAME)))
-	kore-rich-header "$(ULM_WASM_DIR)/definition.kore" -o "$(ULM_WASM_DIR)/header.bin"
 	$(if $(ULM_TEST),,cp "$(ULM_WASM_DIR)/$(ULM_WASM_LIB)" "$(ULM_LIB_DIR)";)
-	$(if $(ULM_TEST),,cp "$(ULM_WASM_DIR)/header.bin"      "$(ULM_LIB_DIR)";)
-
 
-### ULM Wasm Contract Compiler
 
-$(ULM_WASM_COMPILER_TARGET): $(ULM_WASM_TARGET)
-	$(CXX) "$(ULM_HOOKS_DIR)/emit_contract_bytes.cpp" \
-	  -I "$(ULM_KF_INCLUDE_DIR)" \
-	  -I "$(ULM_KF_INCLUDE_DIR)/kllvm" \
-	  -std=c++20 \
-	  -DULM_LANG_ID=wasm \
-	  -Wno-return-type-c-linkage \
-	  -L"$(ULM_LIB_DIR)" \
-	  -lulmkllvm \
-	  -lkwasm \
-	  -o "$(ULM_WASM_COMPILER_TARGET)"
-
-.PHONY: ulm-contract-compiler
-ulm-contract-compiler: $(ULM_WASM_COMPILER_TARGET)
 
 ERC20_DIR=tests/ulm/erc20/rust
 ERC20_SRC=$(shell find "$(ERC20_DIR)" -type f -a '(' -name '*.rs' -or -name '*.toml' -or -name '*.lock' ')')
@@ -223,10 +203,9 @@ $(ERC20_WASM_TARGET): $(ERC20_SRC) $(ERC20_BUILD_DIR)
 	cd $(ERC20_DIR) && cargo build --target=wasm32-unknown-unknown --release
 	cp $(ERC20_DIR)/target/wasm32-unknown-unknown/release/erc20.wasm $@
 
-$(ERC20_BIN_TARGET): $(ERC20_WASM_TARGET) $(ULM_WASM_COMPILER_TARGET) $(ULM_WASM_TARGET)
-	$(eval ULM_WASM_DIR := $(shell $(KDIST) which wasm-semantics.$(ULM_WASM_TARGET_NAME)))
-	poetry -C pykwasm run wasm2kore $(ULM_WASM_DIR) $< $(ERC20_BUILD_DIR)/erc20.kore
-	scripts/compile-contract $(ERC20_BUILD_DIR)/erc20.kore > $@
+$(ERC20_BIN_TARGET): $(ERC20_WASM_TARGET)
+	echo -n "7761736D" > $@
+	xxd -p $< | tr -d '\n' >> $@
 
 .PHONY: erc20-bin
 erc20-bin: $(ERC20_BIN_TARGET)

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
@@ -49,8 +49,8 @@ module BINARY-PARSER-SYNTAX
   imports BINARY-PARSER-BASE-SYNTAX
   imports WASM
 
-  syntax ModuleOrError ::= ModuleDecl | ParseError
-  syntax ModuleOrError ::= parseModule(Bytes)  [function, total]
+  syntax ModuleDeclOrError ::= ModuleDecl | ParseError
+  syntax ModuleDeclOrError ::= parseModule(Bytes)  [function, total]
 endmodule
 
 module BINARY-PARSER  [private]
@@ -95,7 +95,7 @@ module BINARY-PARSER  [private]
 
   rule parseModule(B:Bytes) => checkAllBytesParsed(parseModule(bwi(B, 0)))
 
-  syntax ModuleOrError ::= checkAllBytesParsed(ModuleResult)  [function, total]
+  syntax ModuleDeclOrError ::= checkAllBytesParsed(ModuleResult)  [function, total]
   rule checkAllBytesParsed(moduleResult(M, bwi(B:Bytes, Index:Int))) => M requires Index ==Int lengthBytes(B)
   rule checkAllBytesParsed(E:ParseError) => E
 

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/module.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/module.md
@@ -34,7 +34,7 @@ module BINARY-PARSER-MODULE  [private]
 
   syntax ModuleResult ::= parseModuleSections(UnparsedSectionsResult)  [function, total]
                         | #parseModuleSections1(ParsedSectionsResult, BytesWithIndex)  [function, total]
-                        | #parseModuleSections2(ModuleOrError, BytesWithIndex)  [function, total]
+                        | #parseModuleSections2(ModuleDeclOrError, BytesWithIndex)  [function, total]
 
   rule parseModuleSections(unparsedSectionsResult(S:UnparsedSections, BWI:BytesWithIndex))
       => #parseModuleSections1(parseSections(S), BWI)
@@ -71,8 +71,8 @@ module BINARY-PARSER-MODULE  [private]
       => moduleResult(M, BWI)
   rule #parseModuleSections2(E:ParseError, _:BytesWithIndex) => E
 
-  syntax ModuleOrError ::= addSectionsToModule(Sections, ModuleAndFunctions)  [function, total]
-  syntax ModuleOrError ::= #addSectionsToModule(Sections, ModuleAndFunctions)  [function, total]
+  syntax ModuleDeclOrError ::= addSectionsToModule(Sections, ModuleAndFunctions)  [function, total]
+  syntax ModuleDeclOrError ::= #addSectionsToModule(Sections, ModuleAndFunctions)  [function, total]
   rule addSectionsToModule
           ( .Sections
           , moduleAndFunctions
@@ -104,7 +104,7 @@ module BINARY-PARSER-MODULE  [private]
 
   syntax DefnsOrErrorList ::= List{DefnsOrError, ""}
 
-  syntax ModuleOrError ::= addOrderedDefnsOrErrorToModule(ModuleDecl, DefnsOrErrorList)  [function, total]
+  syntax ModuleDeclOrError ::= addOrderedDefnsOrErrorToModule(ModuleDecl, DefnsOrErrorList)  [function, total]
   rule addOrderedDefnsOrErrorToModule(M:ModuleDecl, .DefnsOrErrorList) => M
   rule addOrderedDefnsOrErrorToModule(M:ModuleDecl, D:Defns Ds:DefnsOrErrorList)
       // We need to reverse the defns because addDefnsToModule adds then in

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
@@ -2,6 +2,7 @@
 requires "wasm.md"
 requires "ulm.k"
 requires "plugin/krypto.md"
+requires "binary-parser.md"
 ```
 
 ```k
@@ -33,6 +34,8 @@ endmodule
 
 ```k
 module ULM-WASM
+    imports BINARY-PARSER
+    imports BINARY-PARSER-SYNTAX
     imports ULM-WASM-SYNTAX
     imports ULM
 ```
@@ -52,8 +55,11 @@ The WASM VM must decode the input program:
 
 2.  In the remote ULM-integrated VM case, a specialized, hooked byte decoder is used.
 
+    If parsing fails, we leave the result at the top of the `<k>` cell, which
+    will help debugging.
     ```remote
-    syntax ModuleDecl ::= decodePgm(Bytes) [function, hook(ULM.decode)]
+    syntax ModuleDeclOrError ::= decodePgm(Bytes) [function, total]
+    rule decodePgm(B:Bytes) => parseModule(B)
     ```
 
 Configuration