Add check for non-symbol productions with overload(_) attribute (#4143

)

For full context, see the original issue (#4142). This PR implements a
simple check for overloaded non-symbol productions, along with a minimal
test case.

Also included in the PR is an example minimised from the C Semantics
that helps to explain _why_ we would want to overload on subsort
productions (and therefore, why the fix for this issue is a check rather
than, say, forbidding the feature).

In brief, the new integration test minimises part of the C expression
grammar, in which we have the following sort hierarchy:
```
    Exp
     |
    Val
   /   \
RVal   LVal
```
We also wish to construct a corresponding hierarchy of left-associative,
comma-separated syntactic lists over this hierarchy (with the exception
being that there is no need for a list of lvalues):
```
    Exps
     |
    Vals
   /
RVals
```

Typically, the solution here would be to implement the list sorts as K
syntactic lists. For example:
```
syntax Exps ::= NeList{Exp, ","}
```

This is, of course, just syntactic sugar, and we can write down an
equivalent set of productions:
```
syntax Exps ::= Exp
              | Exps "," Exp
```

Note here that the singleton production is a _subsorting_ production
that would, by default, not have an associated `klabel`, and therefore
would not be generated as a KORE symbol.

However, a collision with a separate part of the C grammar does indeed
prevent us from using the `NeList` sugar for this, as we require
finer-grained control over the parsing priorities. The issue is with the
comma operator:
```
syntax Exp ::= Exp "," Exp [left, group(comma)]
```

We require the property that each element in the overloaded list-sort
hierarchy has a higher priority than the comma operator, and so we need
to be able to attach groups to both the singleton and comma productions.

When combined with the necessary overloading attributes on the singleton
list subsorting productions, this situation triggers the bug fixed by
this PR.

Fixes #4142

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

@@ -0,0 +1,13 @@
+module CHECKNOSYMBOLOVERLOAD-SYNTAX
+endmodule
+
+module CHECKNOSYMBOLOVERLOAD
+  syntax LVal
+  syntax RVal
+  syntax Val ::= LVal | RVal
+  syntax Exp ::= Val
+
+  syntax RVals ::= RVal [overload(arg)]
+  syntax Vals  ::= Val  [overload(arg), symbol(val)]
+  syntax Exps  ::= Exp  [overload(arg)]
+endmodule

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

@@ -0,0 +1,11 @@
+[Error] Compiler: Production would not be a KORE symbol and therefore cannot be overloaded. Add a `symbol(_)` attribute to the production.
+	Source(checkNoSymbolOverload.k)
+	Location(10,20,10,40)
+	10 |	  syntax RVals ::= RVal [overload(arg)]
+	   .	                   ^~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Production would not be a KORE symbol and therefore cannot be overloaded. Add a `symbol(_)` attribute to the production.
+	Source(checkNoSymbolOverload.k)
+	Location(12,20,12,40)
+	12 |	  syntax Exps  ::= Exp  [overload(arg)]
+	   .	                   ^~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 2 structural errors.

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/Makefile

@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test

@@ -0,0 +1 @@
+rv(0), rv(1), rv(2), (1, 2)

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test.out

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

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test

@@ -0,0 +1 @@
+rv(0), rv(1), rv(2)

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test.out

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

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/test.k

@@ -0,0 +1,39 @@
+module TEST
+  imports DOMAINS
+
+  syntax LVal ::= lv(Int) | lv(Id)
+  syntax RVal ::= rv(Int)
+  syntax Val  ::= LVal | RVal
+
+  syntax Exp  ::= Int
+                | Id
+                | Val
+                | "(" Exp ")" [bracket]
+                > left:
+                  Exp "," Exp [group(comma)]
+
+  syntax RVals ::= RVal           [overload(arg),  group(assignExp), symbol(rval), avoid]
+                 | RVals "," RVal [overload(exps), group(assignExp)]
+
+  syntax Vals  ::= Val            [overload(arg),  group(assignExp), symbol(val),  avoid]
+                 | Vals "," Val   [overload(exps), group(assignExp)]
+
+  syntax Exps  ::= Exp            [overload(arg),  group(assignExp), symbol(exp),  avoid]
+                 | Exps "," Exp   [overload(exps), group(assignExp)]
+
+  syntax Exps ::= Vals
+  syntax Vals ::= RVals
+
+  syntax priority assignExp > comma
+
+  syntax KItem ::= "rvals"
+                 | "vals"
+                 | "exps"
+
+  configuration
+    <k> $PGM:Exps </k>
+
+  rule _:RVals => rvals
+  rule _:Vals  => vals
+  rule _:Exps  => exps  [owise]
+endmodule

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test

@@ -0,0 +1 @@
+rv(0), lv(x), rv(2)

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test.out

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

kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java

@@ -73,6 +73,7 @@ private void checkProduction(Production prod) {
     checkSymbolKLabel(prod);
     checkKLabelOverload(prod);
     checkNullarySymbol(prod);
+    checkNoSymbolOverload(prod);
   }
 
   private <T extends HasAtt & HasLocation> void checkUnrecognizedAtts(T term) {
@@ -360,6 +361,15 @@ private void checkKLabelOverload(Production prod) {
     }
   }
 
+  private void checkNoSymbolOverload(Production prod) {
+    if (prod.klabel().isEmpty() && prod.att().contains(Att.OVERLOAD())) {
+      errors.add(
+          KEMException.compilerError(
+              "Production would not be a KORE symbol and therefore cannot be overloaded. Add a `symbol(_)` attribute to the production.",
+              prod));
+    }
+  }
+
   private void checkNullarySymbol(Production prod) {
     if (prod.att().contains(Att.SYMBOL()) && !prod.att().contains(Att.KLABEL())) {
       if (prod.att().get(Att.SYMBOL()).isEmpty()) {