diff --git a/.dockerignore b/.dockerignore index 9656787..3982d5c 100644 --- a/.dockerignore +++ b/.dockerignore @@ -2,7 +2,6 @@ **/.kprove* **/.kimp **/dist -**/kdist **/.mypy_cache **/.pytest_cache -**/.venv* \ No newline at end of file +**/.venv* diff --git a/.gitignore b/.gitignore index 92e3b78..2aaf52c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,11 +1,9 @@ .build module-imports-graph.svg -tests/specs/verification-kompiled/* .krun* kimp/.kprove* .kimp *~ docker/.image dist -kdist -*venv \ No newline at end of file +*venv diff --git a/Makefile b/Makefile index 381cff8..c48bd61 100644 --- a/Makefile +++ b/Makefile @@ -13,24 +13,15 @@ docker: docker/Dockerfile -f $< -t runtimeverificationinc/imp-semantics-k:$(K_VERSION) . touch $@ -K_SOURCES = $(wildcard kimp/k-src/*.k) -TARGETS = $(patsubst %.k,.build/%-kompiled,$(notdir $(K_SOURCES))) +build: build-kimp -build: build-llvm build-haskell build-kimp - -build-llvm: have-k $(TARGETS:=-llvm) -build-haskell: have-k $(TARGETS:=-haskell) build-kimp: have-k - $(MAKE) -C kimp build + $(MAKE) -C kimp kdist -.build/%-kompiled-llvm: kimp/k-src/%.k $(K_SOURCES) - $(KOMPILE) --output-definition $@ $< -I kimp/k-src --backend llvm -.build/%-kompiled-haskell: kimp/k-src/%.k $(K_SOURCES) - $(KOMPILE) --output-definition $@ $< -I kimp/k-src --backend haskell +.PHONY: have-k +have-k: FOUND_VERSION=$(shell $(KOMPILE) --version | sed -n -e 's/^K version: *v\?\(.*\)$$/\1/p') .PHONY: have-k -have-k: FOUND_VERSION = $(shell $(KOMPILE) --version \ - | sed -n -e 's/^K version: *v\?\([0-9.]*\)$$/\1/p') have-k: @[ ! -z "$(KOMPILE)" ] || \ (echo "K compiler (kompile) not found (use variable KOMPILE to override)."; exit 1) diff --git a/README.md b/README.md index 1c03821..125bed9 100644 --- a/README.md +++ b/README.md @@ -8,9 +8,10 @@ KIMP consists of two major components: * The K definition of IMP; * The `kimp` command-line tool and Python package, that acts as a frontend to the K definition. + ## Trying it out in `docker` (EASY) -We have prepared a docker image that allows both using `kimp` as-is and hacking on it. +We have prepared a Docker image that allows both using `kimp` as-is and hacking on it. First off, clone the project and step into its directory: @@ -30,29 +31,24 @@ This command will download the docker image and mount the current working direct If everything is up and running, feel free to jump straight to the **Usage** section below. If you don't want to use `docker`, read the next section to build `kimp` manually. + ## Installation instructions (ADVANCED) ### Prerequisites Make sure the K Framework is installed and is available on `PATH`. To install K, follow the official [Quick Start](https://github.com/runtimeverification/k#quick-start) instructions. -To build the `kimp` Ptyhon CLI and library, we recommend using the `poetry` Python build tool. Install `poetry` following the instruction [here](https://python-poetry.org/docs/#installation). +To build the `kimp` Python CLI and library, we recommend using the `poetry` Python build tool. Install `poetry` following the instruction [here](https://python-poetry.org/docs/#installation). + ### Building To build the whole codebase, inclusing the `kimp` CLI and the K definition with both backends, LLVM (for concrete execution) and Haskell (for symbolic execution), execute: + ``` make build ``` -The `kimp` executable is a relatively thin wrapper for a number of generic K tools. These tools need access to the output of the K compiler that were produced at the previous step. The most robust way to point `kimp` to the K compiler output is by setting the following three environment variables: - -``` -export K_VERSION=$(cat deps/k_release) -export KIMP_LLVM_DIR=$(realpath ./kimp/kdist/v${K_VERSION}/llvm) -export KIMP_HASKELL_DIR=$(realpath ./kimp/kdist/v${K_VERSION}/haskell) -export KIMP_K_SRC=$(realpath ./kimp/k-src) -``` ### Installing @@ -69,7 +65,7 @@ Alternatively, you can install `kimp` with `pip` into a virtual environment: ``` python -m venv venv source venv/bin/activate -make -C kimp install # this calls pip for you +pip install kimp ``` Within that virtual environment, you can use `kimp` directly. @@ -83,6 +79,7 @@ Within that virtual environment, you can use `kimp` directly. Run `kimp --help` to see the available commands and their arguments. Let us now give examples for both concrete executing and proving: + ### Preparation The K files need to be compiled before anything can be executed. @@ -91,7 +88,9 @@ The `Makefile` defines a `build` target that will executed the `kompile` command ``` make build ``` -If the `*.k` files in `kimp/k-src` change, this step needs to be repeated. + +If the `*.k` files in `kimp/src/kimp/kdist/imp-semantics` change, this step needs to be repeated. + ### Concrete execution @@ -116,6 +115,7 @@ this program adds up the natural numbers up to 10 and should give the following ``` + ### Symbolic execution The K Framework is equipped with a symbolic execution backend that can be used to prove properties of programs. The properties to prove are formulated as K claims, and are essentially statements that one state always rewrites to another state if certain conditions hold. An example K claim that formulates an inductive invariant about the summation program we've executed before can be found in `examples/specs/imp-sum-spec.k`. Let us ask the prover to check this claim: @@ -127,16 +127,11 @@ kimp prove examples/specs/imp-sum-spec.k IMP-SUM-SPEC sum-spec That command would run for some time and output the symbolic execution trace to a file upon completion. We can pretty-print the trace: ``` -kimp show-kcfg IMP-SUM-SPEC sum-spec +kimp show IMP-SUM-SPEC sum-spec ``` or even explore it interactively in a terminal user interface ``` -kimp view-kcfg IMP-SUM-SPEC sum-spec +kimp view IMP-SUM-SPEC sum-spec ``` - - - - - diff --git a/docker/Dockerfile b/docker/Dockerfile index 7aaeb55..77ad348 100644 --- a/docker/Dockerfile +++ b/docker/Dockerfile @@ -23,15 +23,14 @@ ENV K_VERSION=${K_VERSION} \ force_color_prompt=yes # install poetry -RUN pip install poetry +RUN curl -sSL https://install.python-poetry.org | python3 - # install kimp and set env vars for it COPY --chown=k-user:k-group ./kimp /home/k-user/kimp-src -RUN make -C /home/k-user/kimp-src install && \ - rm -r /home/k-user/kimp-src -ENV KIMP_LLVM_DIR=/home/k-user/workspace/kimp/kdist/v${K_VERSION}/llvm \ - KIMP_HASKELL_DIR=/home/k-user/workspace/kimp/kdist/v${K_VERSION}/haskell \ - KIMP_K_SRC=/home/k-user/workspace/kimp/k-src +RUN poetry -C /home/k-user/kimp-src build && \ + pip install /home/k-user/kimp-src/dist/*.whl && \ + rm -r /home/k-user/kimp-src && \ + kdist --verbose build -j2 WORKDIR /home/k-user/workspace ENTRYPOINT ["fixuid", "-q"] diff --git a/kimp/Makefile b/kimp/Makefile index c9a3ee8..90b7b9d 100644 --- a/kimp/Makefile +++ b/kimp/Makefile @@ -1,29 +1,69 @@ POETRY := poetry POETRY_RUN := $(POETRY) run -default: build + +default: check test-unit + +all: check cov .PHONY: clean clean: - rm -rf dist .mypy_cache .pytest_cache + rm -rf dist .coverage cov-* .mypy_cache .pytest_cache find -type d -name __pycache__ -prune -exec rm -rf {} \; .PHONY: build -build: kbuild-imp +build: + $(POETRY) build .PHONY: poetry-install poetry-install: - $(POETRY) install --without dev + $(POETRY) install -.PHONY: kbuild-imp -kbuild-imp: poetry-install - $(POETRY) run kbuild kompile llvm - $(POETRY) run kbuild kompile haskell -.PHONY: install -install: poetry-install - $(POETRY) build - pip install dist/*.whl +# Kompilation + +kdist: kdist-build + +kdist-build: poetry-install + $(POETRY_RUN) kdist --verbose build -j2 + +kdist-clean: poetry-install + $(POETRY_RUN) kdist clean + + +# Tests + +TEST_ARGS := + +test: test-all + +test-all: poetry-install + $(POETRY_RUN) pytest src/tests --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS) + +test-unit: poetry-install + $(POETRY_RUN) pytest src/tests/unit --maxfail=1 --verbose $(TEST_ARGS) + +test-integration: poetry-install + $(POETRY_RUN) pytest src/tests/integration --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS) + + +# Coverage + +COV_ARGS := + +cov: cov-all + +cov-%: TEST_ARGS += --cov=kimp --no-cov-on-fail --cov-branch --cov-report=term + +cov-all: TEST_ARGS += --cov-report=html:cov-all-html $(COV_ARGS) +cov-all: test-all + +cov-unit: TEST_ARGS += --cov-report=html:cov-unit-html $(COV_ARGS) +cov-unit: test-unit + +cov-integration: TEST_ARGS += --cov-report=html:cov-integration-html $(COV_ARGS) +cov-integration: test-integration + # Checks and formatting diff --git a/kimp/k-src/notes.org b/kimp/k-src/notes.org deleted file mode 100644 index da99077..0000000 --- a/kimp/k-src/notes.org +++ /dev/null @@ -1,38 +0,0 @@ -#+Title: Notes about splitting up the PLDI-IMP semantics into different files - -* Full semantics split up into different levels -General idea: -1. Define expressions without variables -2. then with variables, -3. then follow with statements -4. finally add functions/procedures. - -At each level, provide a configuration (if required) so that krun can -be used to evaluate/run things. - -** Changes to expressions.k -- define without variables to start with - - variables come later in their own modules - - extra file for a first configuration to work with (later not - imported any more) -- leave out special operations #balance and #send - - will be added later for the demo proof if needed -- define KResult sort early (on sort `Value`) - -** Extra module for the configuration -- different language levels bring their own configuration (from - variables onwards) - - configurations in separate modules to avoid getting in the way in - the final language -- rules that access a configuration need to be adjacent to it - - variables.k:VARIABLES module for example -- if the K cell has the same sort, we can avoid the duplication - - statements.k:STATEMENTS module for example - -** Changes to Statements -- functions, expressions, and "return" left out - -- initially had a separate ~Stmts~ block in the syntax (using List construct) - - ~{ SS:Stmts }~ rule requires a hack to have the RHS of sort ~K~ - - inefficient: builds up ~.Stmts ~> .Stmts...~ chains during the execution -- therefore changed to use ~Stmt ::= Stmt Stmt~ (and explicit empty block) diff --git a/kimp/kbuild.toml b/kimp/kbuild.toml deleted file mode 100644 index 41e3a65..0000000 --- a/kimp/kbuild.toml +++ /dev/null @@ -1,16 +0,0 @@ -[project] -name = "imp-semantics" -version = "0.1.0" -source = "k-src" - -[targets.llvm] -backend = "llvm" -main-file = "statements.k" -main-module = "STATEMENTS" -syntax-module = "STATEMENTS-SYNTAX" - -[targets.haskell] -backend = "haskell" -main-file = "imp-verification.k" -main-module = "IMP-VERIFICATION" -syntax-module = "IMP-VERIFICATION-SYNTAX" \ No newline at end of file diff --git a/kimp/pyproject.toml b/kimp/pyproject.toml index 819596d..217599b 100644 --- a/kimp/pyproject.toml +++ b/kimp/pyproject.toml @@ -10,13 +10,16 @@ authors = [ "Runtime Verification, Inc. ", ] +[tool.poetry.scripts] +kimp = "kimp.__main__:main" + +[tool.poetry.plugins.kdist] +imp-semantics = "kimp.kdist.plugin" + [tool.poetry.dependencies] python = "^3.10" kframework = "v7.1.170" -[tool.poetry.scripts] -kimp = "kimp.__main__:main" - [tool.poetry.group.dev.dependencies] autoflake = "*" black = "*" diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py index 945cfd1..f16d59f 100644 --- a/kimp/src/kimp/__main__.py +++ b/kimp/src/kimp/__main__.py @@ -2,7 +2,6 @@ import logging import os -import subprocess from argparse import ArgumentParser from pathlib import Path from tempfile import NamedTemporaryFile @@ -21,33 +20,22 @@ _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' -def find_definiton_dir(target: str) -> Path: +def find_target(target: str) -> Path: """ - Find the kompiled definiton directory for a `kbuild` target target: - * if the KIMP_${target.upper}_DIR is set --- use that - * otherwise ask `kbuild` + Find a `kdist` target: + * if KIMP_${target.upper}_DIR is set --- use that + * otherwise ask `kdist` """ - def kbuild_definition_dir(target: str) -> Path: - proc_result = subprocess.run( - ['poetry', 'run', 'kbuild', 'which', target], - capture_output=True, - ) - if proc_result.returncode: - _LOGGER.critical( - f'Could not find kbuild definition for target {target}. Run kbuild kompile {target}, or specify --definition.' - ) - exit(proc_result.returncode) - else: - return Path(proc_result.stdout.splitlines()[0].decode()) - - env_definition_dir = os.environ.get(f'KIMP_{target.upper()}_DIR') - if env_definition_dir: - path = Path(env_definition_dir).resolve() - _LOGGER.info(f'Using kompiled definiton at {str(path)}') + env_target_dir = os.environ.get(f'KIMP_{target.upper()}_DIR') + if env_target_dir: + path = Path(env_target_dir).resolve() + _LOGGER.info(f'Using target at {path}') return path else: - return kbuild_definition_dir(target) + from pyk.kdist import kdist + + return kdist.which(f'imp-semantics.{target}') def find_k_src_dir() -> Path: @@ -90,7 +78,7 @@ def exec_run( imp_parser = None if definition_dir is None: - definition_dir_path = find_definiton_dir('llvm') + definition_dir_path = find_target('llvm') imp_parser = definition_dir_path / 'parser_Stmt_STATEMENTS-SYNTAX' if not imp_parser.is_file(): imp_parser = gen_glr_parser( @@ -132,8 +120,8 @@ def exec_prove( **kwargs: Any, ) -> None: if definition_dir is None: - definition_dir = str(find_definiton_dir('haskell')) - k_src_dir = str(find_k_src_dir()) + definition_dir = str(find_target('haskell')) + k_src_dir = str(find_target('source') / 'imp-semantics') kimp = KIMP(definition_dir, definition_dir, None) @@ -167,7 +155,7 @@ def exec_show( claim_id: str, **kwargs: Any, ) -> None: - definition_dir = str(find_definiton_dir('haskell')) + definition_dir = str(find_target('haskell')) kimp = KIMP(definition_dir, definition_dir, None) kimp.show_kcfg(spec_module, claim_id) @@ -178,7 +166,7 @@ def exec_view( claim_id: str, **kwargs: Any, ) -> None: - definition_dir = str(find_definiton_dir('haskell')) + definition_dir = str(find_target('haskell')) kimp = KIMP(definition_dir, definition_dir, None) kimp.view_kcfg(spec_module, claim_id) diff --git a/kimp/src/kimp/kdist/__init__.py b/kimp/src/kimp/kdist/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/kimp/k-src/calls.k b/kimp/src/kimp/kdist/imp-semantics/calls.k similarity index 100% rename from kimp/k-src/calls.k rename to kimp/src/kimp/kdist/imp-semantics/calls.k diff --git a/kimp/k-src/expressions.k b/kimp/src/kimp/kdist/imp-semantics/expressions.k similarity index 100% rename from kimp/k-src/expressions.k rename to kimp/src/kimp/kdist/imp-semantics/expressions.k diff --git a/kimp/k-src/imp-verification.k b/kimp/src/kimp/kdist/imp-semantics/imp-verification.k similarity index 100% rename from kimp/k-src/imp-verification.k rename to kimp/src/kimp/kdist/imp-semantics/imp-verification.k diff --git a/kimp/k-src/statements.k b/kimp/src/kimp/kdist/imp-semantics/statements.k similarity index 100% rename from kimp/k-src/statements.k rename to kimp/src/kimp/kdist/imp-semantics/statements.k diff --git a/kimp/k-src/variables.k b/kimp/src/kimp/kdist/imp-semantics/variables.k similarity index 100% rename from kimp/k-src/variables.k rename to kimp/src/kimp/kdist/imp-semantics/variables.k diff --git a/kimp/src/kimp/kdist/plugin.py b/kimp/src/kimp/kdist/plugin.py new file mode 100644 index 0000000..b50ffe2 --- /dev/null +++ b/kimp/src/kimp/kdist/plugin.py @@ -0,0 +1,61 @@ +from __future__ import annotations + +import shutil +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 PykBackend, kompile + +if TYPE_CHECKING: + from collections.abc import Callable, Mapping + from typing import Any, Final + + +class SourceTarget(Target): + SRC_DIR: Final = Path(__file__).parent + + def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None: + shutil.copytree(self.SRC_DIR / 'imp-semantics', output_dir / 'imp-semantics') + + def source(self) -> tuple[Path, ...]: + return (self.SRC_DIR,) + + +class KompileTarget(Target): + _kompile_args: Callable[[Path], Mapping[str, Any]] + + def __init__(self, kompile_args: Callable[[Path], Mapping[str, Any]]): + self._kompile_args = kompile_args + + def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None: + kompile_args = self._kompile_args(deps['imp-semantics.source']) + kompile(output_dir=output_dir, verbose=verbose, **kompile_args) + + def context(self) -> dict[str, str]: + return {'k-version': k_version().text} + + def deps(self) -> tuple[str]: + return ('imp-semantics.source',) + + +__TARGETS__: Final = { + 'source': SourceTarget(), + 'llvm': KompileTarget( + lambda src_dir: { + 'backend': PykBackend.LLVM, + 'main_file': src_dir / 'imp-semantics/statements.k', + 'warnings_to_errors': True, + 'gen_glr_bison_parser': True, + 'opt_level': 3, + }, + ), + 'haskell': KompileTarget( + lambda src_dir: { + 'backend': PykBackend.HASKELL, + 'main_file': src_dir / 'imp-semantics/imp-verification.k', + 'warnings_to_errors': True, + }, + ), +} diff --git a/kimp/src/kimp/kimp.py b/kimp/src/kimp/kimp.py index 24393a4..967585a 100644 --- a/kimp/src/kimp/kimp.py +++ b/kimp/src/kimp/kimp.py @@ -11,7 +11,7 @@ from functools import cached_property from pathlib import Path from tempfile import NamedTemporaryFile -from typing import TYPE_CHECKING, Iterable, Iterator, Optional, Union, final +from typing import TYPE_CHECKING, final from pyk.cli.utils import check_dir_path, check_file_path from pyk.cterm.symbolic import CTermSymbolic @@ -28,11 +28,11 @@ from pyk.utils import single if TYPE_CHECKING: + from collections.abc import Iterable, Iterator from subprocess import CompletedProcess from typing import Final from pyk.cterm.cterm import CTerm - from pyk.kast.outer import KDefinition from pyk.kast.pretty import SymbolTable from pyk.kcfg.kcfg import KCFG, KCFGExtendResult from pyk.kore.rpc import FallbackReason @@ -44,12 +44,6 @@ class ImpSemantics(KCFGSemantics): - definition: KDefinition | None - - def __init__(self, definition: KDefinition | None = None): - super().__init__() - self.definition = definition - def is_terminal(self, c: CTerm) -> bool: k_cell = c.cell('K_CELL') if type(k_cell) is KSequence: @@ -97,7 +91,7 @@ class KIMP: imp_parser: Path proof_dir: Path - def __init__(self, llvm_dir: Union[str, Path], haskell_dir: Union[str, Path], imp_parser: Path | None): + def __init__(self, llvm_dir: str | Path, haskell_dir: str | Path, imp_parser: Path | None): llvm_dir = Path(llvm_dir) check_dir_path(llvm_dir) @@ -127,11 +121,11 @@ def krun(self) -> KRun: def run_program( self, - program_file: Union[str, Path], + program_file: str | Path, *, output: KRunOutput = KRunOutput.NONE, check: bool = True, - temp_file: Optional[Union[str, Path]] = None, + temp_file: str | Path | None = None, depth: int | None, ) -> CompletedProcess: def run(program_file: Path) -> CompletedProcess: @@ -187,7 +181,7 @@ def prove( with legacy_explore( self.kprove, - kcfg_semantics=ImpSemantics(self.kprove.definition), + kcfg_semantics=ImpSemantics(), id=spec_label, ) as kcfg_explore: prover = APRProver( diff --git a/kimp/src/tests/integration/test_integration.py b/kimp/src/tests/integration/test_integration.py index e69de29..c51c3eb 100644 --- a/kimp/src/tests/integration/test_integration.py +++ b/kimp/src/tests/integration/test_integration.py @@ -0,0 +1,2 @@ +def test() -> None: + assert True diff --git a/kimp/src/tests/unit/test_unit.py b/kimp/src/tests/unit/test_unit.py index e69de29..c51c3eb 100644 --- a/kimp/src/tests/unit/test_unit.py +++ b/kimp/src/tests/unit/test_unit.py @@ -0,0 +1,2 @@ +def test() -> None: + assert True