diff --git a/package/version b/package/version index 9faa1b7a7..c946ee616 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.5 +0.1.6 diff --git a/pyproject.toml b/pyproject.toml index bb5c253bf..7f58eb3a9 100644 --- a/pyproject.toml +++ b/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. ", diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 0f7b843be..baec8db25 100644 --- a/src/kontrol/__main__.py +++ b/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,28 +549,29 @@ 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.') @@ -572,13 +579,13 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: '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( diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py new file mode 100644 index 000000000..a39fc6aeb --- /dev/null +++ b/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