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