From 394c95b174aa16578a9054abc572110f3d0e938b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Thu, 8 Aug 2024 12:18:56 +0200 Subject: [PATCH] Removing minimize_constraints and adding ability to use booster implies (#4577) This PR improves on the handling and use of the `implies` endpoint in the following two ways: - it allows the use of the Booster implies endpoint - it removes constraint minimization, which calls the implies endpoint and was originally designed to streamline the path condition, but in real-world cases only introduced an overhead. --- pyk/src/pyk/cli/pyk.py | 2 + pyk/src/pyk/cterm/symbolic.py | 35 ++---------- pyk/src/pyk/kcfg/explore.py | 8 ++- pyk/src/pyk/kore/rpc.py | 2 + pyk/src/pyk/ktool/prove_rpc.py | 6 +- pyk/src/pyk/proof/implies.py | 5 +- pyk/src/pyk/proof/reachability.py | 15 +++-- .../tests/integration/cterm/test_simple.py | 56 +------------------ pyk/src/tests/unit/kore/test_client.py | 2 +- 9 files changed, 37 insertions(+), 94 deletions(-) diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index 0ee2c775de0..f4a50ce32a9 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -320,6 +320,7 @@ class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): kore_rpc_command: str | Iterable[str] | None max_depth: int | None max_iterations: int | None + assume_defined: bool show_kcfg: bool @staticmethod @@ -331,6 +332,7 @@ def default() -> dict[str, Any]: 'kore_rpc_command': None, 'max_depth': None, 'max_iterations': None, + 'assume_defined': False, 'show_kcfg': False, } diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index bdefcb59f58..fee3e0abb84 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -25,7 +25,7 @@ kore_server, ) from ..prelude.k import GENERATED_TOP_CELL, K_ITEM -from ..prelude.ml import is_top, mlAnd, mlEquals +from ..prelude.ml import is_top, mlEquals if TYPE_CHECKING: from collections.abc import Iterable, Iterator @@ -92,28 +92,6 @@ def kast_to_kore(self, kinner: KInner) -> Pattern: def kore_to_kast(self, pattern: Pattern) -> KInner: return kore_to_kast(self._definition, pattern) - def minimize_constraints(self, constraints: tuple[KInner, ...], path_condition: KInner) -> tuple[KInner, ...]: - """Minimize given branching constraints with respect to a given path condition.""" - # By construction, this function is to be called with at least two sets of constraints - assert len(constraints) >= 2 - # Determine intersection between all returned sets of branching constraints - flattened_default = [flatten_label('#And', c) for c in constraints] - intersection = set.intersection(*(set(cs) for cs in flattened_default)) - # If intersection is empty, there is nothing to be done - if not intersection: - return constraints - # Check if non-empty intersection is entailed by the path condition - dummy_config = self._definition.empty_config(sort=GENERATED_TOP_CELL) - path_condition_cterm = CTerm(dummy_config, constraints=[path_condition]) - intersection_cterm = CTerm(dummy_config, constraints=intersection) - implication_check = self.implies(path_condition_cterm, intersection_cterm, bind_universally=True) - # The intersection is not entailed, there is nothing to be done - if implication_check.csubst is None: - return constraints - # The intersection is entailed and can be filtered out of the branching constraints - else: - return tuple(mlAnd(c for c in cs if c not in intersection) for cs in flattened_default) - def execute( self, cterm: CTerm, @@ -148,11 +126,6 @@ def execute( self.kore_to_kast(not_none(s.rule_predicate)) if s.rule_predicate is not None else None for s in resp_next_states ) - # Branch constraint minimization makes sense only if there is a proper branching - if len(branching_constraints) >= 2 and all(bc is not None for bc in branching_constraints): - branching_constraints = self.minimize_constraints( - tuple(not_none(bc) for bc in branching_constraints), path_condition=mlAnd(cterm.constraints) - ) next_states = tuple( NextState(CTerm.from_kast(self.kore_to_kast(ns.kore)), c) for ns, c in zip(resp_next_states, branching_constraints, strict=True) @@ -219,6 +192,7 @@ def implies( bind_universally: bool = False, failure_reason: bool = False, module_name: str | None = None, + assume_defined: bool = False, ) -> CTermImplies: _LOGGER.debug(f'Checking implication: {antecedent} #Implies {consequent}') _consequent = consequent.kast @@ -235,7 +209,9 @@ def implies( antecedent_kore = self.kast_to_kore(antecedent.kast) consequent_kore = self.kast_to_kore(_consequent) try: - result = self._kore_client.implies(antecedent_kore, consequent_kore, module_name=module_name) + result = self._kore_client.implies( + antecedent_kore, consequent_kore, module_name=module_name, assume_defined=assume_defined + ) except SmtSolverError as err: raise self._smt_solver_error(err) from err @@ -253,6 +229,7 @@ def implies( bind_universally=bind_universally, failure_reason=False, module_name=module_name, + assume_defined=assume_defined, ) config_match = _config_match.csubst if config_match is None: diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 21859b5e02d..69a02c07b0f 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -72,7 +72,9 @@ def _extract_rule_labels(self, _logs: tuple[LogEntry, ...]) -> list[str]: _rule_lines.append(f'{node_log.result.rule_id}:UNKNOWN') return _rule_lines - def implication_failure_reason(self, antecedent: CTerm, consequent: CTerm) -> tuple[bool, str]: + def implication_failure_reason( + self, antecedent: CTerm, consequent: CTerm, assume_defined: bool = False + ) -> tuple[bool, str]: def _is_cell_subst(csubst: KInner) -> bool: if type(csubst) is KApply and csubst.label.name == '_==K_': csubst_arg = csubst.args[0] @@ -91,7 +93,9 @@ def _is_negative_cell_subst(constraint: KInner) -> bool: return True return False - cterm_implies = self.cterm_symbolic.implies(antecedent, consequent, failure_reason=True) + cterm_implies = self.cterm_symbolic.implies( + antecedent, consequent, failure_reason=True, assume_defined=assume_defined + ) if cterm_implies.csubst is not None: return (True, '') diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 4eeac4cf109..93a8c98a9d5 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -1027,12 +1027,14 @@ def implies( consequent: Pattern, *, module_name: str | None = None, + assume_defined: bool = False, ) -> ImpliesResult: params = filter_none( { 'antecedent': self._state(antecedent), 'consequent': self._state(consequent), 'module': module_name, + 'assume-defined': assume_defined, } ) diff --git a/pyk/src/pyk/ktool/prove_rpc.py b/pyk/src/pyk/ktool/prove_rpc.py index 250381d3f54..df948ff1fdd 100644 --- a/pyk/src/pyk/ktool/prove_rpc.py +++ b/pyk/src/pyk/ktool/prove_rpc.py @@ -48,6 +48,7 @@ def prove_rpc(self, options: ProveOptions) -> list[Proof]: return [ self._prove_claim_rpc( claim, + assume_defined=options.assume_defined, max_depth=options.max_depth, save_directory=options.save_directory, max_iterations=options.max_iterations, @@ -58,6 +59,7 @@ def prove_rpc(self, options: ProveOptions) -> list[Proof]: def _prove_claim_rpc( self, claim: KClaim, + assume_defined: bool, max_depth: int | None = None, save_directory: Path | None = None, max_iterations: int | None = None, @@ -85,10 +87,10 @@ def _prove_claim_rpc( with self._explore_context() as kcfg_explore: if is_functional_claim: assert type(proof) is EqualityProof - prover = ImpliesProver(proof, kcfg_explore) + prover = ImpliesProver(proof, kcfg_explore, assume_defined=assume_defined) else: assert type(proof) is APRProof - prover = APRProver(kcfg_explore, execute_depth=max_depth) + prover = APRProver(kcfg_explore, execute_depth=max_depth, assume_defined=assume_defined) prover.advance_proof(proof, max_iterations=max_iterations) if proof.passed: diff --git a/pyk/src/pyk/proof/implies.py b/pyk/src/pyk/proof/implies.py index f6b59603608..e015e11c31f 100644 --- a/pyk/src/pyk/proof/implies.py +++ b/pyk/src/pyk/proof/implies.py @@ -410,13 +410,15 @@ def lines(self) -> list[str]: class ImpliesProver(Prover[ImpliesProof, ImpliesProofStep, ImpliesProofResult]): proof: ImpliesProof kcfg_explore: KCFGExplore + assume_defined: bool def close(self) -> None: self.kcfg_explore.cterm_symbolic._kore_client.close() - def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore): + def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore, assume_defined: bool = False): self.kcfg_explore = kcfg_explore self.proof = proof + self.assume_defined = assume_defined def step_proof(self, step: ImpliesProofStep) -> list[ImpliesProofResult]: proof_type = type(step.proof).__name__ @@ -450,6 +452,7 @@ def step_proof(self, step: ImpliesProofStep) -> list[ImpliesProofResult]: antecedent=CTerm(config=dummy_config, constraints=[simplified_antecedent]), consequent=CTerm(config=dummy_config, constraints=[simplified_consequent]), bind_universally=step.proof.bind_universally, + assume_defined=self.assume_defined, ) result = _result.csubst if result is not None: diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index fab28f6cc60..2a62fe37f5b 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -671,6 +671,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): always_check_subsumption: bool fast_check_subsumption: bool direct_subproof_rules: bool + assume_defined: bool kcfg_explore: KCFGExplore def __init__( @@ -683,6 +684,7 @@ def __init__( always_check_subsumption: bool = True, fast_check_subsumption: bool = False, direct_subproof_rules: bool = False, + assume_defined: bool = False, ) -> None: self.kcfg_explore = kcfg_explore @@ -694,6 +696,7 @@ def __init__( self.always_check_subsumption = always_check_subsumption self.fast_check_subsumption = fast_check_subsumption self.direct_subproof_rules = direct_subproof_rules + self.assume_defined = assume_defined def close(self) -> None: self.kcfg_explore.cterm_symbolic._kore_client.close() @@ -737,7 +740,7 @@ def _check_subsume(self, node: KCFG.Node, target_node: KCFG.Node, proof_id: str) if self.fast_check_subsumption and not self._may_subsume(node, target_node): _LOGGER.info(f'Skipping full subsumption check because of fast may subsume check {proof_id}: {node.id}') return None - _csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, target_cterm) + _csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, target_cterm, assume_defined=self.assume_defined) csubst = _csubst.csubst if csubst is not None: _LOGGER.info(f'Subsumed into target node {proof_id}: {shorten_hashes((node.id, target_node.id))}') @@ -804,7 +807,9 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: ] def failure_info(self, proof: APRProof) -> FailureInfo: - return APRFailureInfo.from_proof(proof, self.kcfg_explore, counterexample_info=self.counterexample_info) + return APRFailureInfo.from_proof( + proof, self.kcfg_explore, counterexample_info=self.counterexample_info, assume_defined=self.assume_defined + ) @dataclass(frozen=True) @@ -871,7 +876,9 @@ def __init__( ) @staticmethod - def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> APRFailureInfo: + def from_proof( + proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False, assume_defined: bool = False + ) -> APRFailureInfo: target = proof.kcfg.node(proof.target) pending_nodes = {node.id for node in proof.pending} failing_nodes = {node.id for node in proof.failing} @@ -881,7 +888,7 @@ def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: for node in proof.failing: node_cterm, _ = kcfg_explore.cterm_symbolic.simplify(node.cterm) target_cterm, _ = kcfg_explore.cterm_symbolic.simplify(target.cterm) - _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) + _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm, assume_defined=assume_defined) path_condition = kcfg_explore.pretty_print(proof.path_constraints(node.id)) failure_reasons[node.id] = reason path_conditions[node.id] = path_condition diff --git a/pyk/src/tests/integration/cterm/test_simple.py b/pyk/src/tests/integration/cterm/test_simple.py index 4c1718eb245..e461bef15ab 100644 --- a/pyk/src/tests/integration/cterm/test_simple.py +++ b/pyk/src/tests/integration/cterm/test_simple.py @@ -7,7 +7,7 @@ from pyk.cterm import CTerm from pyk.kast.inner import KApply, KSequence, KToken, KVariable from pyk.prelude.kint import leInt -from pyk.prelude.ml import mlAnd, mlEqualsTrue, mlTop +from pyk.prelude.ml import mlEqualsTrue, mlTop from pyk.prelude.utils import token from pyk.testing import CTermSymbolicTest, KPrintTest @@ -43,37 +43,6 @@ def le_int(n: int, var: str) -> KInner: return mlEqualsTrue(leInt(token(n), KVariable(var))) -MINIMIZE_CONSTRAINTS_TEST_DATA: Final = ( - ( - 'no-intersection', - [[le_int(0, 'X')], [le_int(0, 'Y')]], - mlTop(), - [[le_int(0, 'X')], [le_int(0, 'Y')]], - ), - ( - 'intersection-not-entailed', - [ - [le_int(0, 'X'), le_int(0, 'Y')], - [le_int(0, 'X'), le_int(0, 'Z')], - ], - mlTop(), - [[le_int(0, 'X'), le_int(0, 'Y')], [le_int(0, 'X'), le_int(0, 'Z')]], - ), - ( - 'intersection-entailed', - [ - [le_int(0, 'X'), le_int(0, 'Y')], - [le_int(0, 'X'), le_int(0, 'Z')], - ], - le_int(10, 'X'), - [ - [le_int(0, 'Y')], - [le_int(0, 'Z')], - ], - ), -) - - class TestSimpleProof(CTermSymbolicTest, KPrintTest): KOMPILE_MAIN_FILE = K_FILES / 'simple-proofs.k' KOMPILE_ARGS = {'syntax_module': 'SIMPLE-PROOFS'} @@ -161,26 +130,3 @@ def test_simplify( # Then assert actual_k == expected_k assert actual_state == expected_state - - @pytest.mark.parametrize( - 'test_id,constraints,pc,expected_minimized_constraints', - MINIMIZE_CONSTRAINTS_TEST_DATA, - ids=[test_id for test_id, *_ in MINIMIZE_CONSTRAINTS_TEST_DATA], - ) - def test_minimize_constraints( - self, - cterm_symbolic: CTermSymbolic, - test_id: str, - constraints: Iterable[Iterable[KInner]], - pc: KInner, - expected_minimized_constraints: Iterable[Iterable[KInner]], - ) -> None: - # Given - _constraints = tuple(mlAnd(cs) for cs in constraints) - _expected_minimized_constraints = tuple(mlAnd(cs) for cs in expected_minimized_constraints) - - # When - _minimized_constraints = cterm_symbolic.minimize_constraints(_constraints, pc) - - # Then - assert _minimized_constraints == _expected_minimized_constraints diff --git a/pyk/src/tests/unit/kore/test_client.py b/pyk/src/tests/unit/kore/test_client.py index 1973e30c8db..8842da2550d 100644 --- a/pyk/src/tests/unit/kore/test_client.py +++ b/pyk/src/tests/unit/kore/test_client.py @@ -177,7 +177,7 @@ def test_execute( ( int_bottom, int_top, - {'antecedent': kore(int_bottom), 'consequent': kore(int_top)}, + {'antecedent': kore(int_bottom), 'consequent': kore(int_top), 'assume-defined': False}, {'valid': True, 'implication': kore(int_top)}, ImpliesResult(True, int_top, None, None, ()), ),