Building ulm-wasm using kdist (#47)

* ulm-wasm.md: fix #getEntryPoint rule * pykwasm/pyproject.toml: upgraded kframework dependency to be able to use llvm_hidden_visibility * plugin.py: Building ulm-wasm using kdist (without dependencies) * Makefile: changed ulm-wasm target to use kdist
Pi-Squared-Inc · Dec 18, 2024 · c61db98 · c61db98
1 parent c09539c
commit c61db98
Show file tree

Hide file tree

Showing 5 changed files with 81 additions and 63 deletions.
diff --git a/Makefile b/Makefile
@@ -170,45 +170,16 @@ ulm-build: $(ULM_GETH_TARGET)
 
 ### ULM Wasm
 
-ULM_WASM_TYPE = $(if $(ULM_TEST),main,library)
-ULM_WASM_OUT  = $(if $(ULM_TEST),$(ULM_WASM_BIN),$(ULM_WASM_LIB))
-ULM_WASM_SEL  = $(if $(ULM_TEST),k|local,k|remote)
-ULM_LIB_FLAGS = $(if $(ULM_TEST),,-ccopt -L"$(ULM_LIB_DIR)" -ccopt -lulmkllvm -ccopt -shared -ccopt -fPIC -ccopt "$(ULM_HOOKS_DIR)/lang/ulm_language_entry.cpp")
-ULM_HOOK_NMSP = $(if $(ULM_TEST),,ULM)
-
-$(ULM_WASM_TARGET): $(ULM_KRYPTO_TARGET) $(ULM_HOOKS_TARGET) $(ULM_WASM_SRC)
-	kompile \
-	  --hook-namespaces 'KRYPTO $(ULM_HOOK_NMSP)' \
-	  $(if $(DEBUG),-ccopt -O0) \
-	  -ccopt -g \
-	  -ccopt -std=c++20 \
-	  -ccopt -lcrypto \
-	  -ccopt -lsecp256k1 \
-	  -ccopt -lssl \
-	  -ccopt "$(ULM_KRYPTO_TARGET)" \
-	  $(ULM_LIB_FLAGS) \
-	  -ccopt -I"$(ULM_HOOKS_DIR)" \
-	  -ccopt -DULM_LANG_ID=wasm \
-	  --llvm-hidden-visibility \
-	  --llvm-kompile-type $(ULM_WASM_TYPE) \
-	  --llvm-kompile-output "$(ULM_WASM_OUT)" \
-	  -O2 \
-	  -I "$(ULM_HOOKS_DIR)" \
-	  -I "$(ULM_KRYPTO_DIR)/plugin" \
-	  -v \
-	  $(ULM_WASM_MAIN) \
-	  --md-selector "$(ULM_WASM_SEL)" \
-	  --main-module ULM-WASM \
-	  --syntax-module ULM-WASM-SYNTAX \
-	  --emit-json \
-	  $(if $(DEBUG),--debug) \
-	  -o $(ULM_WASM_DIR)
+ULM_WASM_TARGET_NAME = ulm-wasm$(if $(ULM_TEST),-test,)
+
+.PHONY: ulm-wasm
+ulm-wasm: $(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_OUT)" "$(ULM_LIB_DIR)";)
+	$(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)";)
 
-.PHONY: ulm-wasm
-ulm-wasm: $(ULM_WASM_TARGET)
 
 ### ULM Wasm Contract Compiler
 

diff --git a/pykwasm/poetry.lock b/pykwasm/poetry.lock
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
@@ -26,7 +26,7 @@ wasm-semantics = "pykwasm.kdist.plugin"
 python = "^3.10"
 cytoolz = "^0.12.1"
 numpy = "^1.24.2"
-kframework = "7.1.149"
+kframework = "7.1.191"
 py-wasm = { git = "https://github.com/runtimeverification/py-wasm.git", tag="0.2.1" }
 web3 = "7.6.0"
 

diff --git a/pykwasm/src/pykwasm/kdist/plugin.py b/pykwasm/src/pykwasm/kdist/plugin.py
@@ -55,6 +55,47 @@ def deps(self) -> tuple[str]:
         return ('wasm-semantics.source',)
 
 
+def ulm_wasm_args(src_dir: Path, ulm_test: bool = False) -> dict[str, Any]:
+    build_dir = Path(__file__).parent.parent.parent.parent.parent / 'build'
+    ulm_lib_ccopts = []
+    if not ulm_test:
+        ulm_lib_ccopts = [
+            '-L' + str(build_dir / 'lib'),
+            '-lulmkllvm',
+            '-shared',
+            '-fPIC',
+            str(build_dir / 'deps' / 'ulm' / 'kllvm' / 'lang' / 'ulm_language_entry.cpp'),
+        ]
+    return {
+        'backend': PykBackend.LLVM,
+        'hook_namespaces': ['KRYPTO'] + ([] if ulm_test else ['ULM']),
+        'ccopts': [
+            '-g',
+            '-std=c++20',
+            '-lcrypto',
+            '-lsecp256k1',
+            '-lssl',
+            str(build_dir / 'lib' / 'krypto.a'),
+        ]
+        + ulm_lib_ccopts
+        + [
+            '-I' + str(build_dir / 'deps' / 'ulm' / 'kllvm'),
+            '-DULM_LANG_ID=wasm',
+        ],
+        'llvm_hidden_visibility': True,
+        'llvm_kompile_type': 'main' if ulm_test else 'library',
+        'llvm_kompile_output': 'interpreter' if ulm_test else 'libkwasm.so',
+        'opt_level': 2,
+        'include_dirs': [build_dir / 'deps' / 'ulm' / 'kllvm', build_dir / 'deps' / 'plugin' / 'plugin'],
+        'main_file': src_dir / 'wasm-semantics/ulm-wasm.md',
+        'md_selector': 'k|' + ('local' if ulm_test else 'remote'),
+        'main_module': 'ULM-WASM',
+        'syntax_module': 'ULM-WASM-SYNTAX',
+        'emit_json': True,
+        'warnings_to_errors': not ulm_test,
+    }
+
+
 __TARGETS__: Final = {
     'source': SourceTarget(),
     'llvm': KompileTarget(
@@ -90,4 +131,10 @@ def deps(self) -> tuple[str]:
             'warnings_to_errors': True,
         },
     ),
+    'ulm-wasm': KompileTarget(
+        lambda src_dir: ulm_wasm_args(src_dir),
+    ),
+    'ulm-wasm-test': KompileTarget(
+        lambda src_dir: ulm_wasm_args(src_dir, ulm_test=True),
+    ),
 }
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
@@ -184,8 +184,8 @@ In the standalone semantics, the Wasm VM obtains an entrypoint from the configur
 
 ```local
     syntax WasmString ::= #getEntryPoint() [function, total]
-    rule #getEntryPoint() => FUNCNAME
-         [[ <entry> FUNCNAME </entry> ]]
+    rule [[ #getEntryPoint() => FUNCNAME ]]
+         <entry> FUNCNAME </entry>
 ```
 
 In the remote semantics, the Wasm VM has a fixed entrypoint.