diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 99e98a9b9..5e8cf2181 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -39,7 +39,7 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: 'Install Poetry' uses: Gr1N/setup-poetry@v8 @@ -53,7 +53,7 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: 'Install Poetry' uses: Gr1N/setup-poetry@v8 @@ -67,23 +67,24 @@ jobs: steps: - name: 'Check out code' uses: actions/checkout@v3 - with: + with: submodules: recursive - name: Login to Docker Hub uses: docker/login-action@v3 with: username: rvdockerhub - password: ${{ secrets.DOCKERHUB_PASSWORD }} + password: ${{ secrets.DOCKERHUB_PASSWORD }} - name: 'Set up Docker' uses: ./.github/actions/with-docker with: container-name: kwasm-ci-integration-${{ github.sha }} - - name: 'Build LLVM Backend and pykwasm' - run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} make -j2 build-llvm + - name: 'Build pykwasm' + run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} poetry -C pykwasm install + - name: 'Build LLVM definition' + run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.llvm - name: 'Build and run integration tests' - run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} make -C pykwasm cov-integration \ - TEST_ARGS='--llvm-dir ../.build/defn/llvm/test-kompiled' + run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} make -C pykwasm cov-integration - name: 'Tear down Docker' if: always() run: | @@ -105,13 +106,15 @@ jobs: with: username: rvdockerhub password: ${{ secrets.DOCKERHUB_PASSWORD }} - + - name: 'Set up Docker' uses: ./.github/actions/with-docker with: container-name: kwasm-ci-parse-${{ github.sha }} - - name: 'Build LLVM Backend and pykwasm' - run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} make -j2 build-llvm RELEASE=true + - name: 'Build pykwasm' + run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} poetry -C pykwasm install + - name: 'Build LLVM definition' + run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.llvm - name: 'Conformance parse' run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} make test-conformance-parse - name: 'Tear down Docker' @@ -129,23 +132,25 @@ jobs: uses: actions/checkout@v3 with: submodules: recursive - + - name: Login to Docker Hub uses: docker/login-action@v3 with: username: rvdockerhub password: ${{ secrets.DOCKERHUB_PASSWORD }} - + - name: 'Set up Docker' uses: ./.github/actions/with-docker with: container-name: kwasm-ci-conformance-${{ github.sha }} - - name: 'Build LLVM Backend' - run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 build-llvm RELEASE=true + - name: 'Build pykwasm' + run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} poetry -C pykwasm install + - name: 'Build LLVM definition' + run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.llvm - name: 'Simple tests' - run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 TEST_CONCRETE_BACKEND=llvm test-simple + run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 test-simple - name: 'Conformance run' - run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 TEST_CONCRETE_BACKEND=llvm test-conformance-supported + run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 test-conformance-supported - name: 'Tear down Docker' if: always() run: | @@ -165,8 +170,10 @@ jobs: uses: ./.github/actions/with-docker with: container-name: kwasm-ci-prove-${{ github.sha }} - - name: 'Build Haskell Backend' - run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} make -j2 build-haskell build-wrc20 + - name: 'Build pykwasm' + run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} poetry -C pykwasm install + - name: 'Build Haskell definitions' + run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.{kwasm-lemmas,wrc20} -j2 - name: 'Prove' run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} make -j6 test-prove - name: 'Tear down Docker' diff --git a/Makefile b/Makefile index dd0fa2db5..c9242d2d1 100644 --- a/Makefile +++ b/Makefile @@ -1,109 +1,29 @@ -# Settings -# -------- - -BUILD_DIR := .build -DEFN_DIR := $(BUILD_DIR)/defn -K_INCLUDE_DIR ?= $(CURDIR) - .PHONY: all \ - build build-llvm build-haskell build-wrc20 \ test test-execution test-simple test-prove \ test-conformance test-conformance-parse test-conformance-supported \ media presentations reports + all: build + # Building Definition # ------------------- -KOMPILE_OPTS := -LLVM_KOMPILE_OPTS := -HASKELL_KOMPILE_OPTS := - -tangle_selector := k - -SOURCE_FILES := data \ - kwasm-lemmas \ - numeric \ - test \ - wasm \ - wasm-text \ - wrc20 -EXTRA_SOURCE_FILES := -ALL_SOURCE_FILES := $(patsubst %, %.md, $(SOURCE_FILES)) $(EXTRA_SOURCE_FILES) - -build: build-llvm build-haskell build-wrc20 - -ifneq (,$(RELEASE)) - KOMPILE_OPTS += -O2 --gen-glr-bison-parser -else - KOMPILE_OPTS += --debug -endif - -ifeq (,$(RELEASE)) - LLVM_KOMPILE_OPTS += -g -endif - -KOMPILE_LLVM := kompile --backend llvm --md-selector "$(tangle_selector)" \ - $(KOMPILE_OPTS) \ - $(addprefix -ccopt ,$(LLVM_KOMPILE_OPTS)) - -KOMPILE_HASKELL := kompile --backend haskell --md-selector "$(tangle_selector)" \ - $(KOMPILE_OPTS) \ - $(HASKELL_KOMPILE_OPTS) \ - --warnings-to-errors - -### LLVM - -llvm_files := $(ALL_SOURCE_FILES) -llvm_main_module := WASM-TEST -llvm_syntax_module := $(llvm_main_module)-SYNTAX -llvm_main_file := test -llvm_dir := $(DEFN_DIR)/llvm/$(llvm_main_file)-kompiled -llvm_kompiled := $(llvm_dir)/interpreter - -build-llvm: $(llvm_kompiled) - -$(llvm_kompiled): $(llvm_files) - $(KOMPILE_LLVM) $(llvm_main_file).md \ - --output-definition $(llvm_dir) -I $(K_INCLUDE_DIR) \ - --main-module $(llvm_main_module) \ - --syntax-module $(llvm_syntax_module) \ - --emit-json - -### Haskell - -haskell_files := $(ALL_SOURCE_FILES) -haskell_main_module := KWASM-LEMMAS -haskell_syntax_module := WASM-TEXT-SYNTAX -haskell_main_file := kwasm-lemmas -haskell_dir := $(DEFN_DIR)/haskell/$(haskell_main_file)-kompiled -haskell_kompiled := $(haskell_dir)/definition.kore - -build-haskell: $(haskell_kompiled) - -$(haskell_kompiled): $(haskell_files) - $(KOMPILE_HASKELL) $(haskell_main_file).md \ - --output-definition $(haskell_dir) -I $(K_INCLUDE_DIR) \ - --main-module $(haskell_main_module) \ - --syntax-module $(haskell_syntax_module) - -### WRC-20 Verification - -wrc20_files := $(haskell_files) wrc20.md -wrc20_main_module := WRC20-LEMMAS -wrc20_syntax_module := WASM-TEXT-SYNTAX -wrc20_main_file := wrc20 -wrc20_dir := $(DEFN_DIR)/haskell/$(wrc20_main_file)-kompiled -wrc20_kompiled := $(wrc20_dir)/definition.kore - -build-wrc20: $(wrc20_kompiled) - -$(wrc20_kompiled): $(wrc20_files) - $(KOMPILE_HASKELL) $(wrc20_main_file).md \ - --output-definition $(wrc20_dir) -I $(K_INCLUDE_DIR) \ - --main-module $(wrc20_main_module) \ - --syntax-module $(wrc20_syntax_module) +POETRY := poetry -C pykwasm + +.PHONY: pykwasm +pykwasm: + $(POETRY) install + +.PHONY: build +build: pykwasm + $(POETRY) run kdist -v build -j3 + +.PHONY: clean +clean: pykwasm + $(POETRY) run kdist clean + # Testing # ------- @@ -114,31 +34,33 @@ CHECK := git --no-pager diff --no-index --ignore-all-space -R TEST_CONCRETE_BACKEND := llvm TEST_SYMBOLIC_BACKEND := haskell +SOURCE_DIR := pykwasm/src/pykwasm/kdist + test: test-execution test-prove # Generic Test Harnesses -tests/%.run: tests/% $(llvm_kompiled) +tests/%.run: tests/% $(TEST) run --backend $(TEST_CONCRETE_BACKEND) $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/success-$(TEST_CONCRETE_BACKEND).out rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out -tests/%.run-term: tests/% $(llvm_kompiled) +tests/%.run-term: tests/% $(TEST) run --backend $(TEST_CONCRETE_BACKEND) $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out grep --after-context=2 "" tests/$*.$(TEST_CONCRETE_BACKEND)-out > tests/$*.$(TEST_CONCRETE_BACKEND)-out-term $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out-term tests/success-k.out rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out-term -tests/%.parse: tests/% $(llvm_kompiled) +tests/%.parse: tests/% $(TEST) kast --backend $(TEST_CONCRETE_BACKEND) $< kast > $@-out rm -rf $@-out -tests/%.prove: tests/% $(haskell_kompiled) - $(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< $(haskell_main_file) +tests/%.prove: tests/% + $(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< kwasm-lemmas -I $(SOURCE_DIR) -tests/proofs/wrc20-spec.k.prove: tests/proofs/wrc20-spec.k $(wrc20_kompiled) - $(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< $(wrc20_main_file) +tests/proofs/wrc20-spec.k.prove: tests/proofs/wrc20-spec.k + $(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< wrc20 -I $(SOURCE_DIR) ### Execution Tests @@ -169,8 +91,10 @@ proof_tests:=$(wildcard tests/proofs/*-spec.k) test-prove: $(proof_tests:=.prove) + # Analysis # -------- + json_build := $(haskell_dir)/parsed.json $(json_build): @@ -179,6 +103,7 @@ $(json_build): graph-imports: $(json_build) kpyk $(haskell_dir) graph-imports + # Presentation # ------------ diff --git a/kbuild.toml b/kbuild.toml deleted file mode 100644 index 3a909ea98..000000000 --- a/kbuild.toml +++ /dev/null @@ -1,13 +0,0 @@ -[project] -name = "wasm-semantics" -version = "1.0.0" -source = "." - -[targets.llvm] -main-file = 'test.md' -main-module = 'WASM-TEST' -backend='llvm' - -[targets.haskell] -main-file = 'kwasm-lemmas.md' -backend='haskell' diff --git a/kwasm b/kwasm index bb3d12ac6..89b499801 100755 --- a/kwasm +++ b/kwasm @@ -8,7 +8,8 @@ fatal() { echo "[FATAL] $@" ; exit 1 ; } kwasm_dir="${KWASM_DIR:-$(dirname $0)}" build_dir="$kwasm_dir/.build" -defn_dir="${KWASM_DEFN_DIR:-$build_dir/defn}" +kdist_dir="$(poetry -C pykwasm run -- kdist which)" +defn_dir="${KWASM_DEFN_DIR:-$kdist_dir}/wasm-semantics" lib_dir="$build_dir/local/lib" k_release_dir="${K_RELEASE:-$kwasm_dir/deps/k/k-distribution/target/release/k}" if [[ ! -f "${k_release_dir}/bin/kompile" ]]; then @@ -45,13 +46,8 @@ preprocess() { # ------- run_krun() { - local additional_run_args - - additional_run_args=() - ! $bug_report || additional_run_args+=(--haskell-backend-command "kore-exec --bug-report $bug_report_name") - preprocess - krun --definition "$backend_dir/test-kompiled" "$run_file" "${additional_run_args[@]}" "$@" + krun --definition "$defn_dir/llvm" "$run_file" "$@" } run_kast() { @@ -59,7 +55,7 @@ run_kast() { preprocess output_mode="${1:-kast}" ; shift - kast --definition "$backend_dir/test-kompiled" "$run_file" --output "$output_mode" "$@" + kast --definition "$defn_dir/llvm" "$run_file" --output "$output_mode" "$@" } run_prove() { @@ -71,7 +67,7 @@ run_prove() { ! $repl || additional_proof_args+=(--debugger) ! $bug_report || additional_proof_args+=(--haskell-backend-command "kore-exec --bug-report $bug_report_name") - kprove --definition "$backend_dir/$def_module-kompiled" -I "$kwasm_dir" "$run_file" "${additional_proof_args[@]}" "$@" + kprove --definition "$defn_dir/$def_module" -I "$kwasm_dir" "$run_file" "${additional_proof_args[@]}" "$@" } # Main @@ -146,8 +142,6 @@ set -- "${args[@]}" ! $repl || [[ "$backend" == "haskell" ]] || fatal "--repl option only available for Haskell backend." ! $bug_report || [[ "$backend" == "haskell" ]] || fatal "--bug-report option only available for Haskell backend." -backend_dir="$defn_dir/$backend" - # get the run file [[ ! -z ${1:-} ]] || usage_fatal "Must supply a file to run on." run_file="$1" ; shift diff --git a/package/version b/package/version index 7db267292..a2e1aa9d9 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.26 +0.1.27 diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index 06e5a2d4b..bcb6e8b60 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -4,12 +4,15 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pykwasm" -version = "0.1.26" +version = "0.1.27" description = "" authors = [ "Runtime Verification, Inc. ", ] +[tool.poetry.plugins.kdist] +wasm-semantics = "pykwasm.kdist.plugin" + [tool.poetry.dependencies] python = "^3.10" cytoolz = "^0.12.1" diff --git a/pykwasm/src/pykwasm/kdist/__init__.py b/pykwasm/src/pykwasm/kdist/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/auxil.md b/pykwasm/src/pykwasm/kdist/auxil.md similarity index 100% rename from auxil.md rename to pykwasm/src/pykwasm/kdist/auxil.md diff --git a/data.md b/pykwasm/src/pykwasm/kdist/data.md similarity index 100% rename from data.md rename to pykwasm/src/pykwasm/kdist/data.md diff --git a/data/int-type.k b/pykwasm/src/pykwasm/kdist/data/int-type.k similarity index 100% rename from data/int-type.k rename to pykwasm/src/pykwasm/kdist/data/int-type.k diff --git a/data/list-int.k b/pykwasm/src/pykwasm/kdist/data/list-int.k similarity index 100% rename from data/list-int.k rename to pykwasm/src/pykwasm/kdist/data/list-int.k diff --git a/data/list-ref.k b/pykwasm/src/pykwasm/kdist/data/list-ref.k similarity index 100% rename from data/list-ref.k rename to pykwasm/src/pykwasm/kdist/data/list-ref.k diff --git a/data/map-int-to-int.k b/pykwasm/src/pykwasm/kdist/data/map-int-to-int.k similarity index 100% rename from data/map-int-to-int.k rename to pykwasm/src/pykwasm/kdist/data/map-int-to-int.k diff --git a/data/sparse-bytes.k b/pykwasm/src/pykwasm/kdist/data/sparse-bytes.k similarity index 100% rename from data/sparse-bytes.k rename to pykwasm/src/pykwasm/kdist/data/sparse-bytes.k diff --git a/data/tools.k b/pykwasm/src/pykwasm/kdist/data/tools.k similarity index 100% rename from data/tools.k rename to pykwasm/src/pykwasm/kdist/data/tools.k diff --git a/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/kwasm-lemmas.md similarity index 100% rename from kwasm-lemmas.md rename to pykwasm/src/pykwasm/kdist/kwasm-lemmas.md diff --git a/numeric.md b/pykwasm/src/pykwasm/kdist/numeric.md similarity index 100% rename from numeric.md rename to pykwasm/src/pykwasm/kdist/numeric.md diff --git a/pykwasm/src/pykwasm/kdist/plugin.py b/pykwasm/src/pykwasm/kdist/plugin.py new file mode 100644 index 000000000..dbf95582d --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/plugin.py @@ -0,0 +1,71 @@ +from __future__ import annotations + +from pathlib import Path +from typing import TYPE_CHECKING + +from pyk.kbuild.utils import k_version +from pyk.kdist.api import Target +from pyk.ktool.kompile import KompileBackend, kompile + +if TYPE_CHECKING: + from collections.abc import Mapping + from typing import Any, Final + + +SOURCE_DIR: Final = Path(__file__).parent + + +class KompileTarget(Target): + _kompile_args: dict[str, Any] + + def __init__(self, kompile_args: Mapping[str, Any]): + self._kompile_args = dict(kompile_args) + + def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None: + kompile( + output_dir=output_dir, + verbose=verbose, + **self._kompile_args, + ) + + def source(self) -> tuple[Path, ...]: + return (SOURCE_DIR,) + + def context(self) -> dict[str, str]: + return {'k-version': k_version().text} + + +__TARGETS__: Final = { + 'llvm': KompileTarget( + { + 'backend': KompileBackend.LLVM, + 'main_file': SOURCE_DIR / 'test.md', + 'main_module': 'WASM-TEST', + 'syntax_module': 'WASM-TEST-SYNTAX', + 'md_selector': 'k', + 'gen_glr_bison_parser': True, + 'opt_level': 2, + 'ccopts': ['-g'], + }, + ), + 'kwasm-lemmas': KompileTarget( + { + 'backend': KompileBackend.HASKELL, + 'main_file': SOURCE_DIR / 'kwasm-lemmas.md', + 'main_module': 'KWASM-LEMMAS', + 'syntax_module': 'WASM-TEXT-SYNTAX', + 'md_selector': 'k', + 'warning_to_error': True, + }, + ), + 'wrc20': KompileTarget( + { + 'backend': KompileBackend.HASKELL, + 'main_file': SOURCE_DIR / 'wrc20.md', + 'main_module': 'WRC20-LEMMAS', + 'syntax_module': 'WASM-TEXT-SYNTAX', + 'md_selector': 'k', + 'warning_to_error': True, + }, + ), +} diff --git a/test.md b/pykwasm/src/pykwasm/kdist/test.md similarity index 100% rename from test.md rename to pykwasm/src/pykwasm/kdist/test.md diff --git a/wasm-text.md b/pykwasm/src/pykwasm/kdist/wasm-text.md similarity index 100% rename from wasm-text.md rename to pykwasm/src/pykwasm/kdist/wasm-text.md diff --git a/wasm.md b/pykwasm/src/pykwasm/kdist/wasm.md similarity index 100% rename from wasm.md rename to pykwasm/src/pykwasm/kdist/wasm.md diff --git a/wrc20.md b/pykwasm/src/pykwasm/kdist/wrc20.md similarity index 100% rename from wrc20.md rename to pykwasm/src/pykwasm/kdist/wrc20.md diff --git a/pykwasm/src/tests/conftest.py b/pykwasm/src/tests/conftest.py index d452bb084..fa3446575 100644 --- a/pykwasm/src/tests/conftest.py +++ b/pykwasm/src/tests/conftest.py @@ -2,6 +2,7 @@ import pytest from pyk.cli.utils import dir_path +from pyk.kdist import kdist from pyk.ktool.krun import KRun from pytest import Config, Parser @@ -16,12 +17,17 @@ def pytest_addoption(parser: Parser) -> None: @pytest.fixture(scope='session') -def llvm_dir(pytestconfig: Config) -> Path: - ldir = pytestconfig.getoption('llvm_dir') - assert isinstance(ldir, Path) - return ldir +def llvm_dir(pytestconfig: Config) -> Path | None: + return pytestconfig.getoption('llvm_dir') @pytest.fixture(scope='session') -def krun_llvm(llvm_dir: Path) -> KRun: +def krun_llvm(llvm_dir: Path | None) -> KRun: + if llvm_dir is not None: + return KRun(llvm_dir) + + llvm_dir = kdist.which('wasm-semantics.llvm') + if not llvm_dir.is_dir(): + raise ValueError('LLVM definition not found. Run make from the repository root, or pass --llvm-dir') + return KRun(llvm_dir)