diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 7548a2d5ef..c428031270 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -108,7 +108,7 @@ jobs: - name: 'Build kevm-pyk' run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make poetry' - name: 'Build targets' - run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` llvm haskell' + run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` evm-semantics.llvm evm-semantics.haskell' - name: 'Test integration' run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-integration' - name: 'Test conformance' @@ -150,7 +150,7 @@ jobs: - name: 'Build kevm-pyk' run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry' - name: 'Build distribution' - run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin haskell' + run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell' - name: 'Prove Haskell' run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make ${{ matrix.test-suite }} PYTEST_ARGS='-vv ${{ matrix.test-args }}' PYTEST_PARALLEL=4" - name: 'Tear down Docker' diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index e017c68924..52c1630527 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.343" +version = "1.0.344" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 5646c3c0d7..2e5c49a3b6 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.343' +VERSION: Final = '1.0.344' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 8fc57002d9..278205a38d 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -162,7 +162,7 @@ def exec_prove_legacy( _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') if definition_dir is None: - definition_dir = kdist.get('haskell') + definition_dir = kdist.get('evm-semantics.haskell') kevm = KEVM(definition_dir, use_directory=save_directory) @@ -298,7 +298,7 @@ def exec_prove( digest_file = save_directory / 'digest' if save_directory is not None else None if definition_dir is None: - definition_dir = kdist.get('haskell') + definition_dir = kdist.get('evm-semantics.haskell') if smt_timeout is None: smt_timeout = 300 @@ -608,8 +608,10 @@ def exec_run( if target is None: target = 'llvm' + target_fqn = f'evm-semantics.{target}' + _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(kdist.get(target), use_directory=save_directory) + kevm = KEVM(kdist.get(target_fqn), use_directory=save_directory) try: json_read = json.loads(input_file.read_text()) @@ -644,8 +646,10 @@ def exec_kast( if target is None: target = 'llvm' + target_fqn = f'evm-semantics.{target}' + _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(kdist.get(target), use_directory=save_directory) + kevm = KEVM(kdist.get(target_fqn), use_directory=save_directory) try: json_read = json.loads(input_file.read_text()) diff --git a/kevm-pyk/src/kevm_pyk/interpreter.py b/kevm-pyk/src/kevm_pyk/interpreter.py index 2dba308ece..8d1b91c638 100644 --- a/kevm-pyk/src/kevm_pyk/interpreter.py +++ b/kevm-pyk/src/kevm_pyk/interpreter.py @@ -26,7 +26,7 @@ def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, *, check: b def _interpret(gst_data: Any, schedule: str, mode: str, chainid: int) -> CompletedProcess: - interpreter = kdist.get('llvm') / 'interpreter' + interpreter = kdist.get('evm-semantics.llvm') / 'interpreter' init_kore = gst_to_kore(gst_data, schedule, mode, chainid) proc_res = run_process([str(interpreter), '/dev/stdin', '-1', '/dev/stdout'], input=init_kore.text, check=False) return proc_res diff --git a/kevm-pyk/src/kevm_pyk/kdist/__init__.py b/kevm-pyk/src/kevm_pyk/kdist/__init__.py index d81365769c..fa12895612 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/__init__.py +++ b/kevm-pyk/src/kevm_pyk/kdist/__init__.py @@ -1 +1 @@ -from ._kdist import build, check, clean, get, get_or_none, targets, which +from ._kdist import build, clean, get, get_or_none, plugins, resolve, targets, which diff --git a/kevm-pyk/src/kevm_pyk/kdist/__main__.py b/kevm-pyk/src/kevm_pyk/kdist/__main__.py index af74b9f905..a487e02dc2 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/__main__.py +++ b/kevm-pyk/src/kevm_pyk/kdist/__main__.py @@ -1,5 +1,6 @@ from __future__ import annotations +import fnmatch import logging from argparse import ArgumentParser from typing import TYPE_CHECKING @@ -48,9 +49,17 @@ def _exec_build( verbose: bool, debug: bool, ) -> None: + all_target_fqns = kdist.targets() + target_fqns = [] + for pattern in targets: + matches = fnmatch.filter(all_target_fqns, pattern) + if not matches: + raise ValueError(f'No target matches pattern: {pattern!r}') + target_fqns += matches + verbose = verbose or debug kdist.build( - targets=targets, + target_fqns=target_fqns, jobs=jobs, force=force, enable_llvm_debug=enable_llvm_debug, @@ -69,25 +78,19 @@ def _exec_which(target: str | None) -> None: def _exec_list() -> None: - for target in kdist.targets(): - print(target) + plugins = kdist.plugins() + for plugin in plugins: + print(plugin) + for target in plugins[plugin]: + print(f'* {target}') def _parse_arguments() -> Namespace: - targets = kdist.targets() - - def target(s: str) -> str: - # choices does not work well with nargs="*" - if s not in targets: - raise TypeError() - return s - def add_target_arg(parser: ArgumentParser, help_text: str) -> None: parser.add_argument( 'target', metavar='TARGET', nargs='?', - choices=targets, help=help_text, ) @@ -97,9 +100,7 @@ def add_target_arg(parser: ArgumentParser, help_text: str) -> None: command_parser = parser.add_subparsers(dest='command', required=True) build_parser = command_parser.add_parser('build', help='build targets') - build_parser.add_argument( - 'targets', metavar='TARGET', nargs='*', type=target, default=targets, help='target to build' - ) + build_parser.add_argument('targets', metavar='TARGET', nargs='*', default='*', help='target to build') build_parser.add_argument('-f', '--force', action='store_true', default=False, help='force build') build_parser.add_argument('-j', '--jobs', metavar='N', type=int, default=1, help='maximal number of build jobs') build_parser.add_argument( diff --git a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py index f3d986ff7f..4293598013 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py +++ b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py @@ -3,6 +3,7 @@ import concurrent.futures import logging import os +import re import shutil from collections.abc import Mapping from concurrent.futures import ProcessPoolExecutor @@ -10,7 +11,7 @@ from graphlib import CycleError, TopologicalSorter from pathlib import Path from tempfile import TemporaryDirectory -from typing import TYPE_CHECKING +from typing import TYPE_CHECKING, NamedTuple from filelock import SoftFileLock from pyk.utils import check_dir_path, hash_str @@ -32,6 +33,13 @@ _LOGGER: Final = logging.getLogger(__name__) +_ID_PATTERN = re.compile('[a-z0-9]+(-[a-z0-9]+)*') + + +def _valid_id(s: str) -> bool: + return _ID_PATTERN.fullmatch(s) is not None + + def _dist_dir() -> Path: dist_dir_env = os.getenv('KEVM_DIST_DIR') # Used by Nix flake to set the output if dist_dir_env: @@ -42,15 +50,21 @@ def _dist_dir() -> Path: return xdg_cache_home() / f'kdist-{digest}' -def _targets() -> dict[str, Target]: +def _plugins() -> dict[str, dict[str, Target]]: import importlib from importlib.metadata import entry_points plugins = entry_points(group='kdist') - res: dict[str, Target] = {} + res: dict[str, dict[str, Target]] = {} for plugin in plugins: - _LOGGER.info(f'Loading kdist plugin: {plugin.name}') + plugin_name = plugin.name + + if not _valid_id(plugin_name): + _LOGGER.warning(f'Invalid plugin name, skipping: {plugin_name}') + continue + + _LOGGER.info(f'Loading kdist plugin: {plugin_name}') module_name = plugin.value try: _LOGGER.info(f'Importing module: {module_name}') @@ -59,15 +73,7 @@ def _targets() -> dict[str, Target]: _LOGGER.error(f'Module {module_name} cannot be imported', exc_info=True) continue - targets = _load_targets(module) - - # TODO Namespaces - for key, value in targets.items(): - if key in res: - _LOGGER.warning(f'Target with key already defined, skipping: {key} (in {module_name})') - continue - - res[key] = value + res[plugin_name] = _load_targets(module) return res @@ -89,6 +95,10 @@ def _load_targets(module: ModuleType) -> dict[str, Target]: _LOGGER.warning(f'Invalid target key in {module.__name__}: {key!r}') continue + if not _valid_id(key): + _LOGGER.warning(f'Invalid target name (in {module.__name__}): {key}') + continue + if not isinstance(value, Target): _LOGGER.warning(f'Invalid target value in {module.__name__} for key {key}: {value!r}') continue @@ -99,148 +109,183 @@ def _load_targets(module: ModuleType) -> dict[str, Target]: _DIST_DIR: Final = _dist_dir() -_TARGETS: Final = _targets() +_PLUGINS: Final = _plugins() + + +class TargetId(NamedTuple): + plugin: str + target: str + + @property + def fqn(self) -> str: + return f'{self.plugin}.{self.target}' + + @property + def dir(self) -> Path: + return _DIST_DIR / self.plugin / self.target + + +def plugins() -> dict[str, list[str]]: + return {plugin: list(targets) for plugin, targets in _PLUGINS.items()} def targets() -> list[str]: - return list(_TARGETS) + return [TargetId(plugin, target).fqn for plugin, targets in plugins().items() for target in targets] + + +def resolve(target_fqn: str) -> TargetId: + segments = target_fqn.split('.') + if len(segments) != 2: + raise ValueError(f'Expected fully qualified target name, got: {target_fqn!r}') + + plugin, target = segments + if not _valid_id(plugin): + raise ValueError(f'Invalid plugin identifier: {plugin!r}') -def check(target: str) -> None: - if target not in _TARGETS: - raise ValueError(f'Undefined target: {target}') + if not _valid_id(target): + raise ValueError(f'Invalid target identifier: {target!r}') + _plugins = plugins() -def which(target: str | None = None) -> Path: - if target: - check(target) - return _DIST_DIR / target + try: + targets = _plugins[plugin] + except KeyError: + raise ValueError(f'Undefined plugin: {plugin}') from None + + if not target in targets: + raise ValueError(f'Plugin {plugin} does not define target: {target}') + + return TargetId(plugin, target) + + +def which(target_fqn: str | None = None) -> Path: + if target_fqn: + return resolve(target_fqn).dir return _DIST_DIR -def clean(target: str | None = None) -> Path: - res = which(target) +def clean(target_fqn: str | None = None) -> Path: + res = which(target_fqn) shutil.rmtree(res, ignore_errors=True) return res -def get(target: str) -> Path: - res = which(target) +def get(target_fqn: str) -> Path: + res = which(target_fqn) if not res.exists(): - raise ValueError(f'Target is not built: {target}') + raise ValueError(f'Target is not built: {target_fqn}') return res -def get_or_none(target: str) -> Path | None: - res = which(target) +def get_or_none(target_fqn: str) -> Path | None: + res = which(target_fqn) if not res.exists(): return None return res def build( - targets: list[str], + target_fqns: list[str], *, jobs: int = 1, force: bool = False, enable_llvm_debug: bool = False, verbose: bool = False, ) -> None: - deps = _resolve_deps(targets) + deps = _resolve_deps(target_fqns) target_graph = TopologicalSorter(deps) try: target_graph.prepare() except CycleError as err: raise RuntimeError(f'Cyclic dependencies found: {err.args[1]}') from err - _LOGGER.info(f"Building targets: {', '.join(deps)}") + deps_fqns = [target.fqn for target in deps] + _LOGGER.info(f"Building targets: {', '.join(deps_fqns)}") with ProcessPoolExecutor(max_workers=jobs) as pool: - pending: dict[Future[Path], str] = {} + pending: dict[Future[Path], TargetId] = {} - def submit(target: str) -> None: + def submit(target_id: TargetId) -> None: future = pool.submit( _build_target, - target=target, + target_id=target_id, args={'enable_llvm_debug': enable_llvm_debug, 'verbose': verbose}, force=force, ) - pending[future] = target + pending[future] = target_id - for target in target_graph.get_ready(): - submit(target) + for target_id in target_graph.get_ready(): + submit(target_id) while pending: done, _ = concurrent.futures.wait(pending, return_when=concurrent.futures.FIRST_COMPLETED) for future in done: result = future.result() print(result) - target = pending[future] - target_graph.done(target) - for new_target in target_graph.get_ready(): - submit(new_target) + target_id = pending[future] + target_graph.done(target_id) + for new_target_id in target_graph.get_ready(): + submit(new_target_id) pending.pop(future) -def _resolve_deps(targets: Iterable[str]) -> dict[str, list[str]]: - res: dict[str, list[str]] = {} - pending = list(targets) +def _resolve_deps(target_fqns: Iterable[str]) -> dict[TargetId, list[TargetId]]: + res: dict[TargetId, list[TargetId]] = {} + pending = [resolve(target) for target in target_fqns] while pending: - target_name = pending.pop() - if target_name in res: + target_id = pending.pop() + if target_id in res: continue - target = _resolve(target_name) - deps = list(target.deps()) - res[target_name] = deps + plugin, target = target_id + _target = _PLUGINS[plugin][target] + deps = [resolve(target_id) for target_id in _target.deps()] + res[target_id] = deps pending += deps return res -def _resolve(target: str) -> Target: - check(target) - return _TARGETS[target] - - def _build_target( - target: str, + target_id: TargetId, args: dict[str, Any], *, force: bool = False, ) -> Path: - output_dir = which(target) + output_dir = target_id.dir - with _lock(target): + with _lock(target_id): if not force and output_dir.exists(): return output_dir shutil.rmtree(output_dir, ignore_errors=True) output_dir.mkdir(parents=True) - _target = _TARGETS[target] + _target = _PLUGINS[target_id.plugin][target_id.target] deps = {target: which(target) for target in _target.deps()} with ( - _build_dir(target) as build_dir, + _build_dir(target_id) as build_dir, _cwd(build_dir), ): try: _target.build(output_dir, deps=deps, args=args) except BaseException as err: shutil.rmtree(output_dir, ignore_errors=True) - raise RuntimeError(f'Build failed: {target}') from err + raise RuntimeError(f'Build failed: {target_id.fqn}') from err return output_dir -def _lock(target: str) -> FileLock: - lock_file = which(target).with_suffix('.lock') +def _lock(target: TargetId) -> FileLock: + lock_file = target.dir.with_suffix('.lock') lock_file.parent.mkdir(parents=True, exist_ok=True) return SoftFileLock(lock_file) @contextmanager -def _build_dir(target: str) -> Iterator[Path]: - with TemporaryDirectory(prefix=f'kdist-{target}-') as build_dir_str: +def _build_dir(target_id: TargetId) -> Iterator[Path]: + tmp_dir_prefix = f'kdist-{target_id.plugin}-{target_id.target}-' + with TemporaryDirectory(prefix=tmp_dir_prefix) as build_dir_str: build_dir = Path(build_dir_str) yield build_dir diff --git a/kevm-pyk/src/kevm_pyk/kdist/plugin.py b/kevm-pyk/src/kevm_pyk/kdist/plugin.py index 77a1e788d9..0f0f230006 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/plugin.py +++ b/kevm-pyk/src/kevm_pyk/kdist/plugin.py @@ -32,7 +32,7 @@ def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any]) - output_dir=output_dir, enable_llvm_debug=enable_llvm_debug, verbose=verbose, - plugin_dir=deps.get('plugin'), + plugin_dir=deps.get('evm-semantics.plugin'), **self._kompile_args, ) @@ -76,7 +76,7 @@ def build(self, output_dir: Path, deps: dict[str, Any], args: dict[str, Any]) -> 'syntax_module': 'ETHEREUM-SIMULATION', 'optimization': 2, }, - deps=('plugin',), + deps=('evm-semantics.plugin',), ), 'haskell': KEVMTarget( { diff --git a/kevm-pyk/src/tests/integration/test_conformance.py b/kevm-pyk/src/tests/integration/test_conformance.py index 4d8470bf99..5e6826de1b 100644 --- a/kevm-pyk/src/tests/integration/test_conformance.py +++ b/kevm-pyk/src/tests/integration/test_conformance.py @@ -50,7 +50,7 @@ def _assert_exit_code_zero(pattern: Pattern) -> None: if exit_code == int_dv(0): return - pretty = kore_print(pattern, definition_dir=kdist.get('llvm'), output=PrintOutput.PRETTY) + pretty = kore_print(pattern, definition_dir=kdist.get('evm-semantics.llvm'), output=PrintOutput.PRETTY) assert pretty == GOLDEN diff --git a/kevm-pyk/src/tests/integration/test_kast.py b/kevm-pyk/src/tests/integration/test_kast.py index 743173c25a..69ec58e90a 100644 --- a/kevm-pyk/src/tests/integration/test_kast.py +++ b/kevm-pyk/src/tests/integration/test_kast.py @@ -14,7 +14,7 @@ def test_parse() -> None: # When actual = _kast( file=evm_file, - definition_dir=kdist.get('llvm'), + definition_dir=kdist.get('evm-semantics.llvm'), input=KAstInput.PROGRAM, output=KAstOutput.KORE, ).stdout diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index a70c539f47..4b2e1bb147 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -117,7 +117,7 @@ class Target(NamedTuple): def __call__(self, output_dir: Path) -> Path: definition_subdir = 'kompiled' if not self.use_booster else 'kompiled-booster' definition_dir = output_dir / definition_subdir - plugin_dir = kdist.get('plugin') if self.use_booster else None + plugin_dir = kdist.get('evm-semantics.plugin') if self.use_booster else None target = KompileTarget.HASKELL if not self.use_booster else KompileTarget.HASKELL_BOOSTER return kevm_kompile( output_dir=definition_dir, diff --git a/kevm-pyk/src/tests/integration/test_run.py b/kevm-pyk/src/tests/integration/test_run.py index 492dcecd4d..3448506681 100644 --- a/kevm-pyk/src/tests/integration/test_run.py +++ b/kevm-pyk/src/tests/integration/test_run.py @@ -32,7 +32,7 @@ def test_run(gst_file: Path) -> None: # When pattern = interpret(gst_data, 'SHANGHAI', 'NORMAL', 1, check=False) - actual = kore_print(pattern, definition_dir=kdist.get('llvm'), output=PrintOutput.PRETTY) + actual = kore_print(pattern, definition_dir=kdist.get('evm-semantics.llvm'), output=PrintOutput.PRETTY) # Then assert actual == expected diff --git a/package/version b/package/version index 2450a4b43d..2ed9a2a10f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.343 +1.0.344