Add an instance for CTermSymbolic to custom_step (#4700)

Needed for runtimeverification/kontrol#899 to
expose the `simplify` endpoint in the `custom_step` function.

Author: anvacaru

pyk/src/pyk/kcfg/explore.py

@@ -220,7 +220,7 @@ def extend_cterm(
         module_name: str | None = None,
     ) -> list[KCFGExtendResult]:
 
-        custom_step_result = self.kcfg_semantics.custom_step(_cterm)
+        custom_step_result = self.kcfg_semantics.custom_step(_cterm, self.cterm_symbolic)
         if custom_step_result is not None:
             return [custom_step_result]
 

pyk/src/pyk/kcfg/semantics.py

@@ -4,7 +4,7 @@
 from typing import TYPE_CHECKING
 
 if TYPE_CHECKING:
-    from ..cterm import CTerm
+    from ..cterm import CTerm, CTermSymbolic
     from .kcfg import KCFGExtendResult
 
 
@@ -35,7 +35,7 @@ def can_make_custom_step(self, c: CTerm) -> bool: ...
     """Check whether or not the semantics can make a custom step from a given ``CTerm``."""
 
     @abstractmethod
-    def custom_step(self, c: CTerm) -> KCFGExtendResult | None: ...
+    def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None: ...
 
     """Implement a custom semantic step."""
 
@@ -61,7 +61,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
     def can_make_custom_step(self, c: CTerm) -> bool:
         return False
 
-    def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
+    def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None:
         return None
 
     def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool:

pyk/src/tests/integration/ktool/test_imp.py

@@ -21,7 +21,7 @@
     from collections.abc import Iterable
     from typing import Final
 
-    from pyk.cterm import CTerm
+    from pyk.cterm import CTerm, CTermSymbolic
     from pyk.kast.outer import KDefinition
     from pyk.kcfg import KCFGExplore
     from pyk.kcfg.kcfg import KCFGExtendResult
@@ -71,7 +71,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
     def can_make_custom_step(self, c: CTerm) -> bool:
         return False
 
-    def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
+    def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None:
         return None
 
 

pyk/src/tests/integration/proof/test_custom_step.py

@@ -68,7 +68,7 @@ def can_make_custom_step(self, c: CTerm) -> bool:
             and k_cell[0].label.name == 'c_CUSTOM-STEP-SYNTAX_Step'
         )
 
-    def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
+    def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None:
         if self.can_make_custom_step(c):
             new_cterm = CTerm.from_kast(set_cell(c.kast, 'K_CELL', KSequence(KApply('d_CUSTOM-STEP-SYNTAX_Step'))))
             return Step(new_cterm, 1, (), ['CUSTOM-STEP.c.d'], cut=True)
@@ -141,11 +141,17 @@ def _create_kcfg_explore(kcfg_semantics: KCFGSemantics) -> KCFGExplore:
         CUSTOM_STEP_TEST_DATA_APPLY,
         ids=[test_id for test_id, *_ in CUSTOM_STEP_TEST_DATA_APPLY],
     )
-    def test_custom_step_exec(self, test_id: str, cterm: CTerm, expected: KCFGExtendResult | None) -> None:
+    def test_custom_step_exec(
+        self,
+        test_id: str,
+        cterm: CTerm,
+        cterm_symbolic: CTermSymbolic,
+        expected: KCFGExtendResult | None,
+    ) -> None:
 
         # When
         kcfg_semantics = CustomStepSemanticsWithStep()
-        actual = kcfg_semantics.custom_step(cterm)
+        actual = kcfg_semantics.custom_step(cterm, cterm_symbolic)
         # Then
         assert expected == actual