From da04b9be1fb4325e569fdb154f1315d8959199d6 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 5 Feb 2024 16:03:20 +0000 Subject: [PATCH 1/3] Prohibit macro-like attributes on _all_ rules Previously, we only warned in these cases. Making this situation an error rather than a warning means that we can also simplify a lot of code that checked the macro-like attributes on specific sentence types as well. --- .../checks/checkFuncRuleAtt.k.out | 10 +-- .../kframework/compile/checks/CheckAtt.java | 19 +++-- .../compile/checks/CheckFunctions.java | 79 +------------------ 3 files changed, 16 insertions(+), 92 deletions(-) diff --git a/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out b/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out index 489d1e92387..32ed096a2a4 100644 --- a/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out +++ b/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out @@ -1,24 +1,24 @@ -[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules. +[Error] Compiler: The attribute [macro] may only appear on syntax productions. Source(checkFuncRuleAtt.k) Location(11,10,11,18) 11 | rule foo => 0 [macro] . ^~~~~~~~ -[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules. +[Error] Compiler: The attribute [macro-rec] may only appear on syntax productions. Source(checkFuncRuleAtt.k) Location(12,10,12,18) 12 | rule foo => 1 [macro-rec] . ^~~~~~~~ -[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules. +[Error] Compiler: The attribute [alias] may only appear on syntax productions. Source(checkFuncRuleAtt.k) Location(13,10,13,18) 13 | rule foo => 2 [alias] . ^~~~~~~~ -[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules. +[Error] Compiler: The attribute [alias-rec] may only appear on syntax productions. Source(checkFuncRuleAtt.k) Location(14,10,14,18) 14 | rule foo => 3 [alias-rec] . ^~~~~~~~ -[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules. +[Error] Compiler: The attribute [macro] may only appear on syntax productions. Source(checkFuncRuleAtt.k) Location(17,10,18,26) . v~~~~~~~~~~~~~ diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java index 66655010e52..880cf7dc2dd 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java @@ -48,6 +48,7 @@ private void checkSentence(Sentence sentence) { checkUnrecognizedAtts(sentence); checkRestrictedAtts(sentence); checkLabel(sentence); + checkMacro(sentence); if (sentence instanceof Rule rule) { checkRule(rule); @@ -57,7 +58,6 @@ private void checkSentence(Sentence sentence) { } private void checkRule(Rule rule) { - checkMacro(rule); checkNonExecutable(rule); checkSimplification(rule); checkSymbolic(rule); @@ -108,15 +108,14 @@ private void checkLabel(Sentence sentence) { } } - private void checkMacro(Rule rule) { - if (rule.isMacro()) { - kem.registerCompilerWarning( - ExceptionType.FUTURE_ERROR, - errors, - "The attribute [" - + rule.att().getMacro().get() - + "] has been deprecated on rules. Use this label on syntax declarations instead.", - rule); + private void checkMacro(Sentence sentence) { + if (!(sentence instanceof Production) && sentence.isMacro()) { + errors.add( + KEMException.compilerError( + "The attribute [" + + sentence.att().getMacro().get() + + "] may only appear on syntax productions.", + sentence)); } } diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java b/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java index c699bbdc40e..94f7aa07c9f 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java @@ -4,7 +4,6 @@ import java.util.Set; import org.kframework.attributes.Att; import org.kframework.compile.RewriteAwareVisitor; -import org.kframework.definition.Claim; import org.kframework.definition.Context; import org.kframework.definition.ContextAlias; import org.kframework.definition.Module; @@ -21,63 +20,14 @@ public record CheckFunctions(Set errors, Module m) { public void check(Sentence sentence) { if (sentence instanceof Rule rl) { checkFuncAtt(rl); - if (!rl.att().contains(Att.SIMPLIFICATION())) + if (!rl.att().contains(Att.SIMPLIFICATION())) { // functions are allowed on the LHS of simplification rules check(rl.body()); - } else if (sentence instanceof Claim c) { - // functions are allowed on LHS of claims - if (c.att().contains(Att.MACRO()) - || c.att().contains(Att.MACRO_REC()) - || c.att().contains(Att.ALIAS()) - || c.att().contains(Att.ALIAS_REC())) - errors.add( - KEMException.compilerError( - "Attributes " - + Att.MACRO() - + "|" - + Att.MACRO_REC() - + "|" - + Att.ALIAS() - + "|" - + Att.ALIAS_REC() - + " are not allowed on claims.", - c)); + } } else if (sentence instanceof Context ctx) { check(ctx.body()); - if (ctx.att().contains(Att.MACRO()) - || ctx.att().contains(Att.MACRO_REC()) - || ctx.att().contains(Att.ALIAS()) - || ctx.att().contains(Att.ALIAS_REC())) - errors.add( - KEMException.compilerError( - "Attributes " - + Att.MACRO() - + "|" - + Att.MACRO_REC() - + "|" - + Att.ALIAS() - + "|" - + Att.ALIAS_REC() - + " are not allowed on contexts.", - ctx)); } else if (sentence instanceof ContextAlias ctx) { check(ctx.body()); - if (ctx.att().contains(Att.MACRO()) - || ctx.att().contains(Att.MACRO_REC()) - || ctx.att().contains(Att.ALIAS()) - || ctx.att().contains(Att.ALIAS_REC())) - errors.add( - KEMException.compilerError( - "Attributes " - + Att.MACRO() - + "|" - + Att.MACRO_REC() - + "|" - + Att.ALIAS() - + "|" - + Att.ALIAS_REC() - + " are not allowed on contexts.", - ctx)); } } @@ -140,31 +90,6 @@ public void checkFuncAtt(Rule r) { public void apply(KApply k) { if (k.klabel().name().equals("#withConfig")) { super.apply(k); - return; - } - if ((isRHS() && !isLHS()) - || k.klabel() instanceof KVariable - || !m.attributesFor().contains(k.klabel())) { - return; - } - Att attributes = m.attributesFor().apply(k.klabel()); - if (attributes.contains(Att.FUNCTION()) - && (r.att().contains(Att.MACRO()) - || r.att().contains(Att.MACRO_REC()) - || r.att().contains(Att.ALIAS()) - || r.att().contains(Att.ALIAS_REC()))) { - errors.add( - KEMException.compilerError( - "Attributes " - + Att.MACRO() - + "|" - + Att.MACRO_REC() - + "|" - + Att.ALIAS() - + "|" - + Att.ALIAS_REC() - + " are not allowed on function rules.", - r)); } } }.apply(r.body()); From 5d9d227f9796bef4d9cbef989ea6b435094b1e42 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 5 Feb 2024 16:39:34 +0000 Subject: [PATCH 2/3] Simplify macro loop --- .../main/java/org/kframework/backend/kore/ModuleToKORE.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index bf649f679c6..3b7901818ce 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -1689,14 +1689,15 @@ private Att addKoreAttributes( // injective. boolean isInjective = isConstructor; - boolean isMacro = false; + boolean isMacro = prod.isMacro(); boolean isAnywhere = overloads.contains(prod); + if (prod.klabel().isDefined()) { for (Rule r : functionRules.get(prod.klabel().get())) { - isMacro |= ExpandMacros.isMacro(r); isAnywhere |= r.att().contains(Att.ANYWHERE()); } } + isConstructor &= !isMacro; isConstructor &= !isAnywhere; From 0a29e173b898c30cca2d179d55d1ff5594f0ae96 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Tue, 6 Feb 2024 10:39:03 +0000 Subject: [PATCH 3/3] Use existing attribute infrastructure --- .../checks/checkFuncRuleAtt.k.out | 10 ++--- .../kframework/compile/checks/CheckAtt.java | 12 ------ .../scala/org/kframework/attributes/Att.scala | 42 +++++++++---------- 3 files changed, 26 insertions(+), 38 deletions(-) diff --git a/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out b/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out index 32ed096a2a4..02ad205fcdf 100644 --- a/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out +++ b/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out @@ -1,24 +1,24 @@ -[Error] Compiler: The attribute [macro] may only appear on syntax productions. +[Error] Compiler: Rule cannot have the following attributes: [macro] Source(checkFuncRuleAtt.k) Location(11,10,11,18) 11 | rule foo => 0 [macro] . ^~~~~~~~ -[Error] Compiler: The attribute [macro-rec] may only appear on syntax productions. +[Error] Compiler: Rule cannot have the following attributes: [macro-rec] Source(checkFuncRuleAtt.k) Location(12,10,12,18) 12 | rule foo => 1 [macro-rec] . ^~~~~~~~ -[Error] Compiler: The attribute [alias] may only appear on syntax productions. +[Error] Compiler: Rule cannot have the following attributes: [alias] Source(checkFuncRuleAtt.k) Location(13,10,13,18) 13 | rule foo => 2 [alias] . ^~~~~~~~ -[Error] Compiler: The attribute [alias-rec] may only appear on syntax productions. +[Error] Compiler: Rule cannot have the following attributes: [alias-rec] Source(checkFuncRuleAtt.k) Location(14,10,14,18) 14 | rule foo => 3 [alias-rec] . ^~~~~~~~ -[Error] Compiler: The attribute [macro] may only appear on syntax productions. +[Error] Compiler: Rule cannot have the following attributes: [macro] Source(checkFuncRuleAtt.k) Location(17,10,18,26) . v~~~~~~~~~~~~~ diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java index 880cf7dc2dd..8f8f4136437 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java @@ -48,7 +48,6 @@ private void checkSentence(Sentence sentence) { checkUnrecognizedAtts(sentence); checkRestrictedAtts(sentence); checkLabel(sentence); - checkMacro(sentence); if (sentence instanceof Rule rule) { checkRule(rule); @@ -108,17 +107,6 @@ private void checkLabel(Sentence sentence) { } } - private void checkMacro(Sentence sentence) { - if (!(sentence instanceof Production) && sentence.isMacro()) { - errors.add( - KEMException.compilerError( - "The attribute [" - + sentence.att().getMacro().get() - + "] may only appear on syntax productions.", - sentence)); - } - } - private void checkNonExecutable(Rule rule) { boolean isNonExecutable = rule.att().contains(Att.NON_EXECUTABLE()); boolean isFunction = diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index 578036054c8..7127f57f6c0 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -241,10 +241,10 @@ object Att { onlyon3[T1, T2, T3] ++ onlyon[T4] /* Built-in attribute keys which can appear in user source code */ - final val ALIAS = Key.builtin("alias", KeyParameter.Forbidden, onlyon2[Production, Rule]) - final val ALIAS_REC = Key.builtin("alias-rec", KeyParameter.Forbidden, onlyon2[Production, Rule]) - final val ALL_PATH = Key.builtin("all-path", KeyParameter.Forbidden, onlyon2[Claim, Module]) - final val ANYWHERE = Key.builtin("anywhere", KeyParameter.Forbidden, onlyon[Rule]) + final val ALIAS = Key.builtin("alias", KeyParameter.Forbidden, onlyon[Production]) + final val ALIAS_REC = Key.builtin("alias-rec", KeyParameter.Forbidden, onlyon[Production]) + final val ALL_PATH = Key.builtin("all-path", KeyParameter.Forbidden, onlyon2[Claim, Module]) + final val ANYWHERE = Key.builtin("anywhere", KeyParameter.Forbidden, onlyon[Rule]) final val APPLY_PRIORITY = Key.builtin("applyPriority", KeyParameter.Required, onlyon[Production]) final val ASSOC = Key.builtin("assoc", KeyParameter.Forbidden, onlyon[Production]) final val AVOID = Key.builtin("avoid", KeyParameter.Forbidden, onlyon[Production]) @@ -283,23 +283,23 @@ object Att { final val INITIAL = Key.builtin("initial", KeyParameter.Forbidden, onlyon[Production]) final val INITIALIZER = Key.builtin("initializer", KeyParameter.Forbidden, onlyon2[Production, Rule]) - final val INJECTIVE = Key.builtin("injective", KeyParameter.Forbidden, onlyon[Production]) - final val INTERNAL = Key.builtin("internal", KeyParameter.Forbidden, onlyon[Production]) - final val KAST = Key.builtin("kast", KeyParameter.Forbidden, onlyon[Module]) - final val KLABEL = Key.builtin("klabel", KeyParameter.Required, onlyon[Production]) - final val KORE = Key.builtin("kore", KeyParameter.Forbidden, onlyon2[RuleOrClaim, Module]) - final val LABEL = Key.builtin("label", KeyParameter.Required, onlyon[Sentence]) - final val LATEX = Key.builtin("latex", KeyParameter.Required, onlyon[Production]) - final val LEFT = Key.builtin("left", KeyParameter.Forbidden, onlyon[Production]) - final val LOCATIONS = Key.builtin("locations", KeyParameter.Forbidden, onlyon[SyntaxSort]) - final val MACRO = Key.builtin("macro", KeyParameter.Forbidden, onlyon2[Production, Rule]) - final val MACRO_REC = Key.builtin("macro-rec", KeyParameter.Forbidden, onlyon2[Production, Rule]) - final val MAINCELL = Key.builtin("maincell", KeyParameter.Forbidden, onlyon[Production]) - final val MEMO = Key.builtin("memo", KeyParameter.Forbidden, onlyon[Production]) - final val ML_BINDER = Key.builtin("mlBinder", KeyParameter.Forbidden, onlyon[Production]) - final val ML_OP = Key.builtin("mlOp", KeyParameter.Forbidden, onlyon[Production]) - final val MULTIPLICITY = Key.builtin("multiplicity", KeyParameter.Required, onlyon[Production]) - final val NON_ASSOC = Key.builtin("non-assoc", KeyParameter.Forbidden, onlyon[Production]) + final val INJECTIVE = Key.builtin("injective", KeyParameter.Forbidden, onlyon[Production]) + final val INTERNAL = Key.builtin("internal", KeyParameter.Forbidden, onlyon[Production]) + final val KAST = Key.builtin("kast", KeyParameter.Forbidden, onlyon[Module]) + final val KLABEL = Key.builtin("klabel", KeyParameter.Required, onlyon[Production]) + final val KORE = Key.builtin("kore", KeyParameter.Forbidden, onlyon2[RuleOrClaim, Module]) + final val LABEL = Key.builtin("label", KeyParameter.Required, onlyon[Sentence]) + final val LATEX = Key.builtin("latex", KeyParameter.Required, onlyon[Production]) + final val LEFT = Key.builtin("left", KeyParameter.Forbidden, onlyon[Production]) + final val LOCATIONS = Key.builtin("locations", KeyParameter.Forbidden, onlyon[SyntaxSort]) + final val MACRO = Key.builtin("macro", KeyParameter.Forbidden, onlyon[Production]) + final val MACRO_REC = Key.builtin("macro-rec", KeyParameter.Forbidden, onlyon[Production]) + final val MAINCELL = Key.builtin("maincell", KeyParameter.Forbidden, onlyon[Production]) + final val MEMO = Key.builtin("memo", KeyParameter.Forbidden, onlyon[Production]) + final val ML_BINDER = Key.builtin("mlBinder", KeyParameter.Forbidden, onlyon[Production]) + final val ML_OP = Key.builtin("mlOp", KeyParameter.Forbidden, onlyon[Production]) + final val MULTIPLICITY = Key.builtin("multiplicity", KeyParameter.Required, onlyon[Production]) + final val NON_ASSOC = Key.builtin("non-assoc", KeyParameter.Forbidden, onlyon[Production]) final val NON_EXECUTABLE = Key.builtin("non-executable", KeyParameter.Forbidden, onlyon[Rule]) final val NOT_LR1 = Key.builtin("not-lr1", KeyParameter.Forbidden, onlyon[Module]) final val NO_EVALUATORS = Key.builtin("no-evaluators", KeyParameter.Forbidden, onlyon[Production])