From f92542dbf66c3c3875242175d9fb5cd7caf70325 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 31 Jul 2024 10:55:14 +0100 Subject: [PATCH 01/10] Support for non-immediate proof maintenance --- pyk/src/pyk/proof/proof.py | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 27adf9721b0..907e3611c95 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -325,6 +325,7 @@ def parallel_advance_proof( max_iterations: int | None = None, fail_fast: bool = False, max_workers: int = 1, + maintenance_iterations: int = 32, callback: Callable[[P], None] = (lambda x: None), ) -> None: """Advance proof with multithreaded strategy. @@ -347,7 +348,8 @@ def parallel_advance_proof( fail_fast: If the proof is failing after finishing a step, halt execution even if there are still available steps. max_workers: Maximum number of worker threads the pool can spawn. - callback: Callable to run in between each completed step, useful for getting real-time information about the proof. + maintenance_iterations: The number of iterations to be executed between proof maintenance (writing and callback). + callback: Callable to run during proof maintenance, useful for getting real-time information about the proof. """ pending: set[Future[Any]] = set() explored: set[PS] = set() @@ -376,9 +378,10 @@ def submit_steps(_steps: Iterable[PS]) -> None: proof_results = future.result() for result in proof_results: proof.commit(result) - proof.write_proof_data() - callback(proof) iterations += 1 + if iterations % maintenance_iterations == 0: + proof.write_proof_data() + callback(proof) if max_iterations is not None and max_iterations <= iterations: break if fail_fast and proof.failed: From 41e04ce0fb5e1969c9a71ce2fcb7b99ffee3d4e9 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 31 Jul 2024 12:01:25 +0100 Subject: [PATCH 02/10] maintenance every max_workers iterations --- pyk/src/pyk/proof/proof.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 907e3611c95..8fde46b79de 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -325,7 +325,6 @@ def parallel_advance_proof( max_iterations: int | None = None, fail_fast: bool = False, max_workers: int = 1, - maintenance_iterations: int = 32, callback: Callable[[P], None] = (lambda x: None), ) -> None: """Advance proof with multithreaded strategy. @@ -348,7 +347,6 @@ def parallel_advance_proof( fail_fast: If the proof is failing after finishing a step, halt execution even if there are still available steps. max_workers: Maximum number of worker threads the pool can spawn. - maintenance_iterations: The number of iterations to be executed between proof maintenance (writing and callback). callback: Callable to run during proof maintenance, useful for getting real-time information about the proof. """ pending: set[Future[Any]] = set() @@ -379,7 +377,7 @@ def submit_steps(_steps: Iterable[PS]) -> None: for result in proof_results: proof.commit(result) iterations += 1 - if iterations % maintenance_iterations == 0: + if iterations % max_workers == 0: proof.write_proof_data() callback(proof) if max_iterations is not None and max_iterations <= iterations: From 1c43e2e38faf8d6cd0bac0f1de797034d636f22a Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 1 Aug 2024 10:43:23 -0600 Subject: [PATCH 03/10] Update dependency: deps/llvm-backend_release (#4559) Co-authored-by: devops --- deps/llvm-backend_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- llvm-backend/src/main/native/llvm-backend | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 9810a3b1179..9adbab1b3a2 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.64 +0.1.69 diff --git a/flake.lock b/flake.lock index cf8970e0046..628ab9ef296 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1721983376, - "narHash": "sha256-pP56X9zoqV+x6QdjIHWH7gcXcwhz+Q08yD8RwBqiIRQ=", + "lastModified": 1722454948, + "narHash": "sha256-8mcRIlTAmQ1J3oxi0QibxmSlFWkOTRlyWy5kSHJFf6U=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "79011fff66455dd451d39821534bd58f5468227b", + "rev": "5be14fe74740a15cb707c102425032ffdee98281", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.64", + "ref": "v0.1.69", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 24329f46233..edf3b103803 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.64"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.69"; haskell-backend = { url = "github:runtimeverification/haskell-backend/v0.1.51"; inputs.rv-utils.follows = "llvm-backend/rv-utils"; diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 79011fff664..5be14fe7474 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 79011fff66455dd451d39821534bd58f5468227b +Subproject commit 5be14fe74740a15cb707c102425032ffdee98281 From dad78b171ac605bc088e37c0465fd7ddc33be731 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Fri, 2 Aug 2024 02:13:39 -0500 Subject: [PATCH 04/10] Display number of terminal nodes in `one_line_summary` for `APRProof` (#4566) Adds the number of terminal nodes to `one_line_summary` for `APRProof`. Also changes the display to use `|` as dividers instead of `/`. --- pyk/src/pyk/proof/reachability.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index fe747f1cc0f..53b1b26e586 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -509,11 +509,12 @@ def one_line_summary(self) -> str: failing = len(self.failing) branches = len(self.kcfg.ndbranches()) + len(self.kcfg.splits()) vacuous = len(self.kcfg.vacuous) + terminal = len(self.terminal) stuck = len(self.kcfg.stuck) passed = len([cover for cover in self.kcfg.covers() if cover.target.id == self.target]) return ( super().one_line_summary - + f'/{nodes} nodes/{pending} pending/{passed} passed/{failing} failing/{branches} branches/{vacuous} vacuous/{stuck} stuck' + + f'|{nodes} nodes|{pending} pending|{passed} passed|{failing} failing|{branches} branches|{vacuous} vacuous|{terminal} terminal|{stuck} stuck' ) def get_refutation_id(self, node_id: int) -> str: From 80a43a8b353b2b9b6680bc8c23f7cef9f8f84fff Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 2 Aug 2024 06:49:12 -0600 Subject: [PATCH 05/10] Update dependency: deps/haskell-backend_release (#4558) Co-authored-by: devops --- deps/haskell-backend_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- haskell-backend/src/main/native/haskell-backend | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release index 660641b8acd..a0ba2466d24 100644 --- a/deps/haskell-backend_release +++ b/deps/haskell-backend_release @@ -1 +1 @@ -v0.1.51 +v0.1.57 diff --git a/flake.lock b/flake.lock index 628ab9ef296..343c83d8a32 100644 --- a/flake.lock +++ b/flake.lock @@ -65,16 +65,16 @@ "z3": "z3" }, "locked": { - "lastModified": 1722260205, - "narHash": "sha256-Yi7m1bLuAzcP75w8Px0BinjlNcekOSj8g9KjVNDSw6c=", + "lastModified": 1722517294, + "narHash": "sha256-CBuygvM1ksLLp3xNPQcLvm6EQqrf05g92yAh1Eevjuc=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "082335a00314bf32392cb668414e7d8c7bddc800", + "rev": "3e38da9c58e76da39ced663090e6475b957e6599", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.51", + "ref": "v0.1.57", "repo": "haskell-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index edf3b103803..5ade059111a 100644 --- a/flake.nix +++ b/flake.nix @@ -3,7 +3,7 @@ inputs = { llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.69"; haskell-backend = { - url = "github:runtimeverification/haskell-backend/v0.1.51"; + url = "github:runtimeverification/haskell-backend/v0.1.57"; inputs.rv-utils.follows = "llvm-backend/rv-utils"; inputs.nixpkgs.follows = "llvm-backend/nixpkgs"; }; diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend index 082335a0031..3e38da9c58e 160000 --- a/haskell-backend/src/main/native/haskell-backend +++ b/haskell-backend/src/main/native/haskell-backend @@ -1 +1 @@ -Subproject commit 082335a00314bf32392cb668414e7d8c7bddc800 +Subproject commit 3e38da9c58e76da39ced663090e6475b957e6599 From da797e8d29d9391a7794d818e54276a307d5195f Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Mon, 5 Aug 2024 09:41:47 -0600 Subject: [PATCH 06/10] Update dependency: deps/haskell-backend_release (#4571) Co-authored-by: devops --- deps/haskell-backend_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- haskell-backend/src/main/native/haskell-backend | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release index a0ba2466d24..f8e99bbf6a0 100644 --- a/deps/haskell-backend_release +++ b/deps/haskell-backend_release @@ -1 +1 @@ -v0.1.57 +v0.1.58 diff --git a/flake.lock b/flake.lock index 343c83d8a32..90fb6ea5de0 100644 --- a/flake.lock +++ b/flake.lock @@ -65,16 +65,16 @@ "z3": "z3" }, "locked": { - "lastModified": 1722517294, - "narHash": "sha256-CBuygvM1ksLLp3xNPQcLvm6EQqrf05g92yAh1Eevjuc=", + "lastModified": 1722860063, + "narHash": "sha256-5K3BIIbwkMpN4idvAHRrw0JzHRL6Au4ui+7NqkX+c3w=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "3e38da9c58e76da39ced663090e6475b957e6599", + "rev": "7047b0964349727e54425c2c81478caf3dad757c", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.57", + "ref": "v0.1.58", "repo": "haskell-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 5ade059111a..80d9fa75a6c 100644 --- a/flake.nix +++ b/flake.nix @@ -3,7 +3,7 @@ inputs = { llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.69"; haskell-backend = { - url = "github:runtimeverification/haskell-backend/v0.1.57"; + url = "github:runtimeverification/haskell-backend/v0.1.58"; inputs.rv-utils.follows = "llvm-backend/rv-utils"; inputs.nixpkgs.follows = "llvm-backend/nixpkgs"; }; diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend index 3e38da9c58e..7047b096434 160000 --- a/haskell-backend/src/main/native/haskell-backend +++ b/haskell-backend/src/main/native/haskell-backend @@ -1 +1 @@ -Subproject commit 3e38da9c58e76da39ced663090e6475b957e6599 +Subproject commit 7047b0964349727e54425c2c81478caf3dad757c From bcd3983d801125408ce548614b3a197178c8152b Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 6 Aug 2024 11:02:17 +0200 Subject: [PATCH 07/10] Remove the deprecated `"log-timing"` RPC log option (#4573) This option is unused and all its use cases are subsumed by the `-l Timing --log-format json` non-RPC log option. For reference, here's the Haskell Backend PR that stops emitting the timing RPC log entries: https://github.com/runtimeverification/haskell-backend/pull/4015 --- pyk/src/pyk/kore/rpc.py | 29 ------------- .../integration/kore/test_kore_client.py | 43 ------------------- 2 files changed, 72 deletions(-) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 99bb41cac0a..4eeac4cf109 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -570,8 +570,6 @@ class LogEntry(ABC): @classmethod def from_dict(cls: type[LE], dct: Mapping[str, Any]) -> LE: match dct['tag']: - case 'processing-time': - return LogTiming.from_dict(dct) # type: ignore case 'rewrite': return LogRewrite.from_dict(dct) # type: ignore case _: @@ -581,27 +579,6 @@ def from_dict(cls: type[LE], dct: Mapping[str, Any]) -> LE: def to_dict(self) -> dict[str, Any]: ... -@final -@dataclass(frozen=True) -class LogTiming(LogEntry): - class Component(Enum): - KORE_RPC = 'kore-rpc' - BOOSTER = 'booster' - PROXY = 'proxy' - - time: float - component: Component | None - - @classmethod - def from_dict(cls, dct: Mapping[str, Any]) -> LogTiming: - return LogTiming( - time=dct['time'], component=LogTiming.Component(dct['component']) if 'component' in dct else None - ) - - def to_dict(self) -> dict[str, Any]: - return {'tag': 'processing-time', 'time': self.time, 'component': self.component} - - @final @dataclass(frozen=True) class LogRewrite(LogEntry): @@ -1025,7 +1002,6 @@ def execute( module_name: str | None = None, log_successful_rewrites: bool | None = None, log_failed_rewrites: bool | None = None, - log_timing: bool | None = None, ) -> ExecuteResult: params = filter_none( { @@ -1039,7 +1015,6 @@ def execute( 'state': self._state(pattern), 'log-successful-rewrites': log_successful_rewrites, 'log-failed-rewrites': log_failed_rewrites, - 'log-timing': log_timing, } ) @@ -1052,14 +1027,12 @@ def implies( consequent: Pattern, *, module_name: str | None = None, - log_timing: bool | None = None, ) -> ImpliesResult: params = filter_none( { 'antecedent': self._state(antecedent), 'consequent': self._state(consequent), 'module': module_name, - 'log-timing': log_timing, } ) @@ -1071,13 +1044,11 @@ def simplify( pattern: Pattern, *, module_name: str | None = None, - log_timing: bool | None = None, ) -> tuple[Pattern, tuple[LogEntry, ...]]: params = filter_none( { 'state': self._state(pattern), 'module': module_name, - 'log-timing': log_timing, } ) diff --git a/pyk/src/tests/integration/kore/test_kore_client.py b/pyk/src/tests/integration/kore/test_kore_client.py index de0059ca9cf..0eca981a969 100644 --- a/pyk/src/tests/integration/kore/test_kore_client.py +++ b/pyk/src/tests/integration/kore/test_kore_client.py @@ -40,7 +40,6 @@ InvalidModuleError, LogOrigin, LogRewrite, - LogTiming, RewriteFailure, RewriteSuccess, SatResult, @@ -625,48 +624,6 @@ def test( assert actual == expected[server_type] -class TestTimeLogging(KoreClientTest): - KOMPILE_DEFINITION = """ - module TIMING-TEST - imports INT - configuration $PGM:Int - endmodule - """ - KOMPILE_MAIN_MODULE = 'TIMING-TEST' - KOMPILE_ARGS = {'syntax_module': 'TIMING-TEST'} - LLVM_ARGS = KOMPILE_ARGS - - @staticmethod - def config(i: int) -> Pattern: - return generated_top((k(kseq((inj(INT, SORT_K_ITEM, int_dv(i)),))), generated_counter(int_dv(0)))) - - def test_execute(self, kore_client: KoreClient) -> None: - # When - response = kore_client.execute(self.config(0), log_timing=True) - logs = response.logs - - # Then - assert logs - assert all(isinstance(log, LogTiming) for log in logs) - - def test_implies(self, kore_client: KoreClient) -> None: - # When - response = kore_client.implies(EVar('X', INT), int_top, log_timing=True) - logs = response.logs - - # Then - assert logs - assert all(isinstance(log, LogTiming) for log in logs) - - def test_simplify(self, kore_client: KoreClient) -> None: - # When - _, logs = kore_client.simplify(int_top, log_timing=True) - - # Then - assert logs - assert all(isinstance(log, LogTiming) for log in logs) - - class TestAddModule(KoreClientTest): KOMPILE_DEFINITION = """ module INT-CONFIG From 8f42b9c8d20ed50182108751b6225c3befe6d56a Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Tue, 6 Aug 2024 21:38:39 +0200 Subject: [PATCH 08/10] parameter description --- pyk/src/pyk/proof/proof.py | 4 +++- pyk/src/tests/unit/test-data/pyk_toml_test.toml | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 8fde46b79de..6677e0f94f9 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -326,6 +326,7 @@ def parallel_advance_proof( fail_fast: bool = False, max_workers: int = 1, callback: Callable[[P], None] = (lambda x: None), + maintenance_rate: int = 1, ) -> None: """Advance proof with multithreaded strategy. @@ -348,6 +349,7 @@ def parallel_advance_proof( halt execution even if there are still available steps. 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). """ pending: set[Future[Any]] = set() explored: set[PS] = set() @@ -377,7 +379,7 @@ def submit_steps(_steps: Iterable[PS]) -> None: for result in proof_results: proof.commit(result) iterations += 1 - if iterations % max_workers == 0: + if iterations % maintenance_rate == 0: proof.write_proof_data() callback(proof) if max_iterations is not None and max_iterations <= iterations: 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 9919e16f378..74b5870db45 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 8e988f0df136f755635e82ed32ee4e2f826e6f72 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Tue, 6 Aug 2024 21:54:40 +0200 Subject: [PATCH 09/10] reverting accidental change --- 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 74b5870db45..9919e16f378 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 7c2b0ca885f181e7ed79675148243c184a3427be Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Tue, 6 Aug 2024 21:59:16 +0200 Subject: [PATCH 10/10] adding option to Prover.advance_proof --- pyk/src/pyk/proof/proof.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 6677e0f94f9..0d1eef04d2e 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -505,6 +505,7 @@ def advance_proof( max_iterations: int | None = None, fail_fast: bool = False, callback: Callable[[P], None] = (lambda x: None), + maintenance_rate: int = 1, ) -> None: """Advance a proof. @@ -516,6 +517,7 @@ def advance_proof( fail_fast: If the proof is failing after finishing a step, 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). """ iterations = 0 _LOGGER.info(f'Initializing proof: {proof.id}') @@ -536,7 +538,9 @@ def advance_proof( results = self.step_proof(step) for result in results: proof.commit(result) - proof.write_proof_data() - callback(proof) + if iterations % maintenance_rate == 0: + proof.write_proof_data() + callback(proof) + if proof.failed: proof.failure_info = self.failure_info(proof)