Implement a unified flow across all entry points for GST processing (#2820)

* define gst iterator

* apply changes to exec_kast

* update iterator to output kore

* update expected output files

* use _LOGGER instead of print

* Fix syntax error in test-integration target

* tweaks

Author: anvacaru

kevm-pyk/src/kevm_pyk/__main__.py

@@ -32,6 +32,7 @@
 from pyk.proof.tui import APRProofViewer
 from pyk.utils import FrozenDict, hash_str, single
 
+from kevm_pyk.interpreter import iterate_gst
 from kevm_pyk.summarizer import batch_summarize, clear_proofs, summarize
 
 from . import VERSION, config
@@ -41,7 +42,7 @@
     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 .gst_to_kore import SORT_ETHEREUM_SIMULATION, kore_pgm_to_kore
 from .kevm import KEVM, KEVMSemantics, kevm_node_printer
 from .kompile import KompileTarget, kevm_kompile
 from .utils import (
@@ -598,26 +599,38 @@ def exec_run(options: RunOptions) -> None:
 
     try:
         json_read = json.loads(options.input_file.read_text())
-        gst_data = filter_gst_keys(json_read)
-        kore_pattern = gst_to_kore(gst_data, options.schedule, options.mode, options.chainid, options.usegas)
+        if options.gst_name:
+            json_read = {options.gst_name: json_read[options.gst_name]}
+        kore_pattern_list = [
+            (name, kore)
+            for (name, kore) in iterate_gst(json_read, options.schedule, options.mode, options.chainid, options.usegas)
+        ]
     except json.JSONDecodeError:
         pgm_token = KToken(options.input_file.read_text(), KSort('EthereumSimulation'))
         kast_pgm = kevm.parse_token(pgm_token)
         kore_pgm = kevm.kast_to_kore(kast_pgm, sort=KSort('EthereumSimulation'))
-        kore_pattern = kore_pgm_to_kore(
-            kore_pgm, SORT_ETHEREUM_SIMULATION, options.schedule, options.mode, options.chainid, options.usegas
+        kore_pattern_list = [
+            (
+                '',
+                kore_pgm_to_kore(
+                    kore_pgm, SORT_ETHEREUM_SIMULATION, options.schedule, options.mode, options.chainid, options.usegas
+                ),
+            ),
+        ]
+
+    for name, kore_pattern in kore_pattern_list:
+        if name:
+            _LOGGER.info(f'Processing test - {name}')
+        kevm.run(
+            kore_pattern,
+            depth=options.depth,
+            term=True,
+            expand_macros=options.expand_macros,
+            output=options.output,
+            check=True,
+            debugger=options.debugger,
         )
 
-    kevm.run(
-        kore_pattern,
-        depth=options.depth,
-        term=True,
-        expand_macros=options.expand_macros,
-        output=options.output,
-        check=True,
-        debugger=options.debugger,
-    )
-
 
 def exec_kast(options: KastOptions) -> None:
     target = options.target or 'llvm'
@@ -628,17 +641,30 @@ def exec_kast(options: KastOptions) -> None:
 
     try:
         json_read = json.loads(options.input_file.read_text())
-        kore_pattern = gst_to_kore(json_read, options.schedule, options.mode, options.chainid, options.usegas)
+        if options.gst_name:
+            json_read = {options.gst_name: json_read[options.gst_name]}
+        kore_pattern_list = [
+            (name, kore)
+            for (name, kore) in iterate_gst(json_read, options.schedule, options.mode, options.chainid, options.usegas)
+        ]
     except json.JSONDecodeError:
         pgm_token = KToken(options.input_file.read_text(), KSort('EthereumSimulation'))
         kast_pgm = kevm.parse_token(pgm_token)
         kore_pgm = kevm.kast_to_kore(kast_pgm)
-        kore_pattern = kore_pgm_to_kore(
-            kore_pgm, SORT_ETHEREUM_SIMULATION, options.schedule, options.mode, options.chainid, options.usegas
-        )
-
-    output_text = kore_print(kore_pattern, definition_dir=kevm.definition_dir, output=options.output)
-    print(output_text)
+        kore_pattern_list = [
+            (
+                '',
+                kore_pgm_to_kore(
+                    kore_pgm, SORT_ETHEREUM_SIMULATION, options.schedule, options.mode, options.chainid, options.usegas
+                ),
+            ),
+        ]
+
+    for name, kore_pattern in kore_pattern_list:
+        if name:
+            _LOGGER.info(f'Processing test - {name}')
+        output_text = kore_print(kore_pattern, definition_dir=kevm.definition_dir, output=options.output)
+        print(output_text)
 
 
 def exec_summarize(options: SummarizeOptions) -> None:

kevm-pyk/src/kevm_pyk/cli.py

@@ -259,6 +259,13 @@ def _create_argument_parser() -> ArgumentParser:
         ],
     )
     run_args.add_argument('input_file', type=file_path, help='Path to input file.')
+    run_args.add_argument(
+        '--test',
+        type=str,
+        dest='gst_name',
+        default=None,
+        help='Name of the test inside the gst file. By default all tests are processed.',
+    )
     run_args.add_argument(
         '--output',
         type=KRunOutput,
@@ -298,6 +305,13 @@ def _create_argument_parser() -> ArgumentParser:
         ],
     )
     kast_args.add_argument('input_file', type=file_path, help='Path to input file.')
+    kast_args.add_argument(
+        '--test',
+        type=str,
+        dest='gst_name',
+        default=None,
+        help='Name of the test inside the gst file. By default all tests are processed.',
+    )
     kast_args.add_argument(
         '--output',
         type=PrintOutput,
@@ -755,14 +769,11 @@ class RunOptions(
     output: KRunOutput
     expand_macros: bool
     debugger: bool
+    gst_name: str | None
 
     @staticmethod
     def default() -> dict[str, Any]:
-        return {
-            'output': KRunOutput.PRETTY,
-            'expand_macros': True,
-            'debugger': False,
-        }
+        return {'output': KRunOutput.PRETTY, 'expand_macros': True, 'debugger': False, 'gst_name': None}
 
     @staticmethod
     def from_option_string() -> dict[str, str]:
@@ -798,11 +809,13 @@ class KastOptions(
 ):
     input_file: Path
     output: PrintOutput
+    gst_name: str | None
 
     @staticmethod
     def default() -> dict[str, Any]:
         return {
             'output': PrintOutput.KORE,
+            'gst_name': None,
         }
 
     @staticmethod

kevm-pyk/src/kevm_pyk/interpreter.py

@@ -8,12 +8,23 @@
 from .gst_to_kore import filter_gst_keys, gst_to_kore
 
 if TYPE_CHECKING:
+    from collections.abc import Iterator
     from typing import Any
 
-    from pyk.kore.syntax import Pattern
+    from pyk.kore.syntax import App, Pattern
 
 
-def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool, *, check: bool = True) -> Pattern:
+def iterate_gst(
+    gst_data: dict, schedule: str, mode: str, chainid: int, usegas: bool, skipped_keys: frozenset[str] = frozenset()
+) -> Iterator[tuple[str, App]]:
+    """Yield (test_name, kore_pattern) for each test in GST data after filtering discarded keys."""
+    for test_name, test in gst_data.items():
+        if test_name in skipped_keys:
+            continue
+        gst_filtered = {test_name: filter_gst_keys(test)}
+        yield test_name, gst_to_kore(gst_filtered, schedule, mode, chainid, usegas)
+
+
+def interpret(init_kore: Any, *, check: bool = True) -> Pattern:
     """Interpret the given GST data using the LLVM backend."""
-    init_kore = gst_to_kore(filter_gst_keys(gst_data), schedule, mode, chainid, usegas)
     return llvm_interpret(kdist.get('evm-semantics.llvm'), init_kore, check=check)

kevm-pyk/src/tests/integration/test_run.py

@@ -7,7 +7,7 @@
 from pyk.kdist import kdist
 from pyk.kore.tools import PrintOutput, kore_print
 
-from kevm_pyk.interpreter import interpret
+from kevm_pyk.interpreter import interpret, iterate_gst
 
 from ..utils import REPO_ROOT
 
@@ -30,9 +30,11 @@ def test_run(gst_file: Path, update_expected_output: bool) -> None:
     with gst_file.open() as f:
         gst_data = json.load(f)
 
+    actual = ''
     # When
-    pattern = interpret(gst_data, 'PRAGUE', 'NORMAL', 1, True, check=False)
-    actual = kore_print(pattern, definition_dir=kdist.get('evm-semantics.llvm'), output=PrintOutput.PRETTY)
+    for _, init_kore in iterate_gst(gst_data, 'PRAGUE', 'NORMAL', 1, True):
+        pattern = interpret(init_kore, check=False)
+        actual += kore_print(pattern, definition_dir=kdist.get('evm-semantics.llvm'), output=PrintOutput.PRETTY)
 
     # Then
 

kevm-pyk/src/tests/unit/test_gst_to_kore.py

@@ -6,7 +6,7 @@
 import pytest
 from pyk.kore.parser import KoreParser
 
-from kevm_pyk.gst_to_kore import gst_to_kore
+from kevm_pyk.interpreter import iterate_gst
 
 from ..utils import REPO_ROOT
 
@@ -35,17 +35,22 @@ def test_gst_to_kore(gst_path: str, expected_path: str, update_expected_output:
     # Given
     gst_file = REPO_ROOT / gst_path
     gst_data = json.loads(gst_file.read_text())
-
     expected_file = REPO_ROOT / expected_path
-    expected = KoreParser(expected_file.read_text()).pattern()
 
     # When
-    actual = gst_to_kore(gst_data, 'CANCUN', 'NORMAL', 1, True)
+    actuals = [kore for _, kore in iterate_gst(gst_data, 'CANCUN', 'NORMAL', 1, True)]
 
     # Then
     if update_expected_output:
         with expected_file.open('w') as f:
-            actual.write(f)
+            for kore in actuals:
+                kore.write(f)
+                f.write('\n')
         return
 
-    assert actual == expected
+    expected_lines = expected_file.read_text().strip().split('\n')
+    assert len(actuals) == len(expected_lines)
+
+    for actual, expected_line in zip(actuals, expected_lines, strict=True):
+        expected = KoreParser(expected_line).pattern()
+        assert actual == expected

kevm-pyk/src/tests/utils.py

@@ -12,7 +12,7 @@
 from pyk.kore.syntax import App
 from pyk.kore.tools import PrintOutput, kore_print
 
-from kevm_pyk.interpreter import interpret
+from kevm_pyk.interpreter import interpret, iterate_gst
 
 if TYPE_CHECKING:
     from collections.abc import Callable
@@ -88,11 +88,9 @@ def _test(
 
     chain_id = compute_chain_id(gst_file_relative_path)
 
-    for test_name, test in gst_data.items():
+    for test_name, init_kore in iterate_gst(gst_data, schedule, mode, chain_id, usegas, skipped_gst_tests):
         _LOGGER.info(f'Running test: {gst_file} - {test_name}')
-        if test_name in skipped_gst_tests:
-            continue
-        res = interpret({test_name: test}, schedule, mode, chain_id, usegas, check=False)
+        res = interpret(init_kore, check=False)
 
         try:
             _assert_exit_code_zero(res)