Make KCFGExplore aware of aborting requests due to unknwon predicates

package/version

@@ -1 +1 @@
-0.1.543
+0.1.544

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.543"
+version = "0.1.544"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/pyk/kcfg/exploration.py

@@ -34,6 +34,7 @@ def is_explorable(self, node_id: NodeIdLike) -> bool:
             and not self.is_terminal(node_id)
             and not self.kcfg.is_stuck(node_id)
             and not self.kcfg.is_vacuous(node_id)
+            and not self.kcfg.is_undecided(node_id)
         )
 
     #

src/pyk/kcfg/explore.py

@@ -49,6 +49,7 @@
 
 class CTermExecute(NamedTuple):
     state: CTerm
+    unknown_predicate: KInner | None
     next_states: tuple[CTerm, ...]
     depth: int
     vacuous: bool
@@ -100,9 +101,11 @@ def cterm_execute(
             log_failed_simplifications=self._trace_rewrites,
         )
 
+        unknown_predicate = None
         if isinstance(response, AbortedResult):
-            unknown_predicate = response.unknown_predicate.text if response.unknown_predicate else None
-            raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}')
+            unknown_predicate = (
+                self.kprint.kore_to_kast(response.unknown_predicate) if response.unknown_predicate is not None else None
+            )
 
         state = CTerm.from_kast(self.kprint.kore_to_kast(response.state.kore))
         resp_next_states = response.next_states or ()
@@ -113,25 +116,33 @@ def cterm_execute(
 
         return CTermExecute(
             state=state,
+            unknown_predicate=unknown_predicate,
             next_states=next_states,
             depth=response.depth,
             vacuous=response.reason is StopReason.VACUOUS,
             logs=response.logs,
         )
 
-    def cterm_simplify(self, cterm: CTerm) -> tuple[CTerm, tuple[LogEntry, ...]]:
+    def cterm_simplify(self, cterm: CTerm) -> tuple[KInner | None, CTerm, tuple[LogEntry, ...]]:
         _LOGGER.debug(f'Simplifying: {cterm}')
         kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL)
-        kore_simplified, logs = self._kore_client.simplify(kore)
+        kore_unknown_predicate, kore_simplified, logs = self._kore_client.simplify(kore)
         kast_simplified = self.kprint.kore_to_kast(kore_simplified)
-        return CTerm.from_kast(kast_simplified), logs
+        unknown_predicate = (
+            self.kprint.kore_to_kast(kore_unknown_predicate) if kore_unknown_predicate is not None else None
+        )
+        return unknown_predicate, CTerm.from_kast(kast_simplified), logs
 
-    def kast_simplify(self, kast: KInner) -> tuple[KInner, tuple[LogEntry, ...]]:
+    def kast_simplify(self, kast: KInner) -> tuple[KInner | None, KInner, tuple[LogEntry, ...]]:
         _LOGGER.debug(f'Simplifying: {kast}')
         kore = self.kprint.kast_to_kore(kast, GENERATED_TOP_CELL)
-        kore_simplified, logs = self._kore_client.simplify(kore)
+        unknown_predicate_kore, kore_simplified, logs = self._kore_client.simplify(kore)
+        unknown_predicate = None
+        if unknown_predicate_kore is not None:
+            unknown_predicate = self.kprint.kore_to_kast(unknown_predicate_kore)
+            _LOGGER.warning('Could not decide predicate:' + self.kprint.pretty_print(unknown_predicate))
         kast_simplified = self.kprint.kore_to_kast(kore_simplified)
-        return kast_simplified, logs
+        return unknown_predicate, kast_simplified, logs
 
     def cterm_get_model(self, cterm: CTerm, module_name: str | None = None) -> Subst | None:
         _LOGGER.info(f'Getting model: {cterm}')
@@ -279,21 +290,30 @@ def cterm_assume_defined(self, cterm: CTerm) -> CTerm:
         _LOGGER.debug(f'Computing definedness condition for: {cterm}')
         kast = KApply(KLabel('#Ceil', [GENERATED_TOP_CELL, GENERATED_TOP_CELL]), [cterm.config])
         kore = self.kprint.kast_to_kore(kast, GENERATED_TOP_CELL)
-        kore_simplified, _logs = self._kore_client.simplify(kore)
+        unknown_predicate, kore_simplified, _logs = self._kore_client.simplify(kore)
+        if unknown_predicate is not None:
+            _LOGGER.warning(
+                'Could not decide predicate:' + self.kprint.pretty_print(self.kprint.kore_to_kast(unknown_predicate))
+            )
         kast_simplified = self.kprint.kore_to_kast(kore_simplified)
         _LOGGER.debug(f'Definedness condition computed: {kast_simplified}')
         return cterm.add_constraint(kast_simplified)
 
     def simplify(self, cfg: KCFG, logs: dict[int, tuple[LogEntry, ...]]) -> None:
         for node in cfg.nodes:
             _LOGGER.info(f'Simplifying node {self.id}: {shorten_hashes(node.id)}')
-            new_term, next_node_logs = self.cterm_simplify(node.cterm)
+            unknown_predicate, new_term, next_node_logs = self.cterm_simplify(node.cterm)
             if new_term != node.cterm:
                 cfg.replace_node(node.id, new_term)
                 if node.id in logs:
                     logs[node.id] += next_node_logs
                 else:
                     logs[node.id] = next_node_logs
+            if unknown_predicate is not None:
+                _LOGGER.warning(
+                    f'Could not decide predicate while simplifiyng node {node.id}:'
+                    + self.kprint.pretty_print(unknown_predicate)
+                )
 
     def step(
         self,
@@ -387,6 +407,8 @@ def check_extendable(self, kcfg_exploration: KCFGExploration, node: KCFG.Node) -
             raise ValueError(f'Cannot extend vacuous node {self.id}: {node.id}')
         if kcfg_exploration.is_terminal(node.id):
             raise ValueError(f'Cannot extend terminal node {self.id}: {node.id}')
+        if kcfg.is_undecided(node.id):
+            raise ValueError(f'Cannot extend undecided node {self.id}: {node.id}')
 
     def extend_cterm(
         self,
@@ -405,13 +427,13 @@ def extend_cterm(
         branches = []
         for constraint in _branches:
             kast = mlAnd(list(_cterm.constraints) + [constraint])
-            kast, _ = self.kast_simplify(kast)
-            if not CTerm._is_bottom(kast):
+            unknown_predicate, kast, _ = self.kast_simplify(kast)
+            if not CTerm._is_bottom(kast) and unknown_predicate is None:
                 branches.append(constraint)
         if len(branches) > 1:
             return Branch(branches, heuristic=True)
 
-        cterm, next_cterms, depth, vacuous, next_node_logs = self.cterm_execute(
+        cterm, unknown_predicate, next_cterms, depth, vacuous, next_node_logs = self.cterm_execute(
             _cterm,
             depth=execute_depth,
             cut_point_rules=cut_point_rules,
@@ -423,10 +445,12 @@ def extend_cterm(
         if depth > 0:
             return Step(cterm, depth, next_node_logs)
 
-        # Stuck or vacuous
+        # Stuck, Vacuous or Undecided
         if not next_cterms:
             if vacuous:
                 return Vacuous()
+            if unknown_predicate is not None:
+                return Undecided(unknown_predicate)
             return Stuck()
 
         # Cut rule
@@ -472,6 +496,10 @@ def log(message: str, *, warning: bool = False) -> None:
                 kcfg.add_stuck(node.id)
                 log(f'stuck node: {node.id}')
 
+            case Undecided(_):
+                kcfg.add_undecided(node.id)
+                log(f'undecided node: {node.id}')
+
             case Abstract(cterm):
                 new_node = kcfg.create_node(cterm)
                 kcfg.create_cover(node.id, new_node.id)
@@ -533,6 +561,13 @@ class Stuck(ExtendResult):
     ...
 
 
+@final
+@dataclass(frozen=True)
+class Undecided(ExtendResult):
+    unknown_predicate: KInner
+    ...
+
+
 @final
 @dataclass(frozen=True)
 class Abstract(ExtendResult):

src/pyk/kcfg/kcfg.py

@@ -208,6 +208,7 @@ def edges(self) -> tuple[KCFG.Edge, ...]:
     _ndbranches: dict[int, NDBranch]
     _vacuous: set[int]
     _stuck: set[int]
+    _undecided: set[int]
     _aliases: dict[str, int]
     _lock: RLock
     cfg_dir: Path | None
@@ -223,6 +224,7 @@ def __init__(self, cfg_dir: Path | None = None) -> None:
         self._ndbranches = {}
         self._vacuous = set()
         self._stuck = set()
+        self._undecided = set()
         self._aliases = {}
         self._lock = RLock()
         self.cfg_dir = cfg_dir
@@ -677,6 +679,19 @@ def discard_stuck(self, node_id: NodeIdLike) -> None:
         node_id = self._resolve(node_id)
         self._stuck.discard(node_id)
 
+    def add_undecided(self, node_id: NodeIdLike) -> None:
+        self._undecided.add(self._resolve(node_id))
+
+    def remove_undecided(self, node_id: NodeIdLike) -> None:
+        node_id = self._resolve(node_id)
+        if node_id not in self._undecided:
+            raise ValueError(f'Node is not undecided: {node_id}')
+        self._undecided.remove(node_id)
+
+    def discard_undecided(self, node_id: NodeIdLike) -> None:
+        node_id = self._resolve(node_id)
+        self._undecided.discard(node_id)
+
     def splits(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[Split]:
         source_id = self._resolve(source_id) if source_id is not None else None
         target_id = self._resolve(target_id) if target_id is not None else None
@@ -759,6 +774,10 @@ def is_stuck(self, node_id: NodeIdLike) -> bool:
         node_id = self._resolve(node_id)
         return node_id in self._stuck
 
+    def is_undecided(self, node_id: NodeIdLike) -> bool:
+        node_id = self._resolve(node_id)
+        return node_id in self._undecided
+
     def is_split(self, node_id: NodeIdLike) -> bool:
         node_id = self._resolve(node_id)
         return node_id in self._splits
@@ -922,6 +941,7 @@ def write_cfg_data(self) -> None:
 
         vacuous = sorted(self._vacuous)
         stuck = sorted(self._stuck)
+        undecided = sorted(self._undecided)
         aliases = dict(sorted(self._aliases.items()))
         dct: dict[str, list[int] | int | dict[str, int] | list[dict[str, Any]]] = {}
         dct['next'] = self._node_id
@@ -932,6 +952,7 @@ def write_cfg_data(self) -> None:
         dct['ndbranches'] = ndbranches
         dct['vacuous'] = vacuous
         dct['stuck'] = stuck
+        dct['undecided'] = undecided
         dct['aliases'] = aliases
         cfg_json.write_text(json.dumps(dct))
 
@@ -1004,6 +1025,9 @@ def read_cfg_data(cfg_dir: Path, id: str) -> KCFG:
         for stuck_id in dct.get('stuck') or []:
             cfg.add_stuck(stuck_id)
 
+        for undecided_id in dct.get('undecided') or []:
+            cfg.add_undecided(undecided_id)
+
         for alias, node_id in dct.get('aliases', {}).items():
             cfg.add_alias(alias=alias, node_id=node_id)
 

src/pyk/kcfg/show.py

@@ -66,6 +66,8 @@ def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
             attrs.append('leaf')
         if kcfg.is_split(node.id):
             attrs.append('split')
+        if kcfg.is_undecided(node.id):
+            attrs.append('undecided')
         attrs.extend(['@' + alias for alias in sorted(kcfg.aliases(node.id))])
         return attrs
 

src/pyk/kore/rpc.py

@@ -850,7 +850,7 @@ def simplify(
         pattern: Pattern,
         log_successful_simplifications: bool | None = None,
         log_failed_simplifications: bool | None = None,
-    ) -> tuple[Pattern, tuple[LogEntry, ...]]:
+    ) -> tuple[Pattern | None, Pattern, tuple[LogEntry, ...]]:
         params = filter_none(
             {
                 'state': self._state(pattern),
@@ -859,9 +859,16 @@ def simplify(
             }
         )
 
-        result = self._request('simplify', **params)
+        try:
+            result = self._request('simplify', **params)
+        except KoreClientError as err:
+            try:
+                unknown_predicate = kore_term(err.data, Pattern)  # type: ignore
+                return unknown_predicate, pattern, ()
+            except ValueError:
+                raise err
         logs = tuple(LogEntry.from_dict(l) for l in result['logs']) if 'logs' in result else ()
-        return kore_term(result['state'], Pattern), logs  # type: ignore # https://github.com/python/mypy/issues/4717
+        return None, kore_term(result['state'], Pattern), logs  # type: ignore # https://github.com/python/mypy/issues/4717
 
     def get_model(self, pattern: Pattern, module_name: str | None = None) -> GetModelResult:
         params = filter_none(

src/pyk/proof/equality.py

@@ -347,8 +347,8 @@ def advance_proof(self) -> None:
 
         # to prove the equality, we check the implication of the form `constraints #Implies LHS #Equals RHS`, i.e.
         # "LHS equals RHS under these constraints"
-        antecedent_simplified_kast, _ = self.kcfg_explore.kast_simplify(self.proof._antecedent_kast)
-        consequent_simplified_kast, _ = self.kcfg_explore.kast_simplify(self.proof._consequent_kast)
+        _, antecedent_simplified_kast, _ = self.kcfg_explore.kast_simplify(self.proof._antecedent_kast)
+        _, consequent_simplified_kast, _ = self.kcfg_explore.kast_simplify(self.proof._consequent_kast)
         self.proof.simplified_antecedent = antecedent_simplified_kast
         self.proof.simplified_consequent = consequent_simplified_kast
         _LOGGER.info(f'Simplified antecedent: {self.kcfg_explore.kprint.pretty_print(antecedent_simplified_kast)}')

src/pyk/proof/reachability.py

@@ -909,8 +909,8 @@ def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info:
         failure_reasons = {}
         models = {}
         for node in proof.failing:
-            node_cterm, _ = kcfg_explore.cterm_simplify(node.cterm)
-            target_cterm, _ = kcfg_explore.cterm_simplify(target.cterm)
+            _unknwon_predicate, node_cterm, _ = kcfg_explore.cterm_simplify(node.cterm)
+            _unknwon_predicate, target_cterm, _ = kcfg_explore.cterm_simplify(target.cterm)
             _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm)
             path_condition = kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id))
             failure_reasons[node.id] = reason

src/tests/integration/kcfg/test_simple.py

@@ -113,7 +113,7 @@ def test_simplify(
         expected_k, expected_state, *_ = expected_post
 
         # When
-        actual_post, _logs = kcfg_explore.cterm_simplify(self.config(kcfg_explore.kprint, *pre))
+        _unknwon_predicate, actual_post, _logs = kcfg_explore.cterm_simplify(self.config(kcfg_explore.kprint, *pre))
         actual_k = kcfg_explore.kprint.pretty_print(get_cell(actual_post.kast, 'K_CELL'))
         actual_state = kcfg_explore.kprint.pretty_print(get_cell(actual_post.kast, 'STATE_CELL'))
 

src/tests/integration/kore/test_kore_client.py

@@ -330,7 +330,7 @@ def test_simplify(
         expected: Pattern,
     ) -> None:
         # When
-        actual, _logs = kore_client.simplify(pattern)
+        _unknwon_predicate, actual, _logs = kore_client.simplify(pattern)
 
         # Then
         assert actual == expected

src/tests/unit/kore/test_client.py

@@ -201,7 +201,7 @@ def test_simplify(
     rpc_client.assume_response(response)
 
     # When
-    actual, _logs = kore_client.simplify(pattern)
+    _unknwon_predicate, actual, _logs = kore_client.simplify(pattern)
 
     # Then
     rpc_client.assert_request('simplify', **params)