Remove usages of K frontend code (#1007)

This PR finalises the removal of the LLVM backend's dependence on the K frontend, now that we have the shared data structures extracted out to the [`scala-kore` repository](https://github.com/runtimeverification/scala-kore). There are a few smaller changes that make up this PR, but the commit history is clean and can be reviewed commit-by-commit. Once this is merged, the LLVM backend will no longer depend on the K Frontend and we will have eliminated the backwards edge in the K dependency graph! Fixes: #999 --------- Co-authored-by: Samuel Balco <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Mar 6, 2024 · fb17cba · fb17cba
1 parent 9304243
commit fb17cba
Show file tree

Hide file tree

Showing 24 changed files with 192 additions and 6,847 deletions.
diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
diff --git a/default.nix b/default.nix
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -18,21 +18,20 @@
     pybind11-src.url =
       "github:pybind/pybind11/0ba639d6177659c5dc2955ac06ad7b5b0d22e05c";
     pybind11-src.flake = false;
-    mavenix.url = "github:goodlyrottenapple/mavenix";
     # needed by nix/flake-compat-k-unwrapped.nix
     flake-compat = {
       url = "github:edolstra/flake-compat";
       flake = false;
     };
   };
 
-  outputs = { self, nixpkgs, utils, fmt-src, immer-src, rapidjson-src, pybind11-src, mavenix, ... }:
+  outputs = { self, nixpkgs, utils, fmt-src, immer-src, rapidjson-src, pybind11-src, ... }:
     let
       inherit (nixpkgs) lib;
 
-      # put devShell and any other required packages into local overlay
+      # put required packages into local overlay
       # if you have additional overlays, you may add them here
-      localOverlay = import ./nix/overlay.nix; # this should expose devShell
+      localOverlay = import ./nix/overlay.nix;
       depsOverlay = (final: prev: {
         inherit fmt-src immer-src rapidjson-src pybind11-src;
 
@@ -78,6 +77,10 @@
           ] ./matching);
       });
 
+      maven-overlay = (final: prev: {
+        maven = prev.callPackage ./nix/maven.nix { };
+      });
+
       llvm-backend-overlay =
         nixpkgs.lib.composeManyExtensions [ depsOverlay localOverlay ];
 
@@ -89,7 +92,7 @@
               inherit llvm-backend-build-type;
               maven = prev.maven // { inherit (prev) jdk; };
             })
-            mavenix.overlay
+            maven-overlay
             llvm-backend-overlay
           ];
           inherit system;
@@ -113,7 +116,7 @@
             {
               name = "llvm-backend-${toString args.llvm-version}-${args.build-type}";
               value = {
-                inherit (pkgs) llvm-backend llvm-backend-matching llvm-kompile-testing integration-tests devShell;
+                inherit (pkgs) llvm-backend llvm-backend-matching llvm-kompile-testing integration-tests;
               };
             }
         ));
@@ -122,23 +125,8 @@
           inherit (llvm-backend-17-FastBuild) llvm-backend llvm-backend-matching llvm-kompile-testing;
           default = llvm-backend-17-FastBuild.llvm-backend;
           llvm-backend-release = llvm-backend-17-Release.llvm-backend;
-        } // {          
-          update-maven = let pkgs = import nixpkgs { 
-            overlays = [
-              (final: prev: {
-                maven = prev.maven // { inherit (prev) jdk; };
-              })
-              mavenix.overlay
-            ];
-            inherit system; };
-          in pkgs.writeShellScriptBin "update-maven" ''
-            #!/bin/sh
-            ${pkgs.nix}/bin/nix-build --no-out-link -E '(import ./flake-compat-k-unwrapped.nix).packages.${system}.llvm-backend-matching' \
-              || echo "^~~~ expected error"
-            export PATH="${pkgs.gnused}/bin:$PATH"
-            ${pkgs.mavenix-cli}/bin/mvnix-update -l ./nix/llvm-backend-matching.mavenix.lock -E '(import ./flake-compat-k-unwrapped.nix).packages.${system}.llvm-backend-matching'
-          '';
         };
+
         checks = listToChecks [
           llvm-backend-17-Debug.llvm-backend
           llvm-backend-17-Release.llvm-backend
@@ -149,9 +137,9 @@
           llvm-backend-16-FastBuild.integration-tests
           llvm-backend-17-FastBuild.integration-tests
         ];
-        devShells.default = llvm-backend-17-FastBuild.devShell;
       }) // {
         # non-system suffixed items should go here
         overlays.default = llvm-backend-overlay;
+        overlays.maven = maven-overlay;
       };
 }
diff --git a/matching/pom.xml b/matching/pom.xml
@@ -34,8 +34,8 @@
   <dependencies>
     <dependency>
       <groupId>com.runtimeverification.k</groupId>
-      <artifactId>kore</artifactId>
-      <version>${project.version}</version>
+      <artifactId>scala-kore</artifactId>
+      <version>0.3.0</version>
     </dependency>
     <dependency>
       <groupId>org.yaml</groupId>

diff --git a/matching/src/main/java/org/kframework/backend/llvm/matching/MatchingException.java b/matching/src/main/java/org/kframework/backend/llvm/matching/MatchingException.java
@@ -1,5 +1,7 @@
 package org.kframework.backend.llvm.matching;
 
+import com.runtimeverification.k.kore.Pattern;
+
 import java.util.Optional;
 
 public final class MatchingException extends Throwable {
@@ -14,12 +16,23 @@ public enum Type {
     String message;
     Optional<Source> source;
     Optional<Location> location;
+    Optional<Pattern> pattern;
 
-    public MatchingException(Type type, String message, Optional<Source> source, Optional<Location> location) {
+    private MatchingException(Type type, String message, Optional<Source> source, Optional<Location> location, Optional<Pattern> pattern) {
         this.type = type;
         this.message = message;
         this.source = source;
         this.location = location;
+        this.pattern = pattern;
+    }
+
+    public MatchingException(Type type, String message, Optional<Source> source, Optional<Location> location, Pattern pattern) {
+        this(type, message, source, location, Optional.of(pattern));
+    }
+
+
+    public MatchingException(Type type, String message, Optional<Source> source, Optional<Location> location) {
+        this(type, message, source, location, Optional.empty());
     }
 
     public MatchingException(Type type, String message, Source source, Location location) {
@@ -46,4 +59,8 @@ public Optional<Source> getSource() {
     public Optional<Location> getLocation() {
         return location;
     }
+
+    public Optional<Pattern> getPattern() {
+        return pattern;
+    }
 }
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala
@@ -1,7 +1,7 @@
 package org.kframework.backend.llvm.matching
 
+import com.runtimeverification.k.kore.SymbolOrAlias
 import org.kframework.backend.llvm.matching.pattern._
-import org.kframework.parser.kore.SymbolOrAlias
 
 sealed trait Constructor {
   def name: String

diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Generator.scala
@@ -1,5 +1,6 @@
 package org.kframework.backend.llvm.matching
 
+import com.runtimeverification.k.kore._
 import org.kframework.backend.llvm.matching.dt.DecisionTree
 import org.kframework.backend.llvm.matching.pattern.{ Pattern => P }
 import org.kframework.backend.llvm.matching.pattern.AsP
@@ -12,7 +13,6 @@ import org.kframework.backend.llvm.matching.pattern.SortCategory
 import org.kframework.backend.llvm.matching.pattern.SymbolP
 import org.kframework.backend.llvm.matching.pattern.VariableP
 import org.kframework.backend.llvm.matching.pattern.WildcardP
-import org.kframework.parser.kore._
 
 object Generator {
 

diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Heuristics.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Heuristics.scala
@@ -1,7 +1,7 @@
 package org.kframework.backend.llvm.matching
 
+import com.runtimeverification.k.kore.SymbolOrAlias
 import org.kframework.backend.llvm.matching.pattern._
-import org.kframework.parser.kore.SymbolOrAlias
 
 sealed trait Heuristic {
   val needsMatrix: Boolean

diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matching.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matching.scala
@@ -1,11 +1,11 @@
 package org.kframework.backend.llvm.matching
 
+import com.runtimeverification.k.kore._
+import com.runtimeverification.k.kore.parser.TextToKore
 import java.io.File
 import java.io.FileWriter
 import java.util.Optional
 import org.kframework.backend.llvm.matching.dt._
-import org.kframework.parser.kore._
-import org.kframework.parser.kore.parser.TextToKore
 
 object Matching {
   def writeDecisionTreeToFile(