From 93b6d934547e0d7f3a2ff18aaf602f7ed9ec0079 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 28 Nov 2023 18:28:22 +0100 Subject: [PATCH 01/12] Add Unknown nodes to interpret Aborted states returned by `kore-rpc-booster` --- src/pyk/kcfg/explore.py | 32 +++++++++++++------- src/tests/integration/proof/test_cell_map.py | 2 +- 2 files changed, 22 insertions(+), 12 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 72011022f..cffd6ea9a 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -77,7 +77,7 @@ def cterm_execute( cut_point_rules: Iterable[str] | None = None, terminal_rules: Iterable[str] | None = None, module_name: str | None = None, - ) -> tuple[bool, int, CTerm, list[CTerm], tuple[LogEntry, ...]]: + ) -> tuple[KInner | None, bool, int, CTerm, list[CTerm], tuple[LogEntry, ...]]: _LOGGER.debug(f'Executing: {cterm}') kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL) er = self._kore_client.execute( @@ -92,10 +92,6 @@ def cterm_execute( 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)) @@ -103,13 +99,16 @@ def cterm_execute( next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states] next_states = [cterm for cterm in next_states if not cterm.is_bottom] if len(next_states) == 1 and len(next_states) < len(_next_states): - return _is_vacuous, depth + 1, next_states[0], [], er.logs + return None, _is_vacuous, depth + 1, next_states[0], [], er.logs elif len(next_states) == 1: if er.reason == StopReason.CUT_POINT_RULE: - return _is_vacuous, depth, next_state, next_states, er.logs + return None, _is_vacuous, depth, next_state, next_states, er.logs else: next_states = [] - return _is_vacuous, depth, next_state, next_states, er.logs + unknown_predicate = None + if isinstance(er, AbortedResult): + unknown_predicate = self.kprint.kore_to_kast(er.unknown_predicate) if er.unknown_predicate else None + return unknown_predicate, _is_vacuous, depth, next_state, next_states, er.logs def cterm_simplify(self, cterm: CTerm) -> tuple[CTerm, tuple[LogEntry, ...]]: _LOGGER.debug(f'Simplifying: {cterm}') @@ -302,7 +301,7 @@ def step( if len(successors) != 0 and type(successors[0]) is KCFG.Split: raise ValueError(f'Cannot take step from split node {self.id}: {shorten_hashes(node.id)}') _LOGGER.info(f'Taking {depth} steps from node {self.id}: {shorten_hashes(node.id)}') - _, actual_depth, cterm, next_cterms, next_node_logs = self.cterm_execute( + _, _, actual_depth, cterm, next_cterms, next_node_logs = self.cterm_execute( node.cterm, depth=depth, module_name=module_name ) if actual_depth != depth: @@ -405,7 +404,7 @@ def extend_cterm( if len(branches) > 1: return Branch(branches, heuristic=True) - _is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute( + unknown_predicate, _is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute( _cterm, depth=execute_depth, cut_point_rules=cut_point_rules, @@ -417,10 +416,12 @@ def extend_cterm( if depth > 0: return Step(cterm, depth, next_node_logs) - # Stuck or vacuous + # Stuck, vacuous or unknown if not next_cterms: if _is_vacuous: return Vacuous() + if unknown_predicate is not None: + return Unknown(cterm, unknown_predicate, depth) return Stuck() # Cut rule @@ -527,6 +528,15 @@ class Stuck(ExtendResult): ... +@final +@dataclass(frozen=True) +class Unknown(ExtendResult): + cterm: CTerm + unknown_predicate: KInner + depth: int + ... + + @final @dataclass(frozen=True) class Abstract(ExtendResult): diff --git a/src/tests/integration/proof/test_cell_map.py b/src/tests/integration/proof/test_cell_map.py index 02247d470..3121b933a 100644 --- a/src/tests/integration/proof/test_cell_map.py +++ b/src/tests/integration/proof/test_cell_map.py @@ -104,7 +104,7 @@ def test_execute( expected_k, _, _ = expected_post # When - _, actual_depth, actual_post_term, _, _logs = kcfg_explore.cterm_execute( + _, _, actual_depth, actual_post_term, _, _logs = kcfg_explore.cterm_execute( self.config(kcfg_explore.kprint, k, aacounts, accounts), depth=depth ) actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL')) From 9371a76920bd095487338590d5e9cb9ac23e982c Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 29 Nov 2023 13:37:06 +0100 Subject: [PATCH 02/12] Catch JsonRpcError in KoreClient.simplify and pretty-print the unknwon predicate --- src/pyk/kcfg/explore.py | 30 ++++++++++++++----- src/pyk/kore/rpc.py | 13 ++++++-- src/pyk/proof/reachability.py | 4 +-- .../kcfg/test_multiple_definitions.py | 6 ++-- src/tests/integration/kcfg/test_simple.py | 4 +-- .../integration/kore/test_kore_client.py | 2 +- src/tests/integration/proof/test_imp.py | 2 +- src/tests/unit/kore/test_client.py | 2 +- 8 files changed, 43 insertions(+), 20 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index cffd6ea9a..72515f48b 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -20,7 +20,7 @@ ) from ..kast.outer import KRule from ..konvert import krule_to_kore -from ..kore.rpc import AbortedResult, SatResult, StopReason, UnknownResult, UnsatResult +from ..kore.rpc import AbortedResult, JsonRpcError, SatResult, StopReason, UnknownResult, UnsatResult from ..kore.syntax import Import, Module from ..prelude import k from ..prelude.k import GENERATED_TOP_CELL @@ -110,17 +110,24 @@ def cterm_execute( unknown_predicate = self.kprint.kore_to_kast(er.unknown_predicate) if er.unknown_predicate else None return unknown_predicate, _is_vacuous, depth, next_state, next_states, er.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, ...]]: _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_simplified, logs = self._kore_client.simplify(kore) + if unknown_predicate is not None: + _LOGGER.warning( + f"Could not decide predicate:" + self.kprint.pretty_print(self.kprint.kore_to_kast(unknown_predicate)) + ) kast_simplified = self.kprint.kore_to_kast(kore_simplified) return kast_simplified, logs @@ -270,7 +277,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( + f"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) @@ -278,13 +289,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, diff --git a/src/pyk/kore/rpc.py b/src/pyk/kore/rpc.py index 9eb9601eb..9a5e0a2a4 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 JsonRpcError as err: + try: + unknown_predicate = kore_term(err.data, Pattern) # type: ignore + return unknown_predicate, pattern, tuple() + 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/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_multiple_definitions.py b/src/tests/integration/kcfg/test_multiple_definitions.py index b6fd399f2..f0bbd74c3 100644 --- a/src/tests/integration/kcfg/test_multiple_definitions.py +++ b/src/tests/integration/kcfg/test_multiple_definitions.py @@ -44,7 +44,7 @@ def test_execute( kcfg_explore: KCFGExplore, test_id: str, ) -> None: - _, split_depth, split_post_term, split_next_terms, _logs = kcfg_explore.cterm_execute(self.config(), depth=1) + _, _, split_depth, split_post_term, split_next_terms, _logs = kcfg_explore.cterm_execute(self.config(), depth=1) split_k = kcfg_explore.kprint.pretty_print(split_post_term.cell('K_CELL')) split_next_k = [kcfg_explore.kprint.pretty_print(split_post_term.cell('K_CELL')) for term in split_next_terms] @@ -57,13 +57,13 @@ def test_execute( 'a ( X:KItem )', ] == split_next_k - _, step_1_depth, step_1_post_term, step_1_next_terms, _logs = kcfg_explore.cterm_execute( + _, _, step_1_depth, step_1_post_term, step_1_next_terms, _logs = kcfg_explore.cterm_execute( split_next_terms[0], depth=1 ) step_1_k = kcfg_explore.kprint.pretty_print(step_1_post_term.cell('K_CELL')) assert 'c' == step_1_k - _, step_2_depth, step_2_post_term, step_2_next_terms, _logs = kcfg_explore.cterm_execute( + _, _, step_2_depth, step_2_post_term, step_2_next_terms, _logs = kcfg_explore.cterm_execute( split_next_terms[1], depth=1 ) step_2_k = kcfg_explore.kprint.pretty_print(step_1_post_term.cell('K_CELL')) diff --git a/src/tests/integration/kcfg/test_simple.py b/src/tests/integration/kcfg/test_simple.py index b48c35e9f..1e55af7d0 100644 --- a/src/tests/integration/kcfg/test_simple.py +++ b/src/tests/integration/kcfg/test_simple.py @@ -78,7 +78,7 @@ def test_execute( expected_k, expected_state, *_ = expected_post # When - _, actual_depth, actual_post_term, actual_next_terms, _logs = kcfg_explore.cterm_execute( + _, _, actual_depth, actual_post_term, actual_next_terms, _logs = kcfg_explore.cterm_execute( self.config(kcfg_explore.kprint, *pre), depth=depth ) actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL')) @@ -114,7 +114,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/integration/proof/test_imp.py b/src/tests/integration/proof/test_imp.py index dbd6b0869..4f470778a 100644 --- a/src/tests/integration/proof/test_imp.py +++ b/src/tests/integration/proof/test_imp.py @@ -780,7 +780,7 @@ def test_execute( expected_k, expected_state = expected_post # When - _, actual_depth, actual_post_term, actual_next_terms, _logs = kcfg_explore.cterm_execute( + _, _, actual_depth, actual_post_term, actual_next_terms, _logs = kcfg_explore.cterm_execute( self.config(kcfg_explore.kprint, k, state), depth=depth ) actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL')) 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) From 4c29bbdc4151a246a7100a3b8c54684716c2b4d0 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 29 Nov 2023 13:47:31 +0100 Subject: [PATCH 03/12] Catch KoreClientError instead of JsonRpcError --- src/pyk/kore/rpc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/kore/rpc.py b/src/pyk/kore/rpc.py index 9a5e0a2a4..2912ab4f6 100644 --- a/src/pyk/kore/rpc.py +++ b/src/pyk/kore/rpc.py @@ -861,7 +861,7 @@ def simplify( try: result = self._request('simplify', **params) - except JsonRpcError as err: + except KoreClientError as err: try: unknown_predicate = kore_term(err.data, Pattern) # type: ignore return unknown_predicate, pattern, tuple() From 1c16fc478bdd59be02a512f6f51a530a284d7827 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 29 Nov 2023 18:06:45 +0100 Subject: [PATCH 04/12] Return the unknown predicate from kast_simplify --- src/pyk/kcfg/explore.py | 18 +++++++++--------- src/pyk/proof/equality.py | 4 ++-- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 72515f48b..0f53c6f9b 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -120,16 +120,16 @@ def cterm_simplify(self, cterm: CTerm) -> tuple[KInner | None, CTerm, tuple[LogE ) 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) - unknown_predicate, kore_simplified, logs = self._kore_client.simplify(kore) - if unknown_predicate is not None: - _LOGGER.warning( - f"Could not decide predicate:" + self.kprint.pretty_print(self.kprint.kore_to_kast(unknown_predicate)) - ) + 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(f"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}') @@ -414,8 +414,8 @@ 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) 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)}') From 6fee90808f3a2461be7c319a9377bb8b34a18dea Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 29 Nov 2023 19:32:13 +0100 Subject: [PATCH 05/12] Add Undecided KCFG nodes --- src/pyk/kcfg/exploration.py | 1 + src/pyk/kcfg/explore.py | 22 +++++++++++++++++----- src/pyk/kcfg/kcfg.py | 19 +++++++++++++++++++ src/pyk/kcfg/show.py | 2 ++ src/pyk/kore/rpc.py | 3 ++- 5 files changed, 41 insertions(+), 6 deletions(-) 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 0f53c6f9b..29a6787cc 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -107,7 +107,9 @@ def cterm_execute( next_states = [] unknown_predicate = None if isinstance(er, AbortedResult): - unknown_predicate = self.kprint.kore_to_kast(er.unknown_predicate) if er.unknown_predicate else None + unknown_predicate = ( + self.kprint.kore_to_kast(er.unknown_predicate) if er.unknown_predicate is not None else None + ) return unknown_predicate, _is_vacuous, depth, next_state, next_states, er.logs def cterm_simplify(self, cterm: CTerm) -> tuple[KInner | None, CTerm, tuple[LogEntry, ...]]: @@ -396,6 +398,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, @@ -432,14 +436,16 @@ def extend_cterm( if depth > 0: return Step(cterm, depth, next_node_logs) - # Stuck, vacuous or unknown + # Stuck, Vacuous if not next_cterms: if _is_vacuous: return Vacuous() - if unknown_predicate is not None: - return Unknown(cterm, unknown_predicate, depth) return Stuck() + # Undecided + if unknown_predicate is not None: + return Undecided(cterm, unknown_predicate, depth) + # Cut rule if len(next_cterms) == 1: return Step(next_cterms[0], 1, next_node_logs, cut=True) @@ -483,6 +489,12 @@ def log(message: str, *, warning: bool = False) -> None: kcfg.add_stuck(node.id) log(f'stuck node: {node.id}') + case Undecided(cterm, _unknown_predicate, depth): + next_node = kcfg.create_node(cterm) + kcfg.add_undecided(next_node.id) + kcfg.create_edge(node.id, next_node.id, depth) + log(f'undecided node: {node.id}') + case Abstract(cterm): new_node = kcfg.create_node(cterm) kcfg.create_cover(node.id, new_node.id) @@ -546,7 +558,7 @@ class Stuck(ExtendResult): @final @dataclass(frozen=True) -class Unknown(ExtendResult): +class Undecided(ExtendResult): cterm: CTerm unknown_predicate: KInner depth: int diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index a6b4bae32..332f36c25 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 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 2912ab4f6..6594d02cd 100644 --- a/src/pyk/kore/rpc.py +++ b/src/pyk/kore/rpc.py @@ -666,11 +666,11 @@ def from_dict(cls: type[VacuousResult], dct: Mapping[str, Any]) -> VacuousResult @dataclass(frozen=True) class AbortedResult(ExecuteResult): reason = StopReason.ABORTED - next_states = None rule = None state: State depth: int + next_states: tuple[State, ...] unknown_predicate: Pattern | None logs: tuple[LogEntry, ...] @@ -681,6 +681,7 @@ def from_dict(cls: type[AbortedResult], dct: Mapping[str, Any]) -> AbortedResult return AbortedResult( state=State.from_dict(dct['state']), depth=dct['depth'], + next_states=tuple(State.from_dict(next_state) for next_state in dct['next-states']), unknown_predicate=kore_term(dct['unknown-predicate'], Pattern) if dct.get('unknown-predicate') else None, # type: ignore logs=logs, ) From 40819696d1960f76c9d007c5c1a38700019abb63 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 29 Nov 2023 18:33:24 +0000 Subject: [PATCH 06/12] Set Version: 0.1.518 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 8d78bc42e..4adb5745c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.517 +0.1.518 diff --git a/pyproject.toml b/pyproject.toml index 5cefb372b..5b0f0df59 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.517" +version = "0.1.518" description = "" authors = [ "Runtime Verification, Inc. ", From c0b8af86109b1464dc2686da6563ffe40dc1ba25 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 30 Nov 2023 08:21:06 +0100 Subject: [PATCH 07/12] Lint and typecheck --- src/pyk/kcfg/explore.py | 10 +++++----- src/pyk/kore/rpc.py | 2 +- src/tests/unit/kore/test_client.py | 1 + 3 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 29a6787cc..fd7b180af 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -20,7 +20,7 @@ ) from ..kast.outer import KRule from ..konvert import krule_to_kore -from ..kore.rpc import AbortedResult, JsonRpcError, 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 @@ -129,7 +129,7 @@ def kast_simplify(self, kast: KInner) -> tuple[KInner | None, KInner, tuple[LogE unknown_predicate = None if unknown_predicate_kore is not None: unknown_predicate = self.kprint.kore_to_kast(unknown_predicate_kore) - _LOGGER.warning(f"Could not decide predicate:" + self.kprint.pretty_print(unknown_predicate)) + _LOGGER.warning('Could not decide predicate:' + self.kprint.pretty_print(unknown_predicate)) kast_simplified = self.kprint.kore_to_kast(kore_simplified) return unknown_predicate, kast_simplified, logs @@ -282,7 +282,7 @@ def cterm_assume_defined(self, cterm: CTerm) -> CTerm: unknown_predicate, kore_simplified, _logs = self._kore_client.simplify(kore) if unknown_predicate is not None: _LOGGER.warning( - f"Could not decide predicate:" + self.kprint.pretty_print(self.kprint.kore_to_kast(unknown_predicate)) + '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}') @@ -300,7 +300,7 @@ def simplify(self, cfg: KCFG, logs: dict[int, tuple[LogEntry, ...]]) -> None: logs[node.id] = next_node_logs if unknown_predicate is not None: _LOGGER.warning( - f"Could not decide predicate while simplifiyng node {node.id}:" + f'Could not decide predicate while simplifiyng node {node.id}:' + self.kprint.pretty_print(unknown_predicate) ) @@ -489,7 +489,7 @@ def log(message: str, *, warning: bool = False) -> None: kcfg.add_stuck(node.id) log(f'stuck node: {node.id}') - case Undecided(cterm, _unknown_predicate, depth): + case Undecided(cterm, _, depth): next_node = kcfg.create_node(cterm) kcfg.add_undecided(next_node.id) kcfg.create_edge(node.id, next_node.id, depth) diff --git a/src/pyk/kore/rpc.py b/src/pyk/kore/rpc.py index 6594d02cd..03fc1ace7 100644 --- a/src/pyk/kore/rpc.py +++ b/src/pyk/kore/rpc.py @@ -865,7 +865,7 @@ def simplify( except KoreClientError as err: try: unknown_predicate = kore_term(err.data, Pattern) # type: ignore - return unknown_predicate, pattern, tuple() + return unknown_predicate, pattern, () except ValueError: raise err logs = tuple(LogEntry.from_dict(l) for l in result['logs']) if 'logs' in result else () diff --git a/src/tests/unit/kore/test_client.py b/src/tests/unit/kore/test_client.py index daa02dde0..8804c1499 100644 --- a/src/tests/unit/kore/test_client.py +++ b/src/tests/unit/kore/test_client.py @@ -118,6 +118,7 @@ def kore_client(mock: Mock, mock_class: Mock) -> Iterator[KoreClient]: # noqa: }, AbortedResult( state=State(term=int_dv(1), substitution=int_dv(2), predicate=int_dv(3)), + next_states=(), depth=4, unknown_predicate=int_dv(5), logs=(), From 3d30128fddcb97d1a11bce002cf0e26ad7215ebf Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 30 Nov 2023 07:21:32 +0000 Subject: [PATCH 08/12] Set Version: 0.1.519 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 4adb5745c..ac7d5f0eb 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.518 +0.1.519 diff --git a/pyproject.toml b/pyproject.toml index 5b0f0df59..21b3c8e4b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.518" +version = "0.1.519" description = "" authors = [ "Runtime Verification, Inc. ", From 1abd06c8a0c7b853d3263858e63de96083aa175e Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 30 Nov 2023 08:30:15 +0100 Subject: [PATCH 09/12] Drop next states from AbortedResult --- src/pyk/kore/rpc.py | 3 +-- src/tests/unit/kore/test_client.py | 1 - 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/src/pyk/kore/rpc.py b/src/pyk/kore/rpc.py index 03fc1ace7..ac1ce3de3 100644 --- a/src/pyk/kore/rpc.py +++ b/src/pyk/kore/rpc.py @@ -666,11 +666,11 @@ def from_dict(cls: type[VacuousResult], dct: Mapping[str, Any]) -> VacuousResult @dataclass(frozen=True) class AbortedResult(ExecuteResult): reason = StopReason.ABORTED + next_states = None rule = None state: State depth: int - next_states: tuple[State, ...] unknown_predicate: Pattern | None logs: tuple[LogEntry, ...] @@ -681,7 +681,6 @@ def from_dict(cls: type[AbortedResult], dct: Mapping[str, Any]) -> AbortedResult return AbortedResult( state=State.from_dict(dct['state']), depth=dct['depth'], - next_states=tuple(State.from_dict(next_state) for next_state in dct['next-states']), unknown_predicate=kore_term(dct['unknown-predicate'], Pattern) if dct.get('unknown-predicate') else None, # type: ignore logs=logs, ) diff --git a/src/tests/unit/kore/test_client.py b/src/tests/unit/kore/test_client.py index 8804c1499..daa02dde0 100644 --- a/src/tests/unit/kore/test_client.py +++ b/src/tests/unit/kore/test_client.py @@ -118,7 +118,6 @@ def kore_client(mock: Mock, mock_class: Mock) -> Iterator[KoreClient]: # noqa: }, AbortedResult( state=State(term=int_dv(1), substitution=int_dv(2), predicate=int_dv(3)), - next_states=(), depth=4, unknown_predicate=int_dv(5), logs=(), From e9cf6603dd86527182a735fce420fddcbb2a63fd Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 30 Nov 2023 09:28:51 +0100 Subject: [PATCH 10/12] Read and write undecided nodes' set --- src/pyk/kcfg/kcfg.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index 332f36c25..4d94926ba 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -941,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 @@ -951,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)) @@ -1023,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) From 8d4bb89125f1eee48c7b5d2110eca6f74bfb5910 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 30 Nov 2023 09:29:20 +0100 Subject: [PATCH 11/12] Mark nodes with undecided predicates --- src/pyk/kcfg/explore.py | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index fd7b180af..8d4154e7d 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -436,16 +436,14 @@ def extend_cterm( if depth > 0: return Step(cterm, depth, next_node_logs) - # Stuck, Vacuous + # Stuck, Vacuous or Undecided if not next_cterms: if _is_vacuous: return Vacuous() + if unknown_predicate is not None: + return Undecided(unknown_predicate) return Stuck() - # Undecided - if unknown_predicate is not None: - return Undecided(cterm, unknown_predicate, depth) - # Cut rule if len(next_cterms) == 1: return Step(next_cterms[0], 1, next_node_logs, cut=True) @@ -489,10 +487,8 @@ def log(message: str, *, warning: bool = False) -> None: kcfg.add_stuck(node.id) log(f'stuck node: {node.id}') - case Undecided(cterm, _, depth): - next_node = kcfg.create_node(cterm) - kcfg.add_undecided(next_node.id) - kcfg.create_edge(node.id, next_node.id, depth) + case Undecided(_): + kcfg.add_undecided(node.id) log(f'undecided node: {node.id}') case Abstract(cterm): @@ -559,9 +555,7 @@ class Stuck(ExtendResult): @final @dataclass(frozen=True) class Undecided(ExtendResult): - cterm: CTerm unknown_predicate: KInner - depth: int ... From 7156e57f94faefd2e3bbf01cb6fec76a9fdeed15 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 12 Dec 2023 11:29:20 +0000 Subject: [PATCH 12/12] Set Version: 0.1.544 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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. ",