Support more attributes in pyk, skip polymorphic rule handling in frontend

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)

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
 # -----------------

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,15 +25,24 @@
     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(
     params=DEFINITION_FILES,
     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

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

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 <T>
+        <k> $PGM:K </k>
+        <out stream="stdout"> .List </out>
+    </T>
+endmodule