Remove usages of K error handling infrastructure (#1001)

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 first step towards that goal by removing the backend's use of the K exception infrastructure for throwing errors. The K infrastructure is replaced with a simple exception class that the frontend will be able to catch and reinterpret as appropriate. This PR needs a matching change to the K frontend to work, along with appropriate lockstep merging. --------- Co-authored-by: Tamás Tóth <[email protected]>
runtimeverification · Mar 1, 2024 · 30f813a · 30f813a
1 parent 7b744a2
commit 30f813a
Show file tree

Hide file tree

Showing 5 changed files with 73 additions and 23 deletions.
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
@@ -0,0 +1,52 @@
+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 {
+    public enum Type {
+        USELESS_RULE,
+        NON_EXHAUSTIVE_MATCH,
+        INTERNAL_ERROR,
+        COMPILER_ERROR,
+    }
+
+    Type type;
+    String message;
+    Optional<Source> source;
+    Optional<Location> location;
+
+    public MatchingException(Type type, String message, Optional<Source> source, Optional<Location> location) {
+        this.type = type;
+        this.message = message;
+        this.source = source;
+        this.location = location;
+    }
+
+    public MatchingException(Type type, String message, Source source, Location location) {
+        this(type, message, Optional.of(source), Optional.of(location));
+    }
+
+    public MatchingException(Type type, String message) {
+        this(type, message, Optional.empty(), Optional.empty());
+    }
+
+    public Type getType() {
+        return type;
+    }
+
+    @Override
+    public String getMessage() {
+        return message;
+    }
+
+    public Optional<Source> getSource() {
+        return source;
+    }
+
+    public Optional<Location> getLocation() {
+        return location;
+    }
+}
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
@@ -13,7 +13,6 @@ 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._
-import org.kframework.utils.errorsystem.KException
 
 object Generator {
 
@@ -210,7 +209,7 @@ object Generator {
       axioms: IndexedSeq[AxiomInfo],
       sorts: Seq[Sort],
       name: SymbolOrAlias,
-      kem: KException => scala.Unit
+      kem: MatchingException => scala.Unit
   ): DecisionTree = {
     val matrix = genClauseMatrix(symlib, mod, axioms, sorts)
     matrix.checkUsefulness(kem)

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
@@ -6,7 +6,6 @@ import java.util.Optional
 import org.kframework.backend.llvm.matching.dt._
 import org.kframework.parser.kore._
 import org.kframework.parser.kore.parser.TextToKore
-import org.kframework.utils.errorsystem.KException
 
 object Matching {
   def writeDecisionTreeToFile(
@@ -17,7 +16,7 @@ object Matching {
       genSingleRuleTrees: Boolean,
       warn: Boolean,
       genSearch: Boolean,
-      kem: KException => Unit
+      kem: MatchingException => Unit
   ) {
     val defn = new TextToKore().parse(filename)
     outputFolder.mkdirs()

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
@@ -16,8 +16,6 @@ import org.kframework.parser.kore.Sort
 import org.kframework.parser.kore.SymbolOrAlias
 import org.kframework.parser.kore.Variable
 import org.kframework.unparser.ToKast
-import org.kframework.utils.errorsystem.KEMException
-import org.kframework.utils.errorsystem.KException
 
 trait AbstractColumn {
   def column: Column
@@ -744,11 +742,12 @@ class Matrix private (
         try
           row.clause.action.rhsVars.map(v => v -> (grouped(v).head._2, grouped(v).head._1.hookAtt))
         catch {
-          case e: NoSuchElementException =>
-            throw KEMException.internalError(
+          case _: NoSuchElementException =>
+            throw new MatchingException(
+              MatchingException.Type.INTERNAL_ERROR,
               "Could not find binding for variable while compiling pattern matching.",
-              e,
-              row.clause.action
+              row.clause.action.source,
+              row.clause.action.location
             )
         }
       (lhs ++ rhs).sortBy(v => v._1).map(v => v._2)
@@ -1052,23 +1051,22 @@ class Matrix private (
       }
     }
 
-  def checkUsefulness(kem: KException => Unit): Unit =
+  def checkUsefulness(kem: MatchingException => Unit): Unit =
     for (rowIx <- rows.indices)
       if (rowUseless(rowIx)) {
         if (clauses(rowIx).action.source.isPresent && clauses(rowIx).action.location.isPresent) {
           kem(
-            new KException(
-              KException.ExceptionType.USELESS_RULE,
-              KException.KExceptionGroup.COMPILER,
+            new MatchingException(
+              MatchingException.Type.USELESS_RULE,
               "Potentially useless rule detected.",
-              clauses(rowIx).action.source.get,
-              clauses(rowIx).action.location.get
+              clauses(rowIx).action.source,
+              clauses(rowIx).action.location
             )
           )
         }
       }
 
-  def checkExhaustiveness(name: SymbolOrAlias, kem: KException => Unit): Unit = {
+  def checkExhaustiveness(name: SymbolOrAlias, kem: MatchingException => Unit): Unit = {
     Matrix.id = 0
     val id = Matrix.id
     if (Matching.logging) {
@@ -1093,9 +1091,8 @@ class Matrix private (
       val source     = Parser.source(attributes).orElse(null)
 
       kem(
-        new KException(
-          KException.ExceptionType.NON_EXHAUSTIVE_MATCH,
-          KException.KExceptionGroup.COMPILER,
+        new MatchingException(
+          MatchingException.Type.NON_EXHAUSTIVE_MATCH,
           "Non exhaustive match detected: " ++ ToKast(func),
           source,
           location

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,13 +1,15 @@
 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
 import org.kframework.mpfr._
 import org.kframework.parser.kore.CompoundSort
 import org.kframework.parser.kore.Sort
-import org.kframework.parser.kore.SymbolOrAlias
-import org.kframework.utils.errorsystem.KEMException
 
 sealed trait SortCategory {
   def hookAtt: String
@@ -46,7 +48,8 @@ object SortCategory {
       case Some("BUFFER.StringBuffer") => BufferS()
       case Some("MINT.MInt") => MIntS(getBitwidth(s.asInstanceOf[CompoundSort].params(0), symlib))
       case Some("BAG.Bag") =>
-        throw KEMException.compilerError(
+        throw new MatchingException(
+          MatchingException.Type.COMPILER_ERROR,
           "LLVM Backend does not support multisets. If you are seeing this error due to a configuration cell tagged with multiplicity=\"*\", please add either type=\"Map\" or type=\"Set\". If you still need the collection to not contain duplicates, it is recommended you also add a unique identifier each time a cell is created. You can do this with !X:Int."
         );
     }