From 8fa81a30b36edd1d82c68c6f39e9f5e659154b85 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Fri, 1 Mar 2024 13:12:26 +0000 Subject: [PATCH 1/2] Remove usages of K Source and Location --- .../backend/llvm/matching/Location.java | 31 +++++++++++++++++++ .../llvm/matching/MatchingException.java | 3 -- .../backend/llvm/matching/Source.java | 13 ++++++++ .../backend/llvm/matching/Matrix.scala | 5 +-- .../backend/llvm/matching/Parser.scala | 8 ++--- .../llvm/matching/pattern/SortCategory.scala | 3 -- 6 files changed, 48 insertions(+), 15 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..d820adeb6 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) } 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 From 485a6821fa0188c36f5d21d7e694264b1b5f47b9 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Fri, 1 Mar 2024 14:35:12 +0000 Subject: [PATCH 2/2] Fix nulls on exhaustiveness check --- .../scala/org/kframework/backend/llvm/matching/Matrix.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 d820adeb6..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 @@ -1084,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(