Remove KLabel variables (#3877)

This PR removes all logic related to KLabel variables because - They are unsupported by any modern backend - Without KLabel variables, we can assume every variable has sort `S` with `KBott < S <= K`, which addresses some minor annoyances in the sort inferencer. --------- Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Dec 15, 2023 · 8ac8754 · 8ac8754
1 parent 322f223
commit 8ac8754
Show file tree

Hide file tree

Showing 12 changed files with 79 additions and 68 deletions.
diff --git a/k-distribution/include/kframework/builtin/kast.md b/k-distribution/include/kframework/builtin/kast.md
@@ -213,7 +213,6 @@ module KSEQ-SYMBOLIC
   syntax KConfigVar ::= r"(?<![A-Za-z0-9_\\$!\\?@])(\\$)([A-Z][A-Za-z0-9'_]*)"            [token]
   syntax KBott      ::= #KVariable
   syntax KBott      ::= KConfigVar
-  syntax KLabel     ::= #KVariable
 endmodule
 ```
 

diff --git a/k-distribution/tests/regression-new/issue-1528/3.test.out b/k-distribution/tests/regression-new/issue-1528/3.test.out
@@ -1,3 +1,3 @@
 <k>
-  bar ( 1 , 0 ) ~> bar ( 1 , 0 ) ~> bar ( 1 , 0 ) ~> .
+  bar ( 0 , 1 ) ~> bar ( 0 , 1 ) ~> bar ( 0 , 1 ) ~> .
 </k>
diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java
@@ -483,9 +483,6 @@ public static Sort lubSort(
   }
 
   private Production production(KApply term) {
-    if (term.klabel() instanceof KVariable) {
-      throw KEMException.internalError("KORE does not yet support KLabel variables.", term);
-    }
     Option<scala.collection.Set<Production>> prods = mod.productionsFor().get(term.klabel().head());
     if (prods.isEmpty()) {
       throw KEMException.compilerError(

diff --git a/kernel/src/main/java/org/kframework/parser/binary/BinaryParser.java b/kernel/src/main/java/org/kframework/parser/binary/BinaryParser.java
@@ -12,6 +12,7 @@
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
+import org.jetbrains.annotations.NotNull;
 import org.kframework.kore.K;
 import org.kframework.kore.KLabel;
 import org.kframework.kore.KToken;
@@ -24,25 +25,30 @@
  * <p>Format of the KAST binary term is as follows:
  *
  * <p>First five bytes are the magic header "\x7fKAST". Next 3 bytes are the major, minor, and
- * release version of the format. Currently they are set to "\x04\x00\x00".
+ * release version of the format. Currently, they are set to "\x04\x01\x00".
  *
  * <p>Subsequently, the format contains a post-order traversal of the term according to the
  * following rules:
  *
- * <p>* KToken: the byte "\x01" followed by a representation of the string of the token, and then
- * the sort of the token. * KApply: Representation of each child of the KApply followed by the byte
- * "\x02" followed by a representation of the klabel, followed by a 4-byte arity of the KApply. *
- * KSequence: Representation of each child of the KSequence followed by the byte "\x03" followed by
- * a 4-byte length of the KSequence. * KVariable: The byte "\x04" followed by a representation of
- * the name of the variable. * KRewrite: Representation of the LHS of the rewrite, followed by the
- * RHS, followed by the byte "\x05". * InjectedKLabel: The byte "\x06" followed by the
- * representation of the klabel. * KLabel: The representation of the string of the klabel, followed
- * by the byte "\x01" if the klabel is a variable, and "\x00" if it's a concrete klabel. * String: A
- * 4-byte offset in the string intern table. The intern table is commputed as the term is traversed.
- * An offset of 0 means that the string has not appeared before in this term, and is followed by a
- * 4-byte length of the string followed by the String in UTF-16. An offset of 1 means the string
- * refers to the most recent previous string in the intern table. An offset of 2 means the
- * next-most-recent, and so forth.
+ * <ul>
+ *   <li>KToken: the byte "\x01" followed by a representation of the string of the token, and then
+ *       the sort of the token.
+ *   <li>KApply: Representation of each child of the KApply followed by the byte "\x02" followed by
+ *       a representation of the klabel, followed by a 4-byte arity of the KApply.
+ *   <li>KSequence: Representation of each child of the KSequence followed by the byte "\x03"
+ *       followed by a 4-byte length of the KSequence.
+ *   <li>KVariable: The byte "\x04" followed by a representation of the name of the variable.
+ *   <li>KRewrite: Representation of the LHS of the rewrite, followed by the RHS, followed by the
+ *       byte "\x05".
+ *   <li>InjectedKLabel: The byte "\x06" followed by the representation of the klabel.
+ *   <li>KLabel: The representation of the string of the klabel, followed by the byte "\x01" if the
+ *       klabel is a variable, and "\x00" if it's a concrete klabel.
+ *   <li>String: A 4-byte offset in the string intern table. The intern table is computed as the
+ *       term is traversed. An offset of 0 means that the string has not appeared before in this
+ *       term, and is followed by a 4-byte length of the string followed by the String in UTF-16. An
+ *       offset of 1 means the string refers to the most recent previous string in the intern table.
+ *       An offset of 2 means the next-most-recent, and so forth.
+ * </ul>
  *
  * <p>Note one exception to this rule in binary format 4.0.1: if a term is encountered that has
  * already been serialized, instead of serializing it again we serialize the byte '\x08' followed by
@@ -80,8 +86,24 @@ private BinaryParser(ByteBuffer data) {
     this.data = data;
   }
 
-  private K read400(boolean _401) throws IOException {
+  // Version information ordered lexicographically by (major, minor, build)
+  private record BinaryVersion(Integer major, Integer minor, Integer build)
+      implements Comparable<BinaryVersion> {
+    @Override
+    public int compareTo(@NotNull BinaryVersion other) {
+      int majorComp = major.compareTo(other.major);
+      if (majorComp != 0) {
+        return majorComp;
+      }
+      int minorComp = minor.compareTo(other.minor);
+      if (minorComp != 0) {
+        return minorComp;
+      }
+      return build.compareTo(other.build);
+    }
+  }
 
+  private K read(BinaryVersion version) throws IOException {
     Deque<K> stack = new ArrayDeque<>();
     int type = 0;
     while (type != END) {
@@ -98,7 +120,7 @@ private K read400(boolean _401) throws IOException {
           stack.push(token);
           break;
         case KAPPLY:
-          KLabel lbl = readKLabel();
+          KLabel lbl = readKLabel(version);
           arity = data.getInt();
           if (arity == 0) items = EMPTY_KLIST;
           else items = new K[arity];
@@ -125,12 +147,12 @@ private K read400(boolean _401) throws IOException {
           stack.push(KRewrite(left, right));
           break;
         case INJECTEDKLABEL:
-          stack.push(InjectedKLabel(readKLabel()));
+          stack.push(InjectedKLabel(readKLabel(version)));
           break;
         case END:
           break;
         case BACK_REFERENCE:
-          if (!_401)
+          if (version.compareTo(new BinaryVersion(4, 0, 1)) < 0)
             throw KEMException.criticalError("Unexpected code found in KAST binary term: " + type);
           int idx = data.getInt();
           stack.push(kInterns.get(kInterns.size() - idx));
@@ -151,13 +173,18 @@ private K read400(boolean _401) throws IOException {
   private final Map<String, KLabel> klabelCache = new HashMap<>();
   private final Map<String, Map<String, KToken>> ktokenCache = new HashMap<>();
 
-  private KLabel readKLabel() throws IOException {
+  private KLabel readKLabel(BinaryVersion version) {
     String lbl = readString();
-    if (data.get() != 0) return KVariable(lbl);
+    if (version.compareTo(new BinaryVersion(4, 1, 0)) < 0) {
+      if (data.get() == 1) {
+        throw KEMException.compilerError(
+            "Binary data contains variable KLabel, but this is no longer supported.");
+      }
+    }
     return klabelCache.computeIfAbsent(lbl, org.kframework.kore.KORE::KLabel);
   }
 
-  private String readString() throws IOException {
+  private String readString() {
     int idx = data.getInt();
     if (idx == 0) {
       int len = data.getInt();
@@ -192,14 +219,13 @@ public static K parse(ByteBuffer data) {
       int major = data.get();
       int minor = data.get();
       int build = data.get();
-      if (major == 4 && minor == 0 && build == 0) {
-        return new BinaryParser(data).read400(false);
-      } else if (major == 4 && minor == 0 && build == 1) {
-        return new BinaryParser(data).read400(true);
-      } else {
-        throw KEMException.compilerError(
-            "Unsupported version of KAST binary file: " + major + "." + minor + "." + build);
+      if ((major == 4 && minor == 0 && build == 0)
+          || (major == 4 && minor == 0 && build == 1)
+          || (major == 4 && minor == 1 && build == 0)) {
+        return new BinaryParser(data).read(new BinaryVersion(major, minor, build));
       }
+      throw KEMException.compilerError(
+          "Unsupported version of KAST binary file: " + major + "." + minor + "." + build);
     } catch (IOException e) {
       throw KEMException.criticalError("Could not read K term from binary", e);
     }

diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java
@@ -13,7 +13,6 @@
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
 import org.kframework.builtin.KLabels;
-import org.kframework.builtin.Sorts;
 import org.kframework.definition.Module;
 import org.kframework.definition.Production;
 import org.kframework.parser.Ambiguity;
@@ -48,15 +47,10 @@ public Either<java.util.Set<KEMException>, Term> apply(TermCons tc) {
     assert tc.production() != null : this.getClass() + ":" + " production not found." + tc;
     if (tc.production().klabel().isDefined()
         && tc.production().klabel().get().equals(KLabels.KAPP)) {
-      if (!(tc.get(0) instanceof Constant kl)
-          || !((Constant) tc.get(0)).production().sort().equals(Sorts.KLabel()))
-        // TODO: remove check once the java backend is no longer supported.
-        return super.apply(
-            tc); // don't do anything if the label is not a token KLabel (in case of variable or
-      // casted variable)
+      Constant kl = (Constant) tc.get(0);
       String klvalue = kl.value();
       try {
-        klvalue = StringUtil.unescapeKoreKLabel(kl.value());
+        klvalue = StringUtil.unescapeKoreKLabel(klvalue);
       } catch (IllegalArgumentException e) {
         /* ignore */
       } // if possible, unescape
@@ -81,7 +75,7 @@ public Either<java.util.Set<KEMException>, Term> apply(TermCons tc) {
           sol.add(TermCons.apply(terms, prd, tc.location(), tc.source()));
 
       if (sol.size() == 0) {
-        String msg = "Could not find any suitable production for label " + kl.value();
+        String msg = "Could not find any suitable productions for label " + kl.value();
         return Left.apply(Sets.newHashSet(KEMException.innerParserError(msg, kl)));
       } else if (sol.size() == 1) {
         return super.apply(sol.iterator().next());

diff --git a/kernel/src/main/java/org/kframework/unparser/ToBinary.java b/kernel/src/main/java/org/kframework/unparser/ToBinary.java
@@ -32,8 +32,8 @@ public static void apply(OutputStream out, K k) {
       data.writeBytes("KAST");
       // version
       data.writeByte(4);
-      data.writeByte(0);
       data.writeByte(1);
+      data.writeByte(0);
       new ToBinary(data).traverse(k);
       data.writeByte(BinaryParser.END);
     } catch (IOException e) {
@@ -78,7 +78,6 @@ private void traverse(K k) throws IOException {
       data.writeByte(BinaryParser.KAPPLY);
       add_intern(k);
       writeString(app.klabel().name());
-      data.writeBoolean(app.klabel() instanceof KVariable);
       data.writeInt(app.size());
 
     } else if (k instanceof KSequence seq) {
@@ -108,7 +107,6 @@ private void traverse(K k) throws IOException {
       data.writeByte(BinaryParser.INJECTEDKLABEL);
       add_intern(k);
       writeString(inj.klabel().name());
-      data.writeBoolean(inj.klabel() instanceof KVariable);
 
     } else {
       throw KEMException.criticalError("Unimplemented for Binary serialization: ", k);

diff --git a/kernel/src/test/java/org/kframework/parser/inner/RuleGrammarTest.java b/kernel/src/test/java/org/kframework/parser/inner/RuleGrammarTest.java
@@ -36,7 +36,7 @@ public class RuleGrammarTest {
   private FileUtil files;
 
   @Before
-  public void setUp() throws Exception {
+  public void setUp() {
     gen = makeRuleGrammarGenerator();
   }
 
@@ -268,8 +268,10 @@ public void test10() {
             + "syntax Exp ::= Exp \",\" Exp [klabel('Plus), prefer] "
             + "| Exp \"*\" Exp [klabel('Mul)] "
             + "| r\"[0-9]+\" [token] "
+            + "| Foo(K, K, K) "
+            + "syntax K "
             + "endmodule";
-    parseRule("A::KLabel(B::K, C::K, D::K)", def, 0, false);
+    parseRule("Foo(B::K, C::K, D::K)", def, 0, false);
   }
 
   // test config cells

diff --git a/kernel/src/test/java/org/kframework/unparser/BinaryKASTTest.java b/kernel/src/test/java/org/kframework/unparser/BinaryKASTTest.java
@@ -8,6 +8,7 @@
 import org.junit.Ignore;
 import org.junit.Test;
 import org.kframework.kore.K;
+import org.kframework.kore.KLabel;
 import org.kframework.parser.binary.BinaryParser;
 import org.kframework.utils.file.FileUtil;
 
@@ -26,17 +27,17 @@ public class BinaryKASTTest {
                   KRewrite(KVariable("Baz"), KVariable("Baz2")),
                   InjectedKLabel(KLabel("_+_")),
                   KApply(KLabel("foo")))),
-          KApply(KVariable("Lbl"), sharedTerm, sharedTerm, sharedTerm2, sharedTerm));
+          KApply(KLabel("Lbl"), sharedTerm, sharedTerm, sharedTerm2, sharedTerm));
 
   @Test
-  public void testWriteThenRead() throws Exception {
+  public void testWriteThenRead() {
     byte[] str = ToBinary.apply(term);
     K result2 = BinaryParser.parse(str);
     assertEquals(term, result2);
   }
 
   @Test
-  public void testConcatenate() throws Exception {
+  public void testConcatenate() {
     byte[] str = ToBinary.apply(term);
     byte[] krewrite = new byte[str.length * 2 - 8];
     System.arraycopy(str, 0, krewrite, 0, str.length - 1);
@@ -49,7 +50,7 @@ public void testConcatenate() throws Exception {
 
   @Test
   @Ignore
-  public void testLarger() throws Exception {
+  public void testLarger() {
     FileUtil.testFileUtil();
     byte[] kast = FileUtil.loadBytes(new File("/home/dwightguth/c-semantics/tmp-kcc-FzjROvt"));
     K result = BinaryParser.parse(kast);

diff --git a/kernel/src/test/java/org/kframework/unparser/KPrintTest.java b/kernel/src/test/java/org/kframework/unparser/KPrintTest.java
@@ -57,7 +57,7 @@ public void testUnparseThenParse() throws Exception {
         KApply(
             KLabel("<T>"),
             terms.get(3),
-            KApply(KVariable("Lbl"), terms.get(0), terms.get(0), terms.get(1), terms.get(0))));
+            KApply(KLabel("Lbl"), terms.get(0), terms.get(0), terms.get(1), terms.get(0))));
 
     for (K term : terms) {
       for (OutputModes outputMode : outputModes) {

diff --git a/kore/src/main/scala/org/kframework/kore/ADT.scala b/kore/src/main/scala/org/kframework/kore/ADT.scala
@@ -1,12 +1,11 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.kore
 
-import collection.JavaConverters._
 import org.kframework.attributes._
 import org.kframework.builtin.KLabels
 import org.kframework.builtin.Sorts
 import org.kframework.kore
-import org.kframework.kore.KORE.Sort
+import scala.collection.JavaConverters._
 
 /**
  * Abstract Data Types: basic implementations for the inner KORE interfaces.
@@ -69,9 +68,7 @@ object ADT {
       )
   }
 
-  case class KVariable(name: String, att: Att = Att.empty) extends kore.KVariable {
-    def params = Seq()
-  }
+  case class KVariable(name: String, att: Att = Att.empty) extends kore.KVariable {}
 
   case class Sort(name: String, params: kore.Sort*) extends kore.Sort {
     override def toString =
@@ -113,8 +110,6 @@ object SortedADT {
     val sort: Sort =
       if (att.contains(Att.CELL_SORT)) Sorts.K else att.getOptional(classOf[Sort]).orElse(Sorts.K)
 
-    def params = Seq()
-
     override def equals(other: Any) = other match {
       case v: SortedKVariable => name == v.name && sort == v.sort
       // case v: KVariable => throw new UnsupportedOperationException(s"should not mix

diff --git a/kore/src/main/scala/org/kframework/kore/interface.scala b/kore/src/main/scala/org/kframework/kore/interface.scala
@@ -189,10 +189,15 @@ trait KApply extends KItem with KCollection {
 
 trait KSequence extends KCollection with K
 
-trait KVariable extends KItem with KLabel {
+trait KVariable extends KItem {
   def name: String
 
-  def computeHashCode = name.hashCode
+  override def equals(other: Any): Boolean = other match {
+    case l: KVariable => this.name == l.name
+    case _            => false
+  }
+
+  override def computeHashCode: Int = name.hashCode
 }
 
 trait KAs extends K {

diff --git a/kore/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala b/kore/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala
@@ -117,14 +117,8 @@ class TreeNodesToKORE(parseSort: java.util.function.Function[String, Sort]) {
     items.map(down _)
 
   def downKLabel(t: K): KLabel = t match {
-    case t @ KToken(s, sort) if sort == Sorts.KVariable =>
-      KVariable(s.trim, t.att)
-
     case t @ KToken(s, sort) if sort == Sorts.KLabel =>
       KLabel(unquote(t))
-
-    case t @ KApply(KLabel(s), items) if s.startsWith("#SemanticCastTo") =>
-      downKLabel(items.head)
   }
 
   def locationToAtt(l: Optional[Location], s: Optional[Source]): Att = {