Remove the option to opt out of the attribute whitelist

k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java

@@ -98,7 +98,7 @@ protected DefinitionWithContext parseUsingOuter(File definitionFile) {
         def.setMainModule("TEST");
         def.setMainSyntaxModule("TEST");
 
-        ProcessGroupAttributes.apply(def, true);
+        ProcessGroupAttributes.apply(def);
         Context context = new Context();
         return new DefinitionWithContext(def, context);
     }

k-distribution/src/test/java/org/kframework/kore/convertors/TstKILtoKOREIT.java

@@ -53,7 +53,7 @@ public void syntaxWithOR() throws IOException {
     }
 
     protected String convert(DefinitionWithContext defWithContext) {
-        KILtoKORE kilToKore = new KILtoKORE(defWithContext.context, false, false, false);
+        KILtoKORE kilToKore = new KILtoKORE(defWithContext.context, false, false);
         org.kframework.definition.Definition koreDef = kilToKore.apply(defWithContext.definition);
         String koreDefString = koreDef.toString();
         return koreDefString;

k-distribution/tests/regression-new/issue-1169/Makefile

@@ -7,7 +7,7 @@ include ../../../include/kframework/ktest.mak
 
 $(KOMPILED_DIR)/timestamp: $(DEF).k
 	$(KOMPILE) $(DEF).k -E > $(DEF2).k
-	$(KOMPILE) $(DEF2).k --no-pedantic-attributes --no-prelude --main-module TEST --syntax-module TEST
+	$(KOMPILE) $(DEF2).k --no-prelude --main-module TEST --syntax-module TEST
 	rm -rf $(KOMPILED_DIR)
 	mv test2-kompiled $(KOMPILED_DIR)
 

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

@@ -125,7 +125,7 @@ public Function<Definition, Definition> steps() {
         Function1<Definition, Definition> checkSimplificationRules = d -> DefinitionTransformer.from(m -> { m.localRules().foreach(r -> checkSimpIsFunc(m, r)); return m;}, "Check simplification rules").apply(d);
         DefinitionTransformer constantFolding = DefinitionTransformer.fromSentenceTransformer(new ConstantFolding()::fold, "constant expression folding");
         Function1<Definition, Definition> resolveFreshConstants = d ->
-                DefinitionTransformer.from(m -> new ResolveFreshConstants(d, kompileOptions.topCell, files, kompileOptions.outerParsing.pedanticAttributes).resolve(m), "resolving !Var variables").apply(d);
+                DefinitionTransformer.from(m -> new ResolveFreshConstants(d, kompileOptions.topCell, files).resolve(m), "resolving !Var variables").apply(d);
         GenerateCoverage cov = new GenerateCoverage(kompileOptions.coverage, files);
         Function1<Definition, Definition> genCoverage = d -> DefinitionTransformer.fromRuleBodyTransformerWithRule((r, body) -> cov.gen(r, body, d.mainModule()), "generate coverage instrumentation").apply(d);
         DefinitionTransformer numberSentences = DefinitionTransformer.fromSentenceTransformer(NumberSentences::number, "number sentences uniquely");
@@ -200,7 +200,7 @@ public Function<Module, Module> specificationSteps(Definition def) {
                 new AddImplicitComputationCell(configInfo, labelInfo)::apply,
                 "concretizing configuration");
         Function1<Module, Module> resolveFreshConstants = d ->
-                ModuleTransformer.from(new ResolveFreshConstants(def, kompileOptions.topCell, files, kompileOptions.outerParsing.pedanticAttributes)::resolve, "resolving !Var variables").apply(d);
+                ModuleTransformer.from(new ResolveFreshConstants(def, kompileOptions.topCell, files)::resolve, "resolving !Var variables").apply(d);
         Function1<Module, Module> addImplicitCounterCell = ModuleTransformer.fromSentenceTransformer(
                 new AddImplicitCounterCell()::apply,
                 "adding <generatedCounter> to claims if necessary");

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

@@ -59,11 +59,10 @@ public class GenerateSentencesFromConfigDecl {
      * @param ensures The ensures clause of the configuration declaration.
      * @param att The attributes of the configuration declaration.
      * @param m The module the configuration declaration exists in.
-     * @param pedanticAttributes Whether to error check that cell properties are in the attribute whitelist.
      * @return A set of sentences representing the configuration declaration.
      */
-    public static Set<Sentence> gen(K body, K ensures, Att att, Module m, boolean pedanticAttributes) {
-        return genInternal(body, ensures, att, m, pedanticAttributes)._1();
+    public static Set<Sentence> gen(K body, K ensures, Att att, Module m) {
+        return genInternal(body, ensures, att, m)._1();
     }
 
     /**
@@ -77,10 +76,9 @@ public static Set<Sentence> gen(K body, K ensures, Att att, Module m, boolean pe
      *                it is not the top cell of a configuration declaration.
      * @param cfgAtt The attributes of the configuration declaration. Appended to all cell productions generated.
      * @param m The module the configuration declaration is in. Used to get the sort of leaf cells.
-     * @param pedanticAttributes Whether to error check that cell properties are in the attribute whitelist.
      * @return A tuple of the sentences generated, a list of the sorts of the children of the cell, and the body of the initializer.
      */
-    private static Tuple4<Set<Sentence>, List<Sort>, K, Boolean> genInternal(K term, K ensures, Att cfgAtt, Module m, boolean pedanticAttributes) {
+    private static Tuple4<Set<Sentence>, List<Sort>, K, Boolean> genInternal(K term, K ensures, Att cfgAtt, Module m) {
         if (term instanceof KApply) {
             KApply kapp = (KApply) term;
             if (kapp.klabel().name().equals("#configCell")) {
@@ -93,7 +91,7 @@ private static Tuple4<Set<Sentence>, List<Sort>, K, Boolean> genInternal(K term,
                             KToken label = (KToken) startLabel;
                             if (label.sort().equals(Sort("#CellName"))) {
                                 String cellName = label.s();
-                                Att cellProperties = getCellPropertiesAsAtt(kapp.klist().items().get(1), cellName, ensures, pedanticAttributes);
+                                Att cellProperties = getCellPropertiesAsAtt(kapp.klist().items().get(1), cellName, ensures);
                                 Multiplicity multiplicity = convertStringMultiplicity(
                                         cellProperties.getOption(Att.MULTIPLICITY()), term);
                                 boolean isStream = cellProperties.getOption(Att.STREAM()).isDefined();
@@ -103,7 +101,7 @@ private static Tuple4<Set<Sentence>, List<Sort>, K, Boolean> genInternal(K term,
                                 if (kapp.att().contains(Location.class))
                                     att = cfgAtt.add(Location.class, kapp.att().get(Location.class));
                                 Tuple4<Set<Sentence>, List<Sort>, K, Boolean> childResult = genInternal(
-                                        cellContents, null, att, m, pedanticAttributes);
+                                        cellContents, null, att, m);
 
                                 boolean isLeafCell = childResult._4();
                                 Tuple4<Set<Sentence>, Sort, K, Boolean> myResult = computeSentencesOfWellFormedCell(isLeafCell, isStream, multiplicity, att, m, cellName, cellProperties,
@@ -147,15 +145,15 @@ private static Tuple4<Set<Sentence>, List<Sort>, K, Boolean> genInternal(K term,
                     //top level cell, therefore, should be the children of the generatedTop cell
                     KToken cellLabel = KToken(KLabels.GENERATED_TOP_CELL_NAME, Sort("#CellName"));
                     K generatedTop = KApply(KLabel("#configCell"), cellLabel, KApply(KLabel("#cellPropertyListTerminator")), term, cellLabel);
-                    return genInternal(generatedTop, ensures, cfgAtt, m, pedanticAttributes);
+                    return genInternal(generatedTop, ensures, cfgAtt, m);
                 }
                 List<K> cells = Assoc.flatten(kapp.klabel(), kapp.klist().items(), m);
                 Set<Sentence> accumSentences = Set();
                 List<Sort> sorts = Lists.newArrayList();
                 List<K> initializers = Lists.newArrayList();
                 for (K cell : cells) {
                     //for each cell, generate the child and inform the parent of the children it contains
-                    Tuple4<Set<Sentence>, List<Sort>, K, Boolean> childResult = genInternal(cell, null, cfgAtt, m, pedanticAttributes);
+                    Tuple4<Set<Sentence>, List<Sort>, K, Boolean> childResult = genInternal(cell, null, cfgAtt, m);
                     accumSentences = (Set<Sentence>)accumSentences.$bar(childResult._1());
                     sorts.addAll(childResult._2());
                     initializers.add(childResult._3());
@@ -572,7 +570,7 @@ private static KApply optionalCellInitializer(boolean initializeOptionalCell, At
         }
     }
 
-    private static Att getCellPropertiesAsAtt(K k, String cellName, K ensures, boolean pedanticAttributes) {
+    private static Att getCellPropertiesAsAtt(K k, String cellName, K ensures) {
         Att att = Att();
         if (cellName.equals("k")) {
             att = att.add(Att.MAINCELL());
@@ -581,29 +579,28 @@ private static Att getCellPropertiesAsAtt(K k, String cellName, K ensures, boole
             att = att.add(Att.TOPCELL());
         }
         att = att.add(Att.CELL()).add(Att.CELL_NAME(), cellName);
-        return att.addAll(getCellPropertiesAsAtt(k, pedanticAttributes));
+        return att.addAll(getCellPropertiesAsAtt(k));
     }
 
-    private static Att getCellPropertiesAsAtt(K k, boolean pedanticAttributes) {
+    private static Att getCellPropertiesAsAtt(K k) {
         if (k instanceof KApply) {
             KApply kapp = (KApply) k;
             if (kapp.klabel().name().equals("#cellPropertyListTerminator")) {
                 return Att();
             } else if (kapp.klabel().name().equals("#cellPropertyList")) {
                 if (kapp.klist().size() == 2) {
-                    Tuple2<Att.Key, String> attribute = getCellProperty(kapp.klist().items().get(0), pedanticAttributes);
+                    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), pedanticAttributes)),
-                            k,
-                            pedanticAttributes);
+                                    .addAll(getCellPropertiesAsAtt(kapp.klist().items().get(1))),
+                            k);
                 }
             }
         }
         throw KEMException.compilerError("Malformed cell properties", k);
     }
 
-    private static Tuple2<Att.Key, String> getCellProperty(K k, boolean pedanticAttributes) {
+    private static Tuple2<Att.Key, String> getCellProperty(K k) {
         if (k instanceof KApply) {
             KApply kapp = (KApply) k;
             if (kapp.klabel().name().equals("#cellProperty")) {
@@ -612,15 +609,9 @@ private static Tuple2<Att.Key, String> getCellProperty(K k, boolean pedanticAttr
                         KToken keyToken = (KToken) kapp.klist().items().get(0);
                         if (keyToken.sort().equals(Sort("#CellName"))) {
                             Att.Key key = Att.getBuiltinKeyOptional(keyToken.s())
-                                    .or(() -> {
-                                        if (pedanticAttributes) {
-                                            throw KEMException.compilerError("Unrecognized attribute: " + keyToken.s() +
-                                                    "\nHint: User-defined groups can be added with the group=\"...\" attribute.", k);
-                                        }
-                                        return Att.getUserGroupOptional(keyToken.s());
-                                    }).orElseThrow(() ->
-                                            new AssertionError("Attribute '" + keyToken.s() + "' is not a built-in or internal, " +
-                                                    "yet Att.getUserGroupOptional(\"" + keyToken.s() + "\") failed."));
+                                    .orElseThrow(() ->
+                                            KEMException.compilerError("Unrecognized attribute: " + keyToken.s() +
+                                                    "\nHint: User-defined groups can be added with the group=\"...\" attribute.", k));
                             if (kapp.klist().items().get(0) instanceof KToken) {
                                 KToken valueToken = (KToken) kapp.klist().items().get(1);
                                 if (valueToken.sort().equals(Sorts.KString())) {

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

@@ -1,7 +1,6 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.compile;
 
-import org.kframework.Collections;
 import org.kframework.attributes.Att;
 import org.kframework.attributes.HasLocation;
 import org.kframework.kil.Definition;
@@ -10,67 +9,32 @@
 import org.kframework.utils.errorsystem.KEMException;
 import scala.util.Either;
 
-import java.util.List;
-import java.util.Optional;
-import java.util.stream.Collectors;
-
 /**
  * A pass which handles all "user group" attributes. Specifically,
- *
- * - Replace every attribute [group(att1,...,attN)] with the underlying attributes [att1,...,attN].
- * - If --pedantic-attributes is disabled, then additionally convert every unrecognized attribute key to a user group.
- *
+ * the attribute [group(att1,...,attN)] is replaced with the underlying attributes [att1,...,attN].
  */
 public class ProcessGroupAttributes {
-
-    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).
-        List<Att.Key> newGroups = Collections.stream(att.rawKeys())
-                .map((k) -> {
-                    Optional<Att.Key> groupKey = Att.getUserGroupOptional(k.key());
-                    if (groupKey.isEmpty()) {
-                        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());
-        for (Att.Key group : newGroups) {
-            att = att.remove(Att.unsafeRawKey(group.key())).add(group);
-        }
-        return att;
-    }
-
-    public static Att getProcessedAtt(Att att, HasLocation node, boolean pedanticAttributes) {
+    public static Att getProcessedAtt(Att att, HasLocation node) {
         Either<String, Att> newAttOrError = att.withGroupAttAsUserGroups();
         if (newAttOrError.isLeft()) {
             throw KEMException.compilerError(newAttOrError.left().get(), node);
         }
         Att newAtt = newAttOrError.right().get();
-
-        if (!pedanticAttributes) {
-            newAtt = convertRawKeysToUserGroups(newAtt, node);
-        }
         return newAtt;
     }
 
-    public static void apply(Module m, boolean pedanticAttributes) {
-        m.setAttributes(getProcessedAtt(m.getAttributes(), m, pedanticAttributes));
+    public static void apply(Module m) {
+        m.setAttributes(getProcessedAtt(m.getAttributes(), m));
         m.getItems().stream()
                 .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)));
     }
 
-    public static void apply(Definition d, boolean pedanticAttributes) {
+    public static void apply(Definition d) {
         d.getItems().stream()
                 .filter((item) -> item instanceof Module)
-                .forEach((m) -> apply((Module) m, pedanticAttributes));
+                .forEach((m) -> apply((Module) m));
     }
 }

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

@@ -51,7 +51,6 @@ public class ResolveFreshConstants {
     private java.util.Set<KVariable> freshVars = new HashSet<>();
     private Map<KVariable, Integer> offsets = new HashMap<>();
     private final String manualTopCell;
-    private final Boolean pedanticAttributes;
 
     private void reset() {
         freshVars.clear();
@@ -188,11 +187,10 @@ private Sentence resolve(Sentence s) {
         return s;
     }
 
-    public ResolveFreshConstants(Definition def, String manualTopCell, FileUtil files, boolean pedanticAttributes) {
+    public ResolveFreshConstants(Definition def, String manualTopCell, FileUtil files) {
         this.def = def;
         this.manualTopCell = manualTopCell;
         this.files = files;
-        this.pedanticAttributes = pedanticAttributes;
     }
 
     public Module resolve(Module m) {
@@ -226,15 +224,15 @@ public Module resolve(Module m) {
 
                 KToken topCellToken = KToken(KLabels.GENERATED_TOP_CELL_NAME, Sort("#CellName"));
                 K generatedTop = KApply(KLabel("#configCell"), topCellToken, KApply(KLabel("#cellPropertyListTerminator")), KApply(KLabels.CELLS, KApply(KLabel("#externalCell"), cellName), freshCell), topCellToken);
-                Set<Sentence> newSentences = GenerateSentencesFromConfigDecl.gen(generatedTop, BooleanUtils.TRUE, Att.empty(), mod.getExtensionModule(), pedanticAttributes);
+                Set<Sentence> newSentences = GenerateSentencesFromConfigDecl.gen(generatedTop, BooleanUtils.TRUE, Att.empty(), mod.getExtensionModule());
                 sentences = (Set<Sentence>) sentences.$bar(newSentences);
                 sentences = (Set<Sentence>) sentences.$bar(immutable(counterSentences));
             }
         }
         if (m.localKLabels().contains(KLabels.GENERATED_TOP_CELL)) {
             RuleGrammarGenerator gen = new RuleGrammarGenerator(def);
             ParseInModule mod = RuleGrammarGenerator.getCombinedGrammar(gen.getConfigGrammar(m), true, files);
-            Set<Sentence> newSentences = GenerateSentencesFromConfigDecl.gen(freshCell, BooleanUtils.TRUE, Att.empty(), mod.getExtensionModule(), pedanticAttributes);
+            Set<Sentence> newSentences = GenerateSentencesFromConfigDecl.gen(freshCell, BooleanUtils.TRUE, Att.empty(), mod.getExtensionModule());
             sentences = (Set<Sentence>) sentences.$bar(newSentences);
             sentences = (Set<Sentence>) sentences.$bar(immutable(counterSentences));
         }