From 8ac87543f7a65e5f022a27672372a758e29fd675 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Fri, 15 Dec 2023 14:42:31 -0500 Subject: [PATCH] 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 --- .../include/kframework/builtin/kast.md | 1 - .../regression-new/issue-1528/3.test.out | 2 +- .../kframework/compile/AddSortInjections.java | 3 - .../parser/binary/BinaryParser.java | 84 ++++++++++++------- .../disambiguation/KAppToTermConsVisitor.java | 12 +-- .../org/kframework/unparser/ToBinary.java | 4 +- .../parser/inner/RuleGrammarTest.java | 6 +- .../kframework/unparser/BinaryKASTTest.java | 9 +- .../org/kframework/unparser/KPrintTest.java | 2 +- .../main/scala/org/kframework/kore/ADT.scala | 9 +- .../scala/org/kframework/kore/interface.scala | 9 +- .../kframework/parser/TreeNodesToKORE.scala | 6 -- 12 files changed, 79 insertions(+), 68 deletions(-) diff --git a/k-distribution/include/kframework/builtin/kast.md b/k-distribution/include/kframework/builtin/kast.md index da392abe46a..a25f4dd38fd 100644 --- 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"(? - bar ( 1 , 0 ) ~> bar ( 1 , 0 ) ~> bar ( 1 , 0 ) ~> . + bar ( 0 , 1 ) ~> bar ( 0 , 1 ) ~> bar ( 0 , 1 ) ~> . diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java index ea10a19af4c..7ab03cbfeb3 100644 --- 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> 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 index 05d5d27a546..d596cc43891 100644 --- 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 @@ *

Format of the KAST binary term is as follows: * *

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". * *

Subsequently, the format contains a post-order traversal of the term according to the * following rules: * - *

* 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. + *

    + *
  • 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 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. + *
* *

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 { + @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 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 klabelCache = new HashMap<>(); private final Map> 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 index df5d928f050..e0ed60fa158 100644 --- 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, 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, 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 index 7df0dac8e1a..dd4f8eda3a2 100644 --- 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 index 56e627d121b..eec6bf902a1 100644 --- 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 index 192be2d42b3..5a08c52db67 100644 --- 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 index cc550fd6818..1be92ca5b37 100644 --- 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(""), 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 index dc9d9cc186c..1aebdb59a17 100644 --- 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 index cfd6a12600c..5f2e751d152 100644 --- 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 index f4c6c162219..2645186ac8a 100644 --- 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 = {