Refactor summarize command and options in cli.py and __main__.py. (#2725)

- Updated the `exec_summarize` function to support new `SummarizeOptions`, allowing for opcode-specific summarization and an option to clear existing proofs.
- Modified the CLI to replace `ProveOptions` with `SummarizeOptions` for the `summarize` command, enhancing argument handling.
- Introduced a new `clear_proofs` function to remove existing proof files before summarization.
- Improved documentation and help messages for the `summarize` command to clarify usage.

Author: Stevengre

kevm-pyk/src/kevm_pyk/__main__.py

@@ -32,10 +32,15 @@
 from pyk.proof.tui import APRProofViewer
 from pyk.utils import FrozenDict, hash_str, single
 
-from kevm_pyk.summarizer import batch_summarize
+from kevm_pyk.summarizer import batch_summarize, clear_proofs, summarize
 
 from . import VERSION, config
-from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination
+from .cli import (
+    _create_argument_parser,
+    generate_options,
+    get_argument_type_setter,
+    get_option_string_destination,
+)
 from .gst_to_kore import SORT_ETHEREUM_SIMULATION, filter_gst_keys, gst_to_kore, kore_pgm_to_kore
 from .kevm import KEVM, KEVMSemantics, kevm_node_printer
 from .kompile import KompileTarget, kevm_kompile
@@ -65,6 +70,7 @@
         RunOptions,
         SectionEdgeOptions,
         ShowKCFGOptions,
+        SummarizeOptions,
         VersionOptions,
         ViewKCFGOptions,
     )
@@ -636,10 +642,13 @@ def exec_kast(options: KastOptions) -> None:
     print(output_text)
 
 
-def exec_summarize(options: ProveOptions) -> None:
-    # TODO: provide options to summarize specific opcodes using `summarize(opcode)`
-    # TODO: provide options to analyze a specific proof using `analyze_proof(opcode, node_id)`
-    batch_summarize()
+def exec_summarize(options: SummarizeOptions) -> None:
+    if options.clear:
+        clear_proofs()
+    if options.opcode is None:
+        batch_summarize()
+    else:
+        summarize(options.opcode)
 
 
 # Helpers

kevm-pyk/src/kevm_pyk/cli.py

@@ -77,7 +77,7 @@ def generate_options(args: dict[str, Any]) -> LoggingOptions:
         case 'run':
             return RunOptions(args)
         case 'summarize':
-            return ProveOptions(args)
+            return SummarizeOptions(args)
         case _:
             raise ValueError(f'Unrecognized command: {command}')
 
@@ -104,7 +104,7 @@ def get_option_string_destination(command: str, option_string: str) -> str:
         case 'run':
             option_string_destinations = RunOptions.from_option_string()
         case 'summarize':
-            option_string_destinations = ProveOptions.from_option_string()
+            option_string_destinations = SummarizeOptions.from_option_string()
 
     return option_string_destinations.get(option_string, option_string.replace('-', '_'))
 
@@ -134,7 +134,7 @@ def func(par: str) -> str:
         case 'run':
             option_types = RunOptions.get_argument_type()
         case 'summarize':
-            option_types = ProveOptions.get_argument_type()
+            option_types = SummarizeOptions.get_argument_type()
 
     return option_types.get(option_string, func)
 
@@ -191,22 +191,27 @@ def _create_argument_parser() -> ArgumentParser:
         help='Maximum worker threads to use on a single proof to explore separate branches in parallel.',
     )
 
-    command_parser.add_parser(
+    summarize_args = command_parser.add_parser(
         'summarize',
-        help='Summarize an Opcode to execute in a single rewrite step.',
+        help='Summarize a given opcode(s) to execute in a single rewrite step.',
         parents=[
             kevm_cli_args.logging_args,
-            kevm_cli_args.parallel_args,
             kevm_cli_args.k_args,
-            kevm_cli_args.kprove_args,
-            kevm_cli_args.rpc_args,
-            kevm_cli_args.bug_report_args,
-            kevm_cli_args.smt_args,
-            kevm_cli_args.explore_args,
-            # kevm_cli_args.spec_args,
-            config_args.config_args,
         ],
     )
+    summarize_args.add_argument(
+        'opcode',
+        type=str,
+        nargs='?',
+        help='Opcode to summarize. If not provided, all supported opcodes will be summarized.',
+    )
+    summarize_args.add_argument(
+        '--clear',
+        dest='clear',
+        default=False,
+        action='store_true',
+        help='Clear all existing proofs and re-run the summarization process.',
+    )
 
     prune_args = command_parser.add_parser(
         'prune',
@@ -620,6 +625,23 @@ def get_argument_type() -> dict[str, Callable]:
         )
 
 
+class SummarizeOptions(LoggingOptions, KOptions):
+    clear: bool
+    opcode: str | None
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {'clear': False, 'opcode': None}
+
+    @staticmethod
+    def from_option_string() -> dict[str, str]:
+        return LoggingOptions.from_option_string() | KOptions.from_option_string()
+
+    @staticmethod
+    def get_argument_type() -> dict[str, Callable]:
+        return LoggingOptions.get_argument_type() | KOptions.get_argument_type()
+
+
 class PruneOptions(LoggingOptions, KOptions, SpecOptions):
     node: NodeIdLike
 

kevm-pyk/src/kevm_pyk/summarizer.py

@@ -1,6 +1,7 @@
 from __future__ import annotations
 
 import logging
+import shutil
 import time
 import traceback
 from multiprocessing import Pool
@@ -673,8 +674,7 @@ def summarize(opcode_symbol: str) -> tuple[KEVMSummarizer, list[APRProof]]:
     return summarizer, proofs
 
 
-def analyze_proof(opcode: str, node_id: int) -> None:
+def clear_proofs() -> None:
     proof_dir = Path(__file__).parent / 'proofs'
-    save_directory = Path(__file__).parent / 'summaries'
-    summarizer = KEVMSummarizer(proof_dir, save_directory)
-    summarizer.analyze_proof(str(proof_dir / f'{opcode}_SPEC'), node_id)
+    if proof_dir.exists():
+        shutil.rmtree(proof_dir)