Emit user-defined groups as group(_)

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)]

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
 

kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

@@ -876,6 +876,7 @@ public String convertSpecificationModule(Module definition, Module spec, Sentenc
         HashMap<Att.Key, Boolean> 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<Att.Key, Boolean> attributes, Att att) {
-        for (Tuple2<Tuple2<Att.Key, String>, ?> attribute : iterable(att.att())) {
+        for (Tuple2<Tuple2<Att.Key, String>, ?> 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<Att.Key, Boolean> attributes, Att att, StringBuilder sb, Map<String, KVariable> 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<Tuple2<Att.Key, String>, ?> attribute :
             // Sort to stabilize error messages
             stream(att.att()).sorted(Comparator.comparing(Tuple2::toString)).collect(Collectors.toList())) {

kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java

@@ -613,10 +613,6 @@ private static Tuple2<Att.Key, String> 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);

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<Att.Key> newGroups = Collections.stream(att.rawKeys())
                 .map((k) -> {
                     Optional<Att.Key> 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<Att.Key> 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<String, Att> 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) {

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<String, Att> 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();
     }
 
 ////////////////////

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<Att.Key,String> attKeyPair: JavaConverters.seqAsJavaList(att.att().keys().toSeq())) {
+        for (Tuple2<Att.Key,String> 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);

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()