Add AbortedResult to kore.rpc (runtimeverification/pyk#742)

Co-authored-by: devops <[email protected]>

pyk/package/version

@@ -1 +1 @@
-0.1.514
+0.1.515

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.514"
+version = "0.1.515"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

pyk/src/pyk/kcfg/explore.py

@@ -20,7 +20,7 @@
 )
 from ..kast.outer import KRule
 from ..konvert import krule_to_kore
-from ..kore.rpc import SatResult, StopReason, UnknownResult, UnsatResult
+from ..kore.rpc import AbortedResult, SatResult, StopReason, UnknownResult, UnsatResult
 from ..kore.syntax import Import, Module
 from ..prelude import k
 from ..prelude.k import GENERATED_TOP_CELL
@@ -91,6 +91,11 @@ def cterm_execute(
             log_successful_simplifications=self._trace_rewrites if self._trace_rewrites else None,
             log_failed_simplifications=self._trace_rewrites if self._trace_rewrites else None,
         )
+
+        if isinstance(er, AbortedResult):
+            unknown_predicate = er.unknown_predicate.text if er.unknown_predicate else None
+            raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}')
+
         _is_vacuous = er.reason is StopReason.VACUOUS
         depth = er.depth
         next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore))

pyk/src/pyk/kore/rpc.py

@@ -355,6 +355,7 @@ class StopReason(str, Enum):
     CUT_POINT_RULE = 'cut-point-rule'
     TERMINAL_RULE = 'terminal-rule'
     VACUOUS = 'vacuous'
+    ABORTED = 'aborted'
 
 
 @final
@@ -506,6 +507,7 @@ class ExecuteResult(ABC):  # noqa: B024
         StopReason.CUT_POINT_RULE: 'CutPointResult',
         StopReason.TERMINAL_RULE: 'TerminalResult',
         StopReason.VACUOUS: 'VacuousResult',
+        StopReason.ABORTED: 'AbortedResult',
     }
 
     reason: ClassVar[StopReason]
@@ -524,7 +526,7 @@ def from_dict(cls: type[ER], dct: Mapping[str, Any]) -> ER:
     def _check_reason(cls: type[ER], dct: Mapping[str, Any]) -> None:
         reason = StopReason(dct['reason'])
         if reason is not cls.reason:
-            raise ValueError(f"Expected {cls.reason} as 'reason', found: {reason}")
+            raise AssertionError(f"Expected {cls.reason} as 'reason', found: {reason}")
 
 
 @final
@@ -660,6 +662,30 @@ def from_dict(cls: type[VacuousResult], dct: Mapping[str, Any]) -> VacuousResult
         )
 
 
+@final
+@dataclass(frozen=True)
+class AbortedResult(ExecuteResult):
+    reason = StopReason.ABORTED
+    next_states = None
+    rule = None
+
+    state: State
+    depth: int
+    unknown_predicate: Pattern | None
+    logs: tuple[LogEntry, ...]
+
+    @classmethod
+    def from_dict(cls: type[AbortedResult], dct: Mapping[str, Any]) -> AbortedResult:
+        cls._check_reason(dct)
+        logs = tuple(LogEntry.from_dict(l) for l in dct['logs']) if 'logs' in dct else ()
+        return AbortedResult(
+            state=State.from_dict(dct['state']),
+            depth=dct['depth'],
+            unknown_predicate=kore_term(dct['unknown-predicate'], Pattern) if dct.get('unknown-predicate') else None,  # type: ignore
+            logs=logs,
+        )
+
+
 @final
 @dataclass(frozen=True)
 class ImpliesResult:

pyk/src/tests/unit/kore/test_client.py

@@ -8,6 +8,7 @@
 
 from pyk.kore.prelude import INT, int_dv
 from pyk.kore.rpc import (
+    AbortedResult,
     ImpliesResult,
     JsonRpcClient,
     KoreClient,
@@ -106,6 +107,22 @@ def kore_client(mock: Mock, mock_class: Mock) -> Iterator[KoreClient]:  # noqa:
         },
         VacuousResult(State(int_dv(2), int_top, int_top), 1, logs=()),
     ),
+    (
+        int_dv(0),
+        {'state': kore(int_dv(0))},
+        {
+            'state': {'term': kore(int_dv(1)), 'substitution': kore(int_dv(2)), 'predicate': kore(int_dv(3))},
+            'depth': 4,
+            'unknown-predicate': kore(int_dv(5)),
+            'reason': 'aborted',
+        },
+        AbortedResult(
+            state=State(term=int_dv(1), substitution=int_dv(2), predicate=int_dv(3)),
+            depth=4,
+            unknown_predicate=int_dv(5),
+            logs=(),
+        ),
+    ),
 )