From 864e505700b65668086690fe6a6c63fe0681b33a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 6 Nov 2023 11:28:51 +0100 Subject: [PATCH 1/6] Validate plugin and target identifiers --- kevm-pyk/src/kevm_pyk/kdist/_kdist.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py index f3d986ff7f..22cf51264e 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 @@ -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: @@ -50,6 +58,10 @@ def _targets() -> dict[str, Target]: res: dict[str, Target] = {} for plugin in plugins: + 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: @@ -89,6 +101,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 From c7dd50c4dc79d7ff7d1c2d1f3400147bb90f0c30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 6 Nov 2023 14:34:25 +0100 Subject: [PATCH 2/6] Introduce target namespaces --- kevm-pyk/src/kevm_pyk/kdist/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/kdist/__main__.py | 18 +-- kevm-pyk/src/kevm_pyk/kdist/_kdist.py | 155 +++++++++++++++--------- 3 files changed, 106 insertions(+), 69 deletions(-) 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..55de9de1db 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/__main__.py +++ b/kevm-pyk/src/kevm_pyk/kdist/__main__.py @@ -69,25 +69,21 @@ 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 +93,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=targets, 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 22cf51264e..7851175788 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py +++ b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py @@ -11,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 @@ -50,19 +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: - if not _valid_id(plugin.name): - _LOGGER.warning(f'Invalid plugin name, skipping: {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}') + _LOGGER.info(f'Loading kdist plugin: {plugin_name}') module_name = plugin.value try: _LOGGER.info(f'Importing module: {module_name}') @@ -71,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 @@ -115,22 +109,73 @@ 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: str) -> TargetId: + if not target: + raise ValueError('Unexpected empty string') -def check(target: str) -> None: - if target not in _TARGETS: - raise ValueError(f'Undefined target: {target}') + segments = target.split('.') + + if len(segments) > 2: + raise ValueError('Exected at most one period: {target}') + + if len(segments) == 2: + plugin, target = segments + else: + plugin = None + target = segments[0] + + if plugin is not None and not _valid_id(plugin): + raise ValueError(f'Invalid plugin identifer: {plugin!r}') + + if not _valid_id(target): + raise ValueError(f'Invalid target identifier: {target!r}') + + _plugins = plugins() + + if plugin: + 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) + + matching_plugins = [plugin for plugin, targets in _plugins.items() if target in targets] + if not matching_plugins: + raise ValueError(f'No plugin defines target: {target}') + if len(matching_plugins) > 1: + raise ValueError(f'Multiple plugins define target {target}: {matching_plugins}') + return TargetId(matching_plugins[0], target) def which(target: str | None = None) -> Path: if target: - check(target) - return _DIST_DIR / target + return resolve(target).dir return _DIST_DIR @@ -169,94 +214,92 @@ def build( except CycleError as err: raise RuntimeError(f'Cyclic dependencies found: {err.args[1]}') from err - _LOGGER.info(f"Building targets: {', '.join(deps)}") + target_fqns = [target.fqn for target in deps] + _LOGGER.info(f"Building targets: {', '.join(target_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(targets: Iterable[str]) -> dict[TargetId, list[TargetId]]: + res: dict[TargetId, list[TargetId]] = {} + pending = [resolve(target) for target in targets] 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 From 2e6e2bef411d81ca9ec1bf2cb23bc56479b4cd4c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 6 Nov 2023 14:42:52 +0100 Subject: [PATCH 3/6] Use fully qualified target names --- .github/workflows/test-pr.yml | 4 +- kevm-pyk/src/kevm_pyk/__main__.py | 12 ++- kevm-pyk/src/kevm_pyk/interpreter.py | 2 +- kevm-pyk/src/kevm_pyk/kdist/__main__.py | 2 +- kevm-pyk/src/kevm_pyk/kdist/_kdist.py | 82 ++++++++----------- kevm-pyk/src/kevm_pyk/kdist/plugin.py | 4 +- .../src/tests/integration/test_conformance.py | 2 +- kevm-pyk/src/tests/integration/test_kast.py | 2 +- kevm-pyk/src/tests/integration/test_prove.py | 2 +- kevm-pyk/src/tests/integration/test_run.py | 2 +- 10 files changed, 52 insertions(+), 62 deletions(-) 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/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/__main__.py b/kevm-pyk/src/kevm_pyk/kdist/__main__.py index 55de9de1db..3b6d3ab5ed 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/__main__.py +++ b/kevm-pyk/src/kevm_pyk/kdist/__main__.py @@ -50,7 +50,7 @@ def _exec_build( ) -> None: verbose = verbose or debug kdist.build( - targets=targets, + target_fqns=targets, jobs=jobs, force=force, enable_llvm_debug=enable_llvm_debug, diff --git a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py index 7851175788..4293598013 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py +++ b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py @@ -133,89 +133,75 @@ def targets() -> list[str]: return [TargetId(plugin, target).fqn for plugin, targets in plugins().items() for target in targets] -def resolve(target: str) -> TargetId: - if not target: - raise ValueError('Unexpected empty string') +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}') - segments = target.split('.') + plugin, target = segments - if len(segments) > 2: - raise ValueError('Exected at most one period: {target}') - - if len(segments) == 2: - plugin, target = segments - else: - plugin = None - target = segments[0] - - if plugin is not None and not _valid_id(plugin): - raise ValueError(f'Invalid plugin identifer: {plugin!r}') + if not _valid_id(plugin): + raise ValueError(f'Invalid plugin identifier: {plugin!r}') if not _valid_id(target): raise ValueError(f'Invalid target identifier: {target!r}') _plugins = plugins() - if plugin: - 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) - - matching_plugins = [plugin for plugin, targets in _plugins.items() if target in targets] - if not matching_plugins: - raise ValueError(f'No plugin defines target: {target}') - if len(matching_plugins) > 1: - raise ValueError(f'Multiple plugins define target {target}: {matching_plugins}') - return TargetId(matching_plugins[0], target) - - -def which(target: str | None = None) -> Path: - if target: - return resolve(target).dir + 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 - target_fqns = [target.fqn for target in deps] - _LOGGER.info(f"Building targets: {', '.join(target_fqns)}") + 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], TargetId] = {} @@ -244,9 +230,9 @@ def submit(target_id: TargetId) -> None: pending.pop(future) -def _resolve_deps(targets: Iterable[str]) -> dict[TargetId, list[TargetId]]: +def _resolve_deps(target_fqns: Iterable[str]) -> dict[TargetId, list[TargetId]]: res: dict[TargetId, list[TargetId]] = {} - pending = [resolve(target) for target in targets] + pending = [resolve(target) for target in target_fqns] while pending: target_id = pending.pop() if target_id in res: 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 From 1339896b471b2e1e2223a9940f3b540be1c49735 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 6 Nov 2023 15:07:10 +0100 Subject: [PATCH 4/6] Add wildcard feature to command `build` --- kevm-pyk/src/kevm_pyk/kdist/__main__.py | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kdist/__main__.py b/kevm-pyk/src/kevm_pyk/kdist/__main__.py index 3b6d3ab5ed..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( - target_fqns=targets, + target_fqns=target_fqns, jobs=jobs, force=force, enable_llvm_debug=enable_llvm_debug, @@ -77,8 +86,6 @@ def _exec_list() -> None: def _parse_arguments() -> Namespace: - targets = kdist.targets() - def add_target_arg(parser: ArgumentParser, help_text: str) -> None: parser.add_argument( 'target', @@ -93,7 +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='*', 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( From 20c6ce2a47290ccf554028fc2732c612a55fb038 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 8 Nov 2023 13:20:03 +0000 Subject: [PATCH 5/6] Set Version: 1.0.343 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index dd9770e0af..4ddb7e12eb 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.342" +version = "1.0.343" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 9ff53e3a8f..5646c3c0d7 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.342' +VERSION: Final = '1.0.343' diff --git a/package/version b/package/version index 7632c685db..2450a4b43d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.342 +1.0.343 From 8247f3bebe0c6ee5fe3ee495eef5a37607d7b3c1 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 8 Nov 2023 20:28:44 +0000 Subject: [PATCH 6/6] Set Version: 1.0.344 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) 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/package/version b/package/version index 2450a4b43d..2ed9a2a10f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.343 +1.0.344