Add infrastructure to KEVM for Maude Backend (#2118)

* 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 <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
runtimeverification · Nov 6, 2023 · ad4a3d3 · ad4a3d3
1 parent 95528bb
commit ad4a3d3
Show file tree

Hide file tree

Showing 6 changed files with 56 additions and 7 deletions.
diff --git 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. <[email protected]>",

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -1 +1 @@
-1.0.336
+1.0.337
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		VERSION: Final = '1.0.336'
		VERSION: Final = '1.0.337'