From 2fb4bf7efc5c129aa69654620b7172ebde519c71 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 28 Aug 2024 11:27:12 -0600 Subject: [PATCH] Basic defunctionalization for building rules in K (#4610) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Currently, when we are converting a summarized K definition to a module, we have only used it for then feeding that module into the Haskell backend, which does not have the restriction that the generated rules cannot have functions on the LHS of them. Now Pi2 wants to also feed those rules into the LLVM backend, so it's needed that we can defunctionalize the LHS of those rules. This PR achieves that by threading through the needed options to `cterm_build_rule` to defunctionalize the LHS of generated rules. In particular: - Some bugs in the imports of https://github.com/runtimeverification/k/pull/4607 are fixed. Imports are made relative, and a circular import path is broken. - A routine `defunctionalize(KDefinition, KInner) -> tuple[Kinner, list[KInner]]` is added to `kast.manip`, which replaces functions in the supplied term with variables and returns also a list of constraints binding those variables to their original terms. - A unit test-harness, and many tests, are added of the `defunctionalize` routine. - An integration test of `cterm_build_rule` defunctionalization is added over the `simple_proofs.k` test harness. - The "functions" `.Map`, `.Set`, `.List`, and `.RangeMap` are added to the list of "not actually functions, more like constructors" for considering when deciding if something is a function or a constructor. This is exercised by the added test because `.Map` shows up, but is not defunctionalized. - `KCFG.edge.to_rule`, `cterm_build_rule`, and `build_rule` now take an optional `KDefinition`, and if it's supplied, will defunctionalize the LHS of generated rules that it makes. - The routine in `kast.manip` named `minimize_rule` is renamed to `minimize_rule_like`, to reflect better its type. - `KCFG.edge.to_rule` now takes an optional `minimize: bool` parameter, which if supplied will run the `minimize_rule_like` routine over the generated rule. --------- Co-authored-by: Tamás Tóth --- pyk/src/pyk/__main__.py | 4 +- pyk/src/pyk/cterm/cterm.py | 14 ++- pyk/src/pyk/kast/manip.py | 37 ++++++- pyk/src/pyk/kast/outer.py | 4 + pyk/src/pyk/kcfg/exploration.py | 3 +- pyk/src/pyk/kcfg/kcfg.py | 20 ++-- pyk/src/pyk/kcfg/minimize.py | 6 +- pyk/src/pyk/kcfg/show.py | 4 +- .../tests/integration/cterm/test_simple.py | 48 +++++++-- .../integration/proof/test_refute_node.py | 3 +- pyk/src/tests/unit/kast/test_manip.py | 97 +++++++++++++++++++ 11 files changed, 215 insertions(+), 25 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 86b83c8d108..9f1c2dc871f 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -22,7 +22,7 @@ from .kast.inner import KInner from .kast.manip import ( flatten_label, - minimize_rule, + minimize_rule_like, minimize_term, propagate_up_constraints, remove_source_map, @@ -394,7 +394,7 @@ def exec_coverage(options: CoverageOptions) -> None: definition = remove_source_map(read_kast_definition(kompiled_dir / 'compiled.json')) pretty_printer = PrettyPrinter(definition) for rid in options.coverage_file: - rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip()))) + rule = minimize_rule_like(strip_coverage_logger(get_rule_by_id(definition, rid.strip()))) options.output_file.write('\n\n') options.output_file.write('Rule: ' + rid.strip()) options.output_file.write('\nUnparsed:\n') diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 7fc790eced0..10f9f1cb526 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -367,6 +367,7 @@ def cterm_build_rule( final_cterm: CTerm, priority: int | None = None, keep_vars: Iterable[str] = (), + defunc_with: KDefinition | None = None, ) -> tuple[KRule, Subst]: """Return a `KRule` between the supplied initial and final states. @@ -375,6 +376,8 @@ def cterm_build_rule( init_cterm: State to put on LHS of the rule (constraints interpreted as `requires` clause). final_cterm: State to put on RHS of the rule (constraints interpreted as `ensures` clause). keep_vars: Variables to leave in the side-conditions even if not bound in the configuration. + priority: Priority index to use for generated rules. + defunc_with (optional): KDefinition to be able to defunctionalize LHS appropriately. Returns: A tuple ``(rule, var_map)`` where @@ -386,4 +389,13 @@ def cterm_build_rule( """ init_config, *init_constraints = init_cterm final_config, *final_constraints = final_cterm - return build_rule(rule_id, init_config, final_config, init_constraints, final_constraints, priority, keep_vars) + return build_rule( + rule_id, + init_config, + final_config, + init_constraints, + final_constraints, + priority, + keep_vars, + defunc_with=defunc_with, + ) diff --git a/pyk/src/pyk/kast/manip.py b/pyk/src/pyk/kast/manip.py index 92c8ae03a3b..932397bf80c 100644 --- a/pyk/src/pyk/kast/manip.py +++ b/pyk/src/pyk/kast/manip.py @@ -6,7 +6,7 @@ from ..prelude.k import DOTS, GENERATED_TOP_CELL from ..prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool -from ..prelude.ml import is_top, mlAnd, mlBottom, mlEqualsTrue, mlImplies, mlOr, mlTop +from ..prelude.ml import is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlOr, mlTop from ..utils import find_common_items, hash_str, unique from .att import EMPTY_ATT, Atts, KAtt, WithKAtt from .inner import ( @@ -543,7 +543,7 @@ def minimize_term( return term -def minimize_rule(rule: RL, keep_vars: Iterable[str] = ()) -> RL: +def minimize_rule_like(rule: RL, keep_vars: Iterable[str] = ()) -> RL: """Minimize a K rule or claim for pretty-printing. - Variables only used once will be removed. @@ -756,6 +756,7 @@ def build_rule( final_constraints: Iterable[KInner] = (), priority: int | None = None, keep_vars: Iterable[str] = (), + defunc_with: KDefinition | None = None, ) -> tuple[KRule, Subst]: """Return a `KRule` between the supplied initial and final states. @@ -765,7 +766,9 @@ def build_rule( final_config: State to put on RHS of the rule. init_constraints: Constraints to use as `requires` clause. final_constraints: Constraints to use as `ensures` clause. + priority: Priority index to assign to generated rules. keep_vars: Variables to leave in the side-conditions even if not bound in the configuration. + defunc_with: KDefinition for filtering out function symbols on LHS of rules. Returns: A tuple ``(rule, var_map)`` where @@ -778,6 +781,9 @@ def build_rule( init_constraints = [normalize_ml_pred(c) for c in init_constraints] final_constraints = [normalize_ml_pred(c) for c in final_constraints] final_constraints = [c for c in final_constraints if c not in init_constraints] + if defunc_with is not None: + init_config, new_constraints = defunctionalize(defunc_with, init_config) + init_constraints = init_constraints + new_constraints init_term = mlAnd([init_config] + init_constraints) final_term = mlAnd([final_config] + final_constraints) @@ -854,3 +860,30 @@ def _no_cell_rewrite_to_dots(_term: KInner) -> KInner: subst = Subst({cell_name: _no_cell_rewrite_to_dots(cell_contents) for cell_name, cell_contents in _subst.items()}) return subst(config) + + +def defunctionalize(defn: KDefinition, kinner: KInner) -> tuple[KInner, list[KInner]]: + """Turn non-constructor arguments into side-conditions so that a term is only constructor-like. + + Args: + defn: The definition to pull function label information from. + kinner: The term to defunctionalize. + + Returns: + A tuple of the defunctionalized term and the list of constraints generated. + """ + function_symbols = [prod.klabel for prod in defn.functions if prod.klabel is not None] + constraints: list[KInner] = [] + + def _defunctionalize(_kinner: KInner) -> KInner: + if type(_kinner) is KApply and _kinner.label in function_symbols: + sort = defn.sort(_kinner) + assert sort is not None + new_var = abstract_term_safely(_kinner, base_name='F', sort=sort) + var_constraint = mlEquals(new_var, _kinner, arg_sort=sort) + constraints.append(var_constraint) + return new_var + return _kinner + + new_kinner = top_down(_defunctionalize, kinner) + return (new_kinner, list(unique(constraints))) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index 9cfd4fc7e27..5e48cab209a 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -864,6 +864,10 @@ def is_not_actually_function(label: str) -> bool: '_List_', '_Map_', '_RangeMap_', + '.Set', + '.List', + '.Map', + '.RangeMap', 'SetItem', 'ListItem', '_|->_', diff --git a/pyk/src/pyk/kcfg/exploration.py b/pyk/src/pyk/kcfg/exploration.py index 98e27b11b7f..406ecccc254 100644 --- a/pyk/src/pyk/kcfg/exploration.py +++ b/pyk/src/pyk/kcfg/exploration.py @@ -3,6 +3,7 @@ from typing import TYPE_CHECKING from pyk.kcfg.kcfg import KCFG, NodeAttr +from pyk.kcfg.minimize import KCFGMinimizer if TYPE_CHECKING: from collections.abc import Iterable, Mapping @@ -109,4 +110,4 @@ def to_dict(self) -> dict[str, Any]: # Minimizing the KCFG def minimize_kcfg(self) -> None: - self.kcfg.minimize() + KCFGMinimizer(self.kcfg).minimize() diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 88ffa00d9bf..2da3d3e9210 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -18,13 +18,13 @@ extract_rhs, flatten_label, inline_cell_maps, + minimize_rule_like, rename_generated_vars, sort_ac_collections, ) from ..kast.outer import KFlatModule from ..prelude.kbool import andBool from ..utils import ensure_dir_path, not_none -from .minimize import KCFGMinimizer if TYPE_CHECKING: from collections.abc import Iterable, Mapping, MutableMapping @@ -218,7 +218,14 @@ def to_dict(self) -> dict[str, Any]: def from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) -> KCFG.Edge: return KCFG.Edge(nodes[dct['source']], nodes[dct['target']], dct['depth'], tuple(dct['rules'])) - def to_rule(self, label: str, claim: bool = False, priority: int | None = None) -> KRuleLike: + def to_rule( + self, + label: str, + claim: bool = False, + priority: int | None = None, + defunc_with: KDefinition | None = None, + minimize: bool = False, + ) -> KRuleLike: def is_ceil_condition(kast: KInner) -> bool: return type(kast) is KApply and kast.label.name == '#Ceil' @@ -234,7 +241,11 @@ def _simplify_config(config: KInner) -> KInner: if claim: rule, _ = cterm_build_claim(sentence_id, init_cterm, target_cterm) else: - rule, _ = cterm_build_rule(sentence_id, init_cterm, target_cterm, priority=priority) + rule, _ = cterm_build_rule( + sentence_id, init_cterm, target_cterm, priority=priority, defunc_with=defunc_with + ) + if minimize: + rule = minimize_rule_like(rule) return rule def replace_source(self, node: KCFG.Node) -> KCFG.Edge: @@ -1234,9 +1245,6 @@ def write_cfg_data(self) -> None: self._deleted_nodes.clear() self._created_nodes.clear() - def minimize(self) -> None: - KCFGMinimizer(self).minimize() - @staticmethod def read_cfg_data(cfg_dir: Path) -> KCFG: store = KCFGStore(cfg_dir) diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py index 5b6fb8b0577..32945a7269d 100644 --- a/pyk/src/pyk/kcfg/minimize.py +++ b/pyk/src/pyk/kcfg/minimize.py @@ -3,13 +3,13 @@ from functools import reduce from typing import TYPE_CHECKING -from pyk.cterm import CTerm -from pyk.utils import not_none, single +from ..cterm import CTerm +from ..utils import not_none, single if TYPE_CHECKING: from collections.abc import Callable - from pyk.kcfg.kcfg import KCFG, NodeIdLike + from .kcfg import KCFG, NodeIdLike class KCFGMinimizer: diff --git a/pyk/src/pyk/kcfg/show.py b/pyk/src/pyk/kcfg/show.py index 8a6aec3006e..6ace8d1abd8 100644 --- a/pyk/src/pyk/kcfg/show.py +++ b/pyk/src/pyk/kcfg/show.py @@ -9,7 +9,7 @@ from ..kast.manip import ( flatten_label, inline_cell_maps, - minimize_rule, + minimize_rule_like, minimize_term, ml_pred_to_bool, push_down_rewrites, @@ -316,7 +316,7 @@ def _process_sentence(sent: KSentence) -> KSentence: sent = sent.let(body=KCFGShow.hide_cells(sent.body, omit_cells)) if parseable_output: sent = sent.let(body=remove_generated_cells(sent.body)) - sent = minimize_rule(sent) + sent = minimize_rule_like(sent) return sent module = cfg.to_module(module_name) diff --git a/pyk/src/tests/integration/cterm/test_simple.py b/pyk/src/tests/integration/cterm/test_simple.py index e461bef15ab..9ec4d4fc51f 100644 --- a/pyk/src/tests/integration/cterm/test_simple.py +++ b/pyk/src/tests/integration/cterm/test_simple.py @@ -4,11 +4,9 @@ import pytest -from pyk.cterm import CTerm +from pyk.cterm import CTerm, cterm_build_rule from pyk.kast.inner import KApply, KSequence, KToken, KVariable -from pyk.prelude.kint import leInt from pyk.prelude.ml import mlEqualsTrue, mlTop -from pyk.prelude.utils import token from pyk.testing import CTermSymbolicTest, KPrintTest from ..utils import K_FILES @@ -18,7 +16,6 @@ from typing import Final, Union from pyk.cterm import CTermSymbolic - from pyk.kast.inner import KInner from pyk.ktool.kprint import KPrint STATE = Union[tuple[str, str], tuple[str, str, str]] @@ -38,9 +35,13 @@ SIMPLIFY_TEST_DATA: Final = (('bytes-return', ('mybytes', '.Map'), (r'b"\x00\x90\xa0\n\xa1\xf1a" ~> .K', '.Map')),) - -def le_int(n: int, var: str) -> KInner: - return mlEqualsTrue(leInt(token(n), KVariable(var))) +BUILD_RULE_TEST_DATA: Final = ( + ( + 'functional-lhs', + (('mybytes', '.Map'), (r'mybytes ~> .K', '.Map')), + ('( F_e096a1bd:KItem => mybytes )', '.Map', 'F_e096a1bd:KItem ==K mybytes', 'true'), + ), +) class TestSimpleProof(CTermSymbolicTest, KPrintTest): @@ -130,3 +131,36 @@ def test_simplify( # Then assert actual_k == expected_k assert actual_state == expected_state + + @pytest.mark.parametrize( + 'test_id,pre,expected_post', + BUILD_RULE_TEST_DATA, + ids=[test_id for test_id, *_ in BUILD_RULE_TEST_DATA], + ) + def test_cterm_build_rule( + self, + cterm_symbolic: CTermSymbolic, + kprint: KPrint, + test_id: str, + pre: tuple[tuple[str, str, str | None], tuple[str, str, str | None]], + expected_post: tuple[str, str, str | None, str | None], + ) -> None: + # Given + lhs, rhs = pre + expected_k, expected_state, expected_requires, expected_ensures = expected_post + + # When + config_lhs = self.config(kprint, *lhs) + config_rhs = self.config(kprint, *rhs) + rule, _ = cterm_build_rule(test_id, config_lhs, config_rhs, defunc_with=kprint.definition) + rule_body_cterm = CTerm.from_kast(rule.body) + rule_k = kprint.pretty_print(rule_body_cterm.cell('K_CELL')) + rule_state = kprint.pretty_print(rule_body_cterm.cell('STATE_CELL')) + rule_requires = kprint.pretty_print(rule.requires) + rule_ensures = kprint.pretty_print(rule.ensures) + + # Then + assert rule_k == expected_k + assert rule_state == expected_state + assert rule_requires == expected_requires + assert rule_ensures == expected_ensures diff --git a/pyk/src/tests/integration/proof/test_refute_node.py b/pyk/src/tests/integration/proof/test_refute_node.py index 69f5a28bb7e..5203f12a79c 100644 --- a/pyk/src/tests/integration/proof/test_refute_node.py +++ b/pyk/src/tests/integration/proof/test_refute_node.py @@ -11,6 +11,7 @@ from pyk.kast.manip import free_vars from pyk.kast.outer import KClaim from pyk.kcfg import KCFG +from pyk.kcfg.minimize import KCFGMinimizer from pyk.kcfg.semantics import KCFGSemantics from pyk.prelude.kint import gtInt, intToken, leInt from pyk.prelude.ml import is_top, mlEqualsTrue @@ -372,7 +373,7 @@ def test_apr_proof_refute_node_multiple_constraints( prover.advance_proof(proof, max_iterations=4) # After the minimization, nodes 7-10 created by the advancement of the proof # will have multiple constraints in their immediately preceding splits - proof.kcfg.minimize() + KCFGMinimizer(proof.kcfg).minimize() # Then for i in [7, 8, 9, 10]: diff --git a/pyk/src/tests/unit/kast/test_manip.py b/pyk/src/tests/unit/kast/test_manip.py index 71a52f06e8f..093ed8a2690 100644 --- a/pyk/src/tests/unit/kast/test_manip.py +++ b/pyk/src/tests/unit/kast/test_manip.py @@ -5,10 +5,13 @@ import pytest +from pyk.kast import EMPTY_ATT, KAtt +from pyk.kast.att import Atts from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KToken, KVariable, Subst from pyk.kast.manip import ( bool_to_ml_pred, collapse_dots, + defunctionalize, indexed_rewrite, is_term_like, minimize_term, @@ -20,14 +23,17 @@ simplify_bool, split_config_from, ) +from pyk.kast.outer import KDefinition, KFlatModule, KNonTerminal, KProduction, KTerminal from pyk.prelude.k import DOTS, GENERATED_TOP_CELL from pyk.prelude.kbool import BOOL, FALSE, TRUE, andBool, notBool from pyk.prelude.kint import INT, intToken from pyk.prelude.ml import mlAnd, mlBottom, mlEqualsFalse, mlEqualsTrue, mlNot, mlTop +from pyk.prelude.utils import token from ..utils import a, b, c, f, k, x if TYPE_CHECKING: + from collections.abc import Iterable from typing import Final from pyk.kast import KInner @@ -543,3 +549,94 @@ def test_is_term_like(test_id: str, kast: KInner, expected: bool) -> None: ) def test_indexed_rewrite(test_id: str, kast: KInner, rewrites: list[KRewrite], expected: KInner) -> None: assert indexed_rewrite(kast, rewrites) == expected + + +add: Final = KLabel('_+_') +init_s: Final = KLabel('init_s') +to_s: Final = KLabel('to_s') +to_s_2: Final = KLabel('to_s_2') +to_int: Final = KLabel('to_int') + + +def production(klabel: KLabel, sort: KSort, items: Iterable[KSort | str], function: bool) -> KProduction: + _items = tuple(KNonTerminal(item) if isinstance(item, KSort) else KTerminal(item) for item in items) + att = EMPTY_ATT if not function else KAtt((Atts.FUNCTION(None),)) + return KProduction(sort=sort, items=_items, klabel=klabel, att=att) + + +def var_equals(var: str, term: KInner) -> KInner: + return KApply( + KLabel( + '#Equals', + params=( + INT, + GENERATED_TOP_CELL, + ), + ), + [KVariable(var, sort=INT), term], + ) + + +S: Final = KSort('S') +DEFINITION: Final = KDefinition( + main_module_name='TEST', + all_modules=( + KFlatModule( + name='TEST', + sentences=( + production(add, INT, (INT, '+', INT), True), + production(init_s, S, (), False), + production(to_s, S, (INT,), False), + production( + to_s_2, + S, + ( + INT, + S, + ), + False, + ), + production(to_int, INT, (S,), True), + ), + ), + ), +) +TEST_DATA: tuple[tuple[KInner, KInner, list[KInner]], ...] = ( + ( + add(token(1), token(2)), + KVariable('F_eefa6e95', sort=INT), + [var_equals('F_eefa6e95', add(token(1), token(2)))], + ), + (to_s(token(1)), to_s(token(1)), []), + ( + to_s(to_int(to_s(add(token(1), token(2))))), + to_s(KVariable('F_a8146589', sort=INT)), + [var_equals('F_a8146589', to_int(to_s(add(token(1), token(2)))))], + ), + ( + to_s_2(add(token(1), token(2)), init_s()), + to_s_2(KVariable('F_eefa6e95', sort=INT), init_s()), + [var_equals('F_eefa6e95', add(token(1), token(2)))], + ), + (to_s_2(token(1), init_s()), to_s_2(token(1), init_s()), []), + ( + to_s_2(add(token(1), token(2)), to_s(add(token(1), token(2)))), + to_s_2(KVariable('F_eefa6e95', INT), to_s(KVariable('F_eefa6e95', INT))), + [var_equals('F_eefa6e95', add(token(1), token(2)))], + ), + ( + to_s_2(add(token(1), token(2)), to_s(to_int(init_s()))), + to_s_2(KVariable('F_eefa6e95', INT), to_s(KVariable('F_3294e1be', INT))), + [var_equals('F_eefa6e95', add(token(1), token(2))), var_equals('F_3294e1be', to_int(init_s()))], + ), +) + + +@pytest.mark.parametrize('input,expected_output,expected_constraints', TEST_DATA, ids=count()) +def test_defunctionalize(input: KInner, expected_output: KInner, expected_constraints: list[KInner]) -> None: + # When + actual_output, actual_constraints = defunctionalize(DEFINITION, input) + + # Then + assert actual_output == expected_output + assert actual_constraints == expected_constraints