diff --git a/pyk/src/pyk/kast/att.py b/pyk/src/pyk/kast/att.py index b428e79a2c5..3c22d79a128 100644 --- a/pyk/src/pyk/kast/att.py +++ b/pyk/src/pyk/kast/att.py @@ -316,6 +316,7 @@ class Atts: GROUP: Final = AttKey('group', type=_STR) HAS_DOMAIN_VALUES: Final = AttKey('hasDomainValues', type=_NONE) HOOK: Final = AttKey('hook', type=_ANY) + HYBRID: Final = AttKey('hybrid', type=OptionalType(_STR)) IDEM: Final = AttKey('idem', type=_NONE) IMPURE: Final = AttKey('impure', type=_NONE) INDEX: Final = AttKey('index', type=_INT) @@ -338,12 +339,14 @@ class Atts: PRIVATE: Final = AttKey('private', type=_NONE) PRODUCTION: Final = AttKey('org.kframework.definition.Production', type=_ANY) PROJECTION: Final = AttKey('projection', type=_NONE) + PUBLIC: Final = AttKey('public', type=_NONE) RIGHT: Final = AttKey('right', type=_ANY) # RIGHT and RIGHT_INTERNAL on the Frontend RETURNS_UNIT: Final = AttKey('returnsUnit', type=_NONE) SIMPLIFICATION: Final = AttKey('simplification', type=_ANY) SEQSTRICT: Final = AttKey('seqstrict', type=_ANY) SORT: Final = AttKey('org.kframework.kore.Sort', type=_ANY) SOURCE: Final = AttKey('org.kframework.attributes.Source', type=_PATH) + STREAM: Final = AttKey('stream', type=OptionalType(_STR)) SMTLEMMA: Final = AttKey('smt-lemma', type=_NONE) STRICT: Final = AttKey('strict', type=_ANY) SYMBOL: Final = AttKey('symbol', type=_STR) @@ -358,6 +361,7 @@ class Atts: UNIT: Final = AttKey('unit', type=_STR) UNIQUE_ID: Final = AttKey('UNIQUE_ID', type=_ANY) UNPARSE_AVOID: Final = AttKey('unparseAvoid', type=_NONE) + UNUSED: Final = AttKey('unused', type=_NONE) UPDATE: Final = AttKey('update', type=_ANY) USER_LIST: Final = AttKey('userList', type=_ANY) WRAP_ELEMENT: Final = AttKey('wrapElement', type=_ANY) diff --git a/pyk/src/pyk/konvert/_module_to_kore.py b/pyk/src/pyk/konvert/_module_to_kore.py index 2646a45eff8..9d6d0622505 100644 --- a/pyk/src/pyk/konvert/_module_to_kore.py +++ b/pyk/src/pyk/konvert/_module_to_kore.py @@ -747,6 +747,7 @@ def simplified_module(definition: KDefinition, module_name: str | None = None) - Atts.EXIT, Atts.FORMAT, Atts.GROUP, + Atts.HYBRID, Atts.INDEX, Atts.INITIALIZER, Atts.LEFT, @@ -757,17 +758,21 @@ def simplified_module(definition: KDefinition, module_name: str | None = None) - Atts.PRIVATE, Atts.PRODUCTION, Atts.PROJECTION, + Atts.PUBLIC, Atts.RETURNS_UNIT, Atts.RIGHT, Atts.SEQSTRICT, + Atts.STREAM, Atts.STRICT, Atts.TYPE, Atts.TERMINATOR_SYMBOL, + Atts.UNUSED, Atts.USER_LIST, Atts.WRAP_ELEMENT, ], ), DiscardHookAtts(), + DiscardPolymorphicSentences(), AddImpureAtts(), AddSymbolAtts(Atts.MACRO(None), _is_macro), AddSymbolAtts(Atts.FUNCTIONAL(None), _is_functional), @@ -1253,6 +1258,42 @@ def _update(self, production: KProduction) -> KProduction: return production.let(att=production.att.discard(self.keys)) +@dataclass +class DiscardPolymorphicSentences(SingleModulePass): + """Java compatibility: remove rules for polymorphic function labels. + + Java's ComputeTransitiveFunctionDependencies looks up rules by the + post-sort-injection KLabel (e.g. ite{K}), but the production's + attributesFor() key is the parametric form (e.g. ite{SortSort}), so no + rules are ever found and impurity does not propagate through polymorphic + functions. Removing those rules here mirrors that behaviour and avoids + special-casing the quirk in every downstream pass. + + Remove this pass (and re-enable the rules) once Java correctly handles + polymorphic function rules in its dependency analysis. + """ + + def _transform_module(self, module: KFlatModule) -> KFlatModule: + poly_labels = { + prod.klabel.name + for prod in module.productions + if prod.klabel and prod.klabel.params and Atts.FUNCTION in prod.att + } + if not poly_labels: + return module + return module.let(sentences=(sent for sent in module.sentences if not self._is_poly_rule(sent, poly_labels))) + + @staticmethod + def _is_poly_rule(sentence: object, poly_labels: set[str]) -> bool: + if not isinstance(sentence, KRule): + return False + match sentence.body: + case KRewrite(KApply(KLabel(label)), _): + return label in poly_labels + case _: + return False + + # ----------------- # Syntax attributes # ----------------- diff --git a/pyk/src/tests/integration/konvert/test_module_to_kore.py b/pyk/src/tests/integration/konvert/test_module_to_kore.py index 7af929740aa..acfc3b523d4 100644 --- a/pyk/src/tests/integration/konvert/test_module_to_kore.py +++ b/pyk/src/tests/integration/konvert/test_module_to_kore.py @@ -16,7 +16,7 @@ if TYPE_CHECKING: from collections.abc import Container from pathlib import Path - from typing import Final + from typing import Any, Final from pytest import FixtureRequest @@ -25,7 +25,14 @@ from pyk.testing import Kompiler -DEFINITION_FILES: Final = tuple((TEST_DATA_DIR / 'module-to-kore').glob('*.k')) +MODULE_TO_KORE_DIR: Final = TEST_DATA_DIR / 'module-to-kore' + +# Extra kompile kwargs for files that need non-default options. +EXTRA_KOMPILE_ARGS: Final[dict[str, dict[str, Any]]] = { + 'coverage.k': {'coverage': True}, +} + +DEFINITION_FILES: Final = tuple(MODULE_TO_KORE_DIR.glob('*.k')) @pytest.fixture( @@ -33,7 +40,9 @@ ids=[file.name for file in DEFINITION_FILES], ) def definition_dir(request: FixtureRequest, kompile: Kompiler) -> Path: - return kompile(main_file=request.param) + path: Path = request.param + extra = EXTRA_KOMPILE_ARGS.get(path.name, {}) + return kompile(main_file=path, **extra) @pytest.fixture diff --git a/pyk/src/tests/integration/test-data/module-to-kore/coverage.k b/pyk/src/tests/integration/test-data/module-to-kore/coverage.k new file mode 100644 index 00000000000..e9f323e204f --- /dev/null +++ b/pyk/src/tests/integration/test-data/module-to-kore/coverage.k @@ -0,0 +1,16 @@ +// Copyright (c) Runtime Verification, Inc. All Rights Reserved. +// Exercises impurity analysis with coverage instrumentation. +// #ctz uses #if...#fi (ite), which is polymorphic. With --coverage, ite gets +// instrumented rules calling #logToFile (impure), but ite must NOT be marked +// impure — Java skips polymorphic function rules in its dependency graph. +module COVERAGE-SYNTAX + imports INT + imports K-EQUAL +endmodule + +module COVERAGE + imports COVERAGE-SYNTAX + + syntax Int ::= "#ctz" "(" Int ")" [function] + rule #ctz(N) => #if N modInt 2 ==Int 1 #then 0 #else 1 +Int #ctz(N >>Int 1) #fi requires N =/=Int 0 +endmodule diff --git a/pyk/src/tests/integration/test-data/module-to-kore/frontend-only.k b/pyk/src/tests/integration/test-data/module-to-kore/frontend-only.k new file mode 100644 index 00000000000..b9d3ea9b9ca --- /dev/null +++ b/pyk/src/tests/integration/test-data/module-to-kore/frontend-only.k @@ -0,0 +1,18 @@ +module FRONTEND-ONLY-SYNTAX + imports LIST + + syntax Foo ::= "foo" + | bar() [function, unused] + | baz() [function, public] + syntax KResult ::= Foo + syntax KItem ::= do(KItem) [hybrid, strict(1)] +endmodule + +module FRONTEND-ONLY + imports FRONTEND-ONLY-SYNTAX + + configuration + $PGM:K + .List + +endmodule