Add KontrolCLIArgs module (#45)

* __main__, cli: add KontrolCLIArgs module for foundry arguments

* Set Version: 0.1.5

* kontrol/cli: option --foundry-project-root => --root, to mimic direct forge calls better

* Revert "kontrol/cli: option --foundry-project-root => --root, to mimic direct forge calls better"

This reverts commit 0b5fdbd.

* kontrol/cli: adjust to pre-update version of KEVM

* Set Version: 0.1.6

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

package/version

@@ -1 +1 @@
-0.1.5
+0.1.6

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.5"
+version = "0.1.6"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kontrol/__main__.py

@@ -8,12 +8,13 @@
 from argparse import ArgumentParser
 from typing import TYPE_CHECKING
 
-from kevm_pyk.cli import KEVMCLIArgs, node_id_like
+from kevm_pyk.cli import node_id_like
 from kevm_pyk.dist import DistTarget
 from kevm_pyk.utils import arg_pair_of
 from pyk.cli.utils import file_path
 from pyk.proof.tui import APRProofViewer
 
+from .cli import KontrolCLIArgs
 from .foundry import (
     Foundry,
     foundry_get_model,
@@ -417,7 +418,7 @@ def parse(s: str) -> list[T]:
 
         return parse
 
-    kevm_cli_args = KEVMCLIArgs()
+    kontrol_cli_args = KontrolCLIArgs()
     parser = ArgumentParser(prog='kontrol')
 
     command_parser = parser.add_subparsers(dest='command', required=True)
@@ -430,7 +431,12 @@ def parse(s: str) -> list[T]:
     solc_to_k_args = command_parser.add_parser(
         'solc-to-k',
         help='Output helper K definition for given JSON output from solc compiler.',
-        parents=[kevm_cli_args.logging_args, kevm_cli_args.target_args, kevm_cli_args.k_args, kevm_cli_args.k_gen_args],
+        parents=[
+            kontrol_cli_args.logging_args,
+            kontrol_cli_args.target_args,
+            kontrol_cli_args.k_args,
+            kontrol_cli_args.k_gen_args,
+        ],
     )
     solc_to_k_args.add_argument('contract_file', type=file_path, help='Path to contract file.')
     solc_to_k_args.add_argument('contract_name', type=str, help='Name of contract to generate K helpers for.')
@@ -449,11 +455,11 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
         'build',
         help='Kompile K definition corresponding to given output directory.',
         parents=[
-            kevm_cli_args.logging_args,
-            kevm_cli_args.k_args,
-            kevm_cli_args.k_gen_args,
-            kevm_cli_args.kompile_args,
-            kevm_cli_args.foundry_args,
+            kontrol_cli_args.logging_args,
+            kontrol_cli_args.k_args,
+            kontrol_cli_args.k_gen_args,
+            kontrol_cli_args.kompile_args,
+            kontrol_cli_args.foundry_args,
         ],
     )
     build.add_argument(
@@ -475,15 +481,15 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
         'prove',
         help='Run Foundry Proof.',
         parents=[
-            kevm_cli_args.logging_args,
-            kevm_cli_args.parallel_args,
-            kevm_cli_args.k_args,
-            kevm_cli_args.kprove_args,
-            kevm_cli_args.smt_args,
-            kevm_cli_args.rpc_args,
-            kevm_cli_args.bug_report_args,
-            kevm_cli_args.explore_args,
-            kevm_cli_args.foundry_args,
+            kontrol_cli_args.logging_args,
+            kontrol_cli_args.parallel_args,
+            kontrol_cli_args.k_args,
+            kontrol_cli_args.kprove_args,
+            kontrol_cli_args.smt_args,
+            kontrol_cli_args.rpc_args,
+            kontrol_cli_args.bug_report_args,
+            kontrol_cli_args.explore_args,
+            kontrol_cli_args.foundry_args,
         ],
     )
     prove_args.add_argument(
@@ -528,12 +534,12 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
         'show',
         help='Display a given Foundry CFG.',
         parents=[
-            kevm_cli_args.foundry_test_args,
-            kevm_cli_args.logging_args,
-            kevm_cli_args.k_args,
-            kevm_cli_args.kcfg_show_args,
-            kevm_cli_args.display_args,
-            kevm_cli_args.foundry_args,
+            kontrol_cli_args.foundry_test_args,
+            kontrol_cli_args.logging_args,
+            kontrol_cli_args.k_args,
+            kontrol_cli_args.kcfg_show_args,
+            kontrol_cli_args.display_args,
+            kontrol_cli_args.foundry_args,
         ],
     )
     show_args.add_argument(
@@ -543,42 +549,43 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
         action='store_true',
         help='Strip output that is likely to change without the contract logic changing',
     )
+
     command_parser.add_parser(
         'to-dot',
         help='Dump the given CFG for the test as DOT for visualization.',
-        parents=[kevm_cli_args.foundry_test_args, kevm_cli_args.logging_args, kevm_cli_args.foundry_args],
+        parents=[kontrol_cli_args.foundry_test_args, kontrol_cli_args.logging_args, kontrol_cli_args.foundry_args],
     )
 
     command_parser.add_parser(
         'list',
         help='List information about CFGs on disk',
-        parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.foundry_args],
+        parents=[kontrol_cli_args.logging_args, kontrol_cli_args.k_args, kontrol_cli_args.foundry_args],
     )
 
     command_parser.add_parser(
         'view-kcfg',
         help='Display tree view of CFG',
-        parents=[kevm_cli_args.foundry_test_args, kevm_cli_args.logging_args, kevm_cli_args.foundry_args],
+        parents=[kontrol_cli_args.foundry_test_args, kontrol_cli_args.logging_args, kontrol_cli_args.foundry_args],
     )
 
     remove_node = command_parser.add_parser(
         'remove-node',
         help='Remove a node and its successors.',
-        parents=[kevm_cli_args.foundry_test_args, kevm_cli_args.logging_args, kevm_cli_args.foundry_args],
+        parents=[kontrol_cli_args.foundry_test_args, kontrol_cli_args.logging_args, kontrol_cli_args.foundry_args],
     )
     remove_node.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.')
 
     simplify_node = command_parser.add_parser(
         'simplify-node',
         help='Simplify a given node, and potentially replace it.',
         parents=[
-            kevm_cli_args.foundry_test_args,
-            kevm_cli_args.logging_args,
-            kevm_cli_args.smt_args,
-            kevm_cli_args.rpc_args,
-            kevm_cli_args.bug_report_args,
-            kevm_cli_args.display_args,
-            kevm_cli_args.foundry_args,
+            kontrol_cli_args.foundry_test_args,
+            kontrol_cli_args.logging_args,
+            kontrol_cli_args.smt_args,
+            kontrol_cli_args.rpc_args,
+            kontrol_cli_args.bug_report_args,
+            kontrol_cli_args.display_args,
+            kontrol_cli_args.foundry_args,
         ],
     )
     simplify_node.add_argument('node', type=node_id_like, help='Node to simplify in CFG.')
@@ -590,12 +597,12 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
         'step-node',
         help='Step from a given node, adding it to the CFG.',
         parents=[
-            kevm_cli_args.foundry_test_args,
-            kevm_cli_args.logging_args,
-            kevm_cli_args.rpc_args,
-            kevm_cli_args.bug_report_args,
-            kevm_cli_args.smt_args,
-            kevm_cli_args.foundry_args,
+            kontrol_cli_args.foundry_test_args,
+            kontrol_cli_args.logging_args,
+            kontrol_cli_args.rpc_args,
+            kontrol_cli_args.bug_report_args,
+            kontrol_cli_args.smt_args,
+            kontrol_cli_args.foundry_args,
         ],
     )
     step_node.add_argument('node', type=node_id_like, help='Node to step from in CFG.')
@@ -607,9 +614,9 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
         'merge-nodes',
         help='Merge multiple nodes into one branch.',
         parents=[
-            kevm_cli_args.foundry_test_args,
-            kevm_cli_args.logging_args,
-            kevm_cli_args.foundry_args,
+            kontrol_cli_args.foundry_test_args,
+            kontrol_cli_args.logging_args,
+            kontrol_cli_args.foundry_args,
         ],
     )
     merge_node.add_argument(
@@ -625,12 +632,12 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
         'section-edge',
         help='Given an edge in the graph, cut it into sections to get intermediate nodes.',
         parents=[
-            kevm_cli_args.foundry_test_args,
-            kevm_cli_args.logging_args,
-            kevm_cli_args.rpc_args,
-            kevm_cli_args.bug_report_args,
-            kevm_cli_args.smt_args,
-            kevm_cli_args.foundry_args,
+            kontrol_cli_args.foundry_test_args,
+            kontrol_cli_args.logging_args,
+            kontrol_cli_args.rpc_args,
+            kontrol_cli_args.bug_report_args,
+            kontrol_cli_args.smt_args,
+            kontrol_cli_args.foundry_args,
         ],
     )
     section_edge.add_argument('edge', type=arg_pair_of(str, str), help='Edge to section in CFG.')
@@ -640,11 +647,11 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
         'get-model',
         help='Display a model for a given node.',
         parents=[
-            kevm_cli_args.foundry_test_args,
-            kevm_cli_args.logging_args,
-            kevm_cli_args.rpc_args,
-            kevm_cli_args.smt_args,
-            kevm_cli_args.foundry_args,
+            kontrol_cli_args.foundry_test_args,
+            kontrol_cli_args.logging_args,
+            kontrol_cli_args.rpc_args,
+            kontrol_cli_args.smt_args,
+            kontrol_cli_args.foundry_args,
         ],
     )
     get_model.add_argument(

src/kontrol/cli.py

@@ -0,0 +1,54 @@
+from __future__ import annotations
+
+from argparse import ArgumentParser
+from functools import cached_property
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+from kevm_pyk.cli import KEVMCLIArgs
+from pyk.cli.utils import dir_path
+
+if TYPE_CHECKING:
+    from typing import TypeVar
+
+    T = TypeVar('T')
+
+
+class KontrolCLIArgs(KEVMCLIArgs):
+    @cached_property
+    def foundry_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument(
+            '--foundry-project-root',
+            dest='foundry_root',
+            type=dir_path,
+            default=Path('.'),
+            help='Path to Foundry project root directory.',
+        )
+        return args
+
+    @cached_property
+    def foundry_test_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument('test', type=str, help='Test to run')
+        args.add_argument('--id', type=str, default=None, required=False, help='ID of the test')
+        return args
+
+    @cached_property
+    def k_gen_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument(
+            '--require',
+            dest='requires',
+            default=[],
+            action='append',
+            help='Extra K requires to include in generated output.',
+        )
+        args.add_argument(
+            '--module-import',
+            dest='imports',
+            default=[],
+            action='append',
+            help='Extra modules to import into generated main module.',
+        )
+        return args