diff --git a/package/version b/package/version index 466fedc56..3481ae90d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.543 +0.1.544 diff --git a/pyproject.toml b/pyproject.toml index 6ef193834..45ee5aa0b 100644 --- a/pyproject.toml +++ b/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. ", diff --git a/src/pyk/kcfg/exploration.py b/src/pyk/kcfg/exploration.py index f9c1b2641..f01dbfb9f 100644 --- a/src/pyk/kcfg/exploration.py +++ b/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) ) # diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 22b19f792..ed9e6e3bc 100644 --- a/src/pyk/kcfg/explore.py +++ b/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,7 +290,11 @@ 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) @@ -287,13 +302,18 @@ def cterm_assume_defined(self, cterm: CTerm) -> CTerm: 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): diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index a6b4bae32..4d94926ba 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/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) diff --git a/src/pyk/kcfg/show.py b/src/pyk/kcfg/show.py index 596bbcff8..d873a132c 100644 --- a/src/pyk/kcfg/show.py +++ b/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 diff --git a/src/pyk/kore/rpc.py b/src/pyk/kore/rpc.py index df9cbda10..b9ef42ebe 100644 --- a/src/pyk/kore/rpc.py +++ b/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( diff --git a/src/pyk/proof/equality.py b/src/pyk/proof/equality.py index 3a3b2f8fa..a824b4d2e 100644 --- a/src/pyk/proof/equality.py +++ b/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)}') diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index f1a7e1b33..3489e5512 100644 --- a/src/pyk/proof/reachability.py +++ b/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 diff --git a/src/tests/integration/kcfg/test_simple.py b/src/tests/integration/kcfg/test_simple.py index df185a5de..b28564dd7 100644 --- a/src/tests/integration/kcfg/test_simple.py +++ b/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')) diff --git a/src/tests/integration/kore/test_kore_client.py b/src/tests/integration/kore/test_kore_client.py index cabfa89a0..8b52f0999 100644 --- a/src/tests/integration/kore/test_kore_client.py +++ b/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 diff --git a/src/tests/unit/kore/test_client.py b/src/tests/unit/kore/test_client.py index a029ba4ae..daa02dde0 100644 --- a/src/tests/unit/kore/test_client.py +++ b/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)