Remove usages of K source and location classes (#1002)

Part of: #999 We are currently working on removing the reverse dependency that the LLVM backend has on the K frontend's data structures; this PR takes a step towards that goal by removing the backend's use of the K Source and Location classes. These classes are only ever used in the matching compiler as simple PODs that carry around data, so they can be replaced trivially with Java classes here. This PR needs a matching change to the K frontend to work, along with appropriate lockstep merging. Also contains a minor fix in 4b644b0 for an edge case in the exhaustiveness checker for rules with no location; we want to propagate an empty optional here rather than `null`.
runtimeverification · Mar 1, 2024 · 87edd79 · 87edd79
1 parent 30f813a
commit 87edd79
Show file tree

Hide file tree

Showing 6 changed files with 50 additions and 17 deletions.
diff --git a/matching/src/main/java/org/kframework/backend/llvm/matching/Location.java b/matching/src/main/java/org/kframework/backend/llvm/matching/Location.java
@@ -0,0 +1,31 @@
+package org.kframework.backend.llvm.matching;
+
+public class Location {
+    int startLine;
+    int endLine;
+    int startColumn;
+    int endColumn;
+
+    public Location(int startLine, int endLine, int startColumn, int endColumn) {
+        this.startLine = startLine;
+        this.endLine = endLine;
+        this.startColumn = startColumn;
+        this.endColumn = endColumn;
+    }
+
+    public int getStartLine() {
+        return startLine;
+    }
+
+    public int getEndLine() {
+        return endLine;
+    }
+
+    public int getStartColumn() {
+        return startColumn;
+    }
+
+    public int getEndColumn() {
+        return endColumn;
+    }
+}
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,8 +1,5 @@
 package org.kframework.backend.llvm.matching;
 
-import org.kframework.attributes.Location;
-import org.kframework.attributes.Source;
-
 import java.util.Optional;
 
 public final class MatchingException extends Throwable {

diff --git a/matching/src/main/java/org/kframework/backend/llvm/matching/Source.java b/matching/src/main/java/org/kframework/backend/llvm/matching/Source.java
@@ -0,0 +1,13 @@
+package org.kframework.backend.llvm.matching;
+
+public class Source {
+    String source;
+
+    public Source(String source) {
+        this.source = source;
+    }
+
+    public String getSource() {
+        return source;
+    }
+}
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala
@@ -3,9 +3,6 @@ package org.kframework.backend.llvm.matching
 import java.util
 import java.util.concurrent.ConcurrentHashMap
 import java.util.Optional
-import org.kframework.attributes.HasLocation
-import org.kframework.attributes.Location
-import org.kframework.attributes.Source
 import org.kframework.backend.llvm.matching.dt._
 import org.kframework.backend.llvm.matching.pattern._
 import org.kframework.kore.KORE.KApply
@@ -328,7 +325,7 @@ case class Action(
     source: Optional[Source],
     location: Optional[Location],
     nonlinear: Boolean
-) extends HasLocation {
+) {
   override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
 }
 
@@ -1087,8 +1084,8 @@ class Matrix private (
       val k          = fringe.zip(counterexample.get).map(t => t._2.toK(t._1))
       val func       = KApply(symlib.koreToK(name), KList(k))
       val attributes = symlib.signatures(name)._3
-      val location   = Parser.location(attributes).orElse(null)
-      val source     = Parser.source(attributes).orElse(null)
+      val location   = Parser.location(attributes)
+      val source     = Parser.source(attributes)
 
       kem(
         new MatchingException(

diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala
@@ -2,8 +2,6 @@ package org.kframework.backend.llvm.matching
 
 import java.util
 import java.util.Optional
-import org.kframework.attributes.Location
-import org.kframework.attributes.Source
 import org.kframework.parser.kore._
 import org.kframework.parser.kore.implementation.{ DefaultBuilders => B }
 import org.kframework.parser.kore.parser.KoreToK
@@ -161,7 +159,7 @@ object Parser {
   def source(att: Attributes): Optional[Source] =
     if (hasAtt(att, SOURCE)) {
       val sourceStr = getStringAtt(att, SOURCE).get
-      return Optional.of(Source(sourceStr.substring("Source(".length, sourceStr.length - 1)))
+      Optional.of(new Source(sourceStr.substring("Source(".length, sourceStr.length - 1)))
     } else {
       Optional.empty()
     }
@@ -170,8 +168,8 @@ object Parser {
     if (hasAtt(att, LOCATION)) {
       val locStr   = getStringAtt(att, LOCATION).get
       val splitted = locStr.split("[(,)]")
-      return Optional.of(
-        Location(splitted(1).toInt, splitted(2).toInt, splitted(3).toInt, splitted(4).toInt)
+      Optional.of(
+        new Location(splitted(1).toInt, splitted(2).toInt, splitted(3).toInt, splitted(4).toInt)
       )
     } else {
       Optional.empty()

diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala
@@ -1,9 +1,6 @@
 package org.kframework.backend.llvm.matching.pattern
 
 import java.util.regex.{ Pattern => Regex }
-import java.util.Optional
-import org.kframework.attributes.Location
-import org.kframework.attributes.Source
 import org.kframework.backend.llvm.matching._
 import org.kframework.backend.llvm.matching.dt._
 import org.kframework.backend.llvm.matching.MatchingException