From ad4a3d31edf210c8169838b705841d3a401616c5 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 6 Nov 2023 17:41:44 -0600 Subject: [PATCH] Add infrastructure to KEVM for Maude Backend (#2118) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * add MAUDE KompileTarget * add maude_port flag to legacy_explore * add command line arguments * Set Version: 1.0.329 * Set Version: 1.0.330 * Set Version: 1.0.331 * Set Version: 1.0.332 * Set Version: 1.0.333 * Set Version: 1.0.337 --------- Co-authored-by: devops Co-authored-by: Everett Hildenbrandt Co-authored-by: Petar Maksimović --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/cli.py | 14 ++++++++++++++ kevm-pyk/src/kevm_pyk/kompile.py | 27 +++++++++++++++++++++++++-- kevm-pyk/src/kevm_pyk/utils.py | 16 ++++++++++++++-- package/version | 2 +- 6 files changed, 56 insertions(+), 7 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index fd46e8aa5b..474096642e 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.336" +version = "1.0.337" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 685d2ba82a..e10cfe6b55 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.336' +VERSION: Final = '1.0.337' diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 14633bd3a1..211345b549 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -231,6 +231,20 @@ def explore_args(self) -> ArgumentParser: default=None, help='Custom command to start RPC server', ) + args.add_argument( + '--port', + dest='port', + type=int, + default=None, + help='Use existing RPC server on named port', + ) + args.add_argument( + '--maude-port', + dest='maude_port', + type=int, + default=None, + help='Use existing Maude RPC server on named port', + ) args.add_argument( '--failure-information', dest='failure_info', diff --git a/kevm-pyk/src/kevm_pyk/kompile.py b/kevm-pyk/src/kevm_pyk/kompile.py index 9f3d16acb0..d48c9622ef 100644 --- a/kevm-pyk/src/kevm_pyk/kompile.py +++ b/kevm-pyk/src/kevm_pyk/kompile.py @@ -7,7 +7,7 @@ from pathlib import Path from typing import TYPE_CHECKING -from pyk.ktool.kompile import HaskellKompile, KompileArgs, LLVMKompile, LLVMKompileType +from pyk.ktool.kompile import HaskellKompile, KompileArgs, LLVMKompile, LLVMKompileType, MaudeKompile from pyk.utils import run_process from . import config @@ -29,13 +29,14 @@ class KompileTarget(Enum): LLVM = 'llvm' HASKELL = 'haskell' HASKELL_BOOSTER = 'haskell-booster' + MAUDE = 'maude' @property def md_selector(self) -> str: match self: case self.LLVM: return 'k & ! symbolic' - case self.HASKELL | self.HASKELL_BOOSTER: + case self.HASKELL | self.HASKELL_BOOSTER | self.MAUDE: return 'k & ! concrete' case _: raise AssertionError() @@ -106,6 +107,28 @@ def kevm_kompile( ) return kompile(output_dir=output_dir, debug=debug, verbose=verbose) + case KompileTarget.MAUDE: + kompile_maude = MaudeKompile( + base_args=base_args, + ) + kompile_haskell = HaskellKompile(base_args=base_args) + + maude_dir = output_dir / 'kompiled-maude' + + def _kompile_maude() -> None: + kompile_maude(output_dir=maude_dir, debug=debug, verbose=verbose) + + def _kompile_haskell() -> None: + kompile_haskell(output_dir=output_dir, debug=debug, verbose=verbose) + + with concurrent.futures.ThreadPoolExecutor(max_workers=2) as executor: + futures = [ + executor.submit(_kompile_maude), + executor.submit(_kompile_haskell), + ] + [future.result() for future in futures] + + return output_dir case KompileTarget.HASKELL_BOOSTER: assert plugin_dir ccopts = list(ccopts) + _lib_ccopts(plugin_dir, kernel, debug_build=debug_build) diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index fb4b12895a..d7c1d52f1b 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -18,7 +18,7 @@ ) from pyk.kast.outer import KSequence from pyk.kcfg import KCFGExplore -from pyk.kore.rpc import KoreClient, KoreExecLogFormat, kore_server +from pyk.kore.rpc import KoreClient, KoreExecLogFormat, TransportType, kore_server from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver from pyk.proof.equality import EqualityProof, EqualityProver from pyk.utils import single @@ -310,6 +310,7 @@ def legacy_explore( log_axioms_file: Path | None = None, trace_rewrites: bool = False, start_server: bool = True, + maude_port: int | None = None, ) -> Iterator[KCFGExplore]: if start_server: # Old way of handling KCFGExplore, to be removed @@ -337,7 +338,18 @@ def legacy_explore( else: if port is None: raise ValueError('Missing port with start_server=False') - with KoreClient('localhost', port, bug_report=bug_report, bug_report_id=id) as client: + if maude_port is None: + dispatch = None + else: + dispatch = { + 'execute': [('localhost', maude_port, TransportType.HTTP)], + 'simplify': [('localhost', maude_port, TransportType.HTTP)], + 'add-module': [ + ('localhost', maude_port, TransportType.HTTP), + ('localhost', port, TransportType.SINGLE_SOCKET), + ], + } + with KoreClient('localhost', port, bug_report=bug_report, bug_report_id=id, dispatch=dispatch) as client: yield KCFGExplore( kprint=kprint, kore_client=client, diff --git a/package/version b/package/version index af7d9505d1..1e12fc6419 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.336 +1.0.337