Add target namespaces to kdist (#2154)

* Validate plugin and target identifiers * Introduce target namespaces * Use fully qualified target names * Add wildcard feature to command `build` * Set Version: 1.0.343 * Set Version: 1.0.344 --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Nov 9, 2023 · d865f21 · d865f21
1 parent 835ee7b
commit d865f21
Show file tree

Hide file tree

Showing 14 changed files with 147 additions and 97 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -108,7 +108,7 @@ jobs:
       - name: 'Build kevm-pyk'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` llvm haskell'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` evm-semantics.llvm evm-semantics.haskell'
       - name: 'Test integration'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-integration'
       - name: 'Test conformance'
@@ -150,7 +150,7 @@ jobs:
       - name: 'Build kevm-pyk'
         run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build distribution'
-        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin haskell'
+        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell'
       - name: 'Prove Haskell'
         run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make ${{ matrix.test-suite }} PYTEST_ARGS='-vv ${{ matrix.test-args }}' PYTEST_PARALLEL=4"
       - name: 'Tear down Docker'

diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.343"
+version = "1.0.344"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[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.343'
+VERSION: Final = '1.0.344'
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -162,7 +162,7 @@ def exec_prove_legacy(
     _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}')
 
     if definition_dir is None:
-        definition_dir = kdist.get('haskell')
+        definition_dir = kdist.get('evm-semantics.haskell')
 
     kevm = KEVM(definition_dir, use_directory=save_directory)
 
@@ -298,7 +298,7 @@ def exec_prove(
     digest_file = save_directory / 'digest' if save_directory is not None else None
 
     if definition_dir is None:
-        definition_dir = kdist.get('haskell')
+        definition_dir = kdist.get('evm-semantics.haskell')
 
     if smt_timeout is None:
         smt_timeout = 300
@@ -608,8 +608,10 @@ def exec_run(
     if target is None:
         target = 'llvm'
 
+    target_fqn = f'evm-semantics.{target}'
+
     _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}')
-    kevm = KEVM(kdist.get(target), use_directory=save_directory)
+    kevm = KEVM(kdist.get(target_fqn), use_directory=save_directory)
 
     try:
         json_read = json.loads(input_file.read_text())
@@ -644,8 +646,10 @@ def exec_kast(
     if target is None:
         target = 'llvm'
 
+    target_fqn = f'evm-semantics.{target}'
+
     _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}')
-    kevm = KEVM(kdist.get(target), use_directory=save_directory)
+    kevm = KEVM(kdist.get(target_fqn), use_directory=save_directory)
 
     try:
         json_read = json.loads(input_file.read_text())

diff --git a/kevm-pyk/src/kevm_pyk/interpreter.py b/kevm-pyk/src/kevm_pyk/interpreter.py
@@ -26,7 +26,7 @@ def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, *, check: b
 
 
 def _interpret(gst_data: Any, schedule: str, mode: str, chainid: int) -> CompletedProcess:
-    interpreter = kdist.get('llvm') / 'interpreter'
+    interpreter = kdist.get('evm-semantics.llvm') / 'interpreter'
     init_kore = gst_to_kore(gst_data, schedule, mode, chainid)
     proc_res = run_process([str(interpreter), '/dev/stdin', '-1', '/dev/stdout'], input=init_kore.text, check=False)
     return proc_res
diff --git a/kevm-pyk/src/kevm_pyk/kdist/__init__.py b/kevm-pyk/src/kevm_pyk/kdist/__init__.py
@@ -1 +1 @@
-from ._kdist import build, check, clean, get, get_or_none, targets, which
+from ._kdist import build, clean, get, get_or_none, plugins, resolve, targets, which
diff --git a/kevm-pyk/src/kevm_pyk/kdist/__main__.py b/kevm-pyk/src/kevm_pyk/kdist/__main__.py
@@ -1,5 +1,6 @@
 from __future__ import annotations
 
+import fnmatch
 import logging
 from argparse import ArgumentParser
 from typing import TYPE_CHECKING
@@ -48,9 +49,17 @@ def _exec_build(
     verbose: bool,
     debug: bool,
 ) -> None:
+    all_target_fqns = kdist.targets()
+    target_fqns = []
+    for pattern in targets:
+        matches = fnmatch.filter(all_target_fqns, pattern)
+        if not matches:
+            raise ValueError(f'No target matches pattern: {pattern!r}')
+        target_fqns += matches
+
     verbose = verbose or debug
     kdist.build(
-        targets=targets,
+        target_fqns=target_fqns,
         jobs=jobs,
         force=force,
         enable_llvm_debug=enable_llvm_debug,
@@ -69,25 +78,19 @@ def _exec_which(target: str | None) -> None:
 
 
 def _exec_list() -> None:
-    for target in kdist.targets():
-        print(target)
+    plugins = kdist.plugins()
+    for plugin in plugins:
+        print(plugin)
+        for target in plugins[plugin]:
+            print(f'* {target}')
 
 
 def _parse_arguments() -> Namespace:
-    targets = kdist.targets()
-
-    def target(s: str) -> str:
-        #  choices does not work well with nargs="*"
-        if s not in targets:
-            raise TypeError()
-        return s
-
     def add_target_arg(parser: ArgumentParser, help_text: str) -> None:
         parser.add_argument(
             'target',
             metavar='TARGET',
             nargs='?',
-            choices=targets,
             help=help_text,
         )
 
@@ -97,9 +100,7 @@ def add_target_arg(parser: ArgumentParser, help_text: str) -> None:
     command_parser = parser.add_subparsers(dest='command', required=True)
 
     build_parser = command_parser.add_parser('build', help='build targets')
-    build_parser.add_argument(
-        'targets', metavar='TARGET', nargs='*', type=target, default=targets, help='target to build'
-    )
+    build_parser.add_argument('targets', metavar='TARGET', nargs='*', default='*', help='target to build')
     build_parser.add_argument('-f', '--force', action='store_true', default=False, help='force build')
     build_parser.add_argument('-j', '--jobs', metavar='N', type=int, default=1, help='maximal number of build jobs')
     build_parser.add_argument(
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		VERSION: Final = '1.0.343'
		VERSION: Final = '1.0.344'
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		from ._kdist import build, check, clean, get, get_or_none, targets, which
		from ._kdist import build, clean, get, get_or_none, plugins, resolve, targets, which