From 50bf9115a5999bb1b972e1b93862ba1e6841ab63 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 24 Apr 2026 17:27:58 +0000 Subject: [PATCH 1/5] kast/att, konvert/_module_to_kore, test-data/module-to-kore: suppress frontend-only attributes from Kore emission Add `frontend_only: bool` flag to `AttKey` mirroring Java's `KeyRange.FrontendOnly`. Add `Atts.HYBRID`, `Atts.PUBLIC`, `Atts.STREAM`, `Atts.UNUSED` with `frontend_only=True` and proper types matching `KeyParameter.Optional`/`KeyParameter.Forbidden` in `Att.scala`. Include these in `DiscardSymbolAtts` in `simplified_module()` so they are stripped before Kore emission, matching Java's `ModuleToKORE.java` `shouldEmit()` filter. Add integration test cases `unused.k` and `frontend-only.k` (covering all four attributes) to the `module-to-kore` test-data suite. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/att.py | 6 ++++++ pyk/src/pyk/konvert/_module_to_kore.py | 4 ++++ .../test-data/module-to-kore/frontend-only.k | 18 ++++++++++++++++++ 3 files changed, 28 insertions(+) create mode 100644 pyk/src/tests/integration/test-data/module-to-kore/frontend-only.k diff --git a/pyk/src/pyk/kast/att.py b/pyk/src/pyk/kast/att.py index b428e79a2c5..1e0a9ea8f5e 100644 --- a/pyk/src/pyk/kast/att.py +++ b/pyk/src/pyk/kast/att.py @@ -273,6 +273,8 @@ def parse(self, text: str) -> tuple[Color, ...]: class AttKey(Generic[T]): name: str type: AttType[T] = field(compare=False, repr=False, kw_only=True) + # Mirrors Java's KeyRange.FrontendOnly: consumed before Kore emission, must not appear in .kore files. + frontend_only: bool = field(default=False, compare=False, repr=False, kw_only=True) def __call__(self, value: T) -> AttEntry[T]: return AttEntry(self, value) @@ -316,6 +318,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), frontend_only=True) IDEM: Final = AttKey('idem', type=_NONE) IMPURE: Final = AttKey('impure', type=_NONE) INDEX: Final = AttKey('index', type=_INT) @@ -338,12 +341,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, frontend_only=True) 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), frontend_only=True) SMTLEMMA: Final = AttKey('smt-lemma', type=_NONE) STRICT: Final = AttKey('strict', type=_ANY) SYMBOL: Final = AttKey('symbol', type=_STR) @@ -358,6 +363,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, frontend_only=True) 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..28883f89fa8 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,12 +758,15 @@ 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, ], 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 From 278a74f07577895b5e7140e2b6b7a89e5b2517e9 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 24 Apr 2026 17:35:10 +0000 Subject: [PATCH 2/5] kast/att: drop unused frontend_only flag MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The frontend_only field on AttKey was purely decorative — DiscardSymbolAtts is the actual suppression mechanism and its explicit list is the source of truth. Remove the field to keep AttKey simple. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/att.py | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/pyk/src/pyk/kast/att.py b/pyk/src/pyk/kast/att.py index 1e0a9ea8f5e..3c22d79a128 100644 --- a/pyk/src/pyk/kast/att.py +++ b/pyk/src/pyk/kast/att.py @@ -273,8 +273,6 @@ def parse(self, text: str) -> tuple[Color, ...]: class AttKey(Generic[T]): name: str type: AttType[T] = field(compare=False, repr=False, kw_only=True) - # Mirrors Java's KeyRange.FrontendOnly: consumed before Kore emission, must not appear in .kore files. - frontend_only: bool = field(default=False, compare=False, repr=False, kw_only=True) def __call__(self, value: T) -> AttEntry[T]: return AttEntry(self, value) @@ -318,7 +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), frontend_only=True) + 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) @@ -341,14 +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, frontend_only=True) + 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), frontend_only=True) + 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) @@ -363,7 +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, frontend_only=True) + 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) From 6357ecb81ed5c981d88fefb469f845c14105e440 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 24 Apr 2026 18:29:30 +0000 Subject: [PATCH 3/5] konvert/_module_to_kore: fix impurity propagation for polymorphic functions Java's ComputeTransitiveFunctionDependencies groups function rules by their post-sort-injection KLabel (e.g. ite{K}), which doesn't match the parametric production entry in attributesFor() (ite{SortSort}). The mismatch causes Java to silently skip dependency-graph edges for polymorphic function rules, so polymorphic functions are never marked impure transitively. Mirror this behavior in AddImpureAtts._callers() by excluding productions with non-empty klabel.params from the set of labels whose rules are processed. Fixes a false-positive impure{} annotation on ite in coverage-instrumented compilations (81/82 regression-new dirs now agree with Java, up from 78/82). Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/konvert/_module_to_kore.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/konvert/_module_to_kore.py b/pyk/src/pyk/konvert/_module_to_kore.py index 28883f89fa8..1e31ab1d673 100644 --- a/pyk/src/pyk/konvert/_module_to_kore.py +++ b/pyk/src/pyk/konvert/_module_to_kore.py @@ -1037,7 +1037,16 @@ def _impurities(module: KFlatModule) -> set[str]: @staticmethod def _callers(module: KFlatModule) -> dict[str, set[str]]: - function_labels = {prod.klabel.name for prod in module.productions if prod.klabel and Atts.FUNCTION in prod.att} + # Exclude polymorphic productions (klabel.params non-empty). Java's + # ComputeTransitiveFunctionDependencies groups rules by their post-sort-injection + # KLabel (e.g. ite{K}) which doesn't match the parametric attributesFor() entry + # (ite{SortSort}), so polymorphic function rules are silently skipped in Java's + # dependency graph. + function_labels = { + prod.klabel.name + for prod in module.productions + if prod.klabel and not prod.klabel.params and Atts.FUNCTION in prod.att + } res: dict[str, set[str]] = {} for rule in module.rules: From 11629777fc80ff70a49e26ceea31d0a6941caad5 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 24 Apr 2026 18:45:33 +0000 Subject: [PATCH 4/5] konvert/_module_to_kore, test-data/module-to-kore: warn and test for polymorphic rule skipping Add a warning log in AddImpureAtts._callers() when a rule for a polymorphic function (klabel.params non-empty) is encountered and skipped. This makes the silent Java-parity behavior visible at run time. Add coverage.k to the module-to-kore integration test suite: a definition compiled with --coverage that uses #if...#fi (desugaring to the polymorphic ite function). With coverage instrumentation, ite gets rules calling #logToFile (impure), but must NOT be marked impure because Java's dependency analysis also skips polymorphic function rules. The test directly exercises the fix from the previous commit and verifies Python/Java structural-axiom agreement. EXTRA_KOMPILE_ARGS in the test fixture maps filenames to non-default kompile options, keeping all test data files using auto-derived module names. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/konvert/_module_to_kore.py | 13 ++++++++++++- .../integration/konvert/test_module_to_kore.py | 15 ++++++++++++--- .../test-data/module-to-kore/coverage.k | 16 ++++++++++++++++ 3 files changed, 40 insertions(+), 4 deletions(-) create mode 100644 pyk/src/tests/integration/test-data/module-to-kore/coverage.k diff --git a/pyk/src/pyk/konvert/_module_to_kore.py b/pyk/src/pyk/konvert/_module_to_kore.py index 1e31ab1d673..a15d407a82f 100644 --- a/pyk/src/pyk/konvert/_module_to_kore.py +++ b/pyk/src/pyk/konvert/_module_to_kore.py @@ -1042,6 +1042,11 @@ def _callers(module: KFlatModule) -> dict[str, set[str]]: # KLabel (e.g. ite{K}) which doesn't match the parametric attributesFor() entry # (ite{SortSort}), so polymorphic function rules are silently skipped in Java's # dependency graph. + poly_labels = { + prod.klabel.name + for prod in module.productions + if prod.klabel and prod.klabel.params and Atts.FUNCTION in prod.att + } function_labels = { prod.klabel.name for prod in module.productions @@ -1054,7 +1059,13 @@ def _callers(module: KFlatModule) -> dict[str, set[str]]: match rule.body: case KRewrite(KApply(KLabel(label)), rhs): - if label in function_labels: + if label in poly_labels: + _LOGGER.warning( + 'Skipping rules for polymorphic function %s in impurity analysis' + ' — Java also skips these due to sort-parameter mismatch in rulesFor()', + label, + ) + elif label in function_labels: rhs_labels = AddImpureAtts._labels(rhs) for called in rhs_labels: res.setdefault(called, set()).add(label) 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 From afedb7be4b49cfae10c4399d89823da2f81e29d6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 29 Apr 2026 19:47:23 +0000 Subject: [PATCH 5/5] konvert/_module_to_kore: factor out DiscardPolymorphicSentences Java-compat pass Add DiscardPolymorphicSentences(SingleModulePass) that removes KRule sentences whose LHS applies a polymorphic function label (klabel.params non-empty and FUNCTION attribute present), mirroring the silent Java behaviour where ComputeTransitiveFunctionDependencies finds no rules for such labels due to the post-sort-injection KLabel / parametric attributesFor() key mismatch. Inserting this pass before AddImpureAtts lets that pass revert to simple function_labels logic with no poly_labels special-case or warning log. All Java compatibility concern is now in one named, documented place. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/konvert/_module_to_kore.py | 61 ++++++++++++++++---------- 1 file changed, 39 insertions(+), 22 deletions(-) diff --git a/pyk/src/pyk/konvert/_module_to_kore.py b/pyk/src/pyk/konvert/_module_to_kore.py index a15d407a82f..9d6d0622505 100644 --- a/pyk/src/pyk/konvert/_module_to_kore.py +++ b/pyk/src/pyk/konvert/_module_to_kore.py @@ -772,6 +772,7 @@ def simplified_module(definition: KDefinition, module_name: str | None = None) - ], ), DiscardHookAtts(), + DiscardPolymorphicSentences(), AddImpureAtts(), AddSymbolAtts(Atts.MACRO(None), _is_macro), AddSymbolAtts(Atts.FUNCTIONAL(None), _is_functional), @@ -1037,21 +1038,7 @@ def _impurities(module: KFlatModule) -> set[str]: @staticmethod def _callers(module: KFlatModule) -> dict[str, set[str]]: - # Exclude polymorphic productions (klabel.params non-empty). Java's - # ComputeTransitiveFunctionDependencies groups rules by their post-sort-injection - # KLabel (e.g. ite{K}) which doesn't match the parametric attributesFor() entry - # (ite{SortSort}), so polymorphic function rules are silently skipped in Java's - # dependency graph. - poly_labels = { - prod.klabel.name - for prod in module.productions - if prod.klabel and prod.klabel.params and Atts.FUNCTION in prod.att - } - function_labels = { - prod.klabel.name - for prod in module.productions - if prod.klabel and not prod.klabel.params and Atts.FUNCTION in prod.att - } + function_labels = {prod.klabel.name for prod in module.productions if prod.klabel and Atts.FUNCTION in prod.att} res: dict[str, set[str]] = {} for rule in module.rules: @@ -1059,13 +1046,7 @@ def _callers(module: KFlatModule) -> dict[str, set[str]]: match rule.body: case KRewrite(KApply(KLabel(label)), rhs): - if label in poly_labels: - _LOGGER.warning( - 'Skipping rules for polymorphic function %s in impurity analysis' - ' — Java also skips these due to sort-parameter mismatch in rulesFor()', - label, - ) - elif label in function_labels: + if label in function_labels: rhs_labels = AddImpureAtts._labels(rhs) for called in rhs_labels: res.setdefault(called, set()).add(label) @@ -1277,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 # -----------------