Remove kast and kore attributes (#3942)

This PR removes the `kast` and `kore` attributes due to the fact that - All modern backends are KORE-based - Any potential future non-KORE based backend will have different considerations than the previous backends which motivated these attributes, so there's no point keeping existing usages around Additionally, we remove logic in the frontend pertaining to an old usage of `kore` as an attribute on rules which is undocumented and unused in all our semantics. A textual search https://github.com/search?q=org%3Aruntimeverification+%2Fmodule.*%5C%5B.*%28kore%7Ckast%29.*%5C%5D%2F&type=code shows a few lingering usages of `kore` on modules that need to be removed before this is merged: - runtimeverification/pyk#855 - runtimeverification/evm-semantics#2279
runtimeverification · Feb 5, 2024 · 3fee0eb · 3fee0eb
1 parent 14c2c87
commit 3fee0eb
Show file tree

Hide file tree

Showing 13 changed files with 41 additions and 78 deletions.
diff --git a/docs/user_manual.md b/docs/user_manual.md
@@ -2973,10 +2973,8 @@ arguments. A legend describing how to interpret the index follows.
 | `type = "_"`          | cell  | all     | [Collection Cells: `multiplicity` and `type` attributes](#collection-cells-multiplicity-and-type-attributes)                                    |
 | `unboundVariables(_)` | rule  | all     | [The `unboundVariables` attribute](#the-unboundvariables-attribute)                                                                             |
 | `unused`              | prod  | all     | [`unused` attribute](#unused-attribute)                                                                                                         |
-| `kast`                | mod   | all     | Specify that this module should only be included in KAST backends (Java backend).                                                               |
-| `kore`                | mod   | all     | Specify that this module should only be included in Kore backends (Haskell/LLVM backend).                                                       |
 | `concrete`            | mod   | all     | Specify that this module should only be included in concrete backends (LLVM backend).                                                           |
-| `symbolic`            | mod   | all     | Specify that this module should only be included in symbolic backends (Haskell/Java backend).                                                   |
+| `symbolic`            | mod   | all     | Specify that this module should only be included in symbolic backends (Haskell backend).                                                        |
 | `stream = "_"`        | cell  | all     | Specify that this cell should be hooked up to a stream, either `stdin`, `stdout`, or `stderr`.                                                  |
 
 ### Internal Attribute Index

diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java
@@ -4,7 +4,7 @@
 import com.google.inject.Inject;
 import java.io.IOException;
 import java.util.ArrayList;
-import java.util.Arrays;
+import java.util.Collections;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
@@ -79,6 +79,6 @@ public void accept(Backend.Holder h) {
 
   @Override
   public Set<Att.Key> excludedModuleTags() {
-    return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
+    return new HashSet<>(Collections.singletonList(Att.CONCRETE()));
   }
 }
diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md
@@ -189,7 +189,7 @@ module ARRAY-SYMBOLIC [symbolic]
   imports ARRAY-IN-K
 endmodule
 
-module ARRAY-KORE [kore]
+module ARRAY-KORE
   imports ARRAY-IN-K
 endmodule
 
@@ -403,7 +403,7 @@ simplify terms.
 ```k
 endmodule
 
-module MAP-KORE-SYMBOLIC [kore,symbolic,haskell]
+module MAP-KORE-SYMBOLIC [symbolic,haskell]
   imports MAP
   imports private K-EQUAL
   imports private BOOL
@@ -814,7 +814,7 @@ The following lemmas are simplifications that the Haskell backend can
 apply to simplify expressions of sort `Set`.
 
 ```k
-module SET-KORE-SYMBOLIC [kore,symbolic,haskell]
+module SET-KORE-SYMBOLIC [symbolic,haskell]
   imports SET
   imports private K-EQUAL
   imports private BOOL
@@ -1150,7 +1150,7 @@ operations listed above.
   rule B1:Bool =/=Bool B2:Bool => notBool (B1 ==Bool B2)
 endmodule
 
-module BOOL-KORE [kore, symbolic]
+module BOOL-KORE [symbolic]
   imports BOOL-COMMON
 
   rule {true #Equals notBool @B} => {false #Equals @B} [simplification]
@@ -1359,7 +1359,7 @@ module INT-SYMBOLIC [symbolic]
   rule 0 >>Int _ => 0 [simplification]
 endmodule
 
-module INT-SYMBOLIC-KORE [symbolic, kore, haskell]
+module INT-SYMBOLIC-KORE [symbolic, haskell]
   imports INT-COMMON
   imports ML-SYNTAX
   imports private BOOL
@@ -1372,7 +1372,7 @@ module INT-SYMBOLIC-KORE [symbolic, kore, haskell]
   rule #Ceil(@I1:Int <<Int  @I2:Int) => {(@I2 >=Int 0)  #Equals true} #And #Ceil(@I1) #And #Ceil(@I2) [simplification]
 endmodule
 
-module INT-KORE [kore, symbolic]
+module INT-KORE [symbolic]
   imports private K-EQUAL
   imports private BOOL
   imports INT-COMMON
@@ -1894,7 +1894,7 @@ of the above operations in K.
 
 endmodule
 
-module STRING-KORE [kore, symbolic]
+module STRING-KORE [symbolic]
   imports private K-EQUAL
   imports STRING-COMMON
 
@@ -1980,7 +1980,7 @@ endmodule
 ```
 
 ```k
-module BYTES-STRING-ENCODE [kore, symbolic]
+module BYTES-STRING-ENCODE [symbolic]
   imports BYTES-SYNTAX
 ```
 ### Encoding/decoding between Bytes and String
@@ -2182,12 +2182,12 @@ module BYTES-CONCRETE [concrete]
   imports BYTES-HOOKED
 endmodule
 
-module BYTES-KORE [kore]
+module BYTES-KORE
   imports BYTES-HOOKED
   imports BYTES-SYMBOLIC-CEIL
 endmodule
 
-module BYTES-SYMBOLIC-CEIL [symbolic, kore]
+module BYTES-SYMBOLIC-CEIL [symbolic]
   imports BYTES-HOOKED
   imports private INT
   imports private BOOL
@@ -2283,7 +2283,7 @@ module K-EQUAL-SYNTAX
 
 endmodule
 
-module K-EQUAL-KORE [kore, symbolic]
+module K-EQUAL-KORE [symbolic]
   import private BOOL
   import K-EQUAL-SYNTAX
 

diff --git a/k-distribution/include/kframework/builtin/rat.md b/k-distribution/include/kframework/builtin/rat.md
@@ -100,7 +100,7 @@ module RAT-COMMON
   syntax Rat ::= "<" Int "," Int ">Rat" [format(%2 /Rat %4)]
 endmodule
 
-module RAT-SYMBOLIC [symbolic, kore]
+module RAT-SYMBOLIC [symbolic]
   imports private RAT-COMMON
   imports ML-SYNTAX
   imports private BOOL
@@ -112,7 +112,7 @@ module RAT-SYMBOLIC [symbolic, kore]
   [simplification]
 endmodule
 
-module RAT-KORE [kore]
+module RAT-KORE
   imports private RAT-COMMON
   imports private K-EQUAL
 

diff --git a/k-distribution/tests/profiling/evm-semantics/test.k b/k-distribution/tests/profiling/evm-semantics/test.k
@@ -3644,7 +3644,7 @@ module INT-SIMPLIFICATION
   imports public INT-SIMPLIFICATION-HASKELL
 endmodule
 
-module INT-SIMPLIFICATION-HASKELL [kore, symbolic]
+module INT-SIMPLIFICATION-HASKELL [symbolic]
   imports public INT-SIMPLIFICATION-COMMON
   rule A +Int B => B +Int A  [concrete(A), simplification(40), symbolic(B)]
   rule A +Int (B +Int C) => (A +Int B) +Int C  [simplification(40), symbolic(A, B)]
@@ -3750,15 +3750,15 @@ module INT-SIMPLIFICATION-COMMON
        [comm, simplification]
 endmodule
 
-module EVM-OPTIMIZATIONS-LEMMAS [kore, symbolic]
+module EVM-OPTIMIZATIONS-LEMMAS [symbolic]
   imports public EVM
   rule #sizeWordStack(WS           , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0                 [simplification]
   rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N)        requires I <Int #sizeWordStack(WS)  [simplification]
   rule 0 <=Int #sizeWordStack(_ , 0)    => true                                                             [simplification]
   rule #sizeWordStack(_ , 0) <Int N     => false                        requires N <=Int 0                  [simplification]
 endmodule
 
-module EVM-OPTIMIZATIONS [kore]
+module EVM-OPTIMIZATIONS
   imports public EVM
   imports public EVM-OPTIMIZATIONS-LEMMAS
   imports public INT-SIMPLIFICATION

diff --git a/k-distribution/tests/regression-new/checks/restrictedAtts.k b/k-distribution/tests/regression-new/checks/restrictedAtts.k
@@ -1,7 +1,7 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module RESTRICTEDATTS
 
-  syntax Foo  ::= a() [cool, kore, left]
+  syntax Foo  ::= a() [cool, left]
   rule a() => .K [idem, owise]
 
 endmodule
diff --git a/k-distribution/tests/regression-new/checks/restrictedAtts.k.out b/k-distribution/tests/regression-new/checks/restrictedAtts.k.out
@@ -1,8 +1,8 @@
-[Error] Compiler: Production cannot have the following attributes: [cool, kore]
+[Error] Compiler: Production cannot have the following attributes: [cool]
 	Source(restrictedAtts.k)
-	Location(4,19,4,41)
-	4 |	  syntax Foo  ::= a() [cool, kore, left]
-	  .	                  ^~~~~~~~~~~~~~~~~~~~~~
+	Location(4,19,4,35)
+	4 |	  syntax Foo  ::= a() [cool, left]
+	  .	                  ^~~~~~~~~~~~~~~~
 [Error] Compiler: Rule cannot have the following attributes: [idem]
 	Source(restrictedAtts.k)
 	Location(5,8,5,17)

diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -72,7 +72,6 @@
 class RuleInfo {
   boolean isEquation;
   boolean isOwise;
-  boolean isKore;
   boolean isCeil;
   Production production;
   String productionSortStr;
@@ -83,7 +82,6 @@ class RuleInfo {
   public RuleInfo(
       boolean equation,
       boolean owise,
-      boolean kore,
       boolean ceil,
       Production production,
       String prodSortStr,
@@ -92,7 +90,6 @@ public RuleInfo(
       List<K> leftChildren) {
     this.isEquation = equation;
     this.isOwise = owise;
-    this.isKore = kore;
     this.isCeil = ceil;
     this.production = production;
     this.productionSortStr = prodSortStr;
@@ -407,7 +404,7 @@ private void collectTokenSortsAndAttributes(
       collectAttributes(attributes, att);
       RuleInfo ruleInfo = getRuleInfo(r, heatCoolEq, topCellSortStr);
       // only collect priorities of semantics rules
-      if (!ruleInfo.isEquation && !ruleInfo.isKore && !ExpandMacros.isMacro(r)) {
+      if (!ruleInfo.isEquation && !ExpandMacros.isMacro(r)) {
         priorities.add(getPriority(att));
       }
     }
@@ -1025,7 +1022,6 @@ private Optional<SentenceType> getSentenceType(Att att) {
   private RuleInfo getRuleInfo(RuleOrClaim rule, boolean heatCoolEq, String topCellSortStr) {
     boolean equation = false;
     boolean owise = false;
-    boolean kore = rule.att().contains(Att.KORE());
     boolean ceil = false;
     Production production = null;
     Sort productionSort = null;
@@ -1055,7 +1051,7 @@ private RuleInfo getRuleInfo(RuleOrClaim rule, boolean heatCoolEq, String topCel
       }
       if (isFunction(production)
           || rule.att().contains(Att.SIMPLIFICATION())
-          || rule.att().contains(Att.ANYWHERE()) && !kore) {
+          || rule.att().contains(Att.ANYWHERE())) {
         leftChildren = ((KApply) leftPattern).items();
         equation = true;
       } else if ((rule.att().contains(Att.HEAT()) || rule.att().contains(Att.COOL()))
@@ -1072,7 +1068,6 @@ private RuleInfo getRuleInfo(RuleOrClaim rule, boolean heatCoolEq, String topCel
     return new RuleInfo(
         equation,
         owise,
-        kore,
         ceil,
         production,
         productionSortStr,
@@ -1308,17 +1303,6 @@ private void convertRule(
         convert(consideredAttributes, rule.att(), sb, freeVarsMap, rule);
         sb.append("\n\n");
       }
-    } else if (ruleInfo.isKore) {
-      assertNoExistentials(rule, existentials);
-      if (rule instanceof Claim) {
-        sb.append("  claim{} ");
-      } else {
-        sb.append("  axiom{} ");
-      }
-      convert(left, sb);
-      sb.append("\n  ");
-      convert(consideredAttributes, rule.att(), sb, freeVarsMap, rule);
-      sb.append("\n\n");
     } else if (!ExpandMacros.isMacro(rule)) {
       // generate rule LHS
       if (!(rule instanceof Claim)) {

diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java b/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java
@@ -57,8 +57,7 @@ public Sentence apply(Module m, Sentence s) {
   private boolean skipSentence(Sentence s) {
     return ExpandMacros.isMacro(s)
         || s.att().contains(Att.ANYWHERE())
-        || s.att().contains(Att.SIMPLIFICATION())
-        || s.att().contains(Att.KORE());
+        || s.att().contains(Att.SIMPLIFICATION());
   }
 
   // If there are multiple cells mentioned in the split configuration, we don't

diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java b/kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java
@@ -21,12 +21,9 @@ public class CheckConfigurationCells {
 
   private final Module module;
 
-  private final boolean isSymbolicKast;
-
-  public CheckConfigurationCells(Set<KEMException> errors, Module module, boolean isSymbolicKast) {
+  public CheckConfigurationCells(Set<KEMException> errors, Module module) {
     this.errors = errors;
     this.module = module;
-    this.isSymbolicKast = isSymbolicKast;
   }
 
   public void check(Sentence s) {
@@ -60,15 +57,13 @@ private void check(Production p) {
       }
       if (p.att().getOptional(Att.MULTIPLICITY()).orElse("").equals("*")
           && p.att().getOptional(Att.TYPE()).orElse("Bag").equals("Bag")) {
-        if (!isSymbolicKast) {
-          errors.add(
-              KEMException.compilerError(
-                  "Cell bags are only supported on the Java backend. If you want this feature,"
-                      + " comment on https://github.com/runtimeverification/k/issues/1419 . As a"
-                      + " workaround, you can add the attribute type=\"Set\" and add a unique"
-                      + " identifier to each element in the set.",
-                  p));
-        }
+        errors.add(
+            KEMException.compilerError(
+                "Cell bags are only supported on the Java backend. If you want this feature,"
+                    + " comment on https://github.com/runtimeverification/k/issues/1419 . As a"
+                    + " workaround, you can add the attribute type=\"Set\" and add a unique"
+                    + " identifier to each element in the set.",
+                p));
       }
     }
   }

diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java
@@ -243,13 +243,7 @@ public CompiledDefinition run(
     ConfigurationInfoFromModule configInfo =
         new ConfigurationInfoFromModule(kompiledDefinition.mainModule());
 
-    boolean isKast = excludedModuleTags.contains(Att.KORE());
-    Sort rootCell;
-    if (isKast) {
-      rootCell = configInfo.getRootCell();
-    } else {
-      rootCell = Sorts.GeneratedTopCell();
-    }
+    Sort rootCell = Sorts.GeneratedTopCell();
     CompiledDefinition def =
         new CompiledDefinition(
             kompileOptions,
@@ -602,7 +596,6 @@ public void structuralChecks(
       Set<Att.Key> excludedModuleTags) {
     checkAnywhereRules(modules);
     boolean isSymbolic = excludedModuleTags.contains(Att.CONCRETE());
-    boolean isKast = excludedModuleTags.contains(Att.KORE());
     CheckRHSVariables checkRHSVariables =
         new CheckRHSVariables(errors, !isSymbolic, kompileOptions.backend);
     stream(modules).forEach(m -> stream(m.localSentences()).forEach(checkRHSVariables::check));
@@ -611,9 +604,7 @@ public void structuralChecks(
 
     stream(modules)
         .forEach(
-            m ->
-                stream(m.localSentences())
-                    .forEach(new CheckConfigurationCells(errors, m, isSymbolic && isKast)::check));
+            m -> stream(m.localSentences()).forEach(new CheckConfigurationCells(errors, m)::check));
 
     stream(modules)
         .forEach(
@@ -628,10 +619,8 @@ public void structuralChecks(
     stream(modules)
         .forEach(m -> stream(m.localSentences()).forEach(new CheckHOLE(errors, m)::check));
 
-    if (!(isSymbolic && isKast)) { // if it's not the java backend
-      stream(modules)
-          .forEach(m -> stream(m.localSentences()).forEach(new CheckTokens(errors, m)::check));
-    }
+    stream(modules)
+        .forEach(m -> stream(m.localSentences()).forEach(new CheckTokens(errors, m)::check));
 
     stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckK(errors)::check));
 

diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala
@@ -285,9 +285,7 @@ object Att {
     Key.builtin("initializer", KeyParameter.Forbidden, onlyon2[Production, Rule])
   final val INJECTIVE = Key.builtin("injective", KeyParameter.Forbidden, onlyon[Production])
   final val INTERNAL  = Key.builtin("internal", KeyParameter.Forbidden, onlyon[Production])
-  final val KAST      = Key.builtin("kast", KeyParameter.Forbidden, onlyon[Module])
   final val KLABEL    = Key.builtin("klabel", KeyParameter.Required, onlyon[Production])
-  final val KORE      = Key.builtin("kore", KeyParameter.Forbidden, onlyon2[RuleOrClaim, Module])
   final val LABEL     = Key.builtin("label", KeyParameter.Required, onlyon[Sentence])
   final val LATEX     = Key.builtin("latex", KeyParameter.Required, onlyon[Production])
   final val LEFT      = Key.builtin("left", KeyParameter.Forbidden, onlyon[Production])

diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
@@ -5,7 +5,7 @@
 import java.io.File;
 import java.io.IOException;
 import java.util.ArrayList;
-import java.util.Arrays;
+import java.util.Collections;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
@@ -187,6 +187,6 @@ private String getThreshold() {
 
   @Override
   public Set<Att.Key> excludedModuleTags() {
-    return new HashSet<>(Arrays.asList(Att.SYMBOLIC(), Att.KAST()));
+    return new HashSet<>(Collections.singletonList(Att.SYMBOLIC()));
   }
 }