From 87edd7989d8521a9218bc73328cca1b321c87ec3 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Fri, 1 Mar 2024 16:27:07 +0000 Subject: [PATCH] Remove usages of K source and location classes (#1002) Part of: https://github.com/runtimeverification/llvm-backend/issues/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 https://github.com/runtimeverification/llvm-backend/pull/1002/commits/4b644b04278cf030580276288785307167276903 for an edge case in the exhaustiveness checker for rules with no location; we want to propagate an empty optional here rather than `null`. --- .../backend/llvm/matching/Location.java | 31 +++++++++++++++++++ .../llvm/matching/MatchingException.java | 3 -- .../backend/llvm/matching/Source.java | 13 ++++++++ .../backend/llvm/matching/Matrix.scala | 9 ++---- .../backend/llvm/matching/Parser.scala | 8 ++--- .../llvm/matching/pattern/SortCategory.scala | 3 -- 6 files changed, 50 insertions(+), 17 deletions(-) create mode 100644 matching/src/main/java/org/kframework/backend/llvm/matching/Location.java create mode 100644 matching/src/main/java/org/kframework/backend/llvm/matching/Source.java 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 new file mode 100644 index 000000000..36ace2cc1 --- /dev/null +++ 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; + } +} \ No newline at end of file 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 index d2b2d8c98..eb545d38a 100644 --- 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 new file mode 100644 index 000000000..9c69908d8 --- /dev/null +++ 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 index 46ece4a01..7a2d15452 100644 --- 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 index 5a4271b1a..6501aed88 100644 --- 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 index 200d89793..0a37662b3 100644 --- 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