Remove special-casing for group(_) (#3981)

When we originally added `group(_)` to replace unstructured attributes, we treated it as syntactic sugar where `[group(foo1,...,fooN)]` expands internally into `[foo1,...,fooN]`. However, on a second look, this expansion is unnecessary - `group(_)` is only relevant in the `Context` object used by `KILtoKORE` which maps tags in syntax blocks to sets of corresponding `Production`s. In this PR, we then - Remove all the `ProcessGroupAttributes` logic and instead just parse `group(_)` when we build the `Context`. - Remove the special-cased `KeyType.UserGroup` - (Opinionated) Remove the mention of `group(_)` from the "unrecognized attributes" error message. - The hint was useful when we first disallowed unstructured attributes. However, now that `group(_)` and the whitelist are more established, it feels a bit odd to assume any unrecognized attribute is an attempt to create a group. As a side effect of this change, - `syntax` declarations can now only refer to productions by their klabel or group. Previously, any attribute was permitted, and the priority or associativity would apply to everything with that attribute. - Cell properties will no longer expand `<cell group="foo"> </cell>` - This should be disallowed entirely, but see #3982 - We no longer error if a group conflicts with a built-in attribute - Before, this error was required lest `[group(function)]` be treated the same as `[function]`
runtimeverification · Feb 13, 2024 · f7c33c0 · f7c33c0
1 parent 67c8ba5
commit f7c33c0
Show file tree

Hide file tree

Showing 20 changed files with 128 additions and 263 deletions.
diff --git a/k-distribution/include/kframework/builtin/kast.md b/k-distribution/include/kframework/builtin/kast.md
@@ -142,26 +142,26 @@ module ML-SYNTAX [not-lr1]
                        | "#Bottom" [klabel(#Bottom), symbol, group(mlUnary)]
                        | "#True" [klabel(#Top), symbol, group(mlUnary), unparseAvoid]
                        | "#False" [klabel(#Bottom), symbol, group(mlUnary), unparseAvoid]
-                       | "#Not" "(" Sort ")" [klabel(#Not), symbol, mlOp, group(mlUnary)]
+                       | "#Not" "(" Sort ")" [klabel(#Not), symbol, mlOp, group(mlUnary, mlOp)]
 
-  syntax {Sort1, Sort2} Sort2 ::= "#Ceil" "(" Sort1 ")" [klabel(#Ceil), symbol, mlOp, group(mlUnary)]
-                                | "#Floor" "(" Sort1 ")" [klabel(#Floor), symbol, mlOp, group(mlUnary)]
-                                | "{" Sort1 "#Equals" Sort1 "}" [klabel(#Equals), symbol, mlOp, group(mlEquals), comm, format(%1%i%n%2%d%n%3%i%n%4%d%n%5)]
+  syntax {Sort1, Sort2} Sort2 ::= "#Ceil" "(" Sort1 ")" [klabel(#Ceil), symbol, mlOp, group(mlUnary, mlOp)]
+                                | "#Floor" "(" Sort1 ")" [klabel(#Floor), symbol, mlOp, group(mlUnary, mlOp)]
+                                | "{" Sort1 "#Equals" Sort1 "}" [klabel(#Equals), symbol, mlOp, group(mlEquals, mlOp), comm, format(%1%i%n%2%d%n%3%i%n%4%d%n%5)]
 
   syntax priorities mlUnary > mlEquals > mlAnd
 
-  syntax {Sort} Sort ::= Sort "#And" Sort [klabel(#And), symbol, assoc, left, comm, unit(#Top), mlOp, group(mlAnd), format(%i%1%d%n%2%n%i%3%d)]
-                       > Sort "#Or" Sort [klabel(#Or), symbol, assoc, left, comm, unit(#Bottom), mlOp, format(%i%1%d%n%2%n%i%3%d)]
-                       > Sort "#Implies" Sort [klabel(#Implies), symbol, mlOp, group(mlImplies), format(%i%1%d%n%2%n%i%3%d)]
+  syntax {Sort} Sort ::= Sort "#And" Sort [klabel(#And), symbol, assoc, left, comm, unit(#Top), mlOp, group(mlAnd, mlOp), format(%i%1%d%n%2%n%i%3%d)]
+                       > Sort "#Or" Sort [klabel(#Or), symbol, assoc, left, comm, unit(#Bottom), mlOp, group(mlOp), format(%i%1%d%n%2%n%i%3%d)]
+                       > Sort "#Implies" Sort [klabel(#Implies), symbol, mlOp, group(mlImplies, mlOp), format(%i%1%d%n%2%n%i%3%d)]
 
   syntax priorities mlImplies > mlQuantifier
 
-  syntax {Sort1, Sort2} Sort2 ::= "#Exists" Sort1 "." Sort2 [klabel(#Exists), symbol, mlOp, mlBinder, group(mlQuantifier)]
-                                | "#Forall" Sort1 "." Sort2 [klabel(#Forall), symbol, mlOp, mlBinder, group(mlQuantifier)]
+  syntax {Sort1, Sort2} Sort2 ::= "#Exists" Sort1 "." Sort2 [klabel(#Exists), symbol, mlOp, mlBinder, group(mlQuantifier, mlOp)]
+                                | "#Forall" Sort1 "." Sort2 [klabel(#Forall), symbol, mlOp, mlBinder, group(mlQuantifier, mlOp)]
 
-  syntax {Sort} Sort ::= "#AG" "(" Sort ")" [klabel(#AG), symbol, mlOp]
-                       | "#wEF" "(" Sort ")" [klabel(weakExistsFinally), symbol, mlOp]
-                       | "#wAF" "(" Sort ")" [klabel(weakAlwaysFinally), symbol, mlOp]
+  syntax {Sort} Sort ::= "#AG" "(" Sort ")" [klabel(#AG), symbol, mlOp, group(mlOp)]
+                       | "#wEF" "(" Sort ")" [klabel(weakExistsFinally), symbol, mlOp, group(mlOp)]
+                       | "#wAF" "(" Sort ")" [klabel(weakAlwaysFinally), symbol, mlOp, group(mlOp)]
 endmodule
 ```
 

diff --git a/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java b/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java
@@ -13,7 +13,6 @@
 import org.junit.Rule;
 import org.junit.rules.TestName;
 import org.kframework.attributes.Source;
-import org.kframework.compile.ProcessGroupAttributes;
 import org.kframework.kil.Definition;
 import org.kframework.kil.loader.Context;
 import org.kframework.parser.inner.CollectProductionsVisitor;
@@ -100,7 +99,6 @@ protected DefinitionWithContext parseUsingOuter(File definitionFile) {
     def.setItems(Outer.parse(Source.apply(definitionFile.getPath()), definitionText, null));
     def.setMainModule("TEST");
 
-    ProcessGroupAttributes.apply(def);
     Context context = new Context();
     return new DefinitionWithContext(def, context);
   }

diff --git a/k-distribution/tests/regression-new/checks/checkGroup.k b/k-distribution/tests/regression-new/checks/checkGroup.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-module TEST
+module CHECKGROUP
   syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2)]
-               | Int "+" Int [group(function)]
+               | Int "+" Int [group(fun,)]
 endmodule
diff --git a/k-distribution/tests/regression-new/checks/checkGroup.k.out b/k-distribution/tests/regression-new/checks/checkGroup.k.out
@@ -1,5 +1,5 @@
-[Error] Compiler: User-defined group 'function' conflicts with a built-in attribute.
+[Error] Compiler: group(_) attribute expects a comma separated list of groups, each of which consists of a lower case letter followed by any number of alphanumeric or '-' characters.
 	Source(checkGroup.k)
-	Location(4,18,4,47)
-	4 |	               | Int "+" Int [group(function)]
-	  .	                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+	Location(4,18,4,43)
+	4 |	               | Int "+" Int [group(fun,)]
+	  .	                 ^~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out b/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out
@@ -1,9 +1,15 @@
+[Error] Compiler: Module cannot have the following attributes: [group]
+	Source(checkModuleAtts.k)
+	Location(2,1,3,10)
+	  .	v~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+	2 |	module CHECKMODULEATTS [foo, group(bar), baz]
+	3 |	endmodule
+	  .	~~~~~~~~^
 [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.
+[Error] Compiler: Had 2 structural errors.
diff --git a/k-distribution/tests/regression-new/pedanticAttributes/test.k.out b/k-distribution/tests/regression-new/pedanticAttributes/test.k.out
@@ -1,11 +1,9 @@
 [Error] Compiler: Unrecognized attributes: [badAtt]
-Hint: User-defined groups can be added with the group(_) attribute.
 	Source(test.k)
 	Location(3,18,3,71)
 	3 |	  syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2), badAtt(10)]
 	  .	                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 [Error] Compiler: Unrecognized attributes: [badAtt]
-Hint: User-defined groups can be added with the group(_) attribute.
 	Source(test.k)
 	Location(4,18,4,68)
 	4 |	               | Int "+" Int [group(badAttButOkay),badAtt,function]

diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java
@@ -128,8 +128,7 @@ public Function<Definition, Definition> steps() {
                 .apply(d);
     DefinitionTransformer resolveHeatCoolAttribute =
         DefinitionTransformer.fromSentenceTransformer(
-            new ResolveHeatCoolAttribute(new HashSet<>())::resolve,
-            "resolving heat and cool attributes");
+            ResolveHeatCoolAttribute::resolve, "resolving heat and cool attributes");
     DefinitionTransformer resolveAnonVars =
         DefinitionTransformer.fromSentenceTransformer(
             new ResolveAnonVar()::resolve, "resolving \"_\" vars");

diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -1863,8 +1863,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.withUserGroupsAsGroupAtt().att())) {
+    for (Tuple2<Tuple2<Att.Key, String>, ?> attribute : iterable(att.att())) {
       Att.Key name = attribute._1._1;
       Object val = attribute._2;
       String strVal = val.toString();
@@ -2024,9 +2023,6 @@ private void convert(
     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)).toList()) {

diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java
@@ -773,11 +773,9 @@ private static Att getCellPropertiesAsAtt(K k) {
       } else if (kapp.klabel().name().equals("#cellPropertyList")) {
         if (kapp.klist().size() == 2) {
           Tuple2<Att.Key, String> attribute = getCellProperty(kapp.klist().items().get(0));
-          return ProcessGroupAttributes.getProcessedAtt(
-              Att()
-                  .add(attribute._1(), attribute._2())
-                  .addAll(getCellPropertiesAsAtt(kapp.klist().items().get(1))),
-              k);
+          return Att()
+              .add(attribute._1(), attribute._2())
+              .addAll(getCellPropertiesAsAtt(kapp.klist().items().get(1)));
         }
       }
     }
@@ -795,12 +793,7 @@ private static Tuple2<Att.Key, String> getCellProperty(K k) {
                       .orElseThrow(
                           () ->
                               KEMException.compilerError(
-                                  "Unrecognized attribute: "
-                                      + keyToken.s()
-                                      + "\n"
-                                      + "Hint: User-defined groups can be added with the"
-                                      + " group=\"...\" attribute.",
-                                  k));
+                                  "Unrecognized property: " + keyToken.s(), k));
               if (kapp.klist().items().get(0) instanceof KToken) {
                 KToken valueToken = (KToken) kapp.klist().items().get(1);
                 if (valueToken.sort().equals(Sorts.KString())) {

diff --git a/kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java b/kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java b/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java
@@ -5,8 +5,6 @@
 import static org.kframework.definition.Constructors.*;
 import static org.kframework.kore.KORE.*;
 
-import java.util.Optional;
-import java.util.Set;
 import org.kframework.attributes.Att;
 import org.kframework.builtin.BooleanUtils;
 import org.kframework.definition.Context;
@@ -18,18 +16,18 @@
 import org.kframework.kore.KLabel;
 import org.kframework.utils.errorsystem.KEMException;
 
-public record ResolveHeatCoolAttribute(Set<String> unrestrictedRules) {
+public class ResolveHeatCoolAttribute {
 
-  private Rule resolve(Module m, Rule rule) {
+  private static Rule resolve(Module m, Rule rule) {
     return Rule(rule.body(), transform(m, rule.requires(), rule.att()), rule.ensures(), rule.att());
   }
 
-  private Context resolve(Module m, Context context) {
+  private static Context resolve(Module m, Context context) {
     return new Context(
         context.body(), transform(m, context.requires(), context.att()), context.att());
   }
 
-  private K transform(Module m, K requires, Att att) {
+  private static K transform(Module m, K requires, Att att) {
     String sort = att.getOptional(Att.RESULT()).orElse("KResult");
     KLabel lbl = KLabel("is" + sort);
     if (!m.productionsFor().contains(lbl)
@@ -49,19 +47,13 @@ && stream(m.allSorts()).noneMatch(s -> s.toString().equals(sort))) {
       return BooleanUtils.and(requires, BooleanUtils.not(predicate));
     }
     if (att.contains(Att.COOL())) {
-      if (unrestrictedRules.stream()
-          .map(Att::getUserGroupOptional)
-          .flatMap(Optional::stream)
-          .anyMatch(att::contains)) {
-        return requires;
-      }
       return BooleanUtils.and(requires, predicate);
     }
     throw new AssertionError(
         "Called ResolveHeatCoolAttribute::transform on rule without " + "heat or cool attribute");
   }
 
-  public Sentence resolve(Module m, Sentence s) {
+  public static Sentence resolve(Module m, Sentence s) {
     if (!s.att().contains(Att.HEAT()) && !s.att().contains(Att.COOL())) {
       return s;
     }

diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java
@@ -78,8 +78,7 @@ private <T extends HasAtt & HasLocation> void checkUnrecognizedAtts(T term) {
       errors.add(
           KEMException.compilerError(
               "Unrecognized attributes: "
-                  + stream(term.att().unrecognizedKeys()).map(Key::toString).sorted().toList()
-                  + "\nHint: User-defined groups can be added with the group(_) attribute.",
+                  + stream(term.att().unrecognizedKeys()).map(Key::toString).sorted().toList(),
               term));
     }
   }

diff --git a/kernel/src/main/java/org/kframework/kil/Module.java b/kernel/src/main/java/org/kframework/kil/Module.java
@@ -43,11 +43,7 @@ public List<ModuleItem> getItems() {
 
   @Override
   public void toString(StringBuilder sb) {
-    sb.append("module ")
-        .append(name)
-        .append(" ")
-        .append(getAttributes().withUserGroupsAsGroupAtt())
-        .append("\n");
+    sb.append("module ").append(name).append(" ").append(getAttributes()).append("\n");
     for (ModuleItem i : items) {
       i.toString(sb);
       sb.append("\n");

diff --git a/kernel/src/main/java/org/kframework/kil/Production.java b/kernel/src/main/java/org/kframework/kil/Production.java
@@ -253,7 +253,7 @@ public void toString(StringBuilder sb) {
       i.toString(sb);
       sb.append(" ");
     }
-    sb.append(getAttributes().withUserGroupsAsGroupAtt());
+    sb.append(getAttributes());
   }
 
   public void setOwnerModuleName(String ownerModuleName) {

diff --git a/kernel/src/main/java/org/kframework/kil/loader/Context.java b/kernel/src/main/java/org/kframework/kil/loader/Context.java
@@ -1,8 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 package org.kframework.kil.loader;
 
-import static org.kframework.Collections.*;
-
 import com.google.common.collect.HashMultimap;
 import com.google.common.collect.SetMultimap;
 import com.google.inject.Inject;
@@ -11,8 +9,8 @@
 import org.kframework.kil.Production;
 import org.kframework.kompile.KompileOptions;
 import org.kframework.main.GlobalOptions;
+import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.inject.RequestScoped;
-import scala.Tuple2;
 
 @RequestScoped
 public class Context implements Serializable {
@@ -21,7 +19,7 @@ public class Context implements Serializable {
   public Context() {}
 
   /**
-   * Represents a map from all Klabels or attributes in string representation to sets of
+   * Represents a map from all Klabels and group(_) tags in string representation to sets of
    * corresponding productions.
    */
   public SetMultimap<String, Production> tags = HashMultimap.create();
@@ -31,18 +29,23 @@ public Context() {}
   public KompileOptions kompileOptions;
 
   public void addProduction(Production p) {
-    if (p.containsAttribute(Att.GROUP())) {
-      throw new AssertionError(
-          "Must call ExpandGroupAttribute.apply(Definition) before creating a Context.");
-    }
-
     if (p.getKLabel(false) != null) {
       tags.put(p.getKLabel(false), p);
     } else if (p.getAttributes().contains(Att.BRACKET())) {
       tags.put(p.getBracketLabel(false), p);
     }
-    for (Tuple2<Att.Key, String> a : iterable(p.getAttributes().att().keys())) {
-      tags.put(a._1.key(), p);
+    if (p.getAttributes().contains(Att.GROUP())) {
+      String groups = p.getAttributes().get(Att.GROUP());
+      if (!groups.matches("\\s*[a-z][a-zA-Z0-9-]*\\s*(,\\s*[a-z][a-zA-Z0-9-]*\\s*)*")) {
+        throw KEMException.compilerError(
+            "group(_) attribute expects a comma separated list of "
+                + "groups, each of which consists of a lower case letter followed by any "
+                + "number of alphanumeric or '-' characters.",
+            p);
+      }
+      for (String group : groups.split("\\s*,\\s*")) {
+        tags.put(group, p);
+      }
     }
   }
 }
diff --git a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java
@@ -14,7 +14,6 @@
 import org.kframework.attributes.Att;
 import org.kframework.attributes.Location;
 import org.kframework.attributes.Source;
-import org.kframework.compile.ProcessGroupAttributes;
 import org.kframework.compile.checks.CheckBracket;
 import org.kframework.compile.checks.CheckListDecl;
 import org.kframework.definition.Associativity;
@@ -384,9 +383,7 @@ public void applyUserList(
   }
 
   public static org.kframework.attributes.Att convertAttributes(ASTNode t) {
-    Att attributes = ProcessGroupAttributes.getProcessedAtt(t.getAttributes(), t);
-
-    return attributes
+    return t.getAttributes()
         .addAll(attributesFromLocation(t.getLocation()))
         .addAll(attributesFromSource(t.getSource()));
   }

diff --git a/kernel/src/main/java/org/kframework/parser/ParserUtils.java b/kernel/src/main/java/org/kframework/parser/ParserUtils.java
@@ -22,7 +22,6 @@
 import org.kframework.attributes.Att;
 import org.kframework.attributes.Location;
 import org.kframework.attributes.Source;
-import org.kframework.compile.ProcessGroupAttributes;
 import org.kframework.definition.FlatModule;
 import org.kframework.definition.Module;
 import org.kframework.definition.ModuleTransformer;
@@ -82,7 +81,6 @@ public static Module parseMainModuleOuterSyntax(
     def.setItems(Outer.parse(source, definitionText, null));
     def.setMainModule(mainModule);
 
-    ProcessGroupAttributes.apply(def);
     Context context = new Context();
     new CollectProductionsVisitor(context).visit(def);
 
@@ -117,9 +115,6 @@ public List<org.kframework.kil.Module> slurp(
       }
     }
     List<DefinitionItem> items = Outer.parse(source, definitionText, null);
-    items.stream()
-        .filter((d) -> d instanceof org.kframework.kil.Module)
-        .forEach((m) -> ProcessGroupAttributes.apply((org.kframework.kil.Module) m));
 
     if (options.verbose) {
       System.out.println("Importing: " + source);
@@ -227,7 +222,6 @@ public Set<Module> loadModules(
     Definition def = new Definition();
     def.setItems((List<DefinitionItem>) (Object) kilModules);
 
-    ProcessGroupAttributes.apply(def);
     new CollectProductionsVisitor(context).visit(def);
 
     // Tuple4 of moduleName, Source, Location, digest