Add attribute whitelist and group(_) attribute

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java

@@ -78,7 +78,7 @@ public void accept(Backend.Holder h) {
     }
 
     @Override
-    public Set<String> excludedModuleTags() {
-        return new HashSet<>(Arrays.asList(Att.CONCRETE(), "kast"));
+    public Set<Att.Key> excludedModuleTags() {
+        return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
     }
 }

k-distribution/include/kframework/builtin/domains.md

@@ -879,13 +879,13 @@ and `orBool` may be short-circuited in concrete backends, but in symbolic
 ackends, both arguments will be evaluated.
 
 ```k
-  syntax Bool ::= "notBool" Bool          [function, total, klabel(notBool_), symbol, smt-hook(not), boolOperation, latex(\neg_{\scriptstyle\it Bool}{#1}), hook(BOOL.not)]
-                > Bool "andBool" Bool     [function, total, klabel(_andBool_), symbol, left, smt-hook(and), boolOperation, latex({#1}\wedge_{\scriptstyle\it Bool}{#2}), hook(BOOL.and)]
-                | Bool "andThenBool" Bool [function, total, klabel(_andThenBool_), symbol, left, smt-hook(and), boolOperation, hook(BOOL.andThen)]
-                | Bool "xorBool" Bool     [function, total, klabel(_xorBool_), symbol, left, smt-hook(xor), boolOperation, hook(BOOL.xor)]
-                | Bool "orBool" Bool      [function, total, klabel(_orBool_), symbol, left, smt-hook(or), boolOperation, latex({#1}\vee_{\scriptstyle\it Bool}{#2}), hook(BOOL.or)]
-                | Bool "orElseBool" Bool  [function, total, klabel(_orElseBool_), symbol, left, smt-hook(or), boolOperation, hook(BOOL.orElse)]
-                | Bool "impliesBool" Bool [function, total, klabel(_impliesBool_), symbol, left, smt-hook(=>), boolOperation, hook(BOOL.implies)]
+  syntax Bool ::= "notBool" Bool          [function, total, klabel(notBool_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Bool}{#1}), hook(BOOL.not)]
+                > Bool "andBool" Bool     [function, total, klabel(_andBool_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Bool}{#2}), hook(BOOL.and)]
+                | Bool "andThenBool" Bool [function, total, klabel(_andThenBool_), symbol, left, smt-hook(and), group(boolOperation), hook(BOOL.andThen)]
+                | Bool "xorBool" Bool     [function, total, klabel(_xorBool_), symbol, left, smt-hook(xor), group(boolOperation), hook(BOOL.xor)]
+                | Bool "orBool" Bool      [function, total, klabel(_orBool_), symbol, left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Bool}{#2}), hook(BOOL.or)]
+                | Bool "orElseBool" Bool  [function, total, klabel(_orElseBool_), symbol, left, smt-hook(or), group(boolOperation), hook(BOOL.orElse)]
+                | Bool "impliesBool" Bool [function, total, klabel(_impliesBool_), symbol, left, smt-hook(=>), group(boolOperation), hook(BOOL.implies)]
                 > left:
                   Bool "==Bool" Bool      [function, total, klabel(_==Bool_), symbol, left, comm, smt-hook(=), hook(BOOL.eq)]
                 | Bool "=/=Bool" Bool     [function, total, klabel(_=/=Bool_), symbol, left, comm, smt-hook(distinct), hook(BOOL.ne)]
@@ -2038,8 +2038,8 @@ module K-EQUAL-SYNTAX
   imports private BASIC-K
 
   syntax Bool ::= left:
-                  K "==K" K           [function, total, comm, smt-hook(=), hook(KEQUAL.eq), klabel(_==K_), symbol, latex({#1}\mathrel{=_K}{#2}), equalEqualK]
-                | K "=/=K" K          [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), klabel(_=/=K_), symbol, latex({#1}\mathrel{\neq_K}{#2}), notEqualEqualK]
+                  K "==K" K           [function, total, comm, smt-hook(=), hook(KEQUAL.eq), klabel(_==K_), symbol, latex({#1}\mathrel{=_K}{#2}), group(equalEqualK)]
+                | K "=/=K" K          [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), klabel(_=/=K_), symbol, latex({#1}\mathrel{\neq_K}{#2}), group(notEqualEqualK)]
 
   syntax priorities equalEqualK notEqualEqualK > boolOperation mlOp
 

k-distribution/include/kframework/builtin/kast.md

@@ -102,7 +102,7 @@ module KSEQ
              | ".::K"    [klabel(#EmptyK), symbol, unparseAvoid]
   syntax K ::= K "~>" K  [klabel(#KSequence), left, assoc, unit(#EmptyK), symbol]
   syntax left #KSequence
-  syntax {Sort} Sort     ::= "(" Sort ")"    [bracket, defaultBracket, applyPriority(1)]
+  syntax {Sort} Sort     ::= "(" Sort ")"    [bracket, group(defaultBracket), applyPriority(1)]
 endmodule
 ```
 
@@ -138,26 +138,26 @@ The correspondance between K symbols and KORE symbols is as follows:
 module ML-SYNTAX [not-lr1]
   imports SORT-K
 
-  syntax {Sort} Sort ::= "#Top" [klabel(#Top), symbol, mlUnary]
-                       | "#Bottom" [klabel(#Bottom), symbol, mlUnary]
-                       | "#True" [klabel(#Top), symbol, mlUnary, unparseAvoid]
-                       | "#False" [klabel(#Bottom), symbol, mlUnary, unparseAvoid]
-                       | "#Not" "(" Sort ")" [klabel(#Not), symbol, mlOp, mlUnary]
+  syntax {Sort} Sort ::= "#Top" [klabel(#Top), symbol, group(mlUnary)]
+                       | "#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)]
 
-  syntax {Sort1, Sort2} Sort2 ::= "#Ceil" "(" Sort1 ")" [klabel(#Ceil), symbol, mlOp, mlUnary]
-                                | "#Floor" "(" Sort1 ")" [klabel(#Floor), symbol, mlOp, mlUnary]
-                                | "{" Sort1 "#Equals" Sort1 "}" [klabel(#Equals), symbol, mlOp, 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)]
+                                | "#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 priorities mlUnary > mlEquals > mlAnd
 
-  syntax {Sort} Sort ::= Sort "#And" Sort [klabel(#And), symbol, assoc, left, comm, unit(#Top), mlOp, mlAnd, 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), 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, mlImplies, 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 priorities mlImplies > mlQuantifier
 
-  syntax {Sort1, Sort2} Sort2 ::= "#Exists" Sort1 "." Sort2 [klabel(#Exists), symbol, mlOp, mlBinder, mlQuantifier]
-                                | "#Forall" Sort1 "." Sort2 [klabel(#Forall), symbol, mlOp, mlBinder, 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 {Sort} Sort ::= "#AG" "(" Sort ")" [klabel(#AG), symbol, mlOp]
                        | "#wEF" "(" Sort ")" [klabel(weakExistsFinally), symbol, mlOp]
@@ -484,8 +484,8 @@ module K
       change in the future).*/
 
   syntax Bool ::= left:
-                  K ":=K" K           [function, total, klabel(_:=K_), symbol, equalEqualK]
-                | K ":/=K" K          [function, total, klabel(_:/=K_), symbol, notEqualEqualK]
+                  K ":=K" K           [function, total, klabel(_:=K_), symbol, group(equalEqualK)]
+                | K ":/=K" K          [function, total, klabel(_:/=K_), symbol, group(notEqualEqualK)]
 endmodule
 
 // To be used to parse terms in full K

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

@@ -6,6 +6,7 @@
 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.parser.inner.CollectProductionsVisitor;
 import org.kframework.kil.loader.Context;
@@ -96,6 +97,8 @@ protected DefinitionWithContext parseUsingOuter(File definitionFile) {
         def.setItems(Outer.parse(Source.apply(definitionFile.getPath()), definitionText, null));
         def.setMainModule("TEST");
         def.setMainSyntaxModule("TEST");
+
+        ProcessGroupAttributes.apply(def, true);
         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);
+        KILtoKORE kilToKore = new KILtoKORE(defWithContext.context, false, false, false);
         org.kframework.definition.Definition koreDef = kilToKore.apply(defWithContext.definition);
         String koreDefString = koreDef.toString();
         return koreDefString;

k-distribution/src/test/scala/org/kframework/backend/kore/ClaimAttributes.scala

@@ -3,6 +3,7 @@ package org.kframework.backend.kore
 
 import org.junit.Assert._
 import org.junit.Test
+import org.kframework.attributes.Att
 import org.kframework.builtin.KLabels
 import org.kframework.parser.kore._
 
@@ -19,7 +20,7 @@ class ClaimAttributes extends KoreTest {
     var one_path = 0
     var all_path = 0
     for (claim <- claims)  {
-      if (this.hasAttribute(claim.att, "one-path")) {
+      if (this.hasAttribute(claim.att, Att.ONE_PATH.key)) {
         one_path=one_path+1;
         assertEquals(KLabels.RL_wEF.name, claim.pattern.asInstanceOf[Implies]._2.asInstanceOf[Application].head.ctr);
       } else {

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

@@ -4,7 +4,7 @@ module BADFUNCTIONRULEWITHCONTEXT
   imports BOOL
   imports MAP
 
-syntax Int ::= foo(Int) [withConfig, function]
+syntax Int ::= foo(Int) [function]
 
 configuration <k> $PGM:K </k> <bar> 0 </bar>
 

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

@@ -0,0 +1,5 @@
+// Copyright (c) K Team. All Rights Reserved.
+module TEST
+  syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2)]
+               | Int "+" Int [group(function)]
+endmodule

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

@@ -0,0 +1,5 @@
+[Error] Compiler: User-defined group 'function' conflicts with built-in or internal attribute.
+	Source(checkGroup.k)
+	Location(4,18,4,47)
+	4 |	               | Int "+" Int [group(function)]
+	  .	                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

@@ -4,7 +4,7 @@ module NESTEDFUNCTIONCONTEXT
   imports BOOL
   imports MAP
 
-syntax Int ::= foo(Int) [withConfig, function]
+syntax Int ::= foo(Int) [function]
 
 configuration <k> $PGM:K </k> <bar> 0 </bar> <baz> .K </baz>
 

k-distribution/tests/regression-new/group/1.test

@@ -0,0 +1 @@
+6 / 2 - 2 - 1

k-distribution/tests/regression-new/group/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  0 ~> .
+</k>

k-distribution/tests/regression-new/group/Makefile

@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--pedantic-attributes
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/group/test.k

@@ -0,0 +1,27 @@
+// Copyright (c) K Team. All Rights Reserved.
+module TEST-SYNTAX
+  imports INT-SYNTAX
+
+  syntax Int ::=
+      "(" Int ")" [bracket]
+    | "-" 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)]
+
+  syntax priority unmin > muldiv > plusmin
+  syntax left lefty
+  syntax left muldiv
+endmodule
+
+module TEST
+  imports TEST-SYNTAX
+  imports INT
+
+  rule    - I2 => 0    -Int I2
+  rule I1 * I2 => I1   *Int I2
+  rule I1 / I2 => I1 divInt I2
+  rule I1 + I2 => I1   +Int I2
+  rule I1 - I2 => I1   -Int I2
+endmodule

k-distribution/tests/regression-new/pedanticAttributes/Makefile

@@ -0,0 +1,3 @@
+KOMPILE_FLAGS=-w none --syntax-module TEST --pedantic-attributes
+
+include ../../../include/kframework/ktest-fail.mak

k-distribution/tests/regression-new/pedanticAttributes/test.k

@@ -0,0 +1,5 @@
+// Copyright (c) K Team. All Rights Reserved.
+module TEST
+  syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2), badAtt(10)]
+               | Int "+" Int [group(badAttButOkay),badAtt,function]
+endmodule

k-distribution/tests/regression-new/pedanticAttributes/test.k.out

@@ -0,0 +1,13 @@
+[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]
+	  .	                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 2 structural errors.

k-distribution/tests/regression-new/proof-tests/deposit/test/imap.k

@@ -1,9 +1,9 @@
 // Copyright (c) K Team. All Rights Reserved.
 module IMAP-SYNTAX
     imports INT
-    syntax IMap [smt-prelude] // (define-sort IMap () (Array Int Int))
-    syntax IMap ::= IMap "[" Int "<-" Int "]" [function, total, no-evaluators, klabel(store),  smtlib(store),  smt-prelude] //, hook(MAP.update)]
-    syntax Int  ::= IMap "[" Int "]"          [function, klabel(select), smtlib(select), smt-prelude] //, hook(MAP.lookup)]
+    syntax IMap // (define-sort IMap () (Array Int Int))
+    syntax IMap ::= IMap "[" Int "<-" Int "]" [function, total, no-evaluators, klabel(store),  smtlib(store)] //, hook(MAP.update)]
+    syntax Int  ::= IMap "[" Int "]"          [function, klabel(select), smtlib(select)] //, hook(MAP.lookup)]
     syntax IMap ::= ".IMap"
 endmodule
 

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

@@ -124,7 +124,8 @@ 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).resolve(m), "resolving !Var variables").apply(d);
+        Function1<Definition, Definition> resolveFreshConstants = d ->
+                DefinitionTransformer.from(m -> new ResolveFreshConstants(d, kompileOptions.topCell, files, kompileOptions.outerParsing.pedanticAttributes).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");
@@ -198,7 +199,8 @@ public Function<Module, Module> specificationSteps(Definition def) {
         ModuleTransformer addImplicitComputationCell = ModuleTransformer.fromSentenceTransformer(
                 new AddImplicitComputationCell(configInfo, labelInfo)::apply,
                 "concretizing configuration");
-        Function1<Module, Module> resolveFreshConstants = d -> ModuleTransformer.from(new ResolveFreshConstants(def, kompileOptions.topCell, files)::resolve, "resolving !Var variables").apply(d);
+        Function1<Module, Module> resolveFreshConstants = d ->
+                ModuleTransformer.from(new ResolveFreshConstants(def, kompileOptions.topCell, files, kompileOptions.outerParsing.pedanticAttributes)::resolve, "resolving !Var variables").apply(d);
         ModuleTransformer concretizeCells = ModuleTransformer.fromSentenceTransformer(
                 new ConcretizeCells(configInfo, labelInfo, sortInfo, mod)::concretize,
                 "concretizing configuration");
@@ -227,7 +229,7 @@ public Sentence checkSimpIsFunc(Module m, Sentence s) {
         if (s instanceof Rule && (s.att().contains(Att.SIMPLIFICATION()))) {
             KLabel kl = m.matchKLabel((Rule) s);
             Att atts = m.attributesFor().get(kl).getOrElse(Att::empty);
-            if (!(atts.contains(Att.FUNCTION()) || atts.contains(Att.FUNCTIONAL()) || atts.contains("mlOp")))
+            if (!(atts.contains(Att.FUNCTION()) || atts.contains(Att.FUNCTIONAL()) || atts.contains(Att.ML_OP())))
                 throw  KEMException.compilerError("Simplification rules expect function/functional/mlOp symbols at the top of the left hand side term.", s);
         }
         return s;
@@ -259,7 +261,7 @@ private Module removeAnywhereRules(Module m) {
     }
 
     @Override
-    public Set<String> excludedModuleTags() {
-        return Collections.singleton("symbolic");
+    public Set<Att.Key> excludedModuleTags() {
+        return Collections.singleton(Att.SYMBOLIC());
     }
 }