From 2617d4386555a87259a707cb317f418979f07854 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 8 Aug 2023 09:01:21 +0300 Subject: [PATCH 01/21] VacuousResult --- src/pyk/kore/rpc.py | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/pyk/kore/rpc.py b/src/pyk/kore/rpc.py index 1cb6a631b..0ca6f2899 100644 --- a/src/pyk/kore/rpc.py +++ b/src/pyk/kore/rpc.py @@ -279,6 +279,7 @@ class StopReason(str, Enum): BRANCHING = 'branching' CUT_POINT_RULE = 'cut-point-rule' TERMINAL_RULE = 'terminal-rule' + VACUOUS = 'vacuous' @final @@ -429,6 +430,7 @@ class ExecuteResult(ABC): # noqa: B024 StopReason.BRANCHING: 'BranchingResult', StopReason.CUT_POINT_RULE: 'CutPointResult', StopReason.TERMINAL_RULE: 'TerminalResult', + StopReason.VACUOUS: 'VacuousResult', } reason: ClassVar[StopReason] @@ -441,6 +443,7 @@ class ExecuteResult(ABC): # noqa: B024 @classmethod def from_dict(cls: type[ER], dct: Mapping[str, Any]) -> ER: + _LOGGER.info(dct) return globals()[ExecuteResult._TYPES[StopReason(dct['reason'])]].from_dict(dct) # type: ignore @classmethod @@ -450,6 +453,28 @@ def _check_reason(cls: type[ER], dct: Mapping[str, Any]) -> None: raise ValueError(f"Expected {cls.reason} as 'reason', found: {reason}") +@final +@dataclass(frozen=True) +class VacuousResult(ExecuteResult): + reason = StopReason.VACUOUS + next_states = None + rule = None + + state: State + depth: int + logs: tuple[LogEntry, ...] + + @classmethod + def from_dict(cls: type[VacuousResult], dct: Mapping[str, Any]) -> VacuousResult: + cls._check_reason(dct) + logs = tuple(LogEntry.from_dict(l) for l in dct['logs']) if 'logs' in dct else () + return VacuousResult( + state=State.from_dict(dct['state']), + depth=dct['depth'], + logs=logs, + ) + + @final @dataclass(frozen=True) class StuckResult(ExecuteResult): From 4d512523874bfeb3cf1a84495477b65db13bb4bf Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 8 Aug 2023 16:16:28 +0300 Subject: [PATCH 02/21] add set for vacuous nodes in the kcfg --- src/pyk/kcfg/explore.py | 23 ++++++++----- src/pyk/kcfg/kcfg.py | 34 +++++++++++++++++++ src/pyk/kcfg/show.py | 2 ++ src/pyk/kore/rpc.py | 1 - src/pyk/proof/reachability.py | 6 +++- src/tests/integration/kcfg/test_cell_map.py | 2 +- src/tests/integration/kcfg/test_imp.py | 2 +- .../kcfg/test_multiple_definitions.py | 6 ++-- src/tests/integration/kcfg/test_simple.py | 2 +- 9 files changed, 62 insertions(+), 16 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 0859e5371..75611c28f 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -74,7 +74,7 @@ def cterm_execute( cut_point_rules: Iterable[str] | None = None, terminal_rules: Iterable[str] | None = None, module_name: str | None = None, - ) -> tuple[int, CTerm, list[CTerm], tuple[LogEntry, ...]]: + ) -> tuple[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( @@ -88,18 +88,19 @@ def cterm_execute( log_successful_simplifications=self._trace_rewrites, log_failed_simplifications=self._trace_rewrites, ) + _is_vacuous = er.reason == StopReason.VACUOUS depth = er.depth next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore)) _next_states = er.next_states if er.next_states is not None else [] next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states] if len(next_states) == 1 and len(next_states) < len(_next_states): - return depth + 1, next_states[0], [], er.logs + return _is_vacuous, depth + 1, next_states[0], [], er.logs elif len(next_states) == 1: if er.reason == StopReason.CUT_POINT_RULE: - return depth, next_state, next_states, er.logs + return _is_vacuous, depth, next_state, next_states, er.logs else: next_states = [] - return depth, next_state, next_states, er.logs + return _is_vacuous, depth, next_state, next_states, er.logs def cterm_simplify(self, cterm: CTerm) -> tuple[KInner, tuple[LogEntry, ...]]: _LOGGER.debug(f'Simplifying: {cterm}') @@ -296,7 +297,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: @@ -368,6 +369,8 @@ def extend( raise ValueError(f'Cannot extend non-leaf node {self.id}: {node.id}') if kcfg.is_stuck(node.id): raise ValueError(f'Cannot extend stuck node {self.id}: {node.id}') + if kcfg.is_vacuous(node.id): + raise ValueError(f'Cannot extend vacuous node {self.id}: {node.id}') if self._check_abstract(node, kcfg): return @@ -382,7 +385,7 @@ def extend( return _LOGGER.info(f'Extending KCFG from node {self.id}: {shorten_hashes(node.id)}') - depth, cterm, next_cterms, next_node_logs = self.cterm_execute( + _is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute( node.cterm, depth=execute_depth, cut_point_rules=cut_point_rules, @@ -401,8 +404,12 @@ def extend( # Stuck elif len(next_cterms) == 0: - kcfg.add_stuck(node.id) - _LOGGER.info(f'Found stuck node {self.id}: {shorten_hashes(node.id)}') + if _is_vacuous: + kcfg.add_vacuous(node.id) + _LOGGER.warning(f'Found vacuous node {self.id}: {shorten_hashes(node.id)}') + else: + kcfg.add_stuck(node.id) + _LOGGER.info(f'Found stuck node {self.id}: {shorten_hashes(node.id)}') # Cut Rule elif len(next_cterms) == 1: diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index c40af69bb..d6ab9aa02 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -205,6 +205,7 @@ def edges(self) -> tuple[KCFG.Edge, ...]: _covers: dict[int, dict[int, Cover]] _splits: dict[int, Split] _ndbranches: dict[int, NDBranch] + _vacuous: set[int] _stuck: set[int] _aliases: dict[str, int] _lock: RLock @@ -219,6 +220,7 @@ def __init__(self, cfg_dir: Path | None = None) -> None: self._covers = {} self._splits = {} self._ndbranches = {} + self._vacuous = set() self._stuck = set() self._aliases = {} self._lock = RLock() @@ -262,6 +264,10 @@ def nodes(self) -> list[Node]: def root(self) -> list[Node]: return [node for node in self.nodes if self.is_root(node.id)] + @property + def vacuous(self) -> list[Node]: + return [node for node in self.nodes if node.id in self._vacuous] + @property def stuck(self) -> list[Node]: return [node for node in self.nodes if node.id in self._stuck] @@ -315,6 +321,7 @@ def to_dict(self) -> dict[str, Any]: splits = [split.to_dict() for split in self.splits()] ndbranches = [ndbranch.to_dict() for ndbranch in self.ndbranches()] + vacuous = sorted(self._vacuous) stuck = sorted(self._stuck) aliases = dict(sorted(self._aliases.items())) @@ -325,6 +332,7 @@ def to_dict(self) -> dict[str, Any]: 'covers': covers, 'splits': splits, 'ndbranches': ndbranches, + 'vacuous': vacuous, 'stuck': stuck, 'aliases': aliases, } @@ -356,6 +364,9 @@ def from_dict(dct: Mapping[str, Any]) -> KCFG: csubst = CSubst.from_dict(cover_dict['csubst']) cfg.create_cover(source_id, target_id, csubst=csubst) + for vacuous_id in dct.get('vacuous') or []: + cfg.add_vacuous(vacuous_id) + for stuck_id in dct.get('stuck') or []: cfg.add_stuck(stuck_id) @@ -470,6 +481,7 @@ def remove_node(self, node_id: NodeIdLike) -> None: if not self._covers[source_id]: self._covers.pop(source_id) + self._vacuous.discard(node_id) self._stuck.discard(node_id) self._splits = {k: s for k, s in self._splits.items() if k != node_id and node_id not in s.target_ids} @@ -636,6 +648,19 @@ def edge_likes(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLi 'List[KCFG.EdgeLike]', self.covers(source_id=source_id, target_id=target_id) ) + def add_vacuous(self, node_id: NodeIdLike) -> None: + self._vacuous.add(self._resolve(node_id)) + + def remove_vacuous(self, node_id: NodeIdLike) -> None: + node_id = self._resolve(node_id) + if node_id not in self._vacuous: + raise ValueError(f'Node is not vacuous: {node_id}') + self._vacuous.remove(node_id) + + def discard_vacuous(self, node_id: NodeIdLike) -> None: + node_id = self._resolve(node_id) + self._vacuous.discard(node_id) + def add_stuck(self, node_id: NodeIdLike) -> None: self._stuck.add(self._resolve(node_id)) @@ -723,6 +748,10 @@ def is_root(self, node_id: NodeIdLike) -> bool: node_id = self._resolve(node_id) return len(self.predecessors(node_id)) == 0 + def is_vacuous(self, node_id: NodeIdLike) -> bool: + node_id = self._resolve(node_id) + return node_id in self._vacuous + def is_stuck(self, node_id: NodeIdLike) -> bool: node_id = self._resolve(node_id) return node_id in self._stuck @@ -888,6 +917,7 @@ def write_cfg_data(self) -> None: splits = [split.to_dict() for split in self.splits()] ndbranches = [ndbranch.to_dict() for ndbranch in self.ndbranches()] + vacuous = sorted(self._vacuous) stuck = sorted(self._stuck) aliases = dict(sorted(self._aliases.items())) dct: dict[str, list[int] | int | dict[str, int] | list[dict[str, Any]]] = {} @@ -897,6 +927,7 @@ def write_cfg_data(self) -> None: dct['covers'] = covers dct['splits'] = splits dct['ndbranches'] = ndbranches + dct['vacuous'] = vacuous dct['stuck'] = stuck dct['aliases'] = aliases cfg_json.write_text(json.dumps(dct)) @@ -964,6 +995,9 @@ def read_cfg_data(cfg_dir: Path, id: str) -> KCFG: csubst = CSubst.from_dict(cover_dict['csubst']) cfg.create_cover(source_id, target_id, csubst=csubst) + for vacuous_id in dct.get('vacuous') or []: + cfg.add_vacuous(vacuous_id) + for stuck_id in dct.get('stuck') or []: cfg.add_stuck(stuck_id) diff --git a/src/pyk/kcfg/show.py b/src/pyk/kcfg/show.py index 5aba44f11..596bbcff8 100644 --- a/src/pyk/kcfg/show.py +++ b/src/pyk/kcfg/show.py @@ -60,6 +60,8 @@ def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: attrs.append('root') if kcfg.is_stuck(node.id): attrs.append('stuck') + if kcfg.is_vacuous(node.id): + attrs.append('vacuous') if kcfg.is_leaf(node.id): attrs.append('leaf') if kcfg.is_split(node.id): diff --git a/src/pyk/kore/rpc.py b/src/pyk/kore/rpc.py index 0ca6f2899..4c0119747 100644 --- a/src/pyk/kore/rpc.py +++ b/src/pyk/kore/rpc.py @@ -443,7 +443,6 @@ class ExecuteResult(ABC): # noqa: B024 @classmethod def from_dict(cls: type[ER], dct: Mapping[str, Any]) -> ER: - _LOGGER.info(dct) return globals()[ExecuteResult._TYPES[StopReason(dct['reason'])]].from_dict(dct) # type: ignore @classmethod diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 1ccb0cc92..3128defb2 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -113,6 +113,7 @@ def is_pending(self, node_id: NodeIdLike) -> bool: return self.kcfg.is_leaf(node_id) and not ( self.is_terminal(node_id) or self.kcfg.is_stuck(node_id) + or self.kcfg.is_vacuous(node_id) or self.is_target(node_id) or self.is_refuted(node_id) ) @@ -125,7 +126,10 @@ def is_target(self, node_id: NodeIdLike) -> bool: def is_failing(self, node_id: NodeIdLike) -> bool: return self.kcfg.is_leaf(node_id) and not ( - self.is_pending(node_id) or self.is_target(node_id) or self.is_refuted(node_id) + self.is_pending(node_id) + or self.is_target(node_id) + or self.is_refuted(node_id) + or self.kcfg.is_vacuous(node_id) ) def add_terminal(self, node_id: NodeIdLike) -> None: diff --git a/src/tests/integration/kcfg/test_cell_map.py b/src/tests/integration/kcfg/test_cell_map.py index 1779753b6..02247d470 100644 --- a/src/tests/integration/kcfg/test_cell_map.py +++ b/src/tests/integration/kcfg/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')) diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index 06034e208..5391a5692 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -737,7 +737,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/integration/kcfg/test_multiple_definitions.py b/src/tests/integration/kcfg/test_multiple_definitions.py index 2ad52ae6f..b6fd399f2 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 8582da585..47e59ef4d 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')) From 06219b2f3e60c3d260905a08a16fe66d880658b2 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 8 Aug 2023 16:26:17 +0300 Subject: [PATCH 03/21] support vacuous in ARPBMCProof and update Proof summaries --- src/pyk/proof/reachability.py | 13 ++++++++++++- src/tests/unit/test_proof.py | 4 ++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 3128defb2..0aba97914 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -273,6 +273,7 @@ def summary(self) -> CompositeSummary: len(self.kcfg.nodes), len(self.pending), len(self.failing), + len(self.kcfg.vacuous), len(self.kcfg.stuck), len(self.terminal), len(self.node_refutations), @@ -448,12 +449,17 @@ def is_bounded(self, node_id: NodeIdLike) -> bool: def is_failing(self, node_id: NodeIdLike) -> bool: return self.kcfg.is_leaf(node_id) and not ( - self.is_pending(node_id) or self.is_target(node_id) or self.is_refuted(node_id) or self.is_bounded(node_id) + self.is_pending(node_id) + or self.is_target(node_id) + or self.is_refuted(node_id) + or self.is_bounded(node_id) + or self.kcfg.is_vacuous(node_id) ) def is_pending(self, node_id: NodeIdLike) -> bool: return self.kcfg.is_leaf(node_id) and not ( self.is_terminal(node_id) + or self.kcfg.is_vacuous(node_id) or self.kcfg.is_stuck(node_id) or self.is_bounded(node_id) or self.is_target(node_id) @@ -543,6 +549,7 @@ def summary(self) -> CompositeSummary: len(self.kcfg.nodes), len(self.pending), len(self.failing), + len(self.kcfg.vacuous), len(self.kcfg.stuck), len(self.terminal), len(self.node_refutations), @@ -759,6 +766,7 @@ class APRSummary(ProofSummary): nodes: int pending: int failing: int + vacuous: int stuck: int terminal: int refuted: int @@ -773,6 +781,7 @@ def lines(self) -> list[str]: f' nodes: {self.nodes}', f' pending: {self.pending}', f' failing: {self.failing}', + f' vacuous: {self.vacuous}', f' stuck: {self.stuck}', f' terminal: {self.terminal}', f' refuted: {self.refuted}', @@ -897,6 +906,7 @@ class APRBMCSummary(ProofSummary): nodes: int pending: int failing: int + vacuous: int stuck: int terminal: int refuted: int @@ -911,6 +921,7 @@ def lines(self) -> list[str]: f' nodes: {self.nodes}', f' pending: {self.pending}', f' failing: {self.failing}', + f' vacuous: {self.vacuous}', f' stuck: {self.stuck}', f' terminal: {self.terminal}', f' refuted: {self.refuted}', diff --git a/src/tests/unit/test_proof.py b/src/tests/unit/test_proof.py index df550471d..abafa489d 100644 --- a/src/tests/unit/test_proof.py +++ b/src/tests/unit/test_proof.py @@ -321,6 +321,7 @@ def test_apr_proof_summary(proof_dir: Path) -> None: nodes=1, pending=0, failing=0, + vacuous=0, stuck=0, terminal=0, refuted=0, @@ -343,6 +344,7 @@ def test_aprbmc_proof_summary(proof_dir: Path) -> None: nodes=1, pending=0, failing=0, + vacuous=0, stuck=0, terminal=0, refuted=0, @@ -379,6 +381,7 @@ def test_apr_proof_summary_subproofs(proof_dir: Path) -> None: nodes=1, pending=0, failing=0, + vacuous=0, stuck=0, terminal=0, refuted=0, @@ -394,6 +397,7 @@ def test_apr_proof_summary_subproofs(proof_dir: Path) -> None: nodes=2, pending=1, failing=0, + vacuous=0, stuck=0, terminal=0, refuted=0, From 3eb585d1f87acbc897df83ec8085170f2dafc845 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 8 Aug 2023 13:44:21 +0000 Subject: [PATCH 04/21] Set Version: 0.1.405 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 3c5b424b0..27db9c09d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.404 +0.1.405 diff --git a/pyproject.toml b/pyproject.toml index 9a0ba279a..691c13b52 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.404" +version = "0.1.405" description = "" authors = [ "Runtime Verification, Inc. ", From d061436fe1c9ccc766a9f46ffd07aa447ca9ba51 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 8 Aug 2023 21:52:08 +0300 Subject: [PATCH 05/21] format --- src/pyk/kore/rpc.py | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/src/pyk/kore/rpc.py b/src/pyk/kore/rpc.py index 4c0119747..cf7e86310 100644 --- a/src/pyk/kore/rpc.py +++ b/src/pyk/kore/rpc.py @@ -452,28 +452,6 @@ def _check_reason(cls: type[ER], dct: Mapping[str, Any]) -> None: raise ValueError(f"Expected {cls.reason} as 'reason', found: {reason}") -@final -@dataclass(frozen=True) -class VacuousResult(ExecuteResult): - reason = StopReason.VACUOUS - next_states = None - rule = None - - state: State - depth: int - logs: tuple[LogEntry, ...] - - @classmethod - def from_dict(cls: type[VacuousResult], dct: Mapping[str, Any]) -> VacuousResult: - cls._check_reason(dct) - logs = tuple(LogEntry.from_dict(l) for l in dct['logs']) if 'logs' in dct else () - return VacuousResult( - state=State.from_dict(dct['state']), - depth=dct['depth'], - logs=logs, - ) - - @final @dataclass(frozen=True) class StuckResult(ExecuteResult): @@ -585,6 +563,28 @@ def from_dict(cls: type[TerminalResult], dct: Mapping[str, Any]) -> TerminalResu return TerminalResult(state=State.from_dict(dct['state']), depth=dct['depth'], rule=dct['rule'], logs=logs) +@final +@dataclass(frozen=True) +class VacuousResult(ExecuteResult): + reason = StopReason.VACUOUS + next_states = None + rule = None + + state: State + depth: int + logs: tuple[LogEntry, ...] + + @classmethod + def from_dict(cls: type[VacuousResult], dct: Mapping[str, Any]) -> VacuousResult: + cls._check_reason(dct) + logs = tuple(LogEntry.from_dict(l) for l in dct['logs']) if 'logs' in dct else () + return VacuousResult( + state=State.from_dict(dct['state']), + depth=dct['depth'], + logs=logs, + ) + + @final @dataclass(frozen=True) class ImpliesResult: From e02e170b4a969c1160d6689761f088e2e92bc8e2 Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 9 Aug 2023 15:15:10 +0300 Subject: [PATCH 06/21] add code review suggestions --- src/pyk/kcfg/explore.py | 2 +- .../integration/kore/test_kore_client.py | 2 ++ src/tests/unit/kore/test_client.py | 11 ++++++++++ src/tests/unit/test_kcfg.py | 22 +++++++++++++++---- 4 files changed, 32 insertions(+), 5 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 75611c28f..6a24c0d18 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -88,7 +88,7 @@ def cterm_execute( log_successful_simplifications=self._trace_rewrites, log_failed_simplifications=self._trace_rewrites, ) - _is_vacuous = er.reason == StopReason.VACUOUS + _is_vacuous = er.reason is StopReason.VACUOUS depth = er.depth next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore)) _next_states = er.next_states if er.next_states is not None else [] diff --git a/src/tests/integration/kore/test_kore_client.py b/src/tests/integration/kore/test_kore_client.py index d3775654e..a3d605a53 100644 --- a/src/tests/integration/kore/test_kore_client.py +++ b/src/tests/integration/kore/test_kore_client.py @@ -19,6 +19,7 @@ TerminalResult, UnknownResult, UnsatResult, + VacuousResult, ) from pyk.kore.syntax import And, App, Bottom, Equals, EVar, Implies, Module, Top from pyk.testing import BoosterClientTest, KoreClientTest @@ -79,6 +80,7 @@ def state(n: int) -> State: {'terminal_rules': ['KORE-RPC-TEST.r56']}, TerminalResult(state=state(6), depth=2, rule='KORE-RPC-TEST.r56', logs=()), ), + ('vacuous', 3, {}, VacuousResult(state=state(4), depth=2, logs=())), ) diff --git a/src/tests/unit/kore/test_client.py b/src/tests/unit/kore/test_client.py index eeab0158c..10c435fef 100644 --- a/src/tests/unit/kore/test_client.py +++ b/src/tests/unit/kore/test_client.py @@ -17,6 +17,7 @@ TransportType, UnknownResult, UnsatResult, + VacuousResult, ) from pyk.kore.syntax import And, App, Bottom, Module, Top @@ -95,6 +96,16 @@ def kore_client(mock: Mock, mock_class: Mock) -> Iterator[KoreClient]: # noqa: }, StuckResult(State(int_dv(2), int_top, int_top), 1, logs=()), ), + ( + App('IntAdd', (), (int_dv(1), int_dv(1))), + {'state': kore(App('IntAdd', [], [int_dv(1), int_dv(1)]))}, + { + 'state': {'term': kore(int_dv(2)), 'substitution': kore(int_top), 'predicate': kore(int_top)}, + 'depth': 1, + 'reason': 'vacuous', + }, + VacuousResult(State(int_dv(2), int_top, int_top), 1, logs=()), + ), ) diff --git a/src/tests/unit/test_kcfg.py b/src/tests/unit/test_kcfg.py index 68f4a3146..7e4c10f6e 100644 --- a/src/tests/unit/test_kcfg.py +++ b/src/tests/unit/test_kcfg.py @@ -381,6 +381,19 @@ def test_resolve() -> None: assert node(1) == cfg.node(1) +def test_vacuous() -> None: + # Given + d = { + 'nodes': node_dicts(4), + 'edges': edge_dicts((1, 2), (2, 3)), + 'aliases': {'foo': 2}, + } + + cfg = KCFG.from_dict(d) + cfg.add_vacuous(3) + assert cfg.vacuous, node(3) + + def test_aliases() -> None: # Given d = { @@ -476,6 +489,7 @@ def _x_equals(i: int) -> KInner: ), 'ndbranches': ndbranch_dicts((20, [(24, False), (25, True)])), 'stuck': [23], + 'vacuous': [17], } cfg = KCFG.from_dict(d) @@ -514,7 +528,7 @@ def _x_equals(i: int) -> KInner: '┣━━┓ constraint: #Equals ( x , 17 )\n' '┃ ┃ subst: V14 <- V17\n' '┃ │\n' - '┃ └─ 17 (leaf)\n' + '┃ └─ 17 (vacuous, leaf)\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 18 )\n' '┃ ┃ subst: V14 <- V18\n' @@ -522,7 +536,7 @@ def _x_equals(i: int) -> KInner: '┃ ├─ 18\n' '┃ │\n' '┃ │ (1 step)\n' - '┃ └─ 17 (leaf)\n' + '┃ └─ 17 (vacuous, leaf)\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 20 )\n' '┃ ┃ subst: V14 <- V20\n' @@ -621,7 +635,7 @@ def _x_equals(i: int) -> KInner: '┣━━┓ constraint: #Equals ( x , 17 )\n' '┃ ┃ subst: V14 <- V17\n' '┃ │\n' - '┃ └─ 17 (leaf)\n' + '┃ └─ 17 (vacuous, leaf)\n' '┃ \n' '┃ V17\n' '┃ \n' @@ -635,7 +649,7 @@ def _x_equals(i: int) -> KInner: '┃ │ \n' '┃ │\n' '┃ │ (1 step)\n' - '┃ └─ 17 (leaf)\n' + '┃ └─ 17 (vacuous, leaf)\n' '┃ \n' '┃ V17\n' '┃ \n' From 7d68bdc2edacf9e267fa94d9607a5f6eec5ae6ce Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 9 Aug 2023 12:18:29 +0000 Subject: [PATCH 07/21] Set Version: 0.1.407 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 14f436c62..21caf7fb4 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.406 +0.1.407 diff --git a/pyproject.toml b/pyproject.toml index a5b4fa052..bb91b4728 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.406" +version = "0.1.407" description = "" authors = [ "Runtime Verification, Inc. ", From 497316b25b8e2ef3d909e0e8e9c55ef9a1ad155e Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 10 Aug 2023 16:13:30 +0000 Subject: [PATCH 08/21] Set Version: 0.1.409 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index de2758b65..1162c990d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.408 +0.1.409 diff --git a/pyproject.toml b/pyproject.toml index aed206cf3..a87e5b2c4 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.408" +version = "0.1.409" description = "" authors = [ "Runtime Verification, Inc. ", From 7ad3fad1ab051e7861c34fe2ae511a192300e535 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 10 Aug 2023 18:52:38 +0000 Subject: [PATCH 09/21] Set Version: 0.1.412 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 759f8fc7d..d10f1fedc 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.411 +0.1.412 diff --git a/pyproject.toml b/pyproject.toml index 9b8fc36a8..564f79bc2 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.411" +version = "0.1.412" description = "" authors = [ "Runtime Verification, Inc. ", From c0c16dd0eb630f2213790637aad3cd7dad950192 Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 11 Aug 2023 05:34:32 +0300 Subject: [PATCH 10/21] set EXECUTE_BOOSTER_TEST_DATA --- src/tests/integration/kore/test_kore_client.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/tests/integration/kore/test_kore_client.py b/src/tests/integration/kore/test_kore_client.py index b8af6dcdc..bf59de952 100644 --- a/src/tests/integration/kore/test_kore_client.py +++ b/src/tests/integration/kore/test_kore_client.py @@ -85,6 +85,9 @@ def state(n: int) -> State: ) +EXECUTE_BOOSTER_TEST_DATA: Final[tuple[tuple[str, int, Mapping[str, Any], ExecuteResult], ...]] = EXECUTE_TEST_DATA[:-1] + + IMPLIES_TEST_DATA: Final = ( ( '0 -> T', @@ -233,8 +236,8 @@ class TestBooster(BoosterClientTest): @pytest.mark.parametrize( 'test_id,n,params,expected', - EXECUTE_TEST_DATA, - ids=[test_id for test_id, *_ in EXECUTE_TEST_DATA], + EXECUTE_BOOSTER_TEST_DATA, + ids=[test_id for test_id, *_ in EXECUTE_BOOSTER_TEST_DATA], ) def test_execute_booster( self, From 8461621feb8c168a5567d247edfb5d04451a11a6 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 16 Aug 2023 12:46:12 +0000 Subject: [PATCH 11/21] Set Version: 0.1.416 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 5bb6eae1e..0892550dd 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.415 +0.1.416 diff --git a/pyproject.toml b/pyproject.toml index 6272a7533..5c06d1e5b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.415" +version = "0.1.416" description = "" authors = [ "Runtime Verification, Inc. ", From ab6abb758c53f5802762002726ef3a6c65e10bfa Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 1 Sep 2023 10:41:44 +0000 Subject: [PATCH 12/21] Set Version: 0.1.432 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index dbca01d40..adb14616f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.431 +0.1.432 diff --git a/pyproject.toml b/pyproject.toml index 8c087c6a8..bfe14ddc4 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.431" +version = "0.1.432" description = "" authors = [ "Runtime Verification, Inc. ", From 41ba65308ab950773a9df7d01f9cd76a796a5c9c Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 1 Sep 2023 14:19:02 +0300 Subject: [PATCH 13/21] update is_explorable and is_failing --- src/pyk/kcfg/exploration.py | 7 ++++++- src/pyk/proof/reachability.py | 1 + 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/pyk/kcfg/exploration.py b/src/pyk/kcfg/exploration.py index c10ce46aa..f9c1b2641 100644 --- a/src/pyk/kcfg/exploration.py +++ b/src/pyk/kcfg/exploration.py @@ -29,7 +29,12 @@ def is_terminal(self, node_id: NodeIdLike) -> bool: # Explorable node recogniser def is_explorable(self, node_id: NodeIdLike) -> bool: - return self.kcfg.is_leaf(node_id) and not self.is_terminal(node_id) and not self.kcfg.is_stuck(node_id) + return ( + self.kcfg.is_leaf(node_id) + and not self.is_terminal(node_id) + and not self.kcfg.is_stuck(node_id) + and not self.kcfg.is_vacuous(node_id) + ) # # Collectors diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 5fd842309..f18999f0f 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -115,6 +115,7 @@ def is_failing(self, node_id: NodeIdLike) -> bool: and not self.is_explorable(node_id) and not self.is_target(node_id) and not self.is_refuted(node_id) + and not self.kcfg.is_vacuous(node_id) ) def shortest_path_to(self, node_id: NodeIdLike) -> tuple[KCFG.Successor, ...]: From adcf3bd8cb290a7a2a0ed7dc48712969d4939eb2 Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 1 Sep 2023 14:19:11 +0300 Subject: [PATCH 14/21] Revert "set EXECUTE_BOOSTER_TEST_DATA" This reverts commit c0c16dd0eb630f2213790637aad3cd7dad950192. --- src/tests/integration/kore/test_kore_client.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/tests/integration/kore/test_kore_client.py b/src/tests/integration/kore/test_kore_client.py index bf59de952..b8af6dcdc 100644 --- a/src/tests/integration/kore/test_kore_client.py +++ b/src/tests/integration/kore/test_kore_client.py @@ -85,9 +85,6 @@ def state(n: int) -> State: ) -EXECUTE_BOOSTER_TEST_DATA: Final[tuple[tuple[str, int, Mapping[str, Any], ExecuteResult], ...]] = EXECUTE_TEST_DATA[:-1] - - IMPLIES_TEST_DATA: Final = ( ( '0 -> T', @@ -236,8 +233,8 @@ class TestBooster(BoosterClientTest): @pytest.mark.parametrize( 'test_id,n,params,expected', - EXECUTE_BOOSTER_TEST_DATA, - ids=[test_id for test_id, *_ in EXECUTE_BOOSTER_TEST_DATA], + EXECUTE_TEST_DATA, + ids=[test_id for test_id, *_ in EXECUTE_TEST_DATA], ) def test_execute_booster( self, From 5885e4b9391878018f39fd9f3f725c78f138aa7c Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 7 Sep 2023 20:22:47 +0100 Subject: [PATCH 15/21] adding vacuous check in check_terminal --- src/pyk/proof/reachability.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index f18999f0f..9afd4434c 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -581,7 +581,7 @@ def _check_terminal(self, node: KCFG.Node) -> None: if node.id not in self._checked_terminals: _LOGGER.info(f'Checking terminal: {node.id}') self._checked_terminals.add(node.id) - if self.kcfg_explore.kcfg_semantics.is_terminal(node.cterm): + if not self.proof.kcfg.is_vacuous(node.id) and self.kcfg_explore.kcfg_semantics.is_terminal(node.cterm): _LOGGER.info(f'Terminal node: {node.id}.') self.proof._terminal.add(node.id) From be3f7e9940d8d4231592cb2f9afea42532cbb028 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 8 Sep 2023 07:06:07 +0000 Subject: [PATCH 16/21] Set Version: 0.1.437 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 3b3ad01e8..88491bbf1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.436 +0.1.437 diff --git a/pyproject.toml b/pyproject.toml index 507ec6429..77f588ae5 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.436" +version = "0.1.437" description = "" authors = [ "Runtime Verification, Inc. ", From 208de95c099496da41bcfcb6bac4dd756931e268 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 8 Sep 2023 08:28:23 +0100 Subject: [PATCH 17/21] reverting vacuous check --- src/pyk/proof/reachability.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 9afd4434c..f18999f0f 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -581,7 +581,7 @@ def _check_terminal(self, node: KCFG.Node) -> None: if node.id not in self._checked_terminals: _LOGGER.info(f'Checking terminal: {node.id}') self._checked_terminals.add(node.id) - if not self.proof.kcfg.is_vacuous(node.id) and self.kcfg_explore.kcfg_semantics.is_terminal(node.cterm): + if self.kcfg_explore.kcfg_semantics.is_terminal(node.cterm): _LOGGER.info(f'Terminal node: {node.id}.') self.proof._terminal.add(node.id) From 088bf96a5f010cfeb1c5e5a97497a5f683d40eb9 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 8 Sep 2023 08:33:38 +0100 Subject: [PATCH 18/21] filtering bottom states out of returned cterms --- src/pyk/cterm.py | 6 +++++- src/pyk/kcfg/explore.py | 2 ++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index ad57007a4..2abf4ec0b 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -110,7 +110,11 @@ def _is_bottom(kast: KInner) -> bool: flat = flatten_label('#And', kast) if len(flat) == 1: return is_bottom(single(flat)) - return all(CTerm._is_bottom(term) for term in flat) + return any(CTerm._is_bottom(term) for term in flat) + + @property + def is_bottom(self) -> bool: + return CTerm._is_bottom(self.config) or any(CTerm._is_bottom(cterm) for cterm in self.constraints) @staticmethod def _constraint_sort_key(term: KInner) -> tuple[int, str]: diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 8cd5900b3..f748d3c5a 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -394,6 +394,8 @@ def extend( module_name=module_name, ) + next_cterms = [cterm for cterm in next_cterms if not cterm.is_bottom] + # Basic block if depth > 0: next_node = kcfg.create_node(cterm) From 03e21646546893834a10fb1b1501420b403c3267 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 8 Sep 2023 08:39:45 +0100 Subject: [PATCH 19/21] pruning bottom states in pyk --- src/pyk/kcfg/explore.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index f748d3c5a..3f69a26d9 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -94,6 +94,7 @@ def cterm_execute( next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore)) _next_states = er.next_states if er.next_states is not None else [] 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 elif len(next_states) == 1: @@ -394,8 +395,6 @@ def extend( module_name=module_name, ) - next_cterms = [cterm for cterm in next_cterms if not cterm.is_bottom] - # Basic block if depth > 0: next_node = kcfg.create_node(cterm) From 4417c254334f319b0517d284572283adbc67b800 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 8 Sep 2023 08:05:06 +0000 Subject: [PATCH 20/21] Set Version: 0.1.438 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 88491bbf1..88d1eb844 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.437 +0.1.438 diff --git a/pyproject.toml b/pyproject.toml index 77f588ae5..aad04ff1f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.437" +version = "0.1.438" description = "" authors = [ "Runtime Verification, Inc. ", From 89f625112809de7bddb318014a02057c0d7bd46f Mon Sep 17 00:00:00 2001 From: Andrei Date: Fri, 8 Sep 2023 12:05:09 +0300 Subject: [PATCH 21/21] update kore-rpc-test --- src/tests/integration/k-files/kore-rpc-test.k | 3 +++ src/tests/integration/kore/test_kore_client.py | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tests/integration/k-files/kore-rpc-test.k b/src/tests/integration/k-files/kore-rpc-test.k index 4c23a5d48..937dfed5e 100644 --- a/src/tests/integration/k-files/kore-rpc-test.k +++ b/src/tests/integration/k-files/kore-rpc-test.k @@ -1,16 +1,19 @@ module KORE-RPC-TEST-SYNTAX imports INT-SYNTAX + imports BOOL-SYNTAX endmodule module KORE-RPC-TEST imports KORE-RPC-TEST-SYNTAX imports INT + imports BOOL rule [r01]: 0 => 1 rule [r12]: 1 => 2 rule [r23]: 2 => 3 rule [r24]: 2 => 4 + rule [r34]: 3 => 4 ensures false rule [r45]: 4 => 5 rule [r56]: 5 => 6 diff --git a/src/tests/integration/kore/test_kore_client.py b/src/tests/integration/kore/test_kore_client.py index b8af6dcdc..edf981a51 100644 --- a/src/tests/integration/kore/test_kore_client.py +++ b/src/tests/integration/kore/test_kore_client.py @@ -81,7 +81,7 @@ def state(n: int) -> State: {'terminal_rules': ['KORE-RPC-TEST.r56']}, TerminalResult(state=state(6), depth=2, rule='KORE-RPC-TEST.r56', logs=()), ), - ('vacuous', 3, {}, VacuousResult(state=state(4), depth=2, logs=())), + ('vacuous', 3, {}, VacuousResult(state=state(3), depth=0, logs=())), )