diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 7d5b57c69e..79d53ad10c 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.316" +version = "1.0.317" description = "" authors = [ "Runtime Verification, Inc. ", @@ -42,10 +42,13 @@ pyupgrade = "*" [tool.poetry.scripts] kevm = "kevm_pyk.__main__:main" kevm-pyk = "kevm_pyk.__main__:main" -kevm-dist = "kevm_pyk.dist:main" +kevm-dist = "kevm_pyk.kdist.__main__:main" gst-to-kore = "kevm_pyk.gst_to_kore:main" kontrolx = "kontrolx.__main__:main" +[tool.poetry.plugins.kdist] +evm-semantics = "kevm_pyk.kdist.plugin" + [tool.isort] profile = "black" line_length = 120 diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 58b03fac74..1a7d6f6a92 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.316' +VERSION: Final = '1.0.317' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 185a871567..19001c135a 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -26,9 +26,8 @@ from pyk.proof.tui import APRProofViewer from pyk.utils import single -from . import VERSION, config +from . import VERSION, config, kdist from .cli import KEVMCLIArgs, node_id_like -from .dist import DistTarget from .gst_to_kore import SORT_ETHEREUM_SIMULATION, gst_to_kore, kore_pgm_to_kore from .kevm import KEVM, KEVMSemantics, kevm_node_printer from .kompile import KompileTarget, kevm_kompile @@ -160,7 +159,7 @@ def exec_prove_legacy( _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') if definition_dir is None: - definition_dir = DistTarget.HASKELL.get() + definition_dir = kdist.get('haskell') kevm = KEVM(definition_dir, use_directory=save_directory) @@ -231,7 +230,7 @@ def exec_prove( md_selector = 'k' if definition_dir is None: - definition_dir = DistTarget.HASKELL.get() + definition_dir = kdist.get('haskell') if smt_timeout is None: smt_timeout = 300 @@ -525,16 +524,16 @@ def exec_run( schedule: str, mode: str, chainid: int, - target: DistTarget | None = None, + target: str | None = None, save_directory: Path | None = None, debugger: bool = False, **kwargs: Any, ) -> None: if target is None: - target = DistTarget.LLVM + target = 'llvm' _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(target.get(), use_directory=save_directory) + kevm = KEVM(kdist.get(target), use_directory=save_directory) try: json_read = json.loads(input_file.read_text()) @@ -562,15 +561,15 @@ def exec_kast( schedule: str, mode: str, chainid: int, - target: DistTarget | None = None, + target: str | None = None, save_directory: Path | None = None, **kwargs: Any, ) -> None: if target is None: - target = DistTarget.LLVM + target = 'llvm' _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(target.get(), use_directory=save_directory) + kevm = KEVM(kdist.get(target), use_directory=save_directory) try: json_read = json.loads(input_file.read_text()) diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 9dca17a01d..ede83dc77f 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -8,7 +8,6 @@ from pyk.cli.args import KCLIArgs from pyk.cli.utils import dir_path -from .dist import DistTarget from .utils import arg_pair_of if TYPE_CHECKING: @@ -38,7 +37,7 @@ class KEVMCLIArgs(KCLIArgs): @cached_property def target_args(self) -> ArgumentParser: args = ArgumentParser(add_help=False) - args.add_argument('--target', type=DistTarget, choices=list(DistTarget)) + args.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry']) return args @cached_property diff --git a/kevm-pyk/src/kevm_pyk/dist.py b/kevm-pyk/src/kevm_pyk/dist.py deleted file mode 100644 index 1543bab7da..0000000000 --- a/kevm-pyk/src/kevm_pyk/dist.py +++ /dev/null @@ -1,340 +0,0 @@ -from __future__ import annotations - -import logging -import os -import shutil -import time -from argparse import ArgumentParser -from concurrent.futures import ThreadPoolExecutor -from contextlib import contextmanager -from distutils.dir_util import copy_tree -from enum import Enum -from pathlib import Path -from subprocess import CalledProcessError -from tempfile import TemporaryDirectory -from typing import TYPE_CHECKING, Literal - -from pyk.cli.args import KCLIArgs -from pyk.cli.utils import loglevel -from pyk.kbuild.utils import sync_files -from pyk.utils import hash_str, run_process -from xdg_base_dirs import xdg_cache_home - -from . import config -from .kompile import KompileTarget, kevm_kompile - -if TYPE_CHECKING: - from argparse import Namespace - from collections.abc import Iterator, Mapping - from concurrent.futures import Future - from typing import Any, Final - - -_LOGGER: Final = logging.getLogger(__name__) -_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' - - -def _dist_dir() -> Path: - dist_dir_env = os.getenv('KEVM_DIST_DIR') # Used by Nix flake to set the output - if dist_dir_env: - return Path(dist_dir_env).resolve() - - digest = hash_str({'module-dir': config.MODULE_DIR})[:7] - return xdg_cache_home() / f'evm-semantics-{digest}' - - -DIST_DIR: Final = _dist_dir() - - -# --------- -# K targets -# --------- - - -class DistTarget(Enum): - LLVM = 'llvm' - HASKELL = 'haskell' - HASKELL_STANDALONE = 'haskell-standalone' - FOUNDRY = 'foundry' - - @property - def path(self) -> Path: - return DIST_DIR / self.value - - def get(self) -> Path: - if not self.path.exists(): - raise ValueError(f'Target {self.name} is not built') - return self.path - - def get_or_none(self) -> Path | None: - if not self.path.exists(): - return None - return self.path - - def build(self, *, force: bool = False, enable_llvm_debug: bool = False, verbose: bool = False) -> Path: - if force or not self.path.exists(): - self._do_build(enable_llvm_debug=enable_llvm_debug, verbose=verbose) - return self.path - - def clean(self) -> Path: - shutil.rmtree(self.path, ignore_errors=True) - return self.path - - def _do_build(self, *, enable_llvm_debug: bool, verbose: bool) -> None: - _LOGGER.info(f'Building target {self.name}: {self.path}') - DIST_DIR.mkdir(parents=True, exist_ok=True) - try: - kevm_kompile( - output_dir=self.path, enable_llvm_debug=enable_llvm_debug, verbose=verbose, **_TARGET_PARAMS[self] - ) - except RuntimeError: - self.clean() - raise - - -_TARGET_PARAMS: Final[Mapping[DistTarget, Any]] = { - DistTarget.LLVM: { - 'target': KompileTarget.LLVM, - 'main_file': config.EVM_SEMANTICS_DIR / 'driver.md', - 'main_module': 'ETHEREUM-SIMULATION', - 'syntax_module': 'ETHEREUM-SIMULATION', - 'optimization': 2, - }, - DistTarget.HASKELL: { - 'target': KompileTarget.HASKELL, - 'main_file': config.EVM_SEMANTICS_DIR / 'edsl.md', - 'main_module': 'EDSL', - 'syntax_module': 'EDSL', - }, - DistTarget.HASKELL_STANDALONE: { - 'target': KompileTarget.HASKELL_STANDALONE, - 'main_file': config.EVM_SEMANTICS_DIR / 'driver.md', - 'main_module': 'ETHEREUM-SIMULATION', - 'syntax_module': 'ETHEREUM-SIMULATION', - }, - DistTarget.FOUNDRY: { - 'target': KompileTarget.FOUNDRY, - 'main_file': config.EVM_SEMANTICS_DIR / 'foundry.md', - 'main_module': 'FOUNDRY', - 'syntax_module': 'FOUNDRY', - }, -} - - -# -------------- -# Plugin project -# -------------- - - -PLUGIN_DIR: Final = DIST_DIR / 'plugin' - - -def check_plugin() -> Path: - if not PLUGIN_DIR.exists(): - raise ValueError('Plugin project is not built') - return PLUGIN_DIR - - -def build_plugin(*, force: bool = False, verbose: bool = False) -> Path: - if force or not PLUGIN_DIR.exists(): - _do_build_plugin(verbose=verbose) - return PLUGIN_DIR - - -def clean_plugin() -> Path: - shutil.rmtree(PLUGIN_DIR, ignore_errors=True) - return PLUGIN_DIR - - -def _do_build_plugin(*, verbose: bool) -> None: - _LOGGER.info(f'Building Plugin project: {PLUGIN_DIR}') - - sync_files( - source_dir=config.PLUGIN_DIR / 'plugin-c', - target_dir=PLUGIN_DIR / 'plugin-c', - file_names=[ - 'blake2.cpp', - 'blake2.h', - 'crypto.cpp', - 'plugin_util.cpp', - 'plugin_util.h', - ], - ) - - with _plugin_build_env() as build_dir: - try: - run_process(['make', 'libcryptopp', 'libff', 'libsecp256k1', '-j3'], cwd=build_dir, pipe_stdout=not verbose) - except CalledProcessError: - clean_plugin() - raise - - output_dir = build_dir / 'build' - copy_tree(str(output_dir / 'libcryptopp'), str(PLUGIN_DIR / 'libcryptopp')) - copy_tree(str(output_dir / 'libff'), str(PLUGIN_DIR / 'libff')) - copy_tree(str(output_dir / 'libsecp256k1'), str(PLUGIN_DIR / 'libsecp256k1')) - - -@contextmanager -def _plugin_build_env() -> Iterator[Path]: - with TemporaryDirectory(prefix='evm-semantics-plugin-') as build_dir_str: - build_dir = Path(build_dir_str) - copy_tree(str(config.PLUGIN_DIR), str(build_dir)) - yield build_dir - - -# --- -# CLI -# --- - - -def main() -> None: - args = _parse_arguments() - - logging.basicConfig(level=loglevel(args), format=_LOG_FORMAT) - - if args.command == 'build': - _exec_build(**vars(args)) - - elif args.command == 'clean': - _exec_clean(args.target) - - elif args.command == 'which': - _exec_which(args.target) - - else: - raise AssertionError() - - -CliTarget = DistTarget | Literal['plugin'] - - -def _exec_build( - command: str, - targets: list[str], - jobs: int, - force: bool, - enable_llvm_debug: bool, - verbose: bool, - debug: bool, -) -> None: - _LOGGER.info(f"Building targets: {', '.join(targets)}") - - verbose = verbose or debug - - delay_llvm = 'llvm' in targets and 'plugin' in targets - - with ThreadPoolExecutor(max_workers=jobs) as pool: - pending: list[Future] = [] - plugin: Future | None = None - - for target in targets: - if target == 'llvm' and delay_llvm: - continue - - if target == 'plugin': - plugin = pool.submit(build_plugin, force=force, verbose=verbose) - pending.append(plugin) - continue - - pending.append( - pool.submit(DistTarget(target).build, force=force, enable_llvm_debug=enable_llvm_debug, verbose=verbose) - ) - - while pending: - current = next((future for future in pending if future.done()), None) - - if current is None: - time.sleep(0.1) - continue - - result = current.result() - print(result) - - if current == plugin and delay_llvm: - pending += [pool.submit(DistTarget.LLVM.build, force=force)] - - pending.remove(current) - - -def _exec_clean(target: str | None) -> None: - if not target: - shutil.rmtree(DIST_DIR, ignore_errors=True) - print(DIST_DIR) - return - - cli_target = _cli_target(target) - if isinstance(cli_target, DistTarget): - cli_target.clean() - print(cli_target.path) - return - - clean_plugin() - print(PLUGIN_DIR) - - -def _exec_which(target: str | None) -> None: - if not target: - print(DIST_DIR) - return - - cli_target = _cli_target(target) - if isinstance(cli_target, DistTarget): - print(cli_target.path) - return - - print(PLUGIN_DIR) - - -def _parse_arguments() -> Namespace: - targets = [item.value for item in DistTarget] + ['plugin'] - - 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, - ) - - k_cli_args = KCLIArgs() - - parser = ArgumentParser(prog='kevm-dist', parents=[k_cli_args.logging_args]) - 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('-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( - '--enable-llvm-debug', action='store_true', default=True, help='enable debug symbols for the LLVM target' - ) - - clean_parser = command_parser.add_parser('clean', help='clean targets') - add_target_arg(clean_parser, 'target to clean') - - which_parser = command_parser.add_parser('which', help='print target location') - add_target_arg(which_parser, 'target to print directory for') - - return parser.parse_args() - - -def _cli_target(s: str) -> CliTarget: - try: - return DistTarget(s) - except ValueError: - if s == 'plugin': - return 'plugin' - raise TypeError(f'Invalid target: {s}') from None - - -if __name__ == '__main__': - main() diff --git a/kevm-pyk/src/kevm_pyk/interpreter.py b/kevm-pyk/src/kevm_pyk/interpreter.py index bd64764e8d..2dba308ece 100644 --- a/kevm-pyk/src/kevm_pyk/interpreter.py +++ b/kevm-pyk/src/kevm_pyk/interpreter.py @@ -5,7 +5,7 @@ from pyk.kore.parser import KoreParser from pyk.utils import run_process -from .dist import DistTarget +from . import kdist from .gst_to_kore import gst_to_kore if TYPE_CHECKING: @@ -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 = DistTarget.LLVM.get() / 'interpreter' + interpreter = kdist.get('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 new file mode 100644 index 0000000000..ac28be50b9 --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/kdist/__init__.py @@ -0,0 +1 @@ +from ._kdist import Target, build, check, clean, get, get_or_none, targets, which diff --git a/kevm-pyk/src/kevm_pyk/kdist/__main__.py b/kevm-pyk/src/kevm_pyk/kdist/__main__.py new file mode 100644 index 0000000000..fd28feed4e --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/kdist/__main__.py @@ -0,0 +1,154 @@ +from __future__ import annotations + +import logging +import time +from argparse import ArgumentParser +from concurrent.futures import ThreadPoolExecutor +from typing import TYPE_CHECKING + +from pyk.cli.args import KCLIArgs +from pyk.cli.utils import loglevel + +from .. import kdist + +if TYPE_CHECKING: + from argparse import Namespace + from concurrent.futures import Future + from typing import Final + + +_LOGGER: Final = logging.getLogger(__name__) +_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' + + +def main() -> None: + args = _parse_arguments() + + logging.basicConfig(level=loglevel(args), format=_LOG_FORMAT) + + if args.command == 'build': + _exec_build(**vars(args)) + + elif args.command == 'clean': + _exec_clean(args.target) + + elif args.command == 'which': + _exec_which(args.target) + + elif args.command == 'list': + _exec_list() + + else: + raise AssertionError() + + +def _exec_build( + command: str, + targets: list[str], + jobs: int, + force: bool, + enable_llvm_debug: bool, + verbose: bool, + debug: bool, +) -> None: + _LOGGER.info(f"Building targets: {', '.join(targets)}") + + verbose = verbose or debug + + delay_llvm = 'llvm' in targets and 'plugin' in targets + + with ThreadPoolExecutor(max_workers=jobs) as pool: + pending: list[Future] = [] + plugin: Future | None = None + + for target in targets: + if target == 'llvm' and delay_llvm: + continue + + plugin = pool.submit( + kdist.build, target=target, force=force, enable_llvm_debug=enable_llvm_debug, verbose=verbose + ) + pending.append(plugin) + + while pending: + current = next((future for future in pending if future.done()), None) + + if current is None: + time.sleep(0.01) + continue + + result = current.result() + print(result) + + if current == plugin and delay_llvm: + pending.append( + pool.submit( + kdist.build, target='llvm', force=force, enable_llvm_debug=enable_llvm_debug, verbose=verbose + ) + ) + + pending.remove(current) + + +def _exec_clean(target: str | None) -> None: + res = kdist.clean(target) + print(res) + + +def _exec_which(target: str | None) -> None: + res = kdist.which(target) + print(res) + + +def _exec_list() -> None: + targets = kdist.targets() + for target in targets: + print(target) + + +def _parse_arguments() -> Namespace: + targets = list(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, + ) + + k_cli_args = KCLIArgs() + + parser = ArgumentParser(prog='kevm-dist', parents=[k_cli_args.logging_args]) + 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('-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( + '--enable-llvm-debug', action='store_true', default=True, help='enable debug symbols for the LLVM target' + ) + + clean_parser = command_parser.add_parser('clean', help='clean targets') + add_target_arg(clean_parser, 'target to clean') + + which_parser = command_parser.add_parser('which', help='print target location') + add_target_arg(which_parser, 'target to print directory for') + + command_parser.add_parser('list', help='print list of available targets') + + return parser.parse_args() + + +if __name__ == '__main__': + main() diff --git a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py new file mode 100644 index 0000000000..e8a3bde682 --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py @@ -0,0 +1,150 @@ +from __future__ import annotations + +import logging +import os +import shutil +from abc import ABC, abstractmethod +from collections.abc import Mapping +from pathlib import Path +from typing import TYPE_CHECKING + +from pyk.utils import hash_str +from xdg_base_dirs import xdg_cache_home + +from .. import config + +if TYPE_CHECKING: + from types import ModuleType + from typing import Any, Final + + +_LOGGER: Final = logging.getLogger(__name__) +_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' + + +def _dist_dir() -> Path: + dist_dir_env = os.getenv('KEVM_DIST_DIR') # Used by Nix flake to set the output + if dist_dir_env: + return Path(dist_dir_env).resolve() + + digest = hash_str({'module-dir': config.MODULE_DIR})[:7] + return xdg_cache_home() / f'evm-semantics-{digest}' + + +DIST_DIR: Final = _dist_dir() + + +class Target(ABC): + @abstractmethod + def build(self, output_dir: Path, args: dict[str, Any]) -> None: + ... + + +def _load() -> dict[str, Target]: + import importlib + from importlib.metadata import entry_points + + plugins = entry_points(group='kdist') + + res: dict[str, Target] = {} + for plugin in plugins: + _LOGGER.info(f'Loading kdist plugin: {plugin.name}') + module_name = plugin.value + try: + _LOGGER.info(f'Importing module: {module_name}') + module = importlib.import_module(module_name) + except Exception: + _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 + + return res + + +def _load_targets(module: ModuleType) -> dict[str, Target]: + if not hasattr(module, '__TARGETS__'): + _LOGGER.warning(f'Module does not define __TARGETS__: {module.__name__}') + return {} + + targets = module.__TARGETS__ + + if not isinstance(targets, Mapping): + _LOGGER.warning(f'Invalid __TARGETS__ attribute: {module.__name__}') + return {} + + res: dict[str, Target] = {} + for key, value in targets.items(): + if not isinstance(key, str): + _LOGGER.warning(f'Invalid target key in {module.__name__}: {key!r}') + continue + + if not isinstance(value, Target): + _LOGGER.warning(f'Invalid target value in {module.__name__} for key {key}: {value!r}') + continue + + res[key] = value + + return res + + +_TARGETS: dict[str, Target] | None = None + + +def targets() -> dict[str, Target]: + global _TARGETS + if _TARGETS is None: + _TARGETS = _load() + return dict(_TARGETS) + + +def check(target: str) -> None: + if target not in targets(): + raise ValueError('Undefined target: {target}') + + +def which(target: str | None = None) -> Path: + if target: + check(target) + return DIST_DIR / target + return DIST_DIR + + +def clean(target: str | None = None) -> Path: + res = which(target) + shutil.rmtree(res, ignore_errors=True) + return res + + +def get(target: str) -> Path: + res = which(target) + if not res.exists(): + raise ValueError(f'Target is not built: {target}') + return res + + +def get_or_none(target: str) -> Path | None: + res = which(target) + if not res.exists(): + return None + return res + + +def build(target: str, *, force: bool = False, **kwargs: Any) -> Path: + # TODO Locking + output_dir = which(target) + if not force and output_dir.exists(): + return output_dir + + output_dir.mkdir(parents=True) + _target = targets()[target] + _target.build(output_dir, args=kwargs) + return output_dir diff --git a/kevm-pyk/src/kevm_pyk/kdist/plugin.py b/kevm-pyk/src/kevm_pyk/kdist/plugin.py new file mode 100644 index 0000000000..aba302d9b1 --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/kdist/plugin.py @@ -0,0 +1,108 @@ +from __future__ import annotations + +from contextlib import contextmanager +from distutils.dir_util import copy_tree +from pathlib import Path +from tempfile import TemporaryDirectory +from typing import TYPE_CHECKING + +from pyk.kbuild.utils import sync_files +from pyk.utils import run_process + +from .. import config +from ..kompile import KompileTarget, kevm_kompile +from . import Target + +if TYPE_CHECKING: + from collections.abc import Iterator, Mapping + from typing import Any, Final + + +class KEVMTarget(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, args: dict[str, Any]) -> None: + verbose = args.get('verbose', False) + enable_llvm_debug = args.get('enable_llvm_debug', False) + + kevm_kompile( + output_dir=output_dir, + enable_llvm_debug=enable_llvm_debug, + verbose=verbose, + **self._kompile_args, + ) + + +class PluginTarget(Target): + def build(self, output_dir: Path, args: dict[str, Any]) -> None: + verbose = args.get('verbose', False) + + sync_files( + source_dir=config.PLUGIN_DIR / 'plugin-c', + target_dir=output_dir / 'plugin-c', + file_names=[ + 'blake2.cpp', + 'blake2.h', + 'crypto.cpp', + 'plugin_util.cpp', + 'plugin_util.h', + ], + ) + + with self._build_env() as build_dir: + run_process( + ['make', 'libcryptopp', 'libff', 'libsecp256k1', '-j3'], + cwd=build_dir, + pipe_stdout=not verbose, + ) + copy_tree(str(build_dir / 'build/libcryptopp'), str(output_dir / 'libcryptopp')) + copy_tree(str(build_dir / 'build/libff'), str(output_dir / 'libff')) + copy_tree(str(build_dir / 'build/libsecp256k1'), str(output_dir / 'libsecp256k1')) + + @contextmanager + def _build_env(self) -> Iterator[Path]: + with TemporaryDirectory(prefix='evm-semantics-plugin-') as build_dir_str: + build_dir = Path(build_dir_str) + copy_tree(str(config.PLUGIN_DIR), str(build_dir)) + yield build_dir + + +__TARGETS__: Final = { + 'llvm': KEVMTarget( + { + 'target': KompileTarget.LLVM, + 'main_file': config.EVM_SEMANTICS_DIR / 'driver.md', + 'main_module': 'ETHEREUM-SIMULATION', + 'syntax_module': 'ETHEREUM-SIMULATION', + 'optimization': 2, + }, + ), + 'haskell': KEVMTarget( + { + 'target': KompileTarget.HASKELL, + 'main_file': config.EVM_SEMANTICS_DIR / 'edsl.md', + 'main_module': 'EDSL', + 'syntax_module': 'EDSL', + }, + ), + 'haskell-standalone': KEVMTarget( + { + 'target': KompileTarget.HASKELL_STANDALONE, + 'main_file': config.EVM_SEMANTICS_DIR / 'driver.md', + 'main_module': 'ETHEREUM-SIMULATION', + 'syntax_module': 'ETHEREUM-SIMULATION', + }, + ), + 'foundry': KEVMTarget( + { + 'target': KompileTarget.FOUNDRY, + 'main_file': config.EVM_SEMANTICS_DIR / 'foundry.md', + 'main_module': 'FOUNDRY', + 'syntax_module': 'FOUNDRY', + }, + ), + 'plugin': PluginTarget(), +} diff --git a/kevm-pyk/src/kevm_pyk/kompile.py b/kevm-pyk/src/kevm_pyk/kompile.py index 93974e3a7f..e410745765 100644 --- a/kevm-pyk/src/kevm_pyk/kompile.py +++ b/kevm-pyk/src/kevm_pyk/kompile.py @@ -10,7 +10,7 @@ from pyk.ktool.kompile import HaskellKompile, KompileArgs, LLVMKompile, LLVMKompileType from pyk.utils import run_process -from . import config +from . import config, kdist if TYPE_CHECKING: from collections.abc import Iterable @@ -147,8 +147,6 @@ def _kompile_haskell() -> None: def _lib_ccopts(kernel: str, debug_build: bool = False) -> list[str]: - from . import dist - ccopts = ['-std=c++17'] if debug_build: @@ -156,7 +154,7 @@ def _lib_ccopts(kernel: str, debug_build: bool = False) -> list[str]: ccopts += ['-lssl', '-lcrypto'] - plugin_dir = dist.check_plugin() + plugin_dir = kdist.get('plugin') libff_dir = plugin_dir / 'libff' ccopts += [f'{libff_dir}/lib/libff.a', f'-I{libff_dir}/include'] diff --git a/kevm-pyk/src/kontrolx/__main__.py b/kevm-pyk/src/kontrolx/__main__.py index 0f1f420d06..ec9da5f06a 100644 --- a/kevm-pyk/src/kontrolx/__main__.py +++ b/kevm-pyk/src/kontrolx/__main__.py @@ -9,8 +9,8 @@ from pyk.cli.utils import file_path from pyk.proof.tui import APRProofViewer +from kevm_pyk import kdist from kevm_pyk.cli import KEVMCLIArgs, node_id_like -from kevm_pyk.dist import DistTarget from kevm_pyk.utils import arg_pair_of from .foundry import ( @@ -86,14 +86,14 @@ def exec_solc_to_k( main_module: str | None, requires: list[str], imports: list[str], - target: DistTarget | None = None, + target: str | None = None, **kwargs: Any, ) -> None: if target is None: - target = DistTarget.HASKELL + target = 'haskell' k_text = solc_to_k( - definition_dir=target.get(), + definition_dir=kdist.get(target), contract_file=contract_file, contract_name=contract_name, main_module=main_module, diff --git a/kevm-pyk/src/kontrolx/foundry.py b/kevm-pyk/src/kontrolx/foundry.py index b6798fc22c..b9753a51f3 100644 --- a/kevm-pyk/src/kontrolx/foundry.py +++ b/kevm-pyk/src/kontrolx/foundry.py @@ -29,7 +29,7 @@ from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter, APRProofShow from pyk.utils import ensure_dir_path, hash_str, run_process, single, unique -from kevm_pyk.dist import DistTarget +from kevm_pyk import kdist from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics from kevm_pyk.utils import ( KDefinition__expand_macros, @@ -535,7 +535,7 @@ def foundry_kompile( copied_requires = [] copied_requires += [f'requires/{name}' for name in list(requires_paths.keys())] imports = ['FOUNDRY'] - kevm = KEVM(DistTarget.FOUNDRY.get()) + kevm = KEVM(kdist.get('foundry')) empty_config = kevm.definition.empty_config(Foundry.Sorts.FOUNDRY_CELL) bin_runtime_definition = _foundry_to_contract_def( empty_config=empty_config, @@ -552,7 +552,7 @@ def foundry_kompile( ) kevm = KEVM( - DistTarget.FOUNDRY.get(), + kdist.get('foundry'), extra_unparsing_modules=(bin_runtime_definition.all_modules + contract_main_definition.all_modules), ) foundry_contracts_file.write_text(kevm.pretty_print(bin_runtime_definition, unalias=False) + '\n') diff --git a/kevm-pyk/src/tests/integration/test_conformance.py b/kevm-pyk/src/tests/integration/test_conformance.py index 1a09be0991..4d8470bf99 100644 --- a/kevm-pyk/src/tests/integration/test_conformance.py +++ b/kevm-pyk/src/tests/integration/test_conformance.py @@ -9,7 +9,7 @@ from pyk.kore.syntax import App from pyk.kore.tools import PrintOutput, kore_print -from kevm_pyk.dist import DistTarget +from kevm_pyk import kdist from kevm_pyk.interpreter import interpret from ..utils import REPO_ROOT @@ -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=DistTarget.LLVM.get(), output=PrintOutput.PRETTY) + pretty = kore_print(pattern, definition_dir=kdist.get('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 70a74ba848..743173c25a 100644 --- a/kevm-pyk/src/tests/integration/test_kast.py +++ b/kevm-pyk/src/tests/integration/test_kast.py @@ -1,6 +1,6 @@ from pyk.ktool.kprint import KAstInput, KAstOutput, _kast -from kevm_pyk.dist import DistTarget +from kevm_pyk import kdist from ..utils import REPO_ROOT @@ -14,7 +14,7 @@ def test_parse() -> None: # When actual = _kast( file=evm_file, - definition_dir=DistTarget.LLVM.get(), + definition_dir=kdist.get('llvm'), input=KAstInput.PROGRAM, output=KAstOutput.KORE, ).stdout diff --git a/kevm-pyk/src/tests/integration/test_run.py b/kevm-pyk/src/tests/integration/test_run.py index 2b86eabcea..492dcecd4d 100644 --- a/kevm-pyk/src/tests/integration/test_run.py +++ b/kevm-pyk/src/tests/integration/test_run.py @@ -6,7 +6,7 @@ import pytest from pyk.kore.tools import PrintOutput, kore_print -from kevm_pyk.dist import DistTarget +from kevm_pyk import kdist from kevm_pyk.interpreter import interpret from ..utils import REPO_ROOT @@ -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=DistTarget.LLVM.get(), output=PrintOutput.PRETTY) + actual = kore_print(pattern, definition_dir=kdist.get('llvm'), output=PrintOutput.PRETTY) # Then assert actual == expected diff --git a/kevm-pyk/src/tests/integration/utils.py b/kevm-pyk/src/tests/integration/utils.py index c28945d44b..368f669f38 100644 --- a/kevm-pyk/src/tests/integration/utils.py +++ b/kevm-pyk/src/tests/integration/utils.py @@ -5,7 +5,7 @@ from pyk.utils import check_dir_path -from kevm_pyk.dist import DistTarget +from kevm_pyk import kdist from kontrolx.solc_to_k import solc_to_k if TYPE_CHECKING: @@ -23,7 +23,7 @@ def gen_bin_runtime(contract_file: Path, output_dir: Path) -> tuple[Path, str]: main_file = output_dir / f'{contract_name.lower()}-bin-runtime.k' k_text = solc_to_k( - definition_dir=DistTarget.HASKELL.get(), + definition_dir=kdist.get('haskell'), contract_file=contract_file, contract_name=contract_name, main_module=main_module_name, diff --git a/package/version b/package/version index 19e25b6182..7a7992a7f3 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.316 +1.0.317