diff --git a/k-distribution/tests/regression-new/checks/checkGroup.k.out b/k-distribution/tests/regression-new/checks/checkGroup.k.out index 8e3c7a882c1..d23f3e64132 100644 --- a/k-distribution/tests/regression-new/checks/checkGroup.k.out +++ b/k-distribution/tests/regression-new/checks/checkGroup.k.out @@ -1,4 +1,4 @@ -[Error] Compiler: User-defined group 'function' conflicts with built-in or internal attribute. +[Error] Compiler: User-defined group 'function' conflicts with a built-in attribute. Source(checkGroup.k) Location(4,18,4,47) 4 | | Int "+" Int [group(function)] diff --git a/k-distribution/tests/regression-new/group/test.k b/k-distribution/tests/regression-new/group/test.k index 0e763a87971..a7f7c26a39f 100644 --- a/k-distribution/tests/regression-new/group/test.k +++ b/k-distribution/tests/regression-new/group/test.k @@ -7,11 +7,12 @@ module TEST-SYNTAX | "-" Int [function, group(unmin)] | Int "*" Int [function, group(muldiv)] | Int "/" Int [function, group(muldiv)] - | Int "+" Int [function, group(plusmin,lefty)] - | Int "-" Int [function, group(plusmin,lefty)] + // digest is an attribute, but it's internal only, so it should be fine to use as a group + | Int "+" Int [function, group(plusmin,digest)] + | Int "-" Int [function, group(plusmin,digest)] syntax priority unmin > muldiv > plusmin - syntax left lefty + syntax left digest syntax left muldiv endmodule 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 1b1fb3e07c5..801f2b68510 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -876,6 +876,7 @@ public String convertSpecificationModule(Module definition, Module spec, Sentenc HashMap consideredAttributes = new HashMap<>(); consideredAttributes.put(Att.PRIORITY(), true); consideredAttributes.put(Att.LABEL(), true); + consideredAttributes.put(Att.GROUP(), true); consideredAttributes.put(Att.SOURCE(), true); consideredAttributes.put(Att.LOCATION(), true); consideredAttributes.put(Att.UNIQUE_ID(), true); @@ -1673,7 +1674,7 @@ private KLabel computePolyKLabel(KApply k) { private void collectAttributes(Map attributes, Att att) { - for (Tuple2, ?> attribute : iterable(att.att())) { + for (Tuple2, ?> attribute : iterable(att.withUserGroupsAsGroupAtt().att())) { Att.Key name = attribute._1._1; Object val = attribute._2; String strVal = val.toString(); @@ -1832,6 +1833,10 @@ private String getSortStr(Sort sort) { private void convert(Map attributes, Att att, StringBuilder sb, Map freeVarsMap, HasLocation location) { sb.append("["); String conn = ""; + + // Emit user groups as group(_) to prevent conflicts between user groups and internals + att = att.withUserGroupsAsGroupAtt(); + for (Tuple2, ?> attribute : // Sort to stabilize error messages stream(att.att()).sorted(Comparator.comparing(Tuple2::toString)).collect(Collectors.toList())) { diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java index c7945cb0eaa..65a1f4898e5 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java +++ b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java @@ -613,10 +613,6 @@ private static Tuple2 getCellProperty(K k, boolean pedanticAttr if (keyToken.sort().equals(Sort("#CellName"))) { Att.Key key = Att.getBuiltinKeyOptional(keyToken.s()) .or(() -> { - if (Att.getInternalKeyOptional(keyToken.s()).isPresent()) { - throw KEMException.compilerError( - "User-defined attribute '" + keyToken.s() + "' conflicts with an internal attribute.", k); - } if (pedanticAttributes) { throw KEMException.compilerError("Unrecognized attribute: " + keyToken.s() + "\nHint: User-defined groups can be added with the group=\"...\" attribute.", k); diff --git a/kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java b/kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java index de813caa1e1..dbe20609aa5 100644 --- a/kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java +++ b/kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java @@ -8,6 +8,7 @@ import org.kframework.kil.Module; import org.kframework.kil.Syntax; import org.kframework.utils.errorsystem.KEMException; +import scala.util.Either; import java.util.List; import java.util.Optional; @@ -22,20 +23,20 @@ */ public class ProcessGroupAttributes { - private static Att processRawKeys(Att att, HasLocation node) { - // During parsing, attributes my-att are inserted as either + private static Att convertRawKeysToUserGroups(Att att, HasLocation node) { + // During parsing, an attribute my-att is inserted as either // - Key("my-att", KeyType.BuiltIn) if a recognized built-in // - Key("my-att", KeyType.RawKey) otherwise // // Thus, if --pedantic-attributes is disabled, we should replace every Key(..., KeyType.Raw) with - // Key(..., KeyType.UserGroup), unless that raw key happens to conflict with an internal attribute. + // Key(..., KeyType.UserGroup). List newGroups = Collections.stream(att.rawKeys()) .map((k) -> { Optional groupKey = Att.getUserGroupOptional(k.key()); if (groupKey.isEmpty()) { - throw KEMException.compilerError( - "User-defined attribute '" + k.key() + "' conflicts with an " + - "internal attribute.", node); + throw new AssertionError("Found Att.Key(" + k.key() + ", KeyType.RawKey), " + + "but outer parsing should have produced Att.Key(" + k.key() + ", KeyType.BuiltIn) " + + "instead"); } return groupKey.get(); }).collect(Collectors.toList()); @@ -45,44 +46,17 @@ private static Att processRawKeys(Att att, HasLocation node) { return att; } - private static Att expandGroupAttribute(Att att, HasLocation node) { - if (!att.contains(Att.GROUP(), String.class)) { - return att; - } - String groups = att.get(Att.GROUP()).trim(); - if (groups.isEmpty()) { - throw KEMException.compilerError( - "group(_) attribute expects a comma-separated list of arguments.", node); - } - KEMException badCommaException = - KEMException.compilerError("Extraneous ',' in group(_) attribute.", node); - if (groups.startsWith(",") || groups.endsWith(",")) { - throw badCommaException; - } - for (String group : groups.split("\\s*,\\s*")) { - if (group.isEmpty()) { - throw badCommaException; - } - Optional groupKey = Att.getUserGroupOptional(group); - if (groupKey.isEmpty()) { - throw KEMException.compilerError("User-defined group '" + group + - "' conflicts with built-in or internal attribute.", node); - } - if (!group.matches("[a-z][a-zA-Z0-9-]*")) { - throw KEMException.compilerError("Invalid argument '" + group + "' in group(_) attribute. " + - "Expected a lower case letter followed by any number of alphanumeric or '-' characters.", node); - } - att = att.add(groupKey.get()); + public static Att getProcessedAtt(Att att, HasLocation node, boolean pedanticAttributes) { + Either newAttOrError = att.withGroupAttAsUserGroups(); + if (newAttOrError.isLeft()) { + throw KEMException.compilerError(newAttOrError.left().get(), node); } - return att.remove(Att.GROUP()); - } + Att newAtt = newAttOrError.right().get(); - public static Att getProcessedAtt(Att att, HasLocation node, boolean pedanticAttributes) { - Att newAtts = expandGroupAttribute(att, node); if (!pedanticAttributes) { - newAtts = processRawKeys(newAtts, node); + newAtt = convertRawKeysToUserGroups(newAtt, node); } - return newAtts; + return newAtt; } public static void apply(Module m, boolean pedanticAttributes) { @@ -91,9 +65,7 @@ public static void apply(Module m, boolean pedanticAttributes) { .filter((modItem) -> modItem instanceof Syntax) .flatMap((s) -> ((Syntax) s).getPriorityBlocks().stream()) .flatMap((pb) -> pb.getProductions().stream()) - .forEach((p) -> { - p.setAttributes(getProcessedAtt(p.getAttributes(), p, pedanticAttributes)); - }); + .forEach((p) -> p.setAttributes(getProcessedAtt(p.getAttributes(), p, pedanticAttributes))); } public static void apply(Definition d, boolean pedanticAttributes) { diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index 83345789777..24e35f8e183 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -5,6 +5,7 @@ import org.kframework.attributes.Att; import org.kframework.attributes.Location; import org.kframework.attributes.Source; +import org.kframework.compile.ProcessGroupAttributes; import org.kframework.definition.Associativity; import org.kframework.definition.Bubble; import org.kframework.definition.Claim; @@ -37,6 +38,7 @@ import org.kframework.utils.errorsystem.KEMException; import scala.Option; import scala.collection.JavaConverters; +import scala.util.Either; import javax.json.*; import java.io.IOException; @@ -323,19 +325,23 @@ public static Att toAtt(JsonObject data) { } else { Att.Key attKey = Att.getBuiltinKeyOptional(key) + // The JSON is emitted after we may have added internal attributes .or(() -> Att.getInternalKeyOptional(key)) - // The JSON may have been produced with group attributes already expanded. - // As a result, we can't distinguish between intended user groups vs misspelled - // built-ins or internals, so we have to assume everything is a user group. - .or(() -> Att.getUserGroupOptional(key)) .orElseThrow(() -> - new AssertionError("Attribute '" + key + - "' is not a built-in or internal, yet Att.getUserGroupOptional(\"" + - key + "\") failed.")); + KEMException.criticalError("Unrecognized attribute " + key + + " found in KAST Json term when unparsing KATT: " + + attMap + + "\nHint: User-defined groups can be added with the group(_) attribute.") + ); newAtt = newAtt.add(attKey, attMap.getString(key)); } } - return newAtt; + Either newAttOrError = newAtt.withGroupAttAsUserGroups(); + if (newAttOrError.isLeft()) { + throw KEMException.criticalError(newAttOrError.left().get() + + "\nOccurred in KAST Json term when unparsing KATT: " + attMap); + } + return newAttOrError.right().get(); } //////////////////// diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index 22d4e69ff5e..cac9cf1f9b0 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -135,11 +135,14 @@ public static JsonStructure toJson(Definition def) { } public static JsonStructure toJson(Att att) { + // Emit user groups as group(_) to prevent conflicts between user groups and internals + att = att.withUserGroupsAsGroupAtt(); + JsonObjectBuilder jatt = Json.createObjectBuilder(); jatt.add("node", JsonParser.KATT); JsonObjectBuilder jattKeys = Json.createObjectBuilder(); - for (Tuple2 attKeyPair: JavaConverters.seqAsJavaList(att.att().keys().toSeq())) { + for (Tuple2 attKeyPair : JavaConverters.seqAsJavaList(att.att().keys().toSeq())) { if (attKeyPair._1().key().equals(Location.class.getName())) { JsonArrayBuilder locarr = Json.createArrayBuilder(); Location loc = att.get(Location.class); diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index e6ad5614ac9..c7af352fe84 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -3,8 +3,8 @@ package org.kframework.attributes import java.util.Optional import org.kframework.Collections._ +import org.kframework.utils.errorsystem.KEMException -import java.lang.Enum import scala.collection.Set /** @@ -33,7 +33,7 @@ trait AttValue * - Att.getBuiltInKeyOptional(myAttStr), if checking a user-supplied attribute string. Be sure to report an error * if the lookup fails and --pedantic-attributes is enabled. * - Att.getInternalKeyOptional(myAttStr), if expecting an internal key - * - Att.getUserGroupOptional(myAttStr), if expecting a user-group, enforcing that it is neither a built-in nor internal + * - Att.getUserGroupOptional(myAttStr), if expecting a user-group, enforcing that it is not a built-in * * In rare circumstances, you may also use Att.unsafeRawKey(myAttStr) if you pinky-promise to check the keys are valid * and categorize them elsewhere (e.g. during parsing to allow us to report multiple errors) @@ -46,6 +46,42 @@ class Att private (val att: Map[(Att.Key, String), Any]) extends AttributesToStr case _ => false } + // Remove all UserGroups and replace them with a group(_) attribute + def withUserGroupsAsGroupAtt: Att = { + val groups = att.keys.filter(_._1.keyType.equals(Att.KeyType.UserGroup)).toSet; + if (groups.isEmpty) + this + else + Att(att -- groups).add(Att.GROUP, groups.map(_._1.key).mkString(",")) + } + + // Remove the group(_) attribute and insert each of its arguments as a UserGroup + // Returns either Left of an error message or Right of the result + def withGroupAttAsUserGroups: Either[String, Att] = { + if (!contains(Att.GROUP, classOf[String])) + return Right(this) + val groups = get(Att.GROUP).trim + if (groups.isEmpty) + return Left("group(_) attribute expects a comma-separated list of arguments.") + val badComma = Left("Extraneous ',' in group(_) attribute.") + if (groups.startsWith(",") || groups.endsWith(",")) + return badComma + var att = this + for (group <- groups.split("\\s*,\\s*")) { + if (group.isEmpty) + return badComma + val groupKey = Att.getUserGroupOptional(group) + if (groupKey.isEmpty) + return Left("User-defined group '" + group + "' conflicts with a built-in attribute.") + if (!group.matches("[a-z][a-zA-Z0-9-]*")) + return Left("Invalid argument '" + group + "' in group(_) attribute. " + + "Expected a lower case letter followed by any number of alphanumeric or '-' characters.") + att = att.add(groupKey.get) + } + Right(att.remove(Att.GROUP)) + } + + // All those raw keys which are not categorized val rawKeys: Set[Att.Key] = att.map(_._1._1).filter(_.keyType.equals(Att.KeyType.Raw)).toSet @@ -106,7 +142,11 @@ object Att { case object BuiltIn extends KeyType; // Attributes which are compiler-internal and cannot appear in user source code case object Internal extends KeyType; - // Attributes which represent user-defined groups via group(_) + // Attributes which represent user-defined groups via group(_). + // + // WARNING: Although we treat the arguments to group(_) as individual attributes internally, + // for any external interface (emitting KORE, JSON, etc.), we must re-emit them under the group(_) attribute, + // else there will be conflicts when a user group has the same name as an internal attribute. case object UserGroup extends KeyType; // Attributes which may be a BuiltIn/Internal/UserGroup, but have not been checked or categorized // This is mainly used during parsing to delay error checking, allowing us to report multiple errors @@ -313,7 +353,7 @@ object Att { } def getUserGroupOptional(group: String) : Optional[Key] = - if (!keys.contains(Key(group, KeyType.BuiltIn)) && !keys.contains(Key(group, KeyType.Internal))) { + if (!keys.contains(Key(group, KeyType.BuiltIn))) { Optional.of(Key(group, KeyType.UserGroup)) } else { Optional.empty()