From 5bae74047037d0916b9e5a8b319a6122e1703de8 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Wed, 7 Aug 2024 14:50:54 -0600 Subject: [PATCH 1/3] Update dependency: deps/llvm-backend_release (#4565) Co-authored-by: devops Co-authored-by: Dwight Guth Co-authored-by: Roberto Rosmaninho --- .github/workflows/Dockerfile | 1 + README.md | 1 + deps/llvm-backend_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- install-build-deps | 1 + llvm-backend/src/main/native/llvm-backend | 2 +- package/debian/kframework/control.jammy | 2 +- pyk/src/pyk/kllvm/convert.py | 4 ++-- pyk/src/tests/integration/kllvm/test_patterns.py | 2 +- pyk/src/tests/integration/test_string.py | 9 +++++++++ 11 files changed, 23 insertions(+), 11 deletions(-) diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index 7f7197756a9..422333bb4e6 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -65,6 +65,7 @@ RUN apt-get update \ python3-dev \ python3-distutils \ python3-pip \ + xxd \ zlib1g-dev COPY --from=Z3 /usr/bin/z3 /usr/bin/z3 diff --git a/README.md b/README.md index 7a4f9fe2895..ea1be3d0d2e 100644 --- a/README.md +++ b/README.md @@ -104,6 +104,7 @@ The following dependencies are needed either at build time or runtime: * [pkg-config](https://www.freedesktop.org/wiki/Software/pkg-config/) * [python](https://www.python.org) * [stack](https://docs.haskellstack.org/en/stable/README/) +* [xxd](https://github.com/vim/vim/blob/master/runtime/doc/xxd.man) * [zlib](https://www.zlib.net/) * [z3](https://github.com/Z3Prover/z3) (on some distributions libz3 is also needed and packaged separately) Note that you need version 4.12.1 of Z3, diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 9adbab1b3a2..d9ba7470869 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.69 +0.1.75 diff --git a/flake.lock b/flake.lock index 90fb6ea5de0..18b4fa3950e 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1722454948, - "narHash": "sha256-8mcRIlTAmQ1J3oxi0QibxmSlFWkOTRlyWy5kSHJFf6U=", + "lastModified": 1722973323, + "narHash": "sha256-lD8Mc5sftYa4pqyUoglFzYDzTXiJ7m/SiMbeKy2tn2c=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "5be14fe74740a15cb707c102425032ffdee98281", + "rev": "9cb2137d96059c8751bb57216cc1d0cea5746161", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.69", + "ref": "v0.1.75", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 80d9fa75a6c..48ca100e172 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.69"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.75"; haskell-backend = { url = "github:runtimeverification/haskell-backend/v0.1.58"; inputs.rv-utils.follows = "llvm-backend/rv-utils"; diff --git a/install-build-deps b/install-build-deps index ee741eca574..d89338691f9 100755 --- a/install-build-deps +++ b/install-build-deps @@ -34,6 +34,7 @@ inst_Debian() { pkg-config \ python3 \ python3-dev \ + xxd \ z3 \ zlib1g-dev diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 5be14fe7474..9cb2137d960 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 5be14fe74740a15cb707c102425032ffdee98281 +Subproject commit 9cb2137d96059c8751bb57216cc1d0cea5746161 diff --git a/package/debian/kframework/control.jammy b/package/debian/kframework/control.jammy index 635e40cb2d9..b8b3a5acdbf 100644 --- a/package/debian/kframework/control.jammy +++ b/package/debian/kframework/control.jammy @@ -2,7 +2,7 @@ Source: kframework Section: devel Priority: optional Maintainer: Dwight Guth -Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev +Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , xxd , zlib1g-dev Standards-Version: 3.9.6 Homepage: https://github.com/runtimeverification/k diff --git a/pyk/src/pyk/kllvm/convert.py b/pyk/src/pyk/kllvm/convert.py index a705ab8f170..0b68505dc96 100644 --- a/pyk/src/pyk/kllvm/convert.py +++ b/pyk/src/pyk/kllvm/convert.py @@ -108,7 +108,7 @@ def sentence_to_llvm(sentence: Sentence) -> kllvm.Declaration: def pattern_to_llvm(pattern: Pattern) -> kllvm.Pattern: match pattern: case String(value): - return kllvm.StringPattern(value) + return kllvm.StringPattern(value.encode('latin-1')) case VarPattern(name, sort): return kllvm.VariablePattern(name, sort_to_llvm(sort)) case App(symbol, sorts, args): @@ -201,7 +201,7 @@ def llvm_to_sentence(decl: kllvm.Declaration) -> Sentence: def llvm_to_pattern(pattern: kllvm.Pattern) -> Pattern: match pattern: case kllvm.StringPattern(): # type: ignore - return String(pattern.contents) + return String(pattern.contents.decode('latin-1')) case kllvm.VariablePattern(): # type: ignore if pattern.name and pattern.name[0] == '@': return SVar(pattern.name, llvm_to_sort(pattern.sort)) diff --git a/pyk/src/tests/integration/kllvm/test_patterns.py b/pyk/src/tests/integration/kllvm/test_patterns.py index 20b07cf9b5a..d6c6bfff44c 100644 --- a/pyk/src/tests/integration/kllvm/test_patterns.py +++ b/pyk/src/tests/integration/kllvm/test_patterns.py @@ -50,7 +50,7 @@ def test_string() -> None: # Then assert str(pattern) == '"abc"' - assert pattern.contents == 'abc' + assert pattern.contents.decode('latin-1') == 'abc' def test_variable() -> None: diff --git a/pyk/src/tests/integration/test_string.py b/pyk/src/tests/integration/test_string.py index 2847e05ab7c..699542bd180 100644 --- a/pyk/src/tests/integration/test_string.py +++ b/pyk/src/tests/integration/test_string.py @@ -40,6 +40,12 @@ '🙂', ) +SKIPPED_BINDINGS_TESTS: Final = { + '𐍈', + '武天老師', + '🙂', +} + KOMPILE_DEFINITION = """ module STRING-REWRITE imports STRING-SYNTAX @@ -217,6 +223,9 @@ def test_krun(backend: str, definition_dir: Path, text: str) -> None: def test_bindings(runtime: Runtime, text: str) -> None: from pyk.kllvm.convert import llvm_to_pattern, pattern_to_llvm + if text in SKIPPED_BINDINGS_TESTS: + pytest.skip() + # Given kore = kore_config(text, '') expected = kore_config(None, text) 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 2/3] 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, ()), ), From d55c98fa966041c027c8a86137b31a08a4dc54f5 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Thu, 8 Aug 2024 06:03:34 -0500 Subject: [PATCH 3/3] Optimizations for `write_cfg_data` (#4569) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Makes progress in fixing the slowdown as proofs get large. I'll call the "sync time" the time in between receiving a step result and starting to wait for the next step result on the master thread. As proofs get more and more nodes, calling `to_dict()` on every node gets progressively harder and this was taking up a substantial portion of the sync time as proofs got to 500+ nodes. Instead of generating the entire KCFG dict with `KCFG.to_dict()` before passing this to `KCFGStore.write_cfg_data()`, which discards all of this work anyway for the final product and replaces it with just a list of the node IDs, it is significantly faster to just pass it the list of the node IDs and have it use the KCFG object, which already has a dictionary storing nodes by ID to find the vacuous and stuck nodes, and to get the newly created nodes. This way we can call `to_dict()` on each node only when it is first created. To give an idea of a benchmark, I used a `LoopsTest.test_sum_1000()` (linear and long-running) with `--max-depth 1` and `--max-iterations 1000`. Before this change it gets to 1000 iterations in 59:06, and after this change it does it in 40:31. Before the change the sync time as this proof approached 1000 nodes ranged between about 3.4 to 4.2 seconds. After the change ranged from about 1.39 to 1.54 seconds. The big remaining chunk of sync time when the proof gets large seems to be in `get_steps()`. --------- Co-authored-by: Petar Maksimović --- pyk/src/pyk/kcfg/kcfg.py | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index f8c4dfe479b..d3f9247e49f 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -73,23 +73,18 @@ def kcfg_node_path(self, node_id: int) -> Path: return self.kcfg_node_dir / f'{node_id}.json' def write_cfg_data( - self, dct: dict[str, Any], deleted_nodes: Iterable[int] = (), created_nodes: Iterable[int] = () + self, kcfg: KCFG, dct: dict[str, Any], deleted_nodes: Iterable[int] = (), created_nodes: Iterable[int] = () ) -> None: - node_dict = {node_dct['id']: node_dct for node_dct in dct['nodes']} vacuous_nodes = [ - node_id for node_id in node_dict.keys() if KCFGNodeAttr.VACUOUS.value in node_dict[node_id]['attrs'] - ] - stuck_nodes = [ - node_id for node_id in node_dict.keys() if KCFGNodeAttr.STUCK.value in node_dict[node_id]['attrs'] + node_id for node_id in kcfg._nodes.keys() if KCFGNodeAttr.VACUOUS in kcfg._nodes[node_id].attrs ] + stuck_nodes = [node_id for node_id in kcfg._nodes.keys() if KCFGNodeAttr.STUCK in kcfg._nodes[node_id].attrs] dct['vacuous'] = vacuous_nodes dct['stuck'] = stuck_nodes for node_id in deleted_nodes: self.kcfg_node_path(node_id).unlink(missing_ok=True) for node_id in created_nodes: - del node_dict[node_id]['attrs'] - self.kcfg_node_path(node_id).write_text(json.dumps(node_dict[node_id])) - dct['nodes'] = list(node_dict.keys()) + self.kcfg_node_path(node_id).write_text(json.dumps(kcfg._nodes[node_id].to_dict())) self.kcfg_json_path.write_text(json.dumps(dct)) def read_cfg_data(self) -> dict[str, Any]: @@ -542,6 +537,26 @@ def extend( case _: raise AssertionError() + def to_dict_no_nodes(self) -> dict[str, Any]: + nodes = list(self._nodes.keys()) + edges = [edge.to_dict() for edge in self.edges()] + covers = [cover.to_dict() for cover in self.covers()] + splits = [split.to_dict() for split in self.splits()] + ndbranches = [ndbranch.to_dict() for ndbranch in self.ndbranches()] + + aliases = dict(sorted(self._aliases.items())) + + res = { + 'next': self._node_id, + 'nodes': nodes, + 'edges': edges, + 'covers': covers, + 'splits': splits, + 'ndbranches': ndbranches, + 'aliases': aliases, + } + return {k: v for k, v in res.items() if v} + def to_dict(self) -> dict[str, Any]: nodes = [node.to_dict() for node in self.nodes] edges = [edge.to_dict() for edge in self.edges()] @@ -1261,7 +1276,7 @@ def reachable_nodes(self, source_id: NodeIdLike, *, reverse: bool = False) -> se def write_cfg_data(self) -> None: assert self._kcfg_store is not None self._kcfg_store.write_cfg_data( - self.to_dict(), deleted_nodes=self._deleted_nodes, created_nodes=self._created_nodes + self, self.to_dict_no_nodes(), deleted_nodes=self._deleted_nodes, created_nodes=self._created_nodes ) self._deleted_nodes.clear() self._created_nodes.clear()