From f394c778c578a57ba3e948cc65e88eb75537376e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 12 Nov 2024 05:51:43 +0000 Subject: [PATCH] pyk/konvert/_kast_to_kore: working conversion of K functional rules to kore --- pyk/src/pyk/konvert/_kast_to_kore.py | 130 ++++++++++++++++++++------- 1 file changed, 98 insertions(+), 32 deletions(-) diff --git a/pyk/src/pyk/konvert/_kast_to_kore.py b/pyk/src/pyk/konvert/_kast_to_kore.py index f4eb887d57..8b4aa85212 100644 --- a/pyk/src/pyk/konvert/_kast_to_kore.py +++ b/pyk/src/pyk/konvert/_kast_to_kore.py @@ -6,13 +6,32 @@ from ..kast import Atts from ..kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KToken, KVariable, top_down -from ..kast.manip import bool_to_ml_pred, extract_lhs, extract_rhs, flatten_label, var_occurrences +from ..kast.manip import bool_to_ml_pred, extract_lhs, extract_rhs, flatten_label, ml_pred_to_bool, var_occurrences from ..kast.outer import KRule +from ..kore.prelude import BOOL as KORE_BOOL from ..kore.prelude import SORT_K -from ..kore.syntax import DV, And, App, Axiom, EVar, Import, MLPattern, MLQuant, Module, Rewrites, SortApp, String, Top +from ..kore.prelude import TRUE as KORE_TRUE +from ..kore.syntax import ( + DV, + And, + App, + Axiom, + Equals, + EVar, + Implies, + Import, + MLPattern, + MLQuant, + Module, + Rewrites, + SortApp, + SortVar, + String, + Top, +) from ..prelude.bytes import BYTES, pretty_bytes_str from ..prelude.k import K_ITEM, K, inj -from ..prelude.kbool import TRUE +from ..prelude.kbool import BOOL, TRUE, andBool from ..prelude.ml import mlAnd from ..prelude.string import STRING, pretty_string from ._utils import munge @@ -204,34 +223,84 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: krule_lhs_config = extract_lhs(krule_body) krule_rhs_config = extract_rhs(krule_body) - # Assume it's a semantic rule, but more specific sort for functional rules - top_level_k_sort = KSort('GeneratedTopCell') - if isinstance(krule_lhs_config, KApply) and krule_lhs_config.label.name in definition.function_labels: - top_level_k_sort = definition.sort_strict(krule_lhs_config) - top_level_kore_sort = _ksort_to_kore(top_level_k_sort) - - krule_lhs_constraints = [ - bool_to_ml_pred(c, sort=top_level_k_sort) for c in flatten_label('_andBool_', krule.requires) if not c == TRUE - ] - krule_rhs_constraints = [ - bool_to_ml_pred(c, sort=top_level_k_sort) for c in flatten_label('_andBool_', krule.ensures) if not c == TRUE - ] + is_functional = isinstance(krule_lhs_config, KApply) and krule_lhs_config.label.name in definition.function_labels - kast_lhs = mlAnd([krule_lhs_config] + krule_lhs_constraints, sort=top_level_k_sort) - kast_rhs = mlAnd([krule_rhs_config] + krule_rhs_constraints, sort=top_level_k_sort) + top_level_k_sort = KSort('GeneratedTopCell') if not is_functional else definition.sort_strict(krule_lhs_config) + top_level_kore_sort = _ksort_to_kore(top_level_k_sort) + # Do sort inference on the entire rule at once + kast_lhs = mlAnd( + [krule_lhs_config] + + [ + bool_to_ml_pred(constraint, sort=top_level_k_sort) + for constraint in flatten_label('_andBool_', krule.requires) + if not constraint == TRUE + ], + sort=top_level_k_sort, + ) + kast_rhs = mlAnd( + [krule_rhs_config] + + [ + bool_to_ml_pred(constraint, sort=top_level_k_sort) + for constraint in flatten_label('_andBool_', krule.ensures) + if not constraint == TRUE + ], + sort=top_level_k_sort, + ) kast_rule_sorted = definition.sort_vars(KRewrite(kast_lhs, kast_rhs)) - kast_lhs_sorted = extract_lhs(kast_rule_sorted) - kast_rhs_sorted = extract_rhs(kast_rule_sorted) - kore_lhs = kast_to_kore(definition, kast_lhs_sorted, sort=top_level_k_sort) - kore_rhs = kast_to_kore(definition, kast_rhs_sorted, sort=top_level_k_sort) - - # The backend does not like rewrite rules without a precondition - if not isinstance(kore_lhs, And): - kore_lhs = And(top_level_kore_sort, (kore_lhs, Top(top_level_kore_sort))) - - kore_rule = Rewrites(sort=top_level_kore_sort, left=kore_lhs, right=kore_rhs) + kast_lhs_body, *kast_lhs_constraints = flatten_label('#And', extract_lhs(kast_rule_sorted)) + kast_rhs_body, *kast_rhs_constraints = flatten_label('#And', extract_rhs(kast_rule_sorted)) + kore_lhs_body = kast_to_kore(definition, kast_lhs_body, sort=top_level_k_sort) + kore_rhs_body = kast_to_kore(definition, kast_rhs_body, sort=top_level_k_sort) + + axiom_vars: tuple[SortVar, ...] = () + kore_axiom: Pattern + if not is_functional: + kore_lhs_constraints = [ + kast_to_kore(definition, kast_lhs_constraint, sort=top_level_k_sort) + for kast_lhs_constraint in kast_lhs_constraints + ] + kore_rhs_constraints = [ + kast_to_kore(definition, kast_rhs_constraint, sort=top_level_k_sort) + for kast_rhs_constraint in kast_rhs_constraints + ] + kore_lhs_constraint: Pattern = Top(top_level_kore_sort) + if len(kore_lhs_constraints) == 1: + kore_lhs_constraint = kore_lhs_constraints[0] + elif len(kore_lhs_constraints) > 1: + kore_lhs_constraint = And(top_level_kore_sort, kore_lhs_constraints) + kore_lhs = And(top_level_kore_sort, [kore_lhs_body, kore_lhs_constraint]) + kore_rhs = ( + kore_rhs_body + if not kore_rhs_constraints + else And(top_level_kore_sort, [kore_rhs_body] + kore_rhs_constraints) + ) + kore_axiom = Rewrites(sort=top_level_kore_sort, left=kore_lhs, right=kore_rhs) + else: + axiom_sort = SortVar('R') + axiom_vars = (axiom_sort,) + kast_lhs_constraints_bool = [ + ml_pred_to_bool(kast_lhs_constraint) for kast_lhs_constraint in kast_lhs_constraints + ] + kore_antecedent = Equals( + KORE_BOOL, axiom_sort, kast_to_kore(definition, andBool(kast_lhs_constraints_bool), sort=BOOL), KORE_TRUE + ) + kore_ensures: Pattern = Top(top_level_kore_sort) + if kast_rhs_constraints: + kast_rhs_constraints_bool = [ + ml_pred_to_bool(kast_rhs_constraint) for kast_rhs_constraint in kast_rhs_constraints + ] + kore_ensures = Equals( + KORE_BOOL, + top_level_kore_sort, + kast_to_kore(definition, andBool(kast_rhs_constraints_bool), sort=BOOL), + KORE_TRUE, + ) + kore_consequent = Equals( + top_level_kore_sort, axiom_sort, kore_lhs_body, And(top_level_kore_sort, [kore_rhs_body, kore_ensures]) + ) + kore_axiom = Implies(axiom_sort, kore_antecedent, kore_consequent) # Make adjustments to Rule attributes att = krule.att.discard([Atts.PRODUCTION, Atts.UNIQUE_ID, Atts.SOURCE, Atts.LOCATION]) @@ -244,7 +313,7 @@ def krule_to_kore(definition: KDefinition, krule: KRule) -> Axiom: attrs = [_krule_att_to_kore(att_entry, var_occurrences(kast_rule_sorted)) for att_entry in att.entries()] - return Axiom(vars=(), pattern=kore_rule, attrs=attrs) + return Axiom(vars=axiom_vars, pattern=kore_axiom, attrs=attrs) def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Module: @@ -259,11 +328,8 @@ def kflatmodule_to_kore(definition: KDefinition, kflatmodule: KFlatModule) -> Mo def _krule_att_to_kore(att_entry: AttEntry, kast_rule_vars: dict[str, list[KVariable]]) -> App: match att_entry.key: - case Atts.LABEL | Atts.PRIORITY: + case Atts.LABEL | Atts.PRIORITY | Atts.SIMPLIFICATION: return App(symbol=att_entry.key.name, sorts=(), args=(String(str(att_entry.value)),)) - case Atts.SIMPLIFICATION: - args = () if not att_entry.value else (String(str(att_entry.value)),) - return App(symbol=att_entry.key.name, sorts=(), args=args) case Atts.SYMBOLIC | Atts.CONCRETE: if not att_entry.value: return App(symbol=att_entry.key.name, sorts=(), args=())