diff --git a/README.md b/README.md index 125bed9..9a762b9 100644 --- a/README.md +++ b/README.md @@ -11,23 +11,40 @@ KIMP consists of two major components: ## Trying it out in `docker` (EASY) -We have prepared a Docker image that allows both using `kimp` as-is and hacking on it. +The project defines a Docker image that allows both using `kimp` as-is and hacking on it. First off, clone the project and step into its directory: ``` git clone https://github.com/runtimeverification/imp-semantics cd imp-semantics -git checkout bob2024 ``` -Use the following to start a container with an interactive shell: +Then, build the image: ``` -docker run --rm -it -v "$PWD":/home/k-user/workspace -u $(id -u):$(id -g) geo2a/bob24:latest /bin/bash +make docker TAG=imp-semantics:latest ``` -This command will download the docker image and mount the current working directory under `~/workspace`, ensuring you can work on the examples and have them transparently available in the container. +Run the following command to start a container with an interactive shell: + +``` +docker run --rm -it imp-semantics:latest /bin/bash +``` + +The `examples` folder, as well as a test script `smoke-tests.sh` is already copied into the workspace. +You can run the tests with: + +``` +./smoke-test.sh +``` + +To work with files from the host, run the countainer with a volume mounted. +For example, the following command starts the container and mounts the current working directory under `~/workspace`, ensuring you can work on the examples and have them transparently available in the container. + +``` +docker run --rm -it -v "$PWD":/home/k-user/workspace -u $(id -u):$(id -g) imp-semantics:latest /bin/bash +``` 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. diff --git a/kimp/src/kimp/__init__.py b/kimp/src/kimp/__init__.py index e69de29..4599fbe 100644 --- a/kimp/src/kimp/__init__.py +++ b/kimp/src/kimp/__init__.py @@ -0,0 +1 @@ +from .kimp import KImp diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py index 9b83b36..5278870 100644 --- a/kimp/src/kimp/__main__.py +++ b/kimp/src/kimp/__main__.py @@ -1,54 +1,21 @@ from __future__ import annotations import logging -import os from argparse import ArgumentParser -from pathlib import Path from typing import TYPE_CHECKING, Any, Final -from pyk.cli.utils import dir_path, file_path +from pyk.cli.utils import file_path from .kimp import KImp if TYPE_CHECKING: from argparse import Namespace + from pathlib import Path _LOGGER: Final = logging.getLogger(__name__) _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' -def find_target(target: str) -> Path: - """ - Find a `kdist` target: - * if KIMP_${target.upper}_DIR is set --- use that - * otherwise ask `kdist` - """ - - 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: - from pyk.kdist import kdist - - return kdist.which(f'imp-semantics.{target}') - - -def find_k_src_dir() -> Path: - """ - A heuristic way to find the the k-src dir with the K sources is located: - * if KIMP_K_SRC environment variable is set --- use that - * otherwise, use ./k-src and hope it works - """ - ksrc_dir_str = os.environ.get('KIMP_K_SRC') - if ksrc_dir_str is not None: - ksrc_dir = Path(ksrc_dir_str).resolve() - else: - ksrc_dir = Path('./k-src') - return ksrc_dir - - def main() -> None: parser = create_argument_parser() args = parser.parse_args() @@ -65,12 +32,10 @@ def main() -> None: def exec_run( input_file: Path, env_list: list[list[tuple[str, int]]] | None, - definition_dir: Path | None, depth: int | None = None, **kwargs: Any, ) -> None: - definition_dir = find_target('llvm') if definition_dir is None else definition_dir - kimp = KImp(definition_dir, definition_dir) + kimp = KImp() pgm = input_file.read_text() env = {var: val for assign in env_list for var, val in assign} if env_list else {} pattern = kimp.pattern(pgm=pgm, env=env) @@ -79,64 +44,40 @@ def exec_run( def exec_prove( - definition_dir: str, spec_file: str, spec_module: str, claim_id: str, max_iterations: int, max_depth: int, - ignore_return_code: bool = False, reinit: bool = False, **kwargs: Any, ) -> None: - if definition_dir is None: - definition_dir = str(find_target('haskell')) - k_src_dir = str(find_target('source') / 'imp-semantics') - - kimp = KImp(definition_dir, definition_dir) - - try: - kimp.prove( - spec_file=spec_file, - spec_module=spec_module, - claim_id=claim_id, - max_iterations=max_iterations, - max_depth=max_depth, - includes=[k_src_dir], - reinit=reinit, - ) - except ValueError as err: - _LOGGER.critical(err.args) - raise - except RuntimeError as err: - if ignore_return_code: - msg, stdout, stderr = err.args - print(stdout) - print(stderr) - print(msg) - else: - raise + kimp = KImp() + kimp.prove( + spec_file=spec_file, + spec_module=spec_module, + claim_id=claim_id, + max_iterations=max_iterations, + max_depth=max_depth, + reinit=reinit, + ) def exec_show( - definition_dir: str, spec_module: str, claim_id: str, **kwargs: Any, ) -> None: - definition_dir = str(find_target('haskell')) - kimp = KImp(definition_dir, definition_dir) + kimp = KImp() kimp.show_kcfg(spec_module, claim_id) def exec_view( - definition_dir: str, spec_module: str, claim_id: str, **kwargs: Any, ) -> None: - definition_dir = str(find_target('haskell')) - kimp = KImp(definition_dir, definition_dir) + kimp = KImp() kimp.view_kcfg(spec_module, claim_id) @@ -145,12 +86,6 @@ def create_argument_parser() -> ArgumentParser: shared_args = ArgumentParser(add_help=False) shared_args.add_argument('--verbose', '-v', default=False, action='store_true', help='Verbose output.') shared_args.add_argument('--debug', default=False, action='store_true', help='Debug output.') - shared_args.add_argument( - '--definition', - dest='definition_dir', - type=dir_path, - help='Path to compiled K definition to use.', - ) # args shared by proof/prover/kcfg commands spec_file_shared_args = ArgumentParser(add_help=False) diff --git a/kimp/src/kimp/kimp.py b/kimp/src/kimp/kimp.py index 460643d..f309584 100644 --- a/kimp/src/kimp/kimp.py +++ b/kimp/src/kimp/kimp.py @@ -28,7 +28,7 @@ from pyk.utils import single if TYPE_CHECKING: - from collections.abc import Iterable, Iterator, Mapping + from collections.abc import Callable, Iterable, Iterator, Mapping from typing import Final from pyk.cterm.cterm import CTerm @@ -85,28 +85,73 @@ def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: @final @dataclass(frozen=True) -class KImp: +class ImpDist: + source_dir: Path llvm_dir: Path haskell_dir: Path - proof_dir: Path - def __init__(self, llvm_dir: str | Path, haskell_dir: str | Path): + def __init__(self, *, source_dir: str | Path, llvm_dir: str | Path, haskell_dir: str | Path): + source_dir = Path(source_dir) + check_dir_path(source_dir) + llvm_dir = Path(llvm_dir) check_dir_path(llvm_dir) haskell_dir = Path(haskell_dir) check_dir_path(haskell_dir) + object.__setattr__(self, 'source_dir', source_dir) + object.__setattr__(self, 'llvm_dir', llvm_dir) + object.__setattr__(self, 'haskell_dir', haskell_dir) + + @staticmethod + def load() -> ImpDist: + return ImpDist( + source_dir=ImpDist._find('source'), + llvm_dir=ImpDist._find('llvm'), + haskell_dir=ImpDist._find('haskell'), + ) + + @staticmethod + def _find(target: str) -> Path: + """ + Find a `kdist` target: + * if KIMP_${target.upper}_DIR is set --- use that + * otherwise ask `kdist` + """ + + from os import getenv + + from pyk.kdist import kdist + + env_dir = getenv(f'KIMP_{target.upper()}_DIR') + if env_dir: + path = Path(env_dir) + check_dir_path(path) + _LOGGER.info(f'Using target at {path}') + return path + + return kdist.get(f'imp-semantics.{target}') + + +@final +@dataclass(frozen=True) +class KImp: + dist: ImpDist + proof_dir: Path + + def __init__(self) -> None: + dist = ImpDist.load() + proof_dir = Path('.') / '.kimp' / 'proofs' proof_dir.mkdir(exist_ok=True, parents=True) - object.__setattr__(self, 'llvm_dir', llvm_dir) - object.__setattr__(self, 'haskell_dir', haskell_dir) + object.__setattr__(self, 'dist', dist) object.__setattr__(self, 'proof_dir', proof_dir) @cached_property def definition(self) -> KDefinition: - return read_kast_definition(self.llvm_dir / 'compiled.json') + return read_kast_definition(self.dist.llvm_dir / 'compiled.json') @cached_property def format(self) -> Formatter: @@ -114,7 +159,7 @@ def format(self) -> Formatter: @cached_property def kprove(self) -> KProve: - return KProve(definition_dir=self.haskell_dir, use_directory=self.proof_dir) + return KProve(definition_dir=self.dist.haskell_dir, use_directory=self.proof_dir) def run( self, @@ -124,7 +169,7 @@ def run( ) -> Pattern: from pyk.ktool.krun import llvm_interpret - return llvm_interpret(definition_dir=self.llvm_dir, pattern=pattern, depth=depth) + return llvm_interpret(definition_dir=self.dist.llvm_dir, pattern=pattern, depth=depth) def pattern(self, *, pgm: str, env: Mapping[str, int]) -> Pattern: from pyk.kore.prelude import ID, INT, SORT_K_ITEM, inj, map_pattern, top_cell_initializer @@ -151,7 +196,7 @@ def parse(self, pgm: str) -> Pattern: from pyk.kore.parser import KoreParser from pyk.utils import run_process_2 - parser = self.llvm_dir / 'parser_PGM' + parser = self.dist.llvm_dir / 'parser_PGM' args = [str(parser), '/dev/stdin'] kore_text = run_process_2(args, input=pgm).stdout @@ -160,22 +205,48 @@ def parse(self, pgm: str) -> Pattern: def pretty(self, pattern: Pattern, color: bool | None = None) -> str: from pyk.kore.tools import kore_print - return kore_print(pattern, definition_dir=self.llvm_dir, color=bool(color)) + return kore_print(pattern, definition_dir=self.dist.llvm_dir, color=bool(color)) + + def debug(self, pattern: Pattern) -> Callable[[int | None], None]: + """Return a closure that enables step-by-step debugging in a REPL. + + Each call to the function pretty-prints the resulting configuration. + + Example: + step = KImp().debug(pattern) + step() # Run a single step + step(1) # Run a single step + step(0) # Just print the current configuration + step(bound=None) # Run to completion + """ + + def step(bound: int | None = 1) -> None: + nonlocal pattern + pattern = self.run(pattern, depth=bound) + print(self.pretty(pattern, color=True)) + + return step def prove( self, + *, spec_file: str, spec_module: str, - includes: Iterable[str], claim_id: str, max_iterations: int, max_depth: int, reinit: bool, + includes: Iterable[str | Path] | None = None, ) -> None: - include_dirs = [Path(include) for include in includes] + include_dirs = [self.dist.source_dir / 'imp-semantics'] + ( + [Path(include) for include in includes] if includes is not None else [] + ) claims = ClaimLoader(self.kprove).load_claims( - Path(spec_file), spec_module_name=spec_module, claim_labels=[claim_id], include_dirs=include_dirs + Path(spec_file), + spec_module_name=spec_module, + claim_labels=[claim_id], + include_dirs=include_dirs, ) claim = single(claims) spec_label = f'{spec_module}.{claim_id}'