From 61a31724709329df06fefef5d2a42b2fe03451e9 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 15 Feb 2024 15:34:58 -0600 Subject: [PATCH 01/13] Separate logic for ImpliesProof and APRProof into self-contained steps which work with advance_proof loop --- src/pyk/proof/equality.py | 95 +++++++++++++++-------- src/pyk/proof/proof.py | 21 +++++- src/pyk/proof/reachability.py | 138 ++++++++++++++++++++++++++++------ 3 files changed, 201 insertions(+), 53 deletions(-) diff --git a/src/pyk/proof/equality.py b/src/pyk/proof/equality.py index 01a4f053b..2ccdbf9c4 100644 --- a/src/pyk/proof/equality.py +++ b/src/pyk/proof/equality.py @@ -12,7 +12,7 @@ from ..prelude.kbool import BOOL, TRUE from ..prelude.ml import is_bottom, is_top, mlAnd, mlEquals, mlEqualsFalse from ..utils import ensure_dir_path -from .proof import Proof, ProofStatus, ProofSummary, Prover +from .proof import Proof, ProofStatus, ProofStep, ProofSummary, Prover, StepResult if TYPE_CHECKING: from collections.abc import Iterable, Mapping @@ -349,6 +349,52 @@ def lines(self) -> list[str]: ] +@dataclass +class ImpliesProofResult(StepResult): + csubst: CSubst | None + simplified_antecedent: KInner | None + simplified_consequent: KInner | None + + +@dataclass +class ImpliesProofStep(ProofStep): + kcfg_explore: KCFGExplore + antecedent: KInner + consequent: KInner + proof_id: str + + def exec(self) -> StepResult: + # to prove the equality, we check the implication of the form `constraints #Implies LHS #Equals RHS`, i.e. + # "LHS equals RHS under these constraints" + simplified_antecedent, _ = self.kcfg_explore.kast_simplify(self.antecedent) + simplified_consequent, _ = self.kcfg_explore.kast_simplify(self.consequent) + _LOGGER.info(f'Simplified antecedent: {self.kcfg_explore.kprint.pretty_print(simplified_antecedent)}') + _LOGGER.info(f'Simplified consequent: {self.kcfg_explore.kprint.pretty_print(simplified_consequent)}') + + csubst: CSubst + + if is_bottom(simplified_antecedent): + _LOGGER.warning(f'Antecedent of implication (proof constraints) simplifies to #Bottom {self.proof_id}') + csubst = CSubst(Subst({}), ()) + + elif is_top(simplified_consequent): + _LOGGER.warning(f'Consequent of implication (proof equality) simplifies to #Top {self.proof_id}') + csubst = CSubst(Subst({}), ()) + + else: + dummy_config = self.kcfg_explore.kprint.definition.empty_config(sort=GENERATED_TOP_CELL) + implies_result = self.kcfg_explore.cterm_implies( + antecedent=CTerm(config=dummy_config, constraints=[simplified_antecedent]), + consequent=CTerm(config=dummy_config, constraints=[simplified_consequent]), + ) + if implies_result is not None: + csubst = implies_result + + return ImpliesProofResult( + csubst=csubst, simplified_antecedent=simplified_antecedent, simplified_consequent=simplified_consequent + ) + + class ImpliesProver(Prover): proof: ImpliesProof @@ -356,39 +402,28 @@ def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore): super().__init__(kcfg_explore) self.proof = proof - def step_proof(self) -> None: + def get_steps(self) -> Iterable[ProofStep]: proof_type = type(self.proof).__name__ _LOGGER.info(f'Attempting {proof_type} {self.proof.id}') if self.proof.status is not ProofStatus.PENDING: _LOGGER.info(f'{proof_type} finished {self.proof.id}: {self.proof.status}') - return - - # 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) - consequent_simplified_kast, _ = self.kcfg_explore.kast_simplify(self.proof.consequent) - 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)}') - _LOGGER.info(f'Simplified consequent: {self.kcfg_explore.kprint.pretty_print(consequent_simplified_kast)}') - - if is_bottom(antecedent_simplified_kast): - _LOGGER.warning(f'Antecedent of implication (proof constraints) simplifies to #Bottom {self.proof.id}') - self.proof.csubst = CSubst(Subst({}), ()) - - elif is_top(consequent_simplified_kast): - _LOGGER.warning(f'Consequent of implication (proof equality) simplifies to #Top {self.proof.id}') - self.proof.csubst = CSubst(Subst({}), ()) - - else: - # TODO: we should not be forced to include the dummy configuration in the antecedent and consequent - dummy_config = self.kcfg_explore.kprint.definition.empty_config(sort=GENERATED_TOP_CELL) - result = self.kcfg_explore.cterm_implies( - antecedent=CTerm(config=dummy_config, constraints=[self.proof.simplified_antecedent]), - consequent=CTerm(config=dummy_config, constraints=[self.proof.simplified_consequent]), + return [] + return [ + ImpliesProofStep( + antecedent=self.proof.antecedent, + consequent=self.proof.consequent, + kcfg_explore=self.kcfg_explore, + proof_id=self.proof.id, ) - if result is not None: - self.proof.csubst = result + ] - _LOGGER.info(f'{proof_type} finished {self.proof.id}: {self.proof.status}') + def commit(self, result: StepResult) -> None: + proof_type = type(self.proof).__name__ + if isinstance(result, ImpliesProofResult): + self.proof.csubst = result.csubst + self.proof.simplified_antecedent = result.simplified_antecedent + self.proof.simplified_consequent = result.simplified_consequent + _LOGGER.info(f'{proof_type} finished {self.proof.id}: {self.proof.status}') + else: + raise ValueError('Incorrect result type') diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index f32ecb707..70ef43631 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -286,6 +286,16 @@ def lines(self) -> list[str]: return [line for lines in (summary.lines for summary in self.summaries) for line in lines] +class StepResult: + ... + + +class ProofStep: + @abstractmethod + def exec(self) -> StepResult: + ... + + class Prover: kcfg_explore: KCFGExplore proof: Proof @@ -294,7 +304,11 @@ def __init__(self, kcfg_explore: KCFGExplore): self.kcfg_explore = kcfg_explore @abstractmethod - def step_proof(self) -> None: + def get_steps(self) -> Iterable[ProofStep]: + ... + + @abstractmethod + def commit(self, result: StepResult) -> None: ... def advance_proof(self, max_iterations: int | None = None, fail_fast: bool = False) -> None: @@ -306,5 +320,8 @@ def advance_proof(self, max_iterations: int | None = None, fail_fast: bool = Fal if max_iterations is not None and max_iterations <= iterations: return iterations += 1 - self.step_proof() + steps = self.get_steps() + for step in steps: + result = step.exec() + self.commit(result) self.proof.write_proof_data() diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index a8e2ac018..26f259831 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -19,15 +19,17 @@ from ..prelude.ml import mlAnd, mlEquals, mlTop from ..utils import FrozenDict, ensure_dir_path, hash_str, shorten_hashes, single from .equality import ProofSummary, Prover, RefutationProof -from .proof import CompositeSummary, Proof, ProofStatus +from .proof import CompositeSummary, Proof, ProofStatus, ProofStep, StepResult if TYPE_CHECKING: from collections.abc import Iterable, Mapping from pathlib import Path from typing import Any, Final, TypeVar + from ..cterm import CSubst, CTerm from ..kast.outer import KClaim, KDefinition, KFlatModuleList, KRuleLike from ..kcfg import KCFGExplore + from ..kcfg.explore import ExtendResult from ..kcfg.kcfg import NodeIdLike T = TypeVar('T', bound='Proof') @@ -685,30 +687,55 @@ def advance_pending_node( module_name=module_name, ) - def step_proof(self) -> None: + def get_steps(self) -> Iterable[APRProofStep]: self._check_all_terminals() if not self.proof.pending: - return - curr_node = self.proof.pending[0] - - self.advance_pending_node( - node=curr_node, - execute_depth=self.execute_depth, - cut_point_rules=self.cut_point_rules, - terminal_rules=self.terminal_rules, - ) - - self._check_all_terminals() + return [] + steps = [] + target_node = self.proof.kcfg.node(self.proof.target) + for curr_node in self.proof.pending: + steps.append( + APRProofStep( + always_check_subsumption=self.always_check_subsumption, + bmc_depth=self.proof.bmc_depth, + checked_for_bounded=self._checked_for_bounded, + cterm=curr_node.cterm, + cut_point_rules=self.cut_point_rules, + execute_depth=self.execute_depth, + fast_check_subsumption=self.fast_check_subsumption, + is_terminal=self.kcfg_explore.kcfg_semantics.is_terminal(curr_node.cterm), + kcfg_explore=self.kcfg_explore, + module_name=( + self.circularities_module_name + if self.nonzero_depth(curr_node) + else self.dependencies_module_name + ), + node_id=curr_node.id, + proof_id=self.proof.id, + target_cterm=target_node.cterm, + target_is_terminal=self.proof.target in self.proof._terminal, + target_node_id=target_node.id, + terminal_rules=self.terminal_rules, + ) + ) + return steps - for node in self.proof.terminal: - if ( - not node.id in self._checked_for_subsumption - and self.proof.kcfg.is_leaf(node.id) - and not self.proof.is_target(node.id) - ): - self._checked_for_subsumption.add(node.id) - self._check_subsume(node) + def commit(self, result: StepResult) -> None: + if isinstance(result, APRProofExtendResult): + self.kcfg_explore.extend_kcfg( + result.extend_result, self.proof.kcfg, self.proof.kcfg.node(result.node_id), self.proof.logs + ) + elif isinstance(result, APRProofSubsumeResult): + if result.csubst is None: + self.proof._terminal.add(result.node_id) + else: + self.proof.kcfg.create_cover(result.node_id, self.proof.target, csubst=result.csubst) + _LOGGER.info( + f'Subsumed into target node {self.proof.id}: {shorten_hashes((result.node_id, self.proof.target))}' + ) + else: + raise ValueError('Incorrect result type') if self.proof.failed: self.proof.failure_info = self.failure_info() @@ -717,6 +744,75 @@ def failure_info(self) -> APRFailureInfo: return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info) +@dataclass +class APRProofResult(StepResult): + node_id: int + + +@dataclass +class APRProofExtendResult(APRProofResult): + extend_result: ExtendResult + + +@dataclass +class APRProofSubsumeResult(APRProofResult): + csubst: CSubst | None + + +@dataclass(frozen=True, eq=True) +class APRProofStep(ProofStep): + bmc_depth: int | None + node_id: int + target_node_id: int + proof_id: str + fast_check_subsumption: bool + cterm: CTerm + target_cterm: CTerm + kcfg_explore: KCFGExplore + checked_for_bounded: Iterable[int] + target_is_terminal: bool + always_check_subsumption: bool + module_name: str + cut_point_rules: Iterable[str] + terminal_rules: Iterable[str] + execute_depth: int | None + is_terminal: bool + + def _may_subsume(self) -> bool: + node_k_cell = self.cterm.try_cell('K_CELL') + target_k_cell = self.target_cterm.try_cell('K_CELL') + if node_k_cell and target_k_cell and not target_k_cell.match(node_k_cell): + return False + return True + + def _check_subsume(self) -> CSubst | None: + _LOGGER.info( + f'Checking subsumption into target state {self.proof_id}: {shorten_hashes((self.node_id, self.target_node_id))}' + ) + if self.fast_check_subsumption and not self._may_subsume(): + _LOGGER.info( + f'Skipping full subsumption check because of fast may subsume check {self.proof_id}: {self.node_id}' + ) + return None + return self.kcfg_explore.cterm_implies(self.cterm, self.target_cterm) + + def exec(self) -> APRProofResult: + if self.is_terminal or not self.target_is_terminal: + if self.always_check_subsumption: + csubst = self._check_subsume() + if csubst is not None or self.is_terminal: + return APRProofSubsumeResult(csubst=csubst, node_id=self.node_id) + + extend_result = self.kcfg_explore.extend_cterm( + self.cterm, + execute_depth=self.execute_depth, + cut_point_rules=self.cut_point_rules, + terminal_rules=self.terminal_rules, + module_name=self.module_name, + ) + return APRProofExtendResult(node_id=self.node_id, extend_result=extend_result) + + @dataclass(frozen=True) class APRSummary(ProofSummary): id: str From fbe0eb773747a42ccce55e6e244a350c3a86556d Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 15 Feb 2024 21:36:36 +0000 Subject: [PATCH 02/13] Set Version: 0.1.628 --- docs/conf.py | 4 ++-- package/version | 2 +- pyproject.toml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/conf.py b/docs/conf.py index d4af59a9c..a2730dc62 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.627' -release = '0.1.627' +version = '0.1.628' +release = '0.1.628' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index 83ea503f0..1fa102d5a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.627 +0.1.628 diff --git a/pyproject.toml b/pyproject.toml index 04c16c9a1..853405d80 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.627" +version = "0.1.628" description = "" authors = [ "Runtime Verification, Inc. ", From adea08110b7db19f57cb613e4d2f79d83919341f Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 15 Feb 2024 16:35:25 -0600 Subject: [PATCH 03/13] Fix nodes being checked for terminal before starting the next step --- src/pyk/proof/proof.py | 5 ++++ src/pyk/proof/reachability.py | 44 ++++++++++++++++++++++++++++++++++- 2 files changed, 48 insertions(+), 1 deletion(-) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index 70ef43631..1b554b927 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -322,6 +322,11 @@ def advance_proof(self, max_iterations: int | None = None, fail_fast: bool = Fal iterations += 1 steps = self.get_steps() for step in steps: + print(f'b: {self.proof.can_progress}') result = step.exec() + print(f'c: {self.proof.can_progress}') self.commit(result) + print(f'd: {self.proof.can_progress}') + print(f'a: {self.proof.can_progress}') self.proof.write_proof_data() + print(f'abc: {self.proof.can_progress}') diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 26f259831..9891f891c 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -9,6 +9,7 @@ from pyk.kore.rpc import LogEntry +from .show import KCFGShow, NodePrinter from ..kast.inner import KInner, Subst from ..kast.manip import flatten_label, ml_pred_to_bool from ..kast.outer import KFlatModule, KImport, KRule @@ -688,13 +689,32 @@ def advance_pending_node( ) def get_steps(self) -> Iterable[APRProofStep]: - self._check_all_terminals() if not self.proof.pending: return [] steps = [] target_node = self.proof.kcfg.node(self.proof.target) for curr_node in self.proof.pending: + if self.proof.bmc_depth is not None and curr_node.id not in self._checked_for_bounded: + _LOGGER.info(f'Checking bmc depth for node {self.proof.id}: {curr_node.id}') + self._checked_for_bounded.add(curr_node.id) + _prior_loops = [ + succ.source.id + for succ in self.proof.shortest_path_to(curr_node.id) + if self.kcfg_explore.kcfg_semantics.same_loop(succ.source.cterm, curr_node.cterm) + ] + prior_loops: list[NodeIdLike] = [] + for _pl in _prior_loops: + if not ( + self.proof.kcfg.zero_depth_between(_pl, curr_node.id) + or any(self.proof.kcfg.zero_depth_between(_pl, pl) for pl in prior_loops) + ): + prior_loops.append(_pl) + _LOGGER.info(f'Prior loop heads for node {self.proof.id}: {(curr_node.id, prior_loops)}') + if len(prior_loops) > self.proof.bmc_depth: + _LOGGER.warning(f'Bounded node {self.proof.id}: {curr_node.id} at bmc depth {self.proof.bmc_depth}') + self.proof.add_bounded(curr_node.id) + continue steps.append( APRProofStep( always_check_subsumption=self.always_check_subsumption, @@ -719,6 +739,7 @@ def get_steps(self) -> Iterable[APRProofStep]: terminal_rules=self.terminal_rules, ) ) + print(steps) return steps def commit(self, result: StepResult) -> None: @@ -740,6 +761,23 @@ def commit(self, result: StepResult) -> None: if self.proof.failed: self.proof.failure_info = self.failure_info() + self._check_all_terminals() + + for node in self.proof.terminal: + if ( + not node.id in self._checked_for_subsumption + and self.proof.kcfg.is_leaf(node.id) + and not self.proof.is_target(node.id) + ): + self._checked_for_subsumption.add(node.id) + self._check_subsume(node) + + print(f'pending: {self.proof.pending}') + print(f'can_progress: {self.proof.can_progress}') + + show = KCFGShow(self.kcfg_explore.kprint, node_printer=NodePrinter(self.kcfg_explore.kprint, full_printer=True)) + print('\n'.join(show.pretty(self.proof.kcfg))) + def failure_info(self) -> APRFailureInfo: return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info) @@ -797,8 +835,12 @@ def _check_subsume(self) -> CSubst | None: return self.kcfg_explore.cterm_implies(self.cterm, self.target_cterm) def exec(self) -> APRProofResult: + print(f'is_terminal: {self.is_terminal}') + print(f'target_is_terminal: {self.target_is_terminal}') if self.is_terminal or not self.target_is_terminal: + print(f'always_check_subsumption: {self.always_check_subsumption}') if self.always_check_subsumption: + print(f'checking subsumption {self.node_id}') csubst = self._check_subsume() if csubst is not None or self.is_terminal: return APRProofSubsumeResult(csubst=csubst, node_id=self.node_id) From 481d2716d50e4c13b6fc0329da7c88f97c1d2eb3 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 15 Feb 2024 16:43:19 -0600 Subject: [PATCH 04/13] Fix subst not being set --- src/pyk/proof/equality.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/proof/equality.py b/src/pyk/proof/equality.py index 2ccdbf9c4..184f2583c 100644 --- a/src/pyk/proof/equality.py +++ b/src/pyk/proof/equality.py @@ -371,7 +371,7 @@ def exec(self) -> StepResult: _LOGGER.info(f'Simplified antecedent: {self.kcfg_explore.kprint.pretty_print(simplified_antecedent)}') _LOGGER.info(f'Simplified consequent: {self.kcfg_explore.kprint.pretty_print(simplified_consequent)}') - csubst: CSubst + csubst: CSubst | None = None if is_bottom(simplified_antecedent): _LOGGER.warning(f'Antecedent of implication (proof constraints) simplifies to #Bottom {self.proof_id}') From 4f0878718af15f54da34900267ca18051a0be94f Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 16 Feb 2024 12:52:03 -0600 Subject: [PATCH 05/13] Fix max_iteration and fail_fast only executing between step groups --- src/pyk/proof/proof.py | 17 ++++++----------- src/pyk/proof/reachability.py | 9 ++++++--- src/tests/integration/proof/test_imp.py | 6 ++++++ 3 files changed, 18 insertions(+), 14 deletions(-) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index 1b554b927..bada12edd 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -314,19 +314,14 @@ def commit(self, result: StepResult) -> None: def advance_proof(self, max_iterations: int | None = None, fail_fast: bool = False) -> None: iterations = 0 while self.proof.can_progress: - if fail_fast and self.proof.failed: - _LOGGER.warning(f'Terminating proof early because fail_fast is set: {self.proof.id}') - return - if max_iterations is not None and max_iterations <= iterations: - return - iterations += 1 steps = self.get_steps() for step in steps: - print(f'b: {self.proof.can_progress}') + iterations += 1 result = step.exec() - print(f'c: {self.proof.can_progress}') self.commit(result) - print(f'd: {self.proof.can_progress}') - print(f'a: {self.proof.can_progress}') + if fail_fast and self.proof.failed: + _LOGGER.warning(f'Terminating proof early because fail_fast is set: {self.proof.id}') + return + if max_iterations is not None and max_iterations <= iterations: + return self.proof.write_proof_data() - print(f'abc: {self.proof.can_progress}') diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 9891f891c..118be7bcb 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -9,7 +9,7 @@ from pyk.kore.rpc import LogEntry -from .show import KCFGShow, NodePrinter +from .show import KCFGShow, NodePrinter, APRProofNodePrinter from ..kast.inner import KInner, Subst from ..kast.manip import flatten_label, ml_pred_to_bool from ..kast.outer import KFlatModule, KImport, KRule @@ -761,6 +761,9 @@ def commit(self, result: StepResult) -> None: if self.proof.failed: self.proof.failure_info = self.failure_info() + show = KCFGShow(self.kcfg_explore.kprint, node_printer=APRProofNodePrinter(self.proof, self.kcfg_explore.kprint, full_printer=True)) + print('\n+'.join(show.pretty(self.proof.kcfg))) + self._check_all_terminals() for node in self.proof.terminal: @@ -775,8 +778,8 @@ def commit(self, result: StepResult) -> None: print(f'pending: {self.proof.pending}') print(f'can_progress: {self.proof.can_progress}') - show = KCFGShow(self.kcfg_explore.kprint, node_printer=NodePrinter(self.kcfg_explore.kprint, full_printer=True)) - print('\n'.join(show.pretty(self.proof.kcfg))) + show = KCFGShow(self.kcfg_explore.kprint, node_printer=APRProofNodePrinter(self.proof, self.kcfg_explore.kprint, full_printer=True)) + print('\n-'.join(show.pretty(self.proof.kcfg))) def failure_info(self) -> APRFailureInfo: return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info) diff --git a/src/tests/integration/proof/test_imp.py b/src/tests/integration/proof/test_imp.py index ced4e1be7..3effab3ea 100644 --- a/src/tests/integration/proof/test_imp.py +++ b/src/tests/integration/proof/test_imp.py @@ -1120,6 +1120,12 @@ def test_fail_fast( prover = APRProver(proof, kcfg_explore=kcfg_explore) prover.advance_proof(fail_fast=True) +# kcfg_show = KCFGShow( +# kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True) +# ) +# cfg_lines = kcfg_show.show(proof.kcfg) +# _LOGGER.info('\n'.join(cfg_lines)) + # First branch will be reached first and terminate the proof, leaving the second long branch pending (fail_fast=True) assert len(proof.kcfg.leaves) == 3 assert len(proof.pending) == 1 From ec0c7ae0b5bdaa721db081e5d1e2af73fd045bb2 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 16 Feb 2024 12:53:26 -0600 Subject: [PATCH 06/13] Clean up --- src/pyk/proof/reachability.py | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 118be7bcb..9d8beca46 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -739,7 +739,6 @@ def get_steps(self) -> Iterable[APRProofStep]: terminal_rules=self.terminal_rules, ) ) - print(steps) return steps def commit(self, result: StepResult) -> None: @@ -761,9 +760,6 @@ def commit(self, result: StepResult) -> None: if self.proof.failed: self.proof.failure_info = self.failure_info() - show = KCFGShow(self.kcfg_explore.kprint, node_printer=APRProofNodePrinter(self.proof, self.kcfg_explore.kprint, full_printer=True)) - print('\n+'.join(show.pretty(self.proof.kcfg))) - self._check_all_terminals() for node in self.proof.terminal: @@ -775,12 +771,6 @@ def commit(self, result: StepResult) -> None: self._checked_for_subsumption.add(node.id) self._check_subsume(node) - print(f'pending: {self.proof.pending}') - print(f'can_progress: {self.proof.can_progress}') - - show = KCFGShow(self.kcfg_explore.kprint, node_printer=APRProofNodePrinter(self.proof, self.kcfg_explore.kprint, full_printer=True)) - print('\n-'.join(show.pretty(self.proof.kcfg))) - def failure_info(self) -> APRFailureInfo: return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info) @@ -838,12 +828,8 @@ def _check_subsume(self) -> CSubst | None: return self.kcfg_explore.cterm_implies(self.cterm, self.target_cterm) def exec(self) -> APRProofResult: - print(f'is_terminal: {self.is_terminal}') - print(f'target_is_terminal: {self.target_is_terminal}') if self.is_terminal or not self.target_is_terminal: - print(f'always_check_subsumption: {self.always_check_subsumption}') if self.always_check_subsumption: - print(f'checking subsumption {self.node_id}') csubst = self._check_subsume() if csubst is not None or self.is_terminal: return APRProofSubsumeResult(csubst=csubst, node_id=self.node_id) From 9626c12b29b9de52c70ae3ef5baffb1b550851ac Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 16 Feb 2024 12:54:17 -0600 Subject: [PATCH 07/13] Clean up --- src/tests/integration/proof/test_imp.py | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/tests/integration/proof/test_imp.py b/src/tests/integration/proof/test_imp.py index 3effab3ea..ced4e1be7 100644 --- a/src/tests/integration/proof/test_imp.py +++ b/src/tests/integration/proof/test_imp.py @@ -1120,12 +1120,6 @@ def test_fail_fast( prover = APRProver(proof, kcfg_explore=kcfg_explore) prover.advance_proof(fail_fast=True) -# kcfg_show = KCFGShow( -# kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True) -# ) -# cfg_lines = kcfg_show.show(proof.kcfg) -# _LOGGER.info('\n'.join(cfg_lines)) - # First branch will be reached first and terminate the proof, leaving the second long branch pending (fail_fast=True) assert len(proof.kcfg.leaves) == 3 assert len(proof.pending) == 1 From 0f6258a30342f3c21f66ac2eb0ba2c6d5e77a007 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 16 Feb 2024 12:55:17 -0600 Subject: [PATCH 08/13] Clean up --- src/pyk/proof/reachability.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 9d8beca46..0681f5dc5 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -9,7 +9,6 @@ from pyk.kore.rpc import LogEntry -from .show import KCFGShow, NodePrinter, APRProofNodePrinter from ..kast.inner import KInner, Subst from ..kast.manip import flatten_label, ml_pred_to_bool from ..kast.outer import KFlatModule, KImport, KRule @@ -689,7 +688,6 @@ def advance_pending_node( ) def get_steps(self) -> Iterable[APRProofStep]: - if not self.proof.pending: return [] steps = [] From 883fbc2956cf70736a8512fe0078c5e75e871637 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 16 Feb 2024 18:56:18 +0000 Subject: [PATCH 09/13] Set Version: 0.1.630 --- docs/conf.py | 4 ++-- package/version | 2 +- pyproject.toml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/conf.py b/docs/conf.py index b570868e2..7b12a9a5b 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.629' -release = '0.1.629' +version = '0.1.630' +release = '0.1.630' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index 3cc33027a..28e26276b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.629 +0.1.630 diff --git a/pyproject.toml b/pyproject.toml index c5261f2f0..067cdbd48 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.629" +version = "0.1.630" description = "" authors = [ "Runtime Verification, Inc. ", From e445d451b661b023ca7bd13369ccb5aabd3b8c5e Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 16 Feb 2024 15:17:12 -0600 Subject: [PATCH 10/13] Fix proof data not being writen and failure info not being saved at the proper time --- src/pyk/proof/proof.py | 2 +- src/pyk/proof/reachability.py | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index bada12edd..c57009657 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -324,4 +324,4 @@ def advance_proof(self, max_iterations: int | None = None, fail_fast: bool = Fal return if max_iterations is not None and max_iterations <= iterations: return - self.proof.write_proof_data() + self.proof.write_proof_data() diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 0681f5dc5..e3e82f12c 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -755,9 +755,6 @@ def commit(self, result: StepResult) -> None: else: raise ValueError('Incorrect result type') - if self.proof.failed: - self.proof.failure_info = self.failure_info() - self._check_all_terminals() for node in self.proof.terminal: @@ -769,6 +766,9 @@ def commit(self, result: StepResult) -> None: self._checked_for_subsumption.add(node.id) self._check_subsume(node) + if self.proof.failed: + self.proof.failure_info = self.failure_info() + def failure_info(self) -> APRFailureInfo: return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info) From 4325aadaf56882d2183894932c7543825198302e Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 16 Feb 2024 17:17:31 -0600 Subject: [PATCH 11/13] Fix write_proof not being called at the correct time --- src/pyk/proof/proof.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index c57009657..84e6bfa40 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -319,9 +319,9 @@ def advance_proof(self, max_iterations: int | None = None, fail_fast: bool = Fal iterations += 1 result = step.exec() self.commit(result) + self.proof.write_proof_data() if fail_fast and self.proof.failed: _LOGGER.warning(f'Terminating proof early because fail_fast is set: {self.proof.id}') return if max_iterations is not None and max_iterations <= iterations: return - self.proof.write_proof_data() From 4b7443920ddb89e52bcd83bf03894461cec9eb62 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 16 Feb 2024 23:32:13 +0000 Subject: [PATCH 12/13] Set Version: 0.1.632 --- docs/conf.py | 4 ++-- package/version | 2 +- pyproject.toml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/conf.py b/docs/conf.py index d6b1e5ef3..c068c61aa 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.631' -release = '0.1.631' +version = '0.1.632' +release = '0.1.632' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index 6c3237570..05fafe81e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.631 +0.1.632 diff --git a/pyproject.toml b/pyproject.toml index 04a2b81e1..03e9dc2b2 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.631" +version = "0.1.632" description = "" authors = [ "Runtime Verification, Inc. ", From 2b5ee7399c7db57f6e1dc0b8941113691a6a061e Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 19 Feb 2024 20:48:23 -0600 Subject: [PATCH 13/13] Start moving commit and get_steps to proof --- src/pyk/proof/implies.py | 84 +++---- src/pyk/proof/proof.py | 28 ++- src/pyk/proof/reachability.py | 451 ++++++++++++++++++---------------- 3 files changed, 298 insertions(+), 265 deletions(-) diff --git a/src/pyk/proof/implies.py b/src/pyk/proof/implies.py index d0a9d0413..122554338 100644 --- a/src/pyk/proof/implies.py +++ b/src/pyk/proof/implies.py @@ -66,6 +66,32 @@ def status(self) -> ProofStatus: else: return ProofStatus.PASSED + def get_steps(self) -> Iterable[ProofStep]: + proof_type = type(self).__name__ + _LOGGER.info(f'Attempting {proof_type} {self.id}') + + if self.status is not ProofStatus.PENDING: + _LOGGER.info(f'{proof_type} finished {self.id}: {self.status}') + return [] + return [ + ImpliesProofStep( + antecedent=self.antecedent, + consequent=self.consequent, + proof_id=self.id, + bind_universally=self.bind_universally, + ) + ] + + def commit(self, result: StepResult) -> None: + proof_type = type(self).__name__ + if isinstance(result, ImpliesProofResult): + self.csubst = result.csubst + self.simplified_antecedent = result.simplified_antecedent + self.simplified_consequent = result.simplified_consequent + _LOGGER.info(f'{proof_type} finished {self.id}: {self.status}') + else: + raise ValueError('Incorrect result type') + @property def can_progress(self) -> bool: return self.simplified_antecedent is None or self.simplified_consequent is None @@ -381,28 +407,37 @@ class ImpliesProofResult(StepResult): @dataclass class ImpliesProofStep(ProofStep): - kcfg_explore: KCFGExplore antecedent: KInner consequent: KInner bind_universally: bool proof_id: str - def exec(self) -> StepResult: + +class ImpliesProver(Prover): + proof: ImpliesProof + + def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore): + super().__init__(kcfg_explore) + self.proof = proof + + def step_proof(self, step: ProofStep) -> StepResult: + assert isinstance(step, ImpliesProofStep) + # to prove the equality, we check the implication of the form `constraints #Implies LHS #Equals RHS`, i.e. # "LHS equals RHS under these constraints" - simplified_antecedent, _ = self.kcfg_explore.kast_simplify(self.antecedent) - simplified_consequent, _ = self.kcfg_explore.kast_simplify(self.consequent) + simplified_antecedent, _ = self.kcfg_explore.kast_simplify(step.antecedent) + simplified_consequent, _ = self.kcfg_explore.kast_simplify(step.consequent) _LOGGER.info(f'Simplified antecedent: {self.kcfg_explore.kprint.pretty_print(simplified_antecedent)}') _LOGGER.info(f'Simplified consequent: {self.kcfg_explore.kprint.pretty_print(simplified_consequent)}') csubst: CSubst | None = None if is_bottom(simplified_antecedent): - _LOGGER.warning(f'Antecedent of implication (proof constraints) simplifies to #Bottom {self.proof_id}') + _LOGGER.warning(f'Antecedent of implication (proof constraints) simplifies to #Bottom {step.proof_id}') csubst = CSubst(Subst({}), ()) elif is_top(simplified_consequent): - _LOGGER.warning(f'Consequent of implication (proof equality) simplifies to #Top {self.proof_id}') + _LOGGER.warning(f'Consequent of implication (proof equality) simplifies to #Top {step.proof_id}') csubst = CSubst(Subst({}), ()) else: @@ -410,7 +445,7 @@ def exec(self) -> StepResult: implies_result = self.kcfg_explore.cterm_implies( antecedent=CTerm(config=dummy_config, constraints=[simplified_antecedent]), consequent=CTerm(config=dummy_config, constraints=[simplified_consequent]), - bind_universally=self.bind_universally, + bind_universally=step.bind_universally, ) if implies_result is not None: csubst = implies_result @@ -418,38 +453,3 @@ def exec(self) -> StepResult: return ImpliesProofResult( csubst=csubst, simplified_antecedent=simplified_antecedent, simplified_consequent=simplified_consequent ) - - -class ImpliesProver(Prover): - proof: ImpliesProof - - def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore): - super().__init__(kcfg_explore) - self.proof = proof - - def get_steps(self) -> Iterable[ProofStep]: - proof_type = type(self.proof).__name__ - _LOGGER.info(f'Attempting {proof_type} {self.proof.id}') - - if self.proof.status is not ProofStatus.PENDING: - _LOGGER.info(f'{proof_type} finished {self.proof.id}: {self.proof.status}') - return [] - return [ - ImpliesProofStep( - antecedent=self.proof.antecedent, - consequent=self.proof.consequent, - kcfg_explore=self.kcfg_explore, - proof_id=self.proof.id, - bind_universally=self.proof.bind_universally, - ) - ] - - def commit(self, result: StepResult) -> None: - proof_type = type(self.proof).__name__ - if isinstance(result, ImpliesProofResult): - self.proof.csubst = result.csubst - self.proof.simplified_antecedent = result.simplified_antecedent - self.proof.simplified_consequent = result.simplified_consequent - _LOGGER.info(f'{proof_type} finished {self.proof.id}: {self.proof.status}') - else: - raise ValueError('Incorrect result type') diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index 5f51a9495..66cf3e91f 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -36,6 +36,14 @@ class Proof(ABC): _subproofs: dict[str, Proof] admitted: bool + @abstractmethod + def get_steps(self) -> Iterable[ProofStep]: + ... + + @abstractmethod + def commit(self, result: StepResult) -> None: + ... + @property def proof_subdir(self) -> Path | None: if self.proof_dir is None: @@ -291,34 +299,28 @@ class StepResult: class ProofStep: - @abstractmethod - def exec(self) -> StepResult: - ... + ... class Prover: kcfg_explore: KCFGExplore proof: Proof - def __init__(self, kcfg_explore: KCFGExplore): - self.kcfg_explore = kcfg_explore - @abstractmethod - def get_steps(self) -> Iterable[ProofStep]: + def step_proof(self, step: ProofStep) -> StepResult: ... - @abstractmethod - def commit(self, result: StepResult) -> None: - ... + def __init__(self, kcfg_explore: KCFGExplore): + self.kcfg_explore = kcfg_explore def advance_proof(self, max_iterations: int | None = None, fail_fast: bool = False) -> None: iterations = 0 while self.proof.can_progress: - steps = self.get_steps() + steps = self.proof.get_steps() for step in steps: iterations += 1 - result = step.exec() - self.commit(result) + result = self.step_proof(step) + self.proof.commit(result) self.proof.write_proof_data() if fail_fast and self.proof.failed: _LOGGER.warning(f'Terminating proof early because fail_fast is set: {self.proof.id}') diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index bd4bcf6f5..9a75104f1 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -46,6 +46,7 @@ class APRProof(Proof, KCFGExploration): to specify an optional loop iteration bound for each loop in execution. """ + kcfg_explore: KCFGExplore node_refutations: dict[int, RefutationProof] # TODO _node_refutatations init: int target: int @@ -54,11 +55,16 @@ class APRProof(Proof, KCFGExploration): logs: dict[int, tuple[LogEntry, ...]] circularity: bool failure_info: APRFailureInfo | None + _checked_for_bounded: set[int] + _checked_for_terminal: set[int] + _checked_for_subsumption: set[int] + fast_check_subsumption: bool def __init__( self, id: str, kcfg: KCFG, + kcfg_explore: KCFGExplore, terminal: Iterable[int], init: NodeIdLike, target: NodeIdLike, @@ -70,10 +76,12 @@ def __init__( subproof_ids: Iterable[str] = (), circularity: bool = False, admitted: bool = False, + fast_check_subsumption: bool = False, ): Proof.__init__(self, id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted) KCFGExploration.__init__(self, kcfg, terminal) + self.kcfg_explore = kcfg_explore self.failure_info = None self.init = kcfg._resolve(init) self.target = kcfg._resolve(target) @@ -83,6 +91,11 @@ def __init__( self.circularity = circularity self.node_refutations = {} self.kcfg.cfg_dir = self.proof_subdir / 'kcfg' if self.proof_subdir else None + self.fast_check_subsumption = fast_check_subsumption + + self._checked_for_bounded = set() + self._checked_for_terminal = set() + self._checked_for_subsumption = set() if self.proof_dir is not None and self.proof_subdir is not None: ensure_dir_path(self.proof_dir) @@ -101,10 +114,122 @@ def __init__( assert type(subproof) is RefutationProof self.node_refutations[node_id] = subproof + + def nonzero_depth(self, node: KCFG.Node) -> bool: + return not self.kcfg.zero_depth_between(self.init, node.id) + + def _may_subsume(self, node: KCFG.Node) -> bool: + node_k_cell = node.cterm.try_cell('K_CELL') + target_k_cell = self.kcfg.node(self.target).cterm.try_cell('K_CELL') + if node_k_cell and target_k_cell and not target_k_cell.match(node_k_cell): + return False + return True + + def _check_terminal(self, node: KCFG.Node) -> None: + if node.id not in self._checked_for_terminal: + _LOGGER.info(f'Checking terminal: {node.id}') + self._checked_for_terminal.add(node.id) + if self.kcfg_explore.kcfg_semantics.is_terminal(node.cterm): + _LOGGER.info(f'Terminal node: {node.id}.') + self._terminal.add(node.id) + elif self.fast_check_subsumption and self._may_subsume(node): + _LOGGER.info(f'Marking node as terminal because of fast may subsume check {self.id}: {node.id}') + self._terminal.add(node.id) + + def _check_all_terminals(self) -> None: + for node in self.kcfg.nodes: + self._check_terminal(node) + + def get_steps(self) -> Iterable[APRProofStep]: + if not self.pending: + return [] + steps = [] + target_node = self.kcfg.node(self.target) + for curr_node in self.pending: + if self.bmc_depth is not None and curr_node.id not in self._checked_for_bounded: + _LOGGER.info(f'Checking bmc depth for node {self.id}: {curr_node.id}') + self._checked_for_bounded.add(curr_node.id) + _prior_loops = [ + succ.source.id + for succ in self.shortest_path_to(curr_node.id) + if self.kcfg_explore.kcfg_semantics.same_loop(succ.source.cterm, curr_node.cterm) + ] + prior_loops: list[NodeIdLike] = [] + for _pl in _prior_loops: + if not ( + self.kcfg.zero_depth_between(_pl, curr_node.id) + or any(self.kcfg.zero_depth_between(_pl, pl) for pl in prior_loops) + ): + prior_loops.append(_pl) + _LOGGER.info(f'Prior loop heads for node {self.id}: {(curr_node.id, prior_loops)}') + if len(prior_loops) > self.bmc_depth: + _LOGGER.warning(f'Bounded node {self.id}: {curr_node.id} at bmc depth {self.bmc_depth}') + self.add_bounded(curr_node.id) + continue + steps.append( + APRProofStep( + bmc_depth=self.bmc_depth, + checked_for_bounded=self._checked_for_bounded, + cterm=curr_node.cterm, + is_terminal=self.kcfg_explore.kcfg_semantics.is_terminal(curr_node.cterm), + kcfg_explore=self.kcfg_explore, + module_name=( + self.circularities_module_name + if self.nonzero_depth(curr_node) + else self.dependencies_module_name + ), + node_id=curr_node.id, + proof_id=self.id, + target_cterm=target_node.cterm, + target_is_terminal=self.target in self._terminal, + target_node_id=target_node.id, + ) + ) + return steps + + def commit(self, result: StepResult) -> None: + if isinstance(result, APRProofExtendResult): + self.kcfg_explore.extend_kcfg( + result.extend_result, self.kcfg, self.kcfg.node(result.node_id), self.logs + ) + elif isinstance(result, APRProofSubsumeResult): + if result.csubst is None: + self._terminal.add(result.node_id) + else: + self.kcfg.create_cover(result.node_id, self.target, csubst=result.csubst) + _LOGGER.info( + f'Subsumed into target node {self.id}: {shorten_hashes((result.node_id, self.target))}' + ) + else: + raise ValueError('Incorrect result type') + + self._check_all_terminals() + + for node in self.terminal: + if ( + not node.id in self._checked_for_subsumption + and self.kcfg.is_leaf(node.id) + and not self.is_target(node.id) + ): + self._checked_for_subsumption.add(node.id) + self._check_subsume(node) + + if self.failed: + self.failure_info = self.failure_info() + + @property def module_name(self) -> str: return self._make_module_name(self.id) + @property + def circularities_module_name(self) -> str: + return self.module_name + '-CIRCULARITIES-MODULE' + + @property + def dependencies_module_name(self) -> str: + return self.module_name + '-DEPENDS-MODULE' + @property def pending(self) -> list[KCFG.Node]: return [node for node in self.explorable if self.is_pending(node.id)] @@ -540,10 +665,6 @@ class APRProver(Prover): always_check_subsumption: bool fast_check_subsumption: bool - _checked_for_terminal: set[int] - _checked_for_subsumption: set[int] - _checked_for_bounded: set[int] - def __init__( self, proof: APRProof, @@ -591,177 +712,92 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike _inject_module(self.dependencies_module_name, self.main_module_name, dependencies_as_rules) _inject_module(self.circularities_module_name, self.dependencies_module_name, [circularity_rule]) - self._checked_for_terminal = set() - self._checked_for_subsumption = set() - self._checked_for_bounded = set() - self._check_all_terminals() - - def nonzero_depth(self, node: KCFG.Node) -> bool: - return not self.proof.kcfg.zero_depth_between(self.proof.init, node.id) - - def _check_terminal(self, node: KCFG.Node) -> None: - if node.id not in self._checked_for_terminal: - _LOGGER.info(f'Checking terminal: {node.id}') - self._checked_for_terminal.add(node.id) - if self.kcfg_explore.kcfg_semantics.is_terminal(node.cterm): - _LOGGER.info(f'Terminal node: {node.id}.') - self.proof._terminal.add(node.id) - elif self.fast_check_subsumption and self._may_subsume(node): - _LOGGER.info(f'Marking node as terminal because of fast may subsume check {self.proof.id}: {node.id}') - self.proof._terminal.add(node.id) - - def _check_all_terminals(self) -> None: - for node in self.proof.kcfg.nodes: - self._check_terminal(node) - - def _may_subsume(self, node: KCFG.Node) -> bool: - node_k_cell = node.cterm.try_cell('K_CELL') - target_k_cell = self.proof.kcfg.node(self.proof.target).cterm.try_cell('K_CELL') - if node_k_cell and target_k_cell and not target_k_cell.match(node_k_cell): - return False - return True - - def _check_subsume(self, node: KCFG.Node) -> bool: - _LOGGER.info( - f'Checking subsumption into target state {self.proof.id}: {shorten_hashes((node.id, self.proof.target))}' - ) - if self.fast_check_subsumption and not self._may_subsume(node): - _LOGGER.info( - f'Skipping full subsumption check because of fast may subsume check {self.proof.id}: {node.id}' - ) - return False - csubst = self.kcfg_explore.cterm_implies(node.cterm, self.proof.kcfg.node(self.proof.target).cterm) - if csubst is not None: - self.proof.kcfg.create_cover(node.id, self.proof.target, csubst=csubst) - _LOGGER.info(f'Subsumed into target node {self.proof.id}: {shorten_hashes((node.id, self.proof.target))}') - return True - else: - return False + self.proof._check_all_terminals() + +# def _may_subsume(self, node: KCFG.Node) -> bool: +# node_k_cell = node.cterm.try_cell('K_CELL') +# target_k_cell = self.proof.kcfg.node(self.proof.target).cterm.try_cell('K_CELL') +# if node_k_cell and target_k_cell and not target_k_cell.match(node_k_cell): +# return False +# return True + +# def _check_subsume(self, node: KCFG.Node) -> bool: +# _LOGGER.info( +# f'Checking subsumption into target state {self.proof.id}: {shorten_hashes((node.id, self.proof.target))}' +# ) +# if self.fast_check_subsumption and not self._may_subsume(node): +# _LOGGER.info( +# f'Skipping full subsumption check because of fast may subsume check {self.proof.id}: {node.id}' +# ) +# return False +# csubst = self.kcfg_explore.cterm_implies(node.cterm, self.proof.kcfg.node(self.proof.target).cterm) +# if csubst is not None: +# self.proof.kcfg.create_cover(node.id, self.proof.target, csubst=csubst) +# _LOGGER.info(f'Subsumed into target node {self.proof.id}: {shorten_hashes((node.id, self.proof.target))}') +# return True +# else: +# return False + +# def advance_pending_node( +# self, +# node: KCFG.Node, +# execute_depth: int | None = None, +# cut_point_rules: Iterable[str] = (), +# terminal_rules: Iterable[str] = (), +# ) -> None: +# if self.proof.bmc_depth is not None and node.id not in self._checked_for_bounded: +# _LOGGER.info(f'Checking bmc depth for node {self.proof.id}: {node.id}') +# self._checked_for_bounded.add(node.id) +# _prior_loops = [ +# succ.source.id +# for succ in self.proof.shortest_path_to(node.id) +# if self.kcfg_explore.kcfg_semantics.same_loop(succ.source.cterm, node.cterm) +# ] +# prior_loops: list[NodeIdLike] = [] +# for _pl in _prior_loops: +# if not ( +# self.proof.kcfg.zero_depth_between(_pl, node.id) +# or any(self.proof.kcfg.zero_depth_between(_pl, pl) for pl in prior_loops) +# ): +# prior_loops.append(_pl) +# _LOGGER.info(f'Prior loop heads for node {self.proof.id}: {(node.id, prior_loops)}') +# if len(prior_loops) > self.proof.bmc_depth: +# _LOGGER.warning(f'Bounded node {self.proof.id}: {node.id} at bmc depth {self.proof.bmc_depth}') +# self.proof.add_bounded(node.id) +# return +# +# if self.proof.target not in self.proof._terminal: +# if self.always_check_subsumption and self._check_subsume(node): +# return +# +# module_name = self.circularities_module_name if self.nonzero_depth(node) else self.dependencies_module_name +# self.kcfg_explore.extend( +# self.proof, +# node, +# self.proof.logs, +# execute_depth=execute_depth, +# cut_point_rules=cut_point_rules, +# terminal_rules=terminal_rules, +# module_name=module_name, +# ) + + + def step_proof(self, step: ProofStep) -> APRProofResult: + if self.is_terminal or not self.target_is_terminal: + if self.always_check_subsumption: + csubst = self._check_subsume() + if csubst is not None or self.is_terminal: + return APRProofSubsumeResult(csubst=csubst, node_id=self.node_id) - def advance_pending_node( - self, - node: KCFG.Node, - execute_depth: int | None = None, - cut_point_rules: Iterable[str] = (), - terminal_rules: Iterable[str] = (), - ) -> None: - if self.proof.bmc_depth is not None and node.id not in self._checked_for_bounded: - _LOGGER.info(f'Checking bmc depth for node {self.proof.id}: {node.id}') - self._checked_for_bounded.add(node.id) - _prior_loops = [ - succ.source.id - for succ in self.proof.shortest_path_to(node.id) - if self.kcfg_explore.kcfg_semantics.same_loop(succ.source.cterm, node.cterm) - ] - prior_loops: list[NodeIdLike] = [] - for _pl in _prior_loops: - if not ( - self.proof.kcfg.zero_depth_between(_pl, node.id) - or any(self.proof.kcfg.zero_depth_between(_pl, pl) for pl in prior_loops) - ): - prior_loops.append(_pl) - _LOGGER.info(f'Prior loop heads for node {self.proof.id}: {(node.id, prior_loops)}') - if len(prior_loops) > self.proof.bmc_depth: - _LOGGER.warning(f'Bounded node {self.proof.id}: {node.id} at bmc depth {self.proof.bmc_depth}') - self.proof.add_bounded(node.id) - return - - if self.proof.target not in self.proof._terminal: - if self.always_check_subsumption and self._check_subsume(node): - return - - module_name = self.circularities_module_name if self.nonzero_depth(node) else self.dependencies_module_name - self.kcfg_explore.extend( - self.proof, - node, - self.proof.logs, - execute_depth=execute_depth, - cut_point_rules=cut_point_rules, - terminal_rules=terminal_rules, - module_name=module_name, + extend_result = self.kcfg_explore.extend_cterm( + self.cterm, + execute_depth=self.execute_depth, + cut_point_rules=self.cut_point_rules, + terminal_rules=self.terminal_rules, + module_name=self.module_name, ) + return APRProofExtendResult(node_id=self.node_id, extend_result=extend_result) - def get_steps(self) -> Iterable[APRProofStep]: - if not self.proof.pending: - return [] - steps = [] - target_node = self.proof.kcfg.node(self.proof.target) - for curr_node in self.proof.pending: - if self.proof.bmc_depth is not None and curr_node.id not in self._checked_for_bounded: - _LOGGER.info(f'Checking bmc depth for node {self.proof.id}: {curr_node.id}') - self._checked_for_bounded.add(curr_node.id) - _prior_loops = [ - succ.source.id - for succ in self.proof.shortest_path_to(curr_node.id) - if self.kcfg_explore.kcfg_semantics.same_loop(succ.source.cterm, curr_node.cterm) - ] - prior_loops: list[NodeIdLike] = [] - for _pl in _prior_loops: - if not ( - self.proof.kcfg.zero_depth_between(_pl, curr_node.id) - or any(self.proof.kcfg.zero_depth_between(_pl, pl) for pl in prior_loops) - ): - prior_loops.append(_pl) - _LOGGER.info(f'Prior loop heads for node {self.proof.id}: {(curr_node.id, prior_loops)}') - if len(prior_loops) > self.proof.bmc_depth: - _LOGGER.warning(f'Bounded node {self.proof.id}: {curr_node.id} at bmc depth {self.proof.bmc_depth}') - self.proof.add_bounded(curr_node.id) - continue - steps.append( - APRProofStep( - always_check_subsumption=self.always_check_subsumption, - bmc_depth=self.proof.bmc_depth, - checked_for_bounded=self._checked_for_bounded, - cterm=curr_node.cterm, - cut_point_rules=self.cut_point_rules, - execute_depth=self.execute_depth, - fast_check_subsumption=self.fast_check_subsumption, - is_terminal=self.kcfg_explore.kcfg_semantics.is_terminal(curr_node.cterm), - kcfg_explore=self.kcfg_explore, - module_name=( - self.circularities_module_name - if self.nonzero_depth(curr_node) - else self.dependencies_module_name - ), - node_id=curr_node.id, - proof_id=self.proof.id, - target_cterm=target_node.cterm, - target_is_terminal=self.proof.target in self.proof._terminal, - target_node_id=target_node.id, - terminal_rules=self.terminal_rules, - ) - ) - return steps - - def commit(self, result: StepResult) -> None: - if isinstance(result, APRProofExtendResult): - self.kcfg_explore.extend_kcfg( - result.extend_result, self.proof.kcfg, self.proof.kcfg.node(result.node_id), self.proof.logs - ) - elif isinstance(result, APRProofSubsumeResult): - if result.csubst is None: - self.proof._terminal.add(result.node_id) - else: - self.proof.kcfg.create_cover(result.node_id, self.proof.target, csubst=result.csubst) - _LOGGER.info( - f'Subsumed into target node {self.proof.id}: {shorten_hashes((result.node_id, self.proof.target))}' - ) - else: - raise ValueError('Incorrect result type') - - self._check_all_terminals() - - for node in self.proof.terminal: - if ( - not node.id in self._checked_for_subsumption - and self.proof.kcfg.is_leaf(node.id) - and not self.proof.is_target(node.id) - ): - self._checked_for_subsumption.add(node.id) - self._check_subsume(node) - - if self.proof.failed: - self.proof.failure_info = self.failure_info() def failure_info(self) -> APRFailureInfo: return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info) @@ -788,52 +824,47 @@ class APRProofStep(ProofStep): node_id: int target_node_id: int proof_id: str - fast_check_subsumption: bool cterm: CTerm target_cterm: CTerm kcfg_explore: KCFGExplore checked_for_bounded: Iterable[int] target_is_terminal: bool - always_check_subsumption: bool module_name: str - cut_point_rules: Iterable[str] - terminal_rules: Iterable[str] - execute_depth: int | None is_terminal: bool - def _may_subsume(self) -> bool: - node_k_cell = self.cterm.try_cell('K_CELL') - target_k_cell = self.target_cterm.try_cell('K_CELL') - if node_k_cell and target_k_cell and not target_k_cell.match(node_k_cell): - return False - return True - - def _check_subsume(self) -> CSubst | None: - _LOGGER.info( - f'Checking subsumption into target state {self.proof_id}: {shorten_hashes((self.node_id, self.target_node_id))}' - ) - if self.fast_check_subsumption and not self._may_subsume(): - _LOGGER.info( - f'Skipping full subsumption check because of fast may subsume check {self.proof_id}: {self.node_id}' - ) - return None - return self.kcfg_explore.cterm_implies(self.cterm, self.target_cterm) - - def exec(self) -> APRProofResult: - if self.is_terminal or not self.target_is_terminal: - if self.always_check_subsumption: - csubst = self._check_subsume() - if csubst is not None or self.is_terminal: - return APRProofSubsumeResult(csubst=csubst, node_id=self.node_id) - - extend_result = self.kcfg_explore.extend_cterm( - self.cterm, - execute_depth=self.execute_depth, - cut_point_rules=self.cut_point_rules, - terminal_rules=self.terminal_rules, - module_name=self.module_name, - ) - return APRProofExtendResult(node_id=self.node_id, extend_result=extend_result) +# def _may_subsume(self) -> bool: +# node_k_cell = self.cterm.try_cell('K_CELL') +# target_k_cell = self.target_cterm.try_cell('K_CELL') +# if node_k_cell and target_k_cell and not target_k_cell.match(node_k_cell): +# return False +# return True +# +# def _check_subsume(self) -> CSubst | None: +# _LOGGER.info( +# f'Checking subsumption into target state {self.proof_id}: {shorten_hashes((self.node_id, self.target_node_id))}' +# ) +# if self.fast_check_subsumption and not self._may_subsume(): +# _LOGGER.info( +# f'Skipping full subsumption check because of fast may subsume check {self.proof_id}: {self.node_id}' +# ) +# return None +# return self.kcfg_explore.cterm_implies(self.cterm, self.target_cterm) +# +# def exec(self) -> APRProofResult: +# if self.is_terminal or not self.target_is_terminal: +# if self.always_check_subsumption: +# csubst = self._check_subsume() +# if csubst is not None or self.is_terminal: +# return APRProofSubsumeResult(csubst=csubst, node_id=self.node_id) +# +# extend_result = self.kcfg_explore.extend_cterm( +# self.cterm, +# execute_depth=self.execute_depth, +# cut_point_rules=self.cut_point_rules, +# terminal_rules=self.terminal_rules, +# module_name=self.module_name, +# ) +# return APRProofExtendResult(node_id=self.node_id, extend_result=extend_result) @dataclass(frozen=True)