From 94837f7314abef2b1b5f7f7506ae3c314644e3ae Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 11 Dec 2024 14:53:20 +0000 Subject: [PATCH 01/14] KCFG optimizations --- pyk/src/pyk/kcfg/kcfg.py | 21 ++++++++++++++++----- pyk/src/pyk/proof/implies.py | 2 +- pyk/src/pyk/proof/proof.py | 10 +++++++--- pyk/src/pyk/proof/reachability.py | 4 +++- 4 files changed, 27 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 825dd7c3289..a7caef0f001 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -22,7 +22,7 @@ ) from ..kast.outer import KFlatModule from ..prelude.kbool import andBool -from ..utils import ensure_dir_path, not_none +from ..utils import ensure_dir_path, not_none, single if TYPE_CHECKING: from collections.abc import Iterable, Mapping, MutableMapping @@ -557,6 +557,7 @@ def path_length(_path: Iterable[KCFG.Successor]) -> int: def extend( self, extend_result: KCFGExtendResult, + optimize_kcfg: bool, node: KCFG.Node, logs: dict[int, tuple[LogEntry, ...]], ) -> None: @@ -584,10 +585,20 @@ def log(message: str, *, warning: bool = False) -> None: log(f'abstraction node: {node.id}') case Step(cterm, depth, next_node_logs, rule_labels, _): - next_node = self.create_node(cterm) - logs[next_node.id] = next_node_logs - self.create_edge(node.id, next_node.id, depth, rules=rule_labels) - log(f'basic block at depth {depth}: {node.id} --> {next_node.id}') + in_edges = self.edges(target_id=node.id) + if optimize_kcfg and len(in_edges) == 1: + in_edge = single(in_edges) + self.remove_edge(in_edge.source.id, node.id) + self.let_node(node_id=node.id, cterm=cterm) + self.create_edge( + in_edge.source.id, node.id, in_edge.depth + depth, list(in_edge.rules) + rule_labels + ) + log(f'basic block at depth {depth}: node update: {node.id}') + else: + next_node = self.create_node(cterm) + logs[next_node.id] = next_node_logs + self.create_edge(node.id, next_node.id, depth, rules=rule_labels) + log(f'basic block at depth {depth}: {node.id} --> {next_node.id}') case Branch(branches, _): branch_node_ids = self.split_on_constraints(node.id, branches) diff --git a/pyk/src/pyk/proof/implies.py b/pyk/src/pyk/proof/implies.py index e015e11c31f..cddcad30e4c 100644 --- a/pyk/src/pyk/proof/implies.py +++ b/pyk/src/pyk/proof/implies.py @@ -72,7 +72,7 @@ def get_steps(self) -> list[ImpliesProofStep]: return [] return [ImpliesProofStep(self)] - def commit(self, result: ImpliesProofResult) -> None: + def commit(self, optimize_kcfg: bool, result: ImpliesProofResult) -> None: proof_type = type(self).__name__ if isinstance(result, ImpliesProofResult): self.csubst = result.csubst diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 0d1eef04d2e..966cb6bdd78 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -78,7 +78,7 @@ def __init__( ensure_dir_path(self.proof_dir) @abstractmethod - def commit(self, result: SR) -> None: + def commit(self, optimize_kcfg: bool, result: SR) -> None: """Apply the step result of type `SR` to `self`, modifying `self`.""" ... @@ -327,6 +327,7 @@ def parallel_advance_proof( max_workers: int = 1, callback: Callable[[P], None] = (lambda x: None), maintenance_rate: int = 1, + optimize_kcfg: bool = False, ) -> None: """Advance proof with multithreaded strategy. @@ -350,6 +351,7 @@ def parallel_advance_proof( max_workers: Maximum number of worker threads the pool can spawn. callback: Callable to run during proof maintenance, useful for getting real-time information about the proof. maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback). + optimize_kcfg: Optimization of KCFG construction by edge-edge minimization. """ pending: set[Future[Any]] = set() explored: set[PS] = set() @@ -377,7 +379,7 @@ def submit_steps(_steps: Iterable[PS]) -> None: future = done.pop() proof_results = future.result() for result in proof_results: - proof.commit(result) + proof.commit(optimize_kcfg, result) iterations += 1 if iterations % maintenance_rate == 0: proof.write_proof_data() @@ -506,6 +508,7 @@ def advance_proof( fail_fast: bool = False, callback: Callable[[P], None] = (lambda x: None), maintenance_rate: int = 1, + optimize_kcfg: bool = False, ) -> None: """Advance a proof. @@ -518,6 +521,7 @@ def advance_proof( halt execution even if there are still available steps. callback: Callable to run in between each completed step, useful for getting real-time information about the proof. maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback). + optimize_kcfg: Optimization of KCFG construction by edge-edge minimization. """ iterations = 0 _LOGGER.info(f'Initializing proof: {proof.id}') @@ -537,7 +541,7 @@ def advance_proof( iterations += 1 results = self.step_proof(step) for result in results: - proof.commit(result) + proof.commit(optimize_kcfg, result) if iterations % maintenance_rate == 0: proof.write_proof_data() callback(proof) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index d7e706ca939..5f3a15f84d0 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -213,13 +213,14 @@ def get_steps(self) -> list[APRProofStep]: ) return steps - def commit(self, result: APRProofResult) -> None: + def commit(self, optimize_kcfg: bool, result: APRProofResult) -> None: self.prior_loops_cache[result.node_id] = result.prior_loops_cache_update # Result has been cached, use the cache if isinstance(result, APRProofUseCacheResult): assert result.cached_node_id in self._next_steps self.kcfg.extend( extend_result=self._next_steps.pop(result.cached_node_id), + optimize_kcfg=optimize_kcfg, node=self.kcfg.node(result.node_id), logs=self.logs, ) @@ -230,6 +231,7 @@ def commit(self, result: APRProofResult) -> None: self._next_steps[result.node_id] = result.extension_to_cache self.kcfg.extend( extend_result=result.extension_to_apply, + optimize_kcfg=optimize_kcfg, node=self.kcfg.node(result.node_id), logs=self.logs, ) From 35d7bd1a28be42b5fb1a99f288cd8669407a24e7 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 11 Dec 2024 15:23:35 +0000 Subject: [PATCH 02/14] refactoring --- pyk/src/pyk/kcfg/kcfg.py | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index a7caef0f001..e640391ecb3 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -570,6 +570,20 @@ def log(message: str, *, warning: bool = False) -> None: f'Extending current KCFG with the following: {message}{result_info_message}', ) + def optimize_step( + cterm: CTerm, depth: int, next_node_logs: tuple[LogEntry, ...], rule_labels: list[str] + ) -> bool: + in_edges = self.edges(target_id=node.id) + if len(in_edges) == 1: + in_edge = single(in_edges) + self.remove_edge(in_edge.source.id, node.id) + self.let_node(node_id=node.id, cterm=cterm) + self.create_edge(in_edge.source.id, node.id, in_edge.depth + depth, list(in_edge.rules) + rule_labels) + logs[node.id] = logs[node.id] + next_node_logs + log(f'basic block at depth {depth}: node update: {node.id}') + return True + return False + match extend_result: case Vacuous(): self.add_vacuous(node.id) @@ -585,16 +599,7 @@ def log(message: str, *, warning: bool = False) -> None: log(f'abstraction node: {node.id}') case Step(cterm, depth, next_node_logs, rule_labels, _): - in_edges = self.edges(target_id=node.id) - if optimize_kcfg and len(in_edges) == 1: - in_edge = single(in_edges) - self.remove_edge(in_edge.source.id, node.id) - self.let_node(node_id=node.id, cterm=cterm) - self.create_edge( - in_edge.source.id, node.id, in_edge.depth + depth, list(in_edge.rules) + rule_labels - ) - log(f'basic block at depth {depth}: node update: {node.id}') - else: + if not (optimize_kcfg and optimize_step(cterm, depth, next_node_logs, rule_labels)): next_node = self.create_node(cterm) logs[next_node.id] = next_node_logs self.create_edge(node.id, next_node.id, depth, rules=rule_labels) From 31f1df72f9eb2fa44352755d3b256b6564e32ec7 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 11 Dec 2024 17:05:54 +0000 Subject: [PATCH 03/14] adding tests --- pyk/src/pyk/kcfg/kcfg.py | 2 +- pyk/src/tests/integration/proof/test_imp.py | 76 +++++++++++++++++++++ 2 files changed, 77 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index e640391ecb3..ad63586c5a6 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -580,7 +580,7 @@ def optimize_step( self.let_node(node_id=node.id, cterm=cterm) self.create_edge(in_edge.source.id, node.id, in_edge.depth + depth, list(in_edge.rules) + rule_labels) logs[node.id] = logs[node.id] + next_node_logs - log(f'basic block at depth {depth}: node update: {node.id}') + log(f'basic block at depth {depth}: update: {node.id}') return True return False diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 3ad17c599c9..49e6ce5b856 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -566,6 +566,35 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ), ) +APR_PROVE_WITH_OPTIMS_TEST_DATA: Iterable[ + tuple[str, Path, str, str, int | None, int | None, Iterable[str], bool, ProofStatus, int] +] = ( + ( + 'imp-simple-sum-100', + K_FILES / 'imp-simple-spec.k', + 'IMP-SIMPLE-SPEC', + 'sum-100', + None, + None, + [], + True, + ProofStatus.PASSED, + 4, + ), + ( + 'imp-simple-long-branches', + K_FILES / 'imp-simple-spec.k', + 'IMP-SIMPLE-SPEC', + 'long-branches', + None, + None, + [], + True, + ProofStatus.PASSED, + 7, + ), +) + PATH_CONSTRAINTS_TEST_DATA: Iterable[ tuple[str, Path, str, str, int | None, int | None, Iterable[str], Iterable[str], str] ] = ( @@ -918,6 +947,53 @@ def test_all_path_reachability_prove( assert proof.status == proof_status assert leaf_number(proof) == expected_leaf_number + @pytest.mark.parametrize( + 'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,cut_rules,admit_deps,proof_status,expected_max_node_number', + APR_PROVE_WITH_OPTIMS_TEST_DATA, + ids=[test_id for test_id, *_ in APR_PROVE_WITH_OPTIMS_TEST_DATA], + ) + def test_all_path_reachability_prove_with_optims( + self, + kprove: KProve, + kcfg_explore: KCFGExplore, + test_id: str, + spec_file: str, + spec_module: str, + claim_id: str, + max_iterations: int | None, + max_depth: int | None, + cut_rules: Iterable[str], + admit_deps: bool, + proof_status: ProofStatus, + expected_max_node_number: int, + tmp_path_factory: TempPathFactory, + ) -> None: + proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') + spec_modules = kprove.parse_modules(Path(spec_file), module_name=spec_module) + spec_label = f'{spec_module}.{claim_id}' + proofs = APRProof.from_spec_modules( + kprove.definition, + spec_modules, + spec_labels=[spec_label], + logs={}, + proof_dir=proof_dir, + ) + proof = single([p for p in proofs if p.id == spec_label]) + if admit_deps: + for subproof in proof.subproofs: + subproof.admit() + subproof.write_proof_data() + + prover = APRProver(kcfg_explore=kcfg_explore, execute_depth=max_depth, cut_point_rules=cut_rules) + prover.advance_proof(proof, max_iterations=max_iterations) + + kcfg_show = KCFGShow(kprove, node_printer=APRProofNodePrinter(proof, kprove, full_printer=True)) + cfg_lines = kcfg_show.show(proof.kcfg) + _LOGGER.info('\n'.join(cfg_lines)) + + assert proof.status == proof_status + assert proof.kcfg._node_id == expected_max_node_number + def test_terminal_node_subsumption( self, kprove: KProve, From 36a8cf2ad78dd14e44be14350f9f02b446933dc8 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 11 Dec 2024 18:31:22 +0000 Subject: [PATCH 04/14] revisiting approach --- pyk/src/pyk/proof/implies.py | 2 +- pyk/src/pyk/proof/proof.py | 10 ++---- pyk/src/pyk/proof/reachability.py | 34 +++++++++++++++++---- pyk/src/tests/integration/proof/test_imp.py | 12 +++++--- 4 files changed, 39 insertions(+), 19 deletions(-) diff --git a/pyk/src/pyk/proof/implies.py b/pyk/src/pyk/proof/implies.py index cddcad30e4c..e015e11c31f 100644 --- a/pyk/src/pyk/proof/implies.py +++ b/pyk/src/pyk/proof/implies.py @@ -72,7 +72,7 @@ def get_steps(self) -> list[ImpliesProofStep]: return [] return [ImpliesProofStep(self)] - def commit(self, optimize_kcfg: bool, result: ImpliesProofResult) -> None: + def commit(self, result: ImpliesProofResult) -> None: proof_type = type(self).__name__ if isinstance(result, ImpliesProofResult): self.csubst = result.csubst diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 966cb6bdd78..0d1eef04d2e 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -78,7 +78,7 @@ def __init__( ensure_dir_path(self.proof_dir) @abstractmethod - def commit(self, optimize_kcfg: bool, result: SR) -> None: + def commit(self, result: SR) -> None: """Apply the step result of type `SR` to `self`, modifying `self`.""" ... @@ -327,7 +327,6 @@ def parallel_advance_proof( max_workers: int = 1, callback: Callable[[P], None] = (lambda x: None), maintenance_rate: int = 1, - optimize_kcfg: bool = False, ) -> None: """Advance proof with multithreaded strategy. @@ -351,7 +350,6 @@ def parallel_advance_proof( max_workers: Maximum number of worker threads the pool can spawn. callback: Callable to run during proof maintenance, useful for getting real-time information about the proof. maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback). - optimize_kcfg: Optimization of KCFG construction by edge-edge minimization. """ pending: set[Future[Any]] = set() explored: set[PS] = set() @@ -379,7 +377,7 @@ def submit_steps(_steps: Iterable[PS]) -> None: future = done.pop() proof_results = future.result() for result in proof_results: - proof.commit(optimize_kcfg, result) + proof.commit(result) iterations += 1 if iterations % maintenance_rate == 0: proof.write_proof_data() @@ -508,7 +506,6 @@ def advance_proof( fail_fast: bool = False, callback: Callable[[P], None] = (lambda x: None), maintenance_rate: int = 1, - optimize_kcfg: bool = False, ) -> None: """Advance a proof. @@ -521,7 +518,6 @@ def advance_proof( halt execution even if there are still available steps. callback: Callable to run in between each completed step, useful for getting real-time information about the proof. maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback). - optimize_kcfg: Optimization of KCFG construction by edge-edge minimization. """ iterations = 0 _LOGGER.info(f'Initializing proof: {proof.id}') @@ -541,7 +537,7 @@ def advance_proof( iterations += 1 results = self.step_proof(step) for result in results: - proof.commit(optimize_kcfg, result) + proof.commit(result) if iterations % maintenance_rate == 0: proof.write_proof_data() callback(proof) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 5f3a15f84d0..1ce8cd56582 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -40,6 +40,7 @@ class APRProofResult: node_id: int prior_loops_cache_update: tuple[int, ...] + optimize_kcfg: bool @dataclass @@ -213,14 +214,14 @@ def get_steps(self) -> list[APRProofStep]: ) return steps - def commit(self, optimize_kcfg: bool, result: APRProofResult) -> None: + def commit(self, result: APRProofResult) -> None: self.prior_loops_cache[result.node_id] = result.prior_loops_cache_update # Result has been cached, use the cache if isinstance(result, APRProofUseCacheResult): assert result.cached_node_id in self._next_steps self.kcfg.extend( extend_result=self._next_steps.pop(result.cached_node_id), - optimize_kcfg=optimize_kcfg, + optimize_kcfg=result.optimize_kcfg, node=self.kcfg.node(result.node_id), logs=self.logs, ) @@ -231,7 +232,7 @@ def commit(self, optimize_kcfg: bool, result: APRProofResult) -> None: self._next_steps[result.node_id] = result.extension_to_cache self.kcfg.extend( extend_result=result.extension_to_apply, - optimize_kcfg=optimize_kcfg, + optimize_kcfg=result.optimize_kcfg, node=self.kcfg.node(result.node_id), logs=self.logs, ) @@ -717,6 +718,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): assume_defined: bool kcfg_explore: KCFGExplore extra_module: KFlatModule | None + optimize_kcfg: bool def __init__( self, @@ -729,6 +731,7 @@ def __init__( direct_subproof_rules: bool = False, assume_defined: bool = False, extra_module: KFlatModule | None = None, + optimize_kcfg: bool = False, ) -> None: self.kcfg_explore = kcfg_explore @@ -741,6 +744,7 @@ def __init__( self.direct_subproof_rules = direct_subproof_rules self.assume_defined = assume_defined self.extra_module = extra_module + self.optimize_kcfg = optimize_kcfg def close(self) -> None: self.kcfg_explore.cterm_symbolic._kore_client.close() @@ -810,14 +814,24 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: _LOGGER.info(f'Prior loop heads for node {step.node.id}: {(step.node.id, prior_loops)}') if len(prior_loops) > step.bmc_depth: _LOGGER.warning(f'Bounded node {step.proof_id}: {step.node.id} at bmc depth {step.bmc_depth}') - return [APRProofBoundedResult(node_id=step.node.id, prior_loops_cache_update=prior_loops)] + return [ + APRProofBoundedResult( + node_id=step.node.id, optimize_kcfg=self.optimize_kcfg, prior_loops_cache_update=prior_loops + ) + ] # Check if the current node and target are terminal is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(step.node.cterm) target_is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(step.target.cterm) terminal_result: list[APRProofResult] = ( - [APRProofTerminalResult(node_id=step.node.id, prior_loops_cache_update=prior_loops)] if is_terminal else [] + [ + APRProofTerminalResult( + node_id=step.node.id, optimize_kcfg=self.optimize_kcfg, prior_loops_cache_update=prior_loops + ) + ] + if is_terminal + else [] ) # Subsumption is checked if and only if the target node @@ -828,7 +842,12 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: # Information about the subsumed node being terminal must be returned # so that the set of terminal nodes is correctly updated return terminal_result + [ - APRProofSubsumeResult(csubst=csubst, node_id=step.node.id, prior_loops_cache_update=prior_loops) + APRProofSubsumeResult( + csubst=csubst, + optimize_kcfg=self.optimize_kcfg, + node_id=step.node.id, + prior_loops_cache_update=prior_loops, + ) ] if is_terminal: @@ -851,6 +870,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: APRProofUseCacheResult( node_id=step.node.id, cached_node_id=step.use_cache, + optimize_kcfg=self.optimize_kcfg, prior_loops_cache_update=prior_loops, ) ] @@ -878,6 +898,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: extension_to_apply=extend_results[0], extension_to_cache=extend_results[1], prior_loops_cache_update=prior_loops, + optimize_kcfg=self.optimize_kcfg, ) ] @@ -887,6 +908,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: node_id=step.node.id, extension_to_apply=extend_results[0], prior_loops_cache_update=prior_loops, + optimize_kcfg=self.optimize_kcfg, ) ] diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 49e6ce5b856..3708f48f20a 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -566,7 +566,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ), ) -APR_PROVE_WITH_OPTIMS_TEST_DATA: Iterable[ +APR_PROVE_WITH_KCFG_OPTIMS_TEST_DATA: Iterable[ tuple[str, Path, str, str, int | None, int | None, Iterable[str], bool, ProofStatus, int] ] = ( ( @@ -949,10 +949,10 @@ def test_all_path_reachability_prove( @pytest.mark.parametrize( 'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,cut_rules,admit_deps,proof_status,expected_max_node_number', - APR_PROVE_WITH_OPTIMS_TEST_DATA, - ids=[test_id for test_id, *_ in APR_PROVE_WITH_OPTIMS_TEST_DATA], + APR_PROVE_WITH_KCFG_OPTIMS_TEST_DATA, + ids=[test_id for test_id, *_ in APR_PROVE_WITH_KCFG_OPTIMS_TEST_DATA], ) - def test_all_path_reachability_prove_with_optims( + def test_all_path_reachability_prove_with_kcfg_optims( self, kprove: KProve, kcfg_explore: KCFGExplore, @@ -984,7 +984,9 @@ def test_all_path_reachability_prove_with_optims( subproof.admit() subproof.write_proof_data() - prover = APRProver(kcfg_explore=kcfg_explore, execute_depth=max_depth, cut_point_rules=cut_rules) + prover = APRProver( + kcfg_explore=kcfg_explore, execute_depth=max_depth, cut_point_rules=cut_rules, optimize_kcfg=True + ) prover.advance_proof(proof, max_iterations=max_iterations) kcfg_show = KCFGShow(kprove, node_printer=APRProofNodePrinter(proof, kprove, full_printer=True)) From 4b7930d94e0f3db11097ea49359057ec38186deb Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 11 Dec 2024 19:16:06 +0000 Subject: [PATCH 05/14] correction --- pyk/src/tests/integration/proof/test_imp.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 3708f48f20a..28340a780cf 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -591,7 +591,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: [], True, ProofStatus.PASSED, - 7, + 8, ), ) From 7ca5243bde11a69b19c55fa4c92c2e08e1c6cedd Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 11 Dec 2024 20:02:28 +0000 Subject: [PATCH 06/14] KCFG grafting correction --- pyk/src/pyk/kcfg/kcfg.py | 2 +- pyk/src/tests/unit/test-data/pyk_toml_test.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index ad63586c5a6..545aa41795d 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -579,7 +579,7 @@ def optimize_step( self.remove_edge(in_edge.source.id, node.id) self.let_node(node_id=node.id, cterm=cterm) self.create_edge(in_edge.source.id, node.id, in_edge.depth + depth, list(in_edge.rules) + rule_labels) - logs[node.id] = logs[node.id] + next_node_logs + logs[node.id] = logs[node.id] + next_node_logs if node.id in logs else next_node_logs log(f'basic block at depth {depth}: update: {node.id}') return True return False diff --git a/pyk/src/tests/unit/test-data/pyk_toml_test.toml b/pyk/src/tests/unit/test-data/pyk_toml_test.toml index a374fe73737..6a6f47df9b0 100644 --- a/pyk/src/tests/unit/test-data/pyk_toml_test.toml +++ b/pyk/src/tests/unit/test-data/pyk_toml_test.toml @@ -1,6 +1,6 @@ [coverage] output = "default-file" -definition = "/tmp" +definition = "/var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T" [print] input = "kast-json" From 2055c400d32365c024c75eadac9cb6790ac511f2 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 11 Dec 2024 20:03:38 +0000 Subject: [PATCH 07/14] reverting .toml file that keeps changing on every make --- pyk/src/tests/unit/test-data/pyk_toml_test.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/tests/unit/test-data/pyk_toml_test.toml b/pyk/src/tests/unit/test-data/pyk_toml_test.toml index 6a6f47df9b0..a374fe73737 100644 --- a/pyk/src/tests/unit/test-data/pyk_toml_test.toml +++ b/pyk/src/tests/unit/test-data/pyk_toml_test.toml @@ -1,6 +1,6 @@ [coverage] output = "default-file" -definition = "/var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T" +definition = "/tmp" [print] input = "kast-json" From f205776949ab1d5792e68303f06183b965a62a79 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 12 Dec 2024 11:17:46 +0000 Subject: [PATCH 08/14] suggestions from Tamas --- pyk/src/pyk/kcfg/kcfg.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 545aa41795d..3c8e9214734 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -22,7 +22,7 @@ ) from ..kast.outer import KFlatModule from ..prelude.kbool import andBool -from ..utils import ensure_dir_path, not_none, single +from ..utils import ensure_dir_path, not_none if TYPE_CHECKING: from collections.abc import Iterable, Mapping, MutableMapping @@ -557,9 +557,10 @@ def path_length(_path: Iterable[KCFG.Successor]) -> int: def extend( self, extend_result: KCFGExtendResult, - optimize_kcfg: bool, node: KCFG.Node, logs: dict[int, tuple[LogEntry, ...]], + *, + optimize_kcfg: bool, ) -> None: def log(message: str, *, warning: bool = False) -> None: @@ -575,7 +576,7 @@ def optimize_step( ) -> bool: in_edges = self.edges(target_id=node.id) if len(in_edges) == 1: - in_edge = single(in_edges) + in_edge = in_edges[0] self.remove_edge(in_edge.source.id, node.id) self.let_node(node_id=node.id, cterm=cterm) self.create_edge(in_edge.source.id, node.id, in_edge.depth + depth, list(in_edge.rules) + rule_labels) From 5ea08e0727750b686e21c7595cfa3634a00e8192 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 12 Dec 2024 16:56:49 +0000 Subject: [PATCH 09/14] inlining --- pyk/src/pyk/kcfg/kcfg.py | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 3c8e9214734..692584f68ce 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -571,20 +571,6 @@ def log(message: str, *, warning: bool = False) -> None: f'Extending current KCFG with the following: {message}{result_info_message}', ) - def optimize_step( - cterm: CTerm, depth: int, next_node_logs: tuple[LogEntry, ...], rule_labels: list[str] - ) -> bool: - in_edges = self.edges(target_id=node.id) - if len(in_edges) == 1: - in_edge = in_edges[0] - self.remove_edge(in_edge.source.id, node.id) - self.let_node(node_id=node.id, cterm=cterm) - self.create_edge(in_edge.source.id, node.id, in_edge.depth + depth, list(in_edge.rules) + rule_labels) - logs[node.id] = logs[node.id] + next_node_logs if node.id in logs else next_node_logs - log(f'basic block at depth {depth}: update: {node.id}') - return True - return False - match extend_result: case Vacuous(): self.add_vacuous(node.id) @@ -600,7 +586,16 @@ def optimize_step( log(f'abstraction node: {node.id}') case Step(cterm, depth, next_node_logs, rule_labels, _): - if not (optimize_kcfg and optimize_step(cterm, depth, next_node_logs, rule_labels)): + if optimize_kcfg and (len(edges := self.edges(target_id=node.id)) == 1): + in_edge = edges[0] + self.remove_edge(in_edge.source.id, node.id) + self.let_node(node_id=node.id, cterm=cterm) + self.create_edge( + in_edge.source.id, node.id, in_edge.depth + depth, list(in_edge.rules) + rule_labels + ) + logs[node.id] = logs[node.id] + next_node_logs if node.id in logs else next_node_logs + log(f'basic block at depth {depth}: update: {node.id}') + else: next_node = self.create_node(cterm) logs[next_node.id] = next_node_logs self.create_edge(node.id, next_node.id, depth, rules=rule_labels) From f43e051f0185c35454a604fbf282b51bf52c4e3a Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 12 Dec 2024 22:39:39 +0000 Subject: [PATCH 10/14] corrections --- pyk/src/pyk/kcfg/kcfg.py | 28 ++++++++++--------- pyk/src/tests/integration/proof/test_imp.py | 10 +++---- .../tests/unit/test-data/pyk_toml_test.toml | 2 +- 3 files changed, 21 insertions(+), 19 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 692584f68ce..47bd70abf72 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -586,20 +586,22 @@ def log(message: str, *, warning: bool = False) -> None: log(f'abstraction node: {node.id}') case Step(cterm, depth, next_node_logs, rule_labels, _): - if optimize_kcfg and (len(edges := self.edges(target_id=node.id)) == 1): - in_edge = edges[0] + next_node = self.create_node(cterm) + # Optimization for steps consists of on-the-fly merging of consecutive edges and can + # be performed only if the current node has a single predecessor connected by an Edge + if ( + optimize_kcfg + and (len(predecessors := self.predecessors(target_id=node.id)) == 1) + and isinstance(in_edge := predecessors[0], KCFG.Edge) + ): + # The existing edge is removed and the step parameters are updated accordingly self.remove_edge(in_edge.source.id, node.id) - self.let_node(node_id=node.id, cterm=cterm) - self.create_edge( - in_edge.source.id, node.id, in_edge.depth + depth, list(in_edge.rules) + rule_labels - ) - logs[node.id] = logs[node.id] + next_node_logs if node.id in logs else next_node_logs - log(f'basic block at depth {depth}: update: {node.id}') - else: - next_node = self.create_node(cterm) - logs[next_node.id] = next_node_logs - self.create_edge(node.id, next_node.id, depth, rules=rule_labels) - log(f'basic block at depth {depth}: {node.id} --> {next_node.id}') + depth += in_edge.depth + rule_labels = list(in_edge.rules) + rule_labels + next_node_logs = logs[node.id] + next_node_logs if node.id in logs else next_node_logs + self.create_edge(in_edge.source.id, next_node.id, depth, rule_labels) + logs[next_node.id] = next_node_logs + log(f'basic block at depth {depth}: {node.id} --> {next_node.id}') case Branch(branches, _): branch_node_ids = self.split_on_constraints(node.id, branches) diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 28340a780cf..572d43a7808 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -579,7 +579,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: [], True, ProofStatus.PASSED, - 4, + 3, ), ( 'imp-simple-long-branches', @@ -591,7 +591,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: [], True, ProofStatus.PASSED, - 8, + 5, ), ) @@ -948,7 +948,7 @@ def test_all_path_reachability_prove( assert leaf_number(proof) == expected_leaf_number @pytest.mark.parametrize( - 'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,cut_rules,admit_deps,proof_status,expected_max_node_number', + 'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,cut_rules,admit_deps,proof_status,expected_nodes', APR_PROVE_WITH_KCFG_OPTIMS_TEST_DATA, ids=[test_id for test_id, *_ in APR_PROVE_WITH_KCFG_OPTIMS_TEST_DATA], ) @@ -965,7 +965,7 @@ def test_all_path_reachability_prove_with_kcfg_optims( cut_rules: Iterable[str], admit_deps: bool, proof_status: ProofStatus, - expected_max_node_number: int, + expected_nodes: int, tmp_path_factory: TempPathFactory, ) -> None: proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') @@ -994,7 +994,7 @@ def test_all_path_reachability_prove_with_kcfg_optims( _LOGGER.info('\n'.join(cfg_lines)) assert proof.status == proof_status - assert proof.kcfg._node_id == expected_max_node_number + assert len(proof.kcfg._nodes) == expected_nodes def test_terminal_node_subsumption( self, diff --git a/pyk/src/tests/unit/test-data/pyk_toml_test.toml b/pyk/src/tests/unit/test-data/pyk_toml_test.toml index a374fe73737..6a6f47df9b0 100644 --- a/pyk/src/tests/unit/test-data/pyk_toml_test.toml +++ b/pyk/src/tests/unit/test-data/pyk_toml_test.toml @@ -1,6 +1,6 @@ [coverage] output = "default-file" -definition = "/tmp" +definition = "/var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T" [print] input = "kast-json" From 5f278fe7c0c0b9f195aa82010b3f4a68ce8a0daf Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 12 Dec 2024 22:40:09 +0000 Subject: [PATCH 11/14] .toml again... --- pyk/src/tests/unit/test-data/pyk_toml_test.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/tests/unit/test-data/pyk_toml_test.toml b/pyk/src/tests/unit/test-data/pyk_toml_test.toml index 6a6f47df9b0..a374fe73737 100644 --- a/pyk/src/tests/unit/test-data/pyk_toml_test.toml +++ b/pyk/src/tests/unit/test-data/pyk_toml_test.toml @@ -1,6 +1,6 @@ [coverage] output = "default-file" -definition = "/var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T" +definition = "/tmp" [print] input = "kast-json" From c60dd157c33562f996f91b24b014d984d326b203 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 12 Dec 2024 22:44:29 +0000 Subject: [PATCH 12/14] source node correction --- pyk/src/pyk/kcfg/kcfg.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 47bd70abf72..d68c66c8b31 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -586,6 +586,7 @@ def log(message: str, *, warning: bool = False) -> None: log(f'abstraction node: {node.id}') case Step(cterm, depth, next_node_logs, rule_labels, _): + node_id = node.id next_node = self.create_node(cterm) # Optimization for steps consists of on-the-fly merging of consecutive edges and can # be performed only if the current node has a single predecessor connected by an Edge @@ -596,12 +597,13 @@ def log(message: str, *, warning: bool = False) -> None: ): # The existing edge is removed and the step parameters are updated accordingly self.remove_edge(in_edge.source.id, node.id) + node_id = in_edge.source.id depth += in_edge.depth rule_labels = list(in_edge.rules) + rule_labels next_node_logs = logs[node.id] + next_node_logs if node.id in logs else next_node_logs - self.create_edge(in_edge.source.id, next_node.id, depth, rule_labels) + self.create_edge(node_id, next_node.id, depth, rule_labels) logs[next_node.id] = next_node_logs - log(f'basic block at depth {depth}: {node.id} --> {next_node.id}') + log(f'basic block at depth {depth}: {node_id} --> {next_node.id}') case Branch(branches, _): branch_node_ids = self.split_on_constraints(node.id, branches) From 9de21aa941eec9f91f0fe7cf30166fd0c0c3a7b0 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 12 Dec 2024 23:21:26 +0000 Subject: [PATCH 13/14] removing node --- pyk/src/pyk/kcfg/kcfg.py | 1 + 1 file changed, 1 insertion(+) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index d68c66c8b31..57c0e95dc97 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -601,6 +601,7 @@ def log(message: str, *, warning: bool = False) -> None: depth += in_edge.depth rule_labels = list(in_edge.rules) + rule_labels next_node_logs = logs[node.id] + next_node_logs if node.id in logs else next_node_logs + self.remove_node(node.id) self.create_edge(node_id, next_node.id, depth, rule_labels) logs[next_node.id] = next_node_logs log(f'basic block at depth {depth}: {node_id} --> {next_node.id}') From 2ced4e68aa9bf5cfb48ddfa0817dff08ed8d79cc Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 13 Dec 2024 11:21:47 +0000 Subject: [PATCH 14/14] test correction --- pyk/src/tests/integration/proof/test_imp.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 572d43a7808..517051b001b 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -591,7 +591,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: [], True, ProofStatus.PASSED, - 5, + 7, ), )