From 81e2ede293afad9d8a7151a1e6203c143b42aded Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 13 Oct 2023 15:02:53 +0200 Subject: [PATCH 1/8] Extract class `Target` and `KEVMTarget` --- kevm-pyk/src/kevm_pyk/dist.py | 95 +++++++++++++++++++++++------------ 1 file changed, 63 insertions(+), 32 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/dist.py b/kevm-pyk/src/kevm_pyk/dist.py index 1543bab7da..41da21199e 100644 --- a/kevm-pyk/src/kevm_pyk/dist.py +++ b/kevm-pyk/src/kevm_pyk/dist.py @@ -4,6 +4,7 @@ import os import shutil import time +from abc import ABC, abstractmethod from argparse import ArgumentParser from concurrent.futures import ThreadPoolExecutor from contextlib import contextmanager @@ -46,6 +47,67 @@ def _dist_dir() -> Path: DIST_DIR: Final = _dist_dir() +class Target(ABC): + @abstractmethod + def build(self, output_dir: Path, args: dict[str, Any]) -> None: + ... + + +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, + ) + + +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', + }, + ), +} + + # --------- # K targets # --------- @@ -84,43 +146,12 @@ 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] - ) + TARGETS[self.value].build(self.path, {'enable_llvm_debug': enable_llvm_debug, 'verbose': verbose}) 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 # -------------- From 3aba3ea6e8afdb2f4ff4780cecbabfac00bbd7ac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 13 Oct 2023 17:13:50 +0200 Subject: [PATCH 2/8] Use `Target` for building --- kevm-pyk/src/kevm_pyk/__main__.py | 19 +- kevm-pyk/src/kevm_pyk/cli.py | 3 +- kevm-pyk/src/kevm_pyk/dist.py | 235 +++++++----------- kevm-pyk/src/kevm_pyk/interpreter.py | 4 +- kevm-pyk/src/kevm_pyk/kompile.py | 2 +- kevm-pyk/src/kontrolx/__main__.py | 8 +- kevm-pyk/src/kontrolx/foundry.py | 6 +- .../src/tests/integration/test_conformance.py | 4 +- kevm-pyk/src/tests/integration/test_kast.py | 4 +- kevm-pyk/src/tests/integration/test_run.py | 4 +- kevm-pyk/src/tests/integration/utils.py | 4 +- 11 files changed, 122 insertions(+), 171 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 185a871567..18f28af08e 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, dist 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 = dist.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 = dist.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(dist.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(dist.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 index 41da21199e..0833fbfe72 100644 --- a/kevm-pyk/src/kevm_pyk/dist.py +++ b/kevm-pyk/src/kevm_pyk/dist.py @@ -9,11 +9,9 @@ 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 typing import TYPE_CHECKING from pyk.cli.args import KCLIArgs from pyk.cli.utils import loglevel @@ -35,16 +33,9 @@ _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() +# ------- +# Targets +# ------- class Target(ABC): @@ -71,6 +62,40 @@ def build(self, output_dir: Path, args: dict[str, Any]) -> None: ) +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( { @@ -105,112 +130,73 @@ def build(self, output_dir: Path, args: dict[str, Any]) -> None: 'syntax_module': 'FOUNDRY', }, ), + 'plugin': PluginTarget(), } -# --------- -# 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 +# ----- +# Build +# ----- - 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: - TARGETS[self.value].build(self.path, {'enable_llvm_debug': enable_llvm_debug, 'verbose': verbose}) - except RuntimeError: - self.clean() - raise +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}' -# -------------- -# Plugin project -# -------------- +DIST_DIR: Final = _dist_dir() -PLUGIN_DIR: Final = DIST_DIR / 'plugin' +def check(target: str) -> None: + if target not in TARGETS: + raise ValueError('Undefined target: {target}') -def check_plugin() -> Path: - if not PLUGIN_DIR.exists(): - raise ValueError('Plugin project is not built') - return PLUGIN_DIR +def which(target: str | None = None) -> Path: + if target: + check(target) + return DIST_DIR / target + return DIST_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(target: str | None = None) -> Path: + res = which(target) + shutil.rmtree(res, ignore_errors=True) + return res -def clean_plugin() -> Path: - shutil.rmtree(PLUGIN_DIR, ignore_errors=True) - return PLUGIN_DIR +def get(target: str) -> Path: + res = which(target) + if not res.exists(): + raise ValueError('Target is not built: {target}') + return res -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', - ], - ) +def get_or_none(target: str) -> Path | None: + res = which(target) + if not res.exists(): + return None + return res - 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')) +def build(target: str, *, force: bool = False, **kwargs: Any) -> Path: + res = which(target) + if not force and res.exists(): + return res + _target = TARGETS[target] -@contextmanager -def _plugin_build_env() -> Iterator[Path]: - with TemporaryDirectory(prefix='evm-semantics-plugin-') as build_dir_str: + with TemporaryDirectory(prefix=f'kevm-dist-{target}-') as build_dir_str: build_dir = Path(build_dir_str) - copy_tree(str(config.PLUGIN_DIR), str(build_dir)) - yield build_dir + _target.build(output_dir=build_dir, args=kwargs) + # TODO Locking + shutil.copytree(build_dir_str, str(res), dirs_exist_ok=True) + + return res # --- @@ -236,9 +222,6 @@ def main() -> None: raise AssertionError() -CliTarget = DistTarget | Literal['plugin'] - - def _exec_build( command: str, targets: list[str], @@ -262,62 +245,41 @@ def _exec_build( 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) + plugin = pool.submit( + 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.1) + time.sleep(0.01) continue result = current.result() print(result) if current == plugin and delay_llvm: - pending += [pool.submit(DistTarget.LLVM.build, force=force)] + pending.append( + pool.submit(build, target='llvm', force=force, enable_llvm_debug=enable_llvm_debug, verbose=verbose) + ) 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) + res = clean(target) + print(res) 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) + res = which(target) + print(res) def _parse_arguments() -> Namespace: - targets = [item.value for item in DistTarget] + ['plugin'] + targets = list(TARGETS) def target(s: str) -> str: # choices does not work well with nargs="*" @@ -358,14 +320,5 @@ def add_target_arg(parser: ArgumentParser, help_text: str) -> None: 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..eacf8887b7 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 dist 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 = dist.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/kompile.py b/kevm-pyk/src/kevm_pyk/kompile.py index 93974e3a7f..58d7c735b3 100644 --- a/kevm-pyk/src/kevm_pyk/kompile.py +++ b/kevm-pyk/src/kevm_pyk/kompile.py @@ -156,7 +156,7 @@ def _lib_ccopts(kernel: str, debug_build: bool = False) -> list[str]: ccopts += ['-lssl', '-lcrypto'] - plugin_dir = dist.check_plugin() + plugin_dir = dist.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..b1c5546f95 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 dist 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=dist.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..30a1de1725 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 dist 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(dist.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(), + dist.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..d892c30fcd 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 dist 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=dist.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..f7652407ed 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 dist 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=dist.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..66f8ad61e1 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 dist 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=dist.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..6c61bf6ebc 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 dist 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=dist.get('haskell'), contract_file=contract_file, contract_name=contract_name, main_module=main_module_name, From 2d4236dd99fe288fff9d10316d4442461607d5a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 13 Oct 2023 17:57:33 +0200 Subject: [PATCH 3/8] Separate CLI, framework and targets --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 10 +- kevm-pyk/src/kevm_pyk/dist.py | 324 ------------------ kevm-pyk/src/kevm_pyk/interpreter.py | 4 +- kevm-pyk/src/kevm_pyk/kdist/__init__.py | 1 + kevm-pyk/src/kevm_pyk/kdist/__main__.py | 143 ++++++++ kevm-pyk/src/kevm_pyk/kdist/_kdist.py | 93 +++++ kevm-pyk/src/kevm_pyk/kdist/targets.py | 108 ++++++ kevm-pyk/src/kevm_pyk/kompile.py | 6 +- kevm-pyk/src/kontrolx/__main__.py | 4 +- kevm-pyk/src/kontrolx/foundry.py | 6 +- .../src/tests/integration/test_conformance.py | 4 +- kevm-pyk/src/tests/integration/test_kast.py | 4 +- kevm-pyk/src/tests/integration/test_run.py | 4 +- kevm-pyk/src/tests/integration/utils.py | 4 +- 15 files changed, 368 insertions(+), 349 deletions(-) delete mode 100644 kevm-pyk/src/kevm_pyk/dist.py create mode 100644 kevm-pyk/src/kevm_pyk/kdist/__init__.py create mode 100644 kevm-pyk/src/kevm_pyk/kdist/__main__.py create mode 100644 kevm-pyk/src/kevm_pyk/kdist/_kdist.py create mode 100644 kevm-pyk/src/kevm_pyk/kdist/targets.py diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 7d5b57c69e..2f1db1b218 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -42,7 +42,7 @@ 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" diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 18f28af08e..19001c135a 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -26,7 +26,7 @@ from pyk.proof.tui import APRProofViewer from pyk.utils import single -from . import VERSION, config, dist +from . import VERSION, config, kdist from .cli import KEVMCLIArgs, node_id_like from .gst_to_kore import SORT_ETHEREUM_SIMULATION, gst_to_kore, kore_pgm_to_kore from .kevm import KEVM, KEVMSemantics, kevm_node_printer @@ -159,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 = dist.get('haskell') + definition_dir = kdist.get('haskell') kevm = KEVM(definition_dir, use_directory=save_directory) @@ -230,7 +230,7 @@ def exec_prove( md_selector = 'k' if definition_dir is None: - definition_dir = dist.get('haskell') + definition_dir = kdist.get('haskell') if smt_timeout is None: smt_timeout = 300 @@ -533,7 +533,7 @@ def exec_run( target = 'llvm' _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(dist.get(target), use_directory=save_directory) + kevm = KEVM(kdist.get(target), use_directory=save_directory) try: json_read = json.loads(input_file.read_text()) @@ -569,7 +569,7 @@ def exec_kast( target = 'llvm' _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(dist.get(target), 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/dist.py b/kevm-pyk/src/kevm_pyk/dist.py deleted file mode 100644 index 0833fbfe72..0000000000 --- a/kevm-pyk/src/kevm_pyk/dist.py +++ /dev/null @@ -1,324 +0,0 @@ -from __future__ import annotations - -import logging -import os -import shutil -import time -from abc import ABC, abstractmethod -from argparse import ArgumentParser -from concurrent.futures import ThreadPoolExecutor -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.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' - - -# ------- -# Targets -# ------- - - -class Target(ABC): - @abstractmethod - def build(self, output_dir: Path, args: dict[str, Any]) -> None: - ... - - -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(), -} - - -# ----- -# Build -# ----- - - -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() - - -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('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: - res = which(target) - if not force and res.exists(): - return res - - _target = TARGETS[target] - - with TemporaryDirectory(prefix=f'kevm-dist-{target}-') as build_dir_str: - build_dir = Path(build_dir_str) - _target.build(output_dir=build_dir, args=kwargs) - # TODO Locking - shutil.copytree(build_dir_str, str(res), dirs_exist_ok=True) - - return res - - -# --- -# 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() - - -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( - 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(build, target='llvm', force=force, enable_llvm_debug=enable_llvm_debug, verbose=verbose) - ) - - pending.remove(current) - - -def _exec_clean(target: str | None) -> None: - res = clean(target) - print(res) - - -def _exec_which(target: str | None) -> None: - res = which(target) - print(res) - - -def _parse_arguments() -> Namespace: - targets = list(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') - - return parser.parse_args() - - -if __name__ == '__main__': - main() diff --git a/kevm-pyk/src/kevm_pyk/interpreter.py b/kevm-pyk/src/kevm_pyk/interpreter.py index eacf8887b7..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 . import dist +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 = dist.get('llvm') / '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..4c8bd3c641 --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/kdist/__main__.py @@ -0,0 +1,143 @@ +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) + + 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 _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') + + 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..139f8b185d --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py @@ -0,0 +1,93 @@ +from __future__ import annotations + +import logging +import os +import shutil +from abc import ABC, abstractmethod +from pathlib import Path +from tempfile import TemporaryDirectory +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 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 targets() -> dict[str, Target]: + from .targets import TARGETS + + return 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('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: + res = which(target) + if not force and res.exists(): + return res + + _target = targets()[target] + + with TemporaryDirectory(prefix=f'kevm-dist-{target}-') as build_dir_str: + build_dir = Path(build_dir_str) + _target.build(output_dir=build_dir, args=kwargs) + # TODO Locking + shutil.copytree(build_dir_str, str(res), dirs_exist_ok=True) + + return res diff --git a/kevm-pyk/src/kevm_pyk/kdist/targets.py b/kevm-pyk/src/kevm_pyk/kdist/targets.py new file mode 100644 index 0000000000..39038fea5b --- /dev/null +++ b/kevm-pyk/src/kevm_pyk/kdist/targets.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 58d7c735b3..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.get('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 b1c5546f95..ec9da5f06a 100644 --- a/kevm-pyk/src/kontrolx/__main__.py +++ b/kevm-pyk/src/kontrolx/__main__.py @@ -9,7 +9,7 @@ from pyk.cli.utils import file_path from pyk.proof.tui import APRProofViewer -from kevm_pyk import dist +from kevm_pyk import kdist from kevm_pyk.cli import KEVMCLIArgs, node_id_like from kevm_pyk.utils import arg_pair_of @@ -93,7 +93,7 @@ def exec_solc_to_k( target = 'haskell' k_text = solc_to_k( - definition_dir=dist.get(target), + 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 30a1de1725..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 import dist +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(dist.get('foundry')) + 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( - dist.get('foundry'), + 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 d892c30fcd..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 import dist +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=dist.get('llvm'), 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 f7652407ed..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 import dist +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=dist.get('llvm'), + 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 66f8ad61e1..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 import dist +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=dist.get('llvm'), 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 6c61bf6ebc..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 import dist +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=dist.get('haskell'), + definition_dir=kdist.get('haskell'), contract_file=contract_file, contract_name=contract_name, main_module=main_module_name, From c5d61eae216651c9569e12112dca4ff41cc33e5d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 16 Oct 2023 16:49:31 +0200 Subject: [PATCH 4/8] Load targets from plugins --- kevm-pyk/pyproject.toml | 3 + kevm-pyk/src/kevm_pyk/kdist/__main__.py | 11 +++ kevm-pyk/src/kevm_pyk/kdist/_kdist.py | 68 ++++++++++++++++++- .../kevm_pyk/kdist/{targets.py => plugin.py} | 2 +- 4 files changed, 80 insertions(+), 4 deletions(-) rename kevm-pyk/src/kevm_pyk/kdist/{targets.py => plugin.py} (99%) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 2f1db1b218..17733b27e8 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -46,6 +46,9 @@ kevm-dist = "kevm_pyk.kdist.__main__:main" gst-to-kore = "kevm_pyk.gst_to_kore:main" kontrolx = "kontrolx.__main__:main" +[tool.poetry.plugins.kevm-dist] +evm-semantics = "kevm_pyk.kdist.plugin" + [tool.isort] profile = "black" line_length = 120 diff --git a/kevm-pyk/src/kevm_pyk/kdist/__main__.py b/kevm-pyk/src/kevm_pyk/kdist/__main__.py index 4c8bd3c641..fd28feed4e 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/__main__.py +++ b/kevm-pyk/src/kevm_pyk/kdist/__main__.py @@ -35,6 +35,9 @@ def main() -> None: elif args.command == 'which': _exec_which(args.target) + elif args.command == 'list': + _exec_list() + else: raise AssertionError() @@ -97,6 +100,12 @@ def _exec_which(target: str | None) -> None: print(res) +def _exec_list() -> None: + targets = kdist.targets() + for target in targets: + print(target) + + def _parse_arguments() -> Namespace: targets = list(kdist.targets()) @@ -136,6 +145,8 @@ def add_target_arg(parser: ArgumentParser, help_text: str) -> None: 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() diff --git a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py index 139f8b185d..bcecc92832 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py +++ b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py @@ -4,6 +4,7 @@ import os import shutil from abc import ABC, abstractmethod +from collections.abc import Mapping from pathlib import Path from tempfile import TemporaryDirectory from typing import TYPE_CHECKING @@ -14,6 +15,7 @@ from .. import config if TYPE_CHECKING: + from types import ModuleType from typing import Any, Final @@ -39,10 +41,70 @@ def build(self, output_dir: Path, args: dict[str, Any]) -> None: ... -def targets() -> dict[str, Target]: - from .targets import TARGETS +def _load() -> dict[str, Target]: + import importlib + from importlib.metadata import entry_points + + plugins = entry_points(group='kevm-dist') + + res: dict[str, Target] = {} + for plugin in plugins: + _LOGGER.info(f'Loading kevm-dist 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__ - return 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: diff --git a/kevm-pyk/src/kevm_pyk/kdist/targets.py b/kevm-pyk/src/kevm_pyk/kdist/plugin.py similarity index 99% rename from kevm-pyk/src/kevm_pyk/kdist/targets.py rename to kevm-pyk/src/kevm_pyk/kdist/plugin.py index 39038fea5b..aba302d9b1 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/targets.py +++ b/kevm-pyk/src/kevm_pyk/kdist/plugin.py @@ -70,7 +70,7 @@ def _build_env(self) -> Iterator[Path]: yield build_dir -TARGETS: Final = { +__TARGETS__: Final = { 'llvm': KEVMTarget( { 'target': KompileTarget.LLVM, From 1f5ae976b234ccc0b017f08079fb1fdf9058e347 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 16 Oct 2023 17:18:39 +0200 Subject: [PATCH 5/8] Fix error message --- kevm-pyk/src/kevm_pyk/kdist/_kdist.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py index bcecc92832..b7e25d6c71 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py +++ b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py @@ -128,7 +128,7 @@ def clean(target: str | None = None) -> Path: def get(target: str) -> Path: res = which(target) if not res.exists(): - raise ValueError('Target is not built: {target}') + raise ValueError(f'Target is not built: {target}') return res From 7b6de14fa78405f78068e4ba9664cb686996ee48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 16 Oct 2023 17:29:33 +0200 Subject: [PATCH 6/8] Rename plugin group --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/kdist/_kdist.py | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 17733b27e8..2f79b04a2a 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -46,7 +46,7 @@ kevm-dist = "kevm_pyk.kdist.__main__:main" gst-to-kore = "kevm_pyk.gst_to_kore:main" kontrolx = "kontrolx.__main__:main" -[tool.poetry.plugins.kevm-dist] +[tool.poetry.plugins.kdist] evm-semantics = "kevm_pyk.kdist.plugin" [tool.isort] diff --git a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py index b7e25d6c71..60712904c1 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py +++ b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py @@ -45,11 +45,11 @@ def _load() -> dict[str, Target]: import importlib from importlib.metadata import entry_points - plugins = entry_points(group='kevm-dist') + plugins = entry_points(group='kdist') res: dict[str, Target] = {} for plugin in plugins: - _LOGGER.info(f'Loading kevm-dist plugin: {plugin.name}') + _LOGGER.info(f'Loading kdist plugin: {plugin.name}') module_name = plugin.value try: _LOGGER.info(f'Importing module: {module_name}') From 83b339dd561cd5c86df83e4515580d615baeaea0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 16 Oct 2023 18:23:10 +0200 Subject: [PATCH 7/8] Write directly to `output_dir` --- kevm-pyk/src/kevm_pyk/kdist/_kdist.py | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py index 60712904c1..e8a3bde682 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/_kdist.py +++ b/kevm-pyk/src/kevm_pyk/kdist/_kdist.py @@ -6,7 +6,6 @@ from abc import ABC, abstractmethod from collections.abc import Mapping from pathlib import Path -from tempfile import TemporaryDirectory from typing import TYPE_CHECKING from pyk.utils import hash_str @@ -140,16 +139,12 @@ def get_or_none(target: str) -> Path | None: def build(target: str, *, force: bool = False, **kwargs: Any) -> Path: - res = which(target) - if not force and res.exists(): - return res + # TODO Locking + output_dir = which(target) + if not force and output_dir.exists(): + return output_dir + output_dir.mkdir(parents=True) _target = targets()[target] - - with TemporaryDirectory(prefix=f'kevm-dist-{target}-') as build_dir_str: - build_dir = Path(build_dir_str) - _target.build(output_dir=build_dir, args=kwargs) - # TODO Locking - shutil.copytree(build_dir_str, str(res), dirs_exist_ok=True) - - return res + _target.build(output_dir, args=kwargs) + return output_dir From 6a76e05063f42c87cfb8b70863b46d6e99b9a07c Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 16 Oct 2023 16:28:01 +0000 Subject: [PATCH 8/8] Set Version: 1.0.317 --- 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 2f79b04a2a..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. ", 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/package/version b/package/version index 19e25b6182..7a7992a7f3 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.316 +1.0.317