From 01d3ab043a170c6570974caa77939872dc54aa59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 9 Oct 2024 09:34:46 +0200 Subject: [PATCH 1/3] Add Python 3.13 to `pyk` code quality CI job (#4656) - Fix a few `TypeError`-s - Add Python 3.13 to code quality matrix --- .github/workflows/test-pr.yml | 2 +- pyk/src/tests/integration/proof/test_imp.py | 182 +++++++++--------- .../tests/integration/proof/test_mini_kevm.py | 50 +++-- 3 files changed, 113 insertions(+), 121 deletions(-) diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index a32a018ee22..3e4c05270ff 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -35,7 +35,7 @@ jobs: strategy: fail-fast: false matrix: - python-version: ['3.10', '3.11', '3.12'] + python-version: ['3.10', '3.11', '3.12', '3.13'] defaults: run: working-directory: ./pyk diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index a5231d43bdd..55ef85ca96a 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -892,31 +892,31 @@ def test_all_path_reachability_prove( expected_leaf_number: int, tmp_path_factory: TempPathFactory, ) -> None: - with tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') as proof_dir: - spec_modules = kprove.get_claim_modules(Path(spec_file), spec_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() + proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') + spec_modules = kprove.get_claim_modules(Path(spec_file), spec_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) + 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)) + 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 leaf_number(proof) == expected_leaf_number + assert proof.status == proof_status + assert leaf_number(proof) == expected_leaf_number def test_terminal_node_subsumption( self, @@ -929,24 +929,24 @@ def test_terminal_node_subsumption( spec_module: str = 'IMP-SIMPLE-SPEC' claim_id: str = 'terminal-node-subsumption' cut_rules: Iterable[str] = [] - with tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') as proof_dir: - spec_modules = kprove.get_claim_modules(Path(spec_file), spec_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]) - prover = APRProver(kcfg_explore=kcfg_explore, execute_depth=7, cut_point_rules=cut_rules) - prover.advance_proof(proof, max_iterations=1) - # We have reached a terminal node, but not yet checked subsumption - assert proof.status != ProofStatus.PASSED - # The next advance only checks subsumption - prover.advance_proof(proof, max_iterations=1) - assert proof.status == ProofStatus.PASSED + proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') + spec_modules = kprove.get_claim_modules(Path(spec_file), spec_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]) + prover = APRProver(kcfg_explore=kcfg_explore, execute_depth=7, cut_point_rules=cut_rules) + prover.advance_proof(proof, max_iterations=1) + # We have reached a terminal node, but not yet checked subsumption + assert proof.status != ProofStatus.PASSED + # The next advance only checks subsumption + prover.advance_proof(proof, max_iterations=1) + assert proof.status == ProofStatus.PASSED @pytest.mark.parametrize( 'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,terminal_rules,cut_rules,expected_constraint', @@ -1440,34 +1440,32 @@ def test_all_path_reachability_prove_parallel( tmp_path_factory: TempPathFactory, create_prover: Callable[[int, Iterable[str]], Prover], ) -> None: - with tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') as proof_dir: - spec_modules = kprove.get_claim_modules(Path(spec_file), spec_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() + proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') + spec_modules = kprove.get_claim_modules(Path(spec_file), spec_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() - _create_prover = partial(create_prover, max_depth, cut_rules) + _create_prover = partial(create_prover, max_depth, cut_rules) - parallel_advance_proof( - proof=proof, max_iterations=max_iterations, create_prover=_create_prover, max_workers=2 - ) + parallel_advance_proof(proof=proof, max_iterations=max_iterations, create_prover=_create_prover, max_workers=2) - 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)) + 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 leaf_number(proof) == expected_leaf_number + assert proof.status == proof_status + assert leaf_number(proof) == expected_leaf_number def test_all_path_reachability_prove_parallel_resources( self, @@ -1481,39 +1479,37 @@ def test_all_path_reachability_prove_parallel_resources( spec_module = 'IMP-SIMPLE-SPEC' claim_id = 'addition-1' - with tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') as proof_dir: - spec_modules = kprove.get_claim_modules(Path(spec_file), spec_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]) + proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') + spec_modules = kprove.get_claim_modules(Path(spec_file), spec_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]) - _create_prover = partial(create_prover, 1, []) + _create_prover = partial(create_prover, 1, []) - provers_created = 0 + provers_created = 0 - class MyAPRProver(APRProver): - provers_closed: int = 0 + class MyAPRProver(APRProver): + provers_closed: int = 0 - def close(self) -> None: - MyAPRProver.provers_closed += 1 - super().close() + def close(self) -> None: + MyAPRProver.provers_closed += 1 + super().close() - def create_prover_res_counter() -> APRProver: - nonlocal provers_created - provers_created += 1 - prover = _create_prover() - prover.__class__ = MyAPRProver - assert type(prover) is MyAPRProver - return prover + def create_prover_res_counter() -> APRProver: + nonlocal provers_created + provers_created += 1 + prover = _create_prover() + prover.__class__ = MyAPRProver + assert type(prover) is MyAPRProver + return prover - parallel_advance_proof( - proof=proof, max_iterations=2, create_prover=create_prover_res_counter, max_workers=2 - ) + parallel_advance_proof(proof=proof, max_iterations=2, create_prover=create_prover_res_counter, max_workers=2) - assert provers_created == MyAPRProver.provers_closed + assert provers_created == MyAPRProver.provers_closed diff --git a/pyk/src/tests/integration/proof/test_mini_kevm.py b/pyk/src/tests/integration/proof/test_mini_kevm.py index af651edc19c..f7f78576603 100644 --- a/pyk/src/tests/integration/proof/test_mini_kevm.py +++ b/pyk/src/tests/integration/proof/test_mini_kevm.py @@ -76,33 +76,29 @@ def test_all_path_reachability_prove( expected_leaf_number: int, tmp_path_factory: TempPathFactory, ) -> None: - with tmp_path_factory.mktemp('apr_tmp_proofs') as proof_dir: - claim = single( - kprove.get_claims( - Path(spec_file), spec_module_name=spec_module, claim_labels=[f'{spec_module}.{claim_id}'] - ) - ) - proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proof_dir) - - new_init_cterm = kcfg_explore.cterm_symbolic.assume_defined(proof.kcfg.node(proof.init).cterm) - proof.kcfg.let_node(proof.init, cterm=new_init_cterm) - kcfg_explore.simplify(proof.kcfg, {}) - - 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, minimize=False) - ) - cfg_lines = kcfg_show.show(proof.kcfg) - _LOGGER.info('\n'.join(cfg_lines)) - - assert proof.status == proof_status - assert leaf_number(proof) == expected_leaf_number + proof_dir = tmp_path_factory.mktemp('apr_tmp_proofs') + claim = single( + kprove.get_claims(Path(spec_file), spec_module_name=spec_module, claim_labels=[f'{spec_module}.{claim_id}']) + ) + proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proof_dir) + + new_init_cterm = kcfg_explore.cterm_symbolic.assume_defined(proof.kcfg.node(proof.init).cterm) + proof.kcfg.let_node(proof.init, cterm=new_init_cterm) + kcfg_explore.simplify(proof.kcfg, {}) + + 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, minimize=False)) + cfg_lines = kcfg_show.show(proof.kcfg) + _LOGGER.info('\n'.join(cfg_lines)) + + assert proof.status == proof_status + assert leaf_number(proof) == expected_leaf_number def test_implication_failure_reason_cell_mismatch( self, From 5ced750ab679bcbc244a3b9304607760a7bfa9e8 Mon Sep 17 00:00:00 2001 From: Palina Date: Thu, 10 Oct 2024 18:49:25 +0800 Subject: [PATCH 2/3] TOML: use `default` profile values by default when another profile is active (#4657) Follow up to https://github.com/runtimeverification/kontrol/pull/825. In Foundry, when parsing TOML config files, values set in a default profile (e.g., `[prove.default]` in `kontrol.toml`) are inherited by other profiles unless they are explicitly overridden in those profiles, which helps avoid redefining shared configuration settings between profiles ([Foundry docs](https://book.getfoundry.sh/config/)). We'd like to support the same behavior in `kontrol.toml`. Similarly to a change made in https://github.com/runtimeverification/kontrol/pull/825 to the `foundry.toml` parsing, this PR enforces reading the values set in both active and `default` profiles and using the default ones for values that are not set in the active profile. This PR also adds a `test_prove_legacy_profiles` test that ensures that both `default` and active profile's values are used. I do realise, however, that this behavior (other profiles inheriting from `default`) is non-standard, so I'd appreciate any feedback on this PR. Maybe it'd be better if I added another parameter in `get_profile` that would enable this behavior only if the function is called by Kontrol? --- pyk/src/pyk/cli/pyk.py | 4 +++- .../tests/unit/test-data/pyk_toml_test.toml | 5 ++++- pyk/src/tests/unit/test_toml_args.py | 22 +++++++++++++++++++ 3 files changed, 29 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index f4a50ce32a9..077f18358a4 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -579,7 +579,9 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s if len(profile_list) == 0 or profile_list[0] not in toml_profile: return {k: v for k, v in toml_profile.items() if type(v) is not dict} elif len(profile_list) == 1: - return {k: v for k, v in toml_profile[profile_list[0]].items() if type(v) is not dict} + active_profile = {k: v for k, v in toml_profile.get(profile_list[0], {}).items() if type(v) is not dict} + default_profile = {k: v for k, v in toml_profile.get('default', {}).items() if type(v) is not dict} + return {**default_profile, **active_profile} return get_profile(toml_profile[profile_list[0]], profile_list[1:]) toml_args: dict[str, Any] = {} 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..a374fe73737 100644 --- a/pyk/src/tests/unit/test-data/pyk_toml_test.toml +++ b/pyk/src/tests/unit/test-data/pyk_toml_test.toml @@ -6,9 +6,12 @@ definition = "/tmp" input = "kast-json" no-minimize = true -[prove-legacy] +[prove-legacy.default] kArgs = ["arg 1","args 2"] +[prove-legacy.verbose] +verbose = true + [coverage.a_profile] verbose = true output = "a-profile-file" \ No newline at end of file diff --git a/pyk/src/tests/unit/test_toml_args.py b/pyk/src/tests/unit/test_toml_args.py index 8f3db569e69..455e838eed3 100644 --- a/pyk/src/tests/unit/test_toml_args.py +++ b/pyk/src/tests/unit/test_toml_args.py @@ -62,6 +62,28 @@ def test_prove_legacy_kargs() -> None: assert len(args_dict['k_args']) == 2 +def test_prove_legacy_profiles() -> None: + parser = create_argument_parser() + cmd_args = [ + 'prove-legacy', + '--config-file', + str(TEST_TOML), + '--config-profile', + 'verbose', + tempfile.gettempdir(), + str(TEST_TOML), + str(TEST_TOML), + 'spec-module', + 'cmd_args', + ] + args = parser.parse_args(cmd_args) + args_dict = parse_toml_args(args) + assert len(args_dict['k_args']) == 2 + assert hasattr(args, 'verbose') + assert 'verbose' in args_dict + assert args_dict['verbose'] + + def test_toml_read() -> None: change_in_toml('definition = "(.*)"', f'definition = "{tempfile.gettempdir()}"') parser = create_argument_parser() From 5b3bdb5396bb60af2089a7d90e92a1e3b3e9876f Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 11 Oct 2024 17:24:47 -0600 Subject: [PATCH 3/3] Update dependency: deps/llvm-backend_release (#4659) 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 5d5322df683..5c5330a6efb 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.98 +0.1.99 diff --git a/flake.lock b/flake.lock index 4e61a7d413f..d462efff1a9 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1727813652, - "narHash": "sha256-x29OdXQARnaith+dz88R3O056tlJcC4VqFbFzlbqLEc=", + "lastModified": 1728677554, + "narHash": "sha256-9+xXyy2Pbw04RBOTgYcNv/ilNcUMwH3E12WtNNL0Ey0=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "812ea2ad00c91b7b5d144bd2624c7293802db45f", + "rev": "3db6947cb1c97a97bdcaf2ee990dbd18b7f251e7", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.98", + "ref": "v0.1.99", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 0f3c5c47467..2d6987874dc 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.98"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.99"; haskell-backend = { url = "github:runtimeverification/haskell-backend/v0.1.76"; 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 812ea2ad00c..3db6947cb1c 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 812ea2ad00c91b7b5d144bd2624c7293802db45f +Subproject commit 3db6947cb1c97a97bdcaf2ee990dbd18b7f251e7