From 46665b06b848177ee03cdea1eb98445587a6eda9 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Sun, 4 Feb 2024 13:42:07 -0800 Subject: [PATCH] Clean up `CheckAtt` (#3943) This PR refactors `CheckAtt` to more clearly separate the checks on different attributes. Most of the change here is just shuffling code between functions, but we additionally - Implemented `HasAtt` and `HasLocation` for `Module` so we can use the same `checkUnrecognizedAtts` and `checkRestrictedAtts` functions for both modules and sentences - In doing so, fixed a bug where we failed to check restricted attributes on modules at all - Corrected the whitelist to allow `one-path` and `all-path` on `Module` as well as `Claim` - Slightly changed a few error messages - Removed a manual check for attribute values on `binder`, as this is now covered by the general check --- .../tests/regression-new/checks/binder.k | 2 - .../tests/regression-new/checks/binder.k.out | 13 +- .../checks/checkModuleAtts.k.out | 10 +- .../regression-new/checks/invalidLabel.k.out | 6 +- .../checks/restrictedAtts.k.out | 4 +- .../kframework/compile/checks/CheckAtt.java | 273 +++++++++--------- .../java/org/kframework/kompile/Kompile.java | 8 +- .../scala/org/kframework/attributes/Att.scala | 6 +- .../org/kframework/definition/outer.scala | 7 +- 9 files changed, 170 insertions(+), 159 deletions(-) diff --git a/k-distribution/tests/regression-new/checks/binder.k b/k-distribution/tests/regression-new/checks/binder.k index 4ce3df5315a..62c12a285bb 100644 --- a/k-distribution/tests/regression-new/checks/binder.k +++ b/k-distribution/tests/regression-new/checks/binder.k @@ -6,8 +6,6 @@ module BINDER syntax Error ::= foo() [binder] - syntax Error ::= foo(KVar, Error) [binder(1 -> 2)] - syntax Error ::= foo(Error, Error) [binder] syntax Correct ::= foo(KVar, Error) [binder] diff --git a/k-distribution/tests/regression-new/checks/binder.k.out b/k-distribution/tests/regression-new/checks/binder.k.out index 69a38162084..8f2fa012a31 100644 --- a/k-distribution/tests/regression-new/checks/binder.k.out +++ b/k-distribution/tests/regression-new/checks/binder.k.out @@ -3,14 +3,9 @@ Location(7,20,7,34) 7 | syntax Error ::= foo() [binder] . ^~~~~~~~~~~~~~ -[Error] Compiler: Attribute value for 'binder' attribute is not supported. - Source(binder.k) - Location(9,20,9,53) - 9 | syntax Error ::= foo(KVar, Error) [binder(1 -> 2)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Error] Compiler: First child of binder must have a sort with the 'KVAR.KVar' hook attribute. Source(binder.k) - Location(11,20,11,46) - 11 | syntax Error ::= foo(Error, Error) [binder] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~ -[Error] Compiler: Had 3 structural errors. + Location(9,20,9,46) + 9 | syntax Error ::= foo(Error, Error) [binder] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~ +[Error] Compiler: Had 2 structural errors. diff --git a/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out b/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out index 067550da1c3..1463581f382 100644 --- a/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out +++ b/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out @@ -1,3 +1,9 @@ -[Error] Compiler: Had 1 structural errors. -[Error] Compiler: Unrecognized attributes on module CHECKMODULEATTS: [baz, foo] +[Error] Compiler: Unrecognized attributes: [baz, foo] Hint: User-defined groups can be added with the group(_) attribute. + Source(checkModuleAtts.k) + Location(2,1,3,10) + . v~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + 2 | module CHECKMODULEATTS [foo, group(bar), baz] + 3 | endmodule + . ~~~~~~~~^ +[Error] Compiler: Had 1 structural errors. diff --git a/k-distribution/tests/regression-new/checks/invalidLabel.k.out b/k-distribution/tests/regression-new/checks/invalidLabel.k.out index b52f6f0652c..0af6e51d1b3 100644 --- a/k-distribution/tests/regression-new/checks/invalidLabel.k.out +++ b/k-distribution/tests/regression-new/checks/invalidLabel.k.out @@ -1,14 +1,14 @@ -[Error] Compiler: Rule label 'INVALIDLABEL.foo`bar' cannot contain whitespace or backticks. +[Error] Compiler: Label 'INVALIDLABEL.foo`bar' cannot contain whitespace or backticks. Source(invalidLabel.k) Location(6,19,6,32) 6 | rule [foo`bar]: true => false . ^~~~~~~~~~~~~ -[Error] Compiler: Rule label 'foo bar' cannot contain whitespace or backticks. +[Error] Compiler: Label 'foo bar' cannot contain whitespace or backticks. Source(invalidLabel.k) Location(7,8,7,21) 7 | rule false => true [label(foo bar)] . ^~~~~~~~~~~~~ -[Error] Compiler: Rule label 'foo`bar' cannot contain whitespace or backticks. +[Error] Compiler: Label 'foo`bar' cannot contain whitespace or backticks. Source(invalidLabel.k) Location(8,8,8,14) 8 | rule 0 => 1 [label(foo`bar)] diff --git a/k-distribution/tests/regression-new/checks/restrictedAtts.k.out b/k-distribution/tests/regression-new/checks/restrictedAtts.k.out index 6d714c4d637..b3bbfa04a7b 100644 --- a/k-distribution/tests/regression-new/checks/restrictedAtts.k.out +++ b/k-distribution/tests/regression-new/checks/restrictedAtts.k.out @@ -1,9 +1,9 @@ -[Error] Compiler: Production sentences can not have the following attributes: [cool, kore] +[Error] Compiler: Production cannot have the following attributes: [cool, kore] Source(restrictedAtts.k) Location(4,19,4,41) 4 | syntax Foo ::= a() [cool, kore, left] . ^~~~~~~~~~~~~~~~~~~~~~ -[Error] Compiler: Rule sentences can not have the following attributes: [idem] +[Error] Compiler: Rule cannot have the following attributes: [idem] Source(restrictedAtts.k) Location(5,8,5,17) 5 | rule a() => .K [idem, owise] 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 c01f42a57c1..66655010e52 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java @@ -11,6 +11,7 @@ import org.kframework.attributes.Att.Key; import org.kframework.attributes.HasLocation; import org.kframework.builtin.Sorts; +import org.kframework.definition.HasAtt; import org.kframework.definition.Module; import org.kframework.definition.Production; import org.kframework.definition.ProductionItem; @@ -21,46 +22,77 @@ import org.kframework.utils.errorsystem.KEMException; import org.kframework.utils.errorsystem.KException.ExceptionType; import org.kframework.utils.errorsystem.KExceptionManager; +import scala.Tuple2; -/** Created by dwightguth on 1/25/16. */ +/** Check that attributes are well-formed and placed on the correct syntactic elements. */ public class CheckAtt { private final scala.collection.Set macros; private final Set errors; private final KExceptionManager kem; private final Module m; - private final boolean isSymbolicKast; - public CheckAtt( - Set errors, KExceptionManager kem, Module m, boolean isSymbolicKast) { + public CheckAtt(Set errors, KExceptionManager kem, Module m) { this.errors = errors; this.kem = kem; this.m = m; - this.isSymbolicKast = isSymbolicKast; this.macros = m.macroKLabels(); } - public void checkUnrecognizedModuleAtts() { - if (!m.att().unrecognizedKeys().isEmpty()) { + public void check() { + checkUnrecognizedAtts(m); + checkRestrictedAtts(m); + stream(m.localSentences()).forEach(this::checkSentence); + } + + private void checkSentence(Sentence sentence) { + checkUnrecognizedAtts(sentence); + checkRestrictedAtts(sentence); + checkLabel(sentence); + + if (sentence instanceof Rule rule) { + checkRule(rule); + } else if (sentence instanceof Production prod) { + checkProduction(prod); + } + } + + private void checkRule(Rule rule) { + checkMacro(rule); + checkNonExecutable(rule); + checkSimplification(rule); + checkSymbolic(rule); + } + + private void checkProduction(Production prod) { + checkHookedSortConstructors(prod); + checkBinder(prod); + checkFormat(prod); + checkFunctional(prod); + checkTotal(prod); + } + + private void checkUnrecognizedAtts(T term) { + if (!term.att().unrecognizedKeys().isEmpty()) { errors.add( KEMException.compilerError( - "Unrecognized attributes on module " - + m.name() - + ": " - + stream(m.att().unrecognizedKeys()).map(Key::toString).sorted().toList() - + "\nHint: User-defined groups can be added with the group(_) attribute.")); + "Unrecognized attributes: " + + stream(term.att().unrecognizedKeys()).map(Key::toString).sorted().toList() + + "\nHint: User-defined groups can be added with the group(_) attribute.", + term)); } } - public void check(Sentence sentence) { - checkUnrecognizedAtts(sentence); - checkRestrictedAtts(sentence); - if (sentence instanceof Rule) { - check(sentence.att(), sentence); - check((Rule) sentence); - } else if (sentence instanceof Production) { - check((Production) sentence); + private void checkRestrictedAtts(T term) { + Class cls = term.getClass(); + Att att = term.att(); + Set keys = stream(att.att().keySet()).map(Tuple2::_1).collect(Collectors.toSet()); + keys.removeIf(k -> k.allowedSentences().exists(c -> c.isAssignableFrom(cls))); + if (!keys.isEmpty()) { + List sortedKeys = keys.stream().map(Key::toString).sorted().toList(); + errors.add( + KEMException.compilerError( + cls.getSimpleName() + " cannot have the following attributes: " + sortedKeys, term)); } - checkLabel(sentence); } private static final Pattern whitespace = Pattern.compile("\\s"); @@ -71,85 +103,109 @@ private void checkLabel(Sentence sentence) { if (label.contains("`") || whitespace.matcher(label).find()) { errors.add( KEMException.compilerError( - "Rule label '" + label + "' cannot contain whitespace or backticks.", sentence)); + "Label '" + label + "' cannot contain whitespace or backticks.", sentence)); } } } - private void checkUnrecognizedAtts(Sentence sentence) { - if (!sentence.att().unrecognizedKeys().isEmpty()) { + 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 checkNonExecutable(Rule rule) { + boolean isNonExecutable = rule.att().contains(Att.NON_EXECUTABLE()); + boolean isFunction = + m.attributesFor().getOrElse(m.matchKLabel(rule), Att::empty).contains(Att.FUNCTION()); + + if (isNonExecutable && !isFunction) { errors.add( KEMException.compilerError( - "Unrecognized attributes: " - + stream(sentence.att().unrecognizedKeys()).map(Key::toString).sorted().toList() - + "\nHint: User-defined groups can be added with the group(_) attribute.", - sentence)); + "non-executable attribute is only supported on function rules.", rule)); } } - private void checkRestrictedAtts(Sentence sentence) { - Class cls = sentence.getClass(); - Att att = sentence.att(); - Set keys = stream(att.att().keySet()).map(k -> k._1()).collect(Collectors.toSet()); - keys.removeIf(k -> k.allowedSentences().exists(c -> c.isAssignableFrom(cls))); - if (!keys.isEmpty()) { - List sortedKeys = keys.stream().map(k -> k.toString()).sorted().toList(); + private void checkSimplification(Rule rule) { + Att att = rule.att(); + if (att.contains(Att.OWISE()) && att.contains(Att.SIMPLIFICATION())) { errors.add( KEMException.compilerError( - cls.getSimpleName() - + " sentences can not have the following attributes: " - + sortedKeys, - sentence)); + "owise attribute is not supported on simplification rules.", rule)); + } + if (att.contains(Att.PRIORITY()) && att.contains(Att.SIMPLIFICATION())) { + errors.add( + KEMException.compilerError( + "priority attribute is not supported on simplification rules.", rule)); + } + if (att.contains(Att.ANYWHERE()) && att.contains(Att.SIMPLIFICATION())) { + errors.add( + KEMException.compilerError( + "anywhere attribute is not supported on simplification rules.", rule)); } } - private void check(Production prod) { - if (!prod.sort().equals(Sorts.KItem())) { - Att sortAtt = m.sortAttributesFor().getOrElse(prod.sort().head(), () -> Att.empty()); - if (sortAtt.contains(Att.HOOK()) - && !sortAtt.get(Att.HOOK()).equals("ARRAY.Array") - && !(sortAtt.get(Att.HOOK()).equals("KVAR.KVar") && isSymbolicKast)) { - if (!prod.att().contains(Att.FUNCTION()) - && !prod.att().contains(Att.BRACKET()) - && !prod.att().contains(Att.TOKEN()) - && !prod.att().contains(Att.MACRO()) - && !(prod.klabel().isDefined() && macros.contains(prod.klabel().get()))) { - if (!(prod.sort().equals(Sorts.K()) - && ((prod.klabel().isDefined() - && (prod.klabel().get().name().equals("#EmptyK") - || prod.klabel().get().name().equals("#KSequence"))) - || prod.isSubsort()))) { - if (!(sortAtt.contains(Att.CELL_COLLECTION()) && prod.isSubsort())) { - errors.add( - KEMException.compilerError( - "Cannot add new constructors to hooked sort " + prod.sort(), prod)); - } + private void checkSymbolic(Rule rule) { + if (rule.att().contains(Att.ANYWHERE()) && rule.att().contains(Att.SYMBOLIC())) { + errors.add( + KEMException.compilerError( + "anywhere attribute is not supported on symbolic rules.", rule)); + } + } + + private void checkHookedSortConstructors(Production prod) { + if (prod.sort().equals(Sorts.KItem())) { + return; + } + Att sortAtt = m.sortAttributesFor().getOrElse(prod.sort().head(), Att::empty); + if (sortAtt.contains(Att.HOOK()) && !sortAtt.get(Att.HOOK()).equals("ARRAY.Array")) { + if (!prod.att().contains(Att.FUNCTION()) + && !prod.att().contains(Att.BRACKET()) + && !prod.att().contains(Att.TOKEN()) + && !prod.att().contains(Att.MACRO()) + && !(prod.klabel().isDefined() && macros.contains(prod.klabel().get()))) { + if (!(prod.sort().equals(Sorts.K()) + && ((prod.klabel().isDefined() + && (prod.klabel().get().name().equals("#EmptyK") + || prod.klabel().get().name().equals("#KSequence"))) + || prod.isSubsort()))) { + if (!(sortAtt.contains(Att.CELL_COLLECTION()) && prod.isSubsort())) { + errors.add( + KEMException.compilerError( + "Cannot add new constructors to hooked sort " + prod.sort(), prod)); } } } } - if (prod.att().contains(Att.BINDER()) && !isSymbolicKast) { - if (!prod.att().get(Att.BINDER()).equals("")) { - errors.add( - KEMException.compilerError( - "Attribute value for 'binder' attribute is not supported.", prod)); - } - if (prod.nonterminals().size() < 2) { - errors.add( - KEMException.compilerError( - "Binder productions must have at least two nonterminals.", prod)); - } else if (!m.sortAttributesFor() - .get(prod.nonterminals().apply(0).sort().head()) - .getOrElse(() -> Att.empty()) - .getOptional(Att.HOOK()) - .orElse("") - .equals("KVAR.KVar")) { - errors.add( - KEMException.compilerError( - "First child of binder must have a sort with the 'KVAR.KVar' hook attribute.", - prod)); - } + } + + private void checkBinder(Production prod) { + if (!prod.att().contains(Att.BINDER())) { + return; + } + if (prod.nonterminals().size() < 2) { + errors.add( + KEMException.compilerError( + "Binder productions must have at least two nonterminals.", prod)); + } else if (!m.sortAttributesFor() + .get(prod.nonterminals().apply(0).sort().head()) + .getOrElse(Att::empty) + .getOptional(Att.HOOK()) + .orElse("") + .equals("KVAR.KVar")) { + errors.add( + KEMException.compilerError( + "First child of binder must have a sort with the 'KVAR.KVar' hook attribute.", prod)); } + } + + private void checkFormat(Production prod) { boolean hasColors = false; int ncolors = 0; if (prod.att().contains(Att.COLORS())) { @@ -252,6 +308,9 @@ private void check(Production prod) { + " colors instead.", prod)); } + } + + private void checkFunctional(Production prod) { if (prod.att().contains(Att.FUNCTIONAL())) { kem.registerCompilerWarning( ExceptionType.FUTURE_ERROR, @@ -260,6 +319,9 @@ private void check(Production prod) { + " attributes 'function' and 'total' instead.", prod); } + } + + private void checkTotal(Production prod) { if (prod.att().contains(Att.TOTAL()) && !prod.att().contains(Att.FUNCTION())) { errors.add( KEMException.compilerError( @@ -268,53 +330,4 @@ private void check(Production prod) { prod)); } } - - private void check(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); - } - - checkNonExecutable(rule); - } - - private void checkNonExecutable(Rule rule) { - boolean isNonExecutable = rule.att().contains(Att.NON_EXECUTABLE()); - boolean isFunction = - m.attributesFor().getOrElse(m.matchKLabel(rule), Att::empty).contains(Att.FUNCTION()); - - if (isNonExecutable && !isFunction) { - errors.add( - KEMException.compilerError( - "non-executable attribute is only supported on function rules.", rule)); - } - } - - private void check(Att att, HasLocation loc) { - if (att.contains(Att.OWISE()) && att.contains(Att.SIMPLIFICATION())) { - errors.add( - KEMException.compilerError( - "owise attribute is not supported on simplification rules.", loc)); - } - if (att.contains(Att.PRIORITY()) && att.contains(Att.SIMPLIFICATION())) { - errors.add( - KEMException.compilerError( - "priority attribute is not supported on simplification rules.", loc)); - } - if (att.contains(Att.ANYWHERE()) && att.contains(Att.SIMPLIFICATION())) { - errors.add( - KEMException.compilerError( - "anywhere attribute is not supported on simplification rules.", loc)); - } - if (att.contains(Att.ANYWHERE()) && att.contains(Att.SYMBOLIC())) { - errors.add( - KEMException.compilerError( - "anywhere attribute is not supported on symbolic rules.", loc)); - } - } } diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 4f0283ff7e3..1ba5ebd50e7 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -607,13 +607,7 @@ public void structuralChecks( new CheckRHSVariables(errors, !isSymbolic, kompileOptions.backend); stream(modules).forEach(m -> stream(m.localSentences()).forEach(checkRHSVariables::check)); - stream(modules) - .forEach( - m -> { - CheckAtt checkAtt = new CheckAtt(errors, kem, m, isSymbolic && isKast); - checkAtt.checkUnrecognizedModuleAtts(); - stream(m.localSentences()).forEach(checkAtt::check); - }); + stream(modules).forEach(m -> new CheckAtt(errors, kem, m).check()); stream(modules) .forEach( diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index 793ab02e5e8..578036054c8 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -243,13 +243,13 @@ object Att { /* 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, onlyon[Claim]) + 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]) final val BAG = Key.builtin("bag", KeyParameter.Forbidden, onlyon[Production]) - final val BINDER = Key.builtin("binder", KeyParameter.Optional, onlyon[Production]) + final val BINDER = Key.builtin("binder", KeyParameter.Forbidden, onlyon[Production]) final val BRACKET = Key.builtin("bracket", KeyParameter.Forbidden, onlyon[Production]) final val CELL = Key.builtin("cell", KeyParameter.Forbidden, onlyon[Production]) final val CELL_COLLECTION = @@ -303,7 +303,7 @@ object Att { 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]) - final val ONE_PATH = Key.builtin("one-path", KeyParameter.Forbidden, onlyon[Claim]) + final val ONE_PATH = Key.builtin("one-path", KeyParameter.Forbidden, onlyon2[Claim, Module]) final val OWISE = Key.builtin("owise", KeyParameter.Forbidden, onlyon[Rule]) final val PARSER = Key.builtin("parser", KeyParameter.Required, onlyon[Production]) final val PREC = Key.builtin("prec", KeyParameter.Required, onlyon[Production]) diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index 72ed7e8e242..989c942f81a 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -106,10 +106,15 @@ case class Module( with OuterKORE with Sorting with Serializable - with AttValue { + with AttValue + with HasAtt + with HasLocation { assert(att != null) + def location: Optional[Location] = att.getOptional(classOf[Location]) + def source: Optional[Source] = att.getOptional(classOf[Source]) + lazy val fullImports: Set[Module] = imports.map(_.module) private lazy val importedSentences = fullImports.flatMap(_.sentences)