Check parameters on attributes

k-distribution/tests/regression-new/checks/attParamForbidden.k

@@ -0,0 +1,7 @@
+// Copyright (c) K Team. All Rights Reserved.
+module ATTPARAMFORBIDDEN
+
+  syntax Foo  ::= a()
+  rule a() => .K [owise(1)]
+
+endmodule

k-distribution/tests/regression-new/checks/attParamForbidden.k.out

@@ -0,0 +1,5 @@
+[Error] Compiler: Parameters for the attribute 'owise' are forbidden.
+	Source(attParamForbidden.k)
+	Location(5,19,5,27)
+	5 |	  rule a() => .K [owise(1)]
+	  .	                  ^~~~~~~~

k-distribution/tests/regression-new/checks/attParamRequired.k

@@ -0,0 +1,7 @@
+// Copyright (c) K Team. All Rights Reserved.
+module ATTPARAMREQUIRED
+
+  syntax Foo  ::= a()
+  rule a() => .K [prec]
+
+endmodule

k-distribution/tests/regression-new/checks/attParamRequired.k.out

@@ -0,0 +1,5 @@
+[Error] Compiler: Parameters for the attribute 'prec' are required.
+	Source(attParamRequired.k)
+	Location(5,19,5,23)
+	5 |	  rule a() => .K [prec]
+	  .	                  ^~~~

kernel/src/main/java/org/kframework/kil/ASTNode.java

@@ -90,6 +90,7 @@ public void setSource(Source source) {
     /**
      * Append an attribute to the list of attributes. In particular,
      * - inserting a key from the attribute whitelist if the attribute is recognized as a built-in
+     * - add the source location to any exceptions (ie. parameter restrictions) thrown when inserting the key
      * - otherwise, inserting an unrecognized key to be errored on later
      *
      * @param key
@@ -100,7 +101,11 @@ public void addBuiltInOrUnrecognizedAttribute(String key, String val, Source sou
         if (att.contains(attKey)) {
             throw KEMException.outerParserError("Duplicate attribute: " + key, source, loc);
         }
-        att = att.add(attKey, val);
+        try {
+            att = att.add(attKey, val);
+        } catch (KEMException e) {
+            throw e.withLocation(loc, source);
+        }
     }
 
     /**

kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java

@@ -533,7 +533,7 @@ public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(Module mod,
         Att att = mod.att();
         List<String> notLrModules = stream(mod.importedModules()).filter(m -> m.att().contains(Att.NOT_LR1())).map(Module::name).collect(Collectors.toList());
         if (!notLrModules.isEmpty()) {
-          att = att.add(Att.NOT_LR1(), notLrModules.toString());
+          att = att.add(Att.NOT_LR1_MODULES(), notLrModules.toString());
         }
         Module extensionM = new Module(mod.name() + "-EXTENSION", Set(Import(origMod, true)), immutable(extensionProds), att);
         Module disambM = new Module(mod.name() + "-DISAMB", Set(), immutable(disambProds), att);

kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java

@@ -117,8 +117,8 @@ public static Module transformByPriorityAndAssociativity(Module module) {
   }
 
   public static void writeParser(Module module, Module disambModule, Scanner scanner, Sort start, File path, boolean glr, long stackDepth, KExceptionManager kem) {
-    if (module.att().contains(Att.NOT_LR1())) {
-        kem.registerInnerParserWarning(ExceptionType.NON_LR_GRAMMAR, "Skipping modules " + module.att().get(Att.NOT_LR1()) + " tagged as " + Att.NOT_LR1() + " which are not supported by Bison.");
+    if (module.att().contains(Att.NOT_LR1_MODULES())) {
+        kem.registerInnerParserWarning(ExceptionType.NON_LR_GRAMMAR, "Skipping modules " + module.att().get(Att.NOT_LR1_MODULES()) + " tagged as " + Att.NOT_LR1() + " which are not supported by Bison.");
     }
     module = transformByPriorityAndAssociativity(module);
     StringBuilder bison = new StringBuilder();