Merge remote-tracking branch 'origin/develop'

runtimeverification · Mar 1, 2024 · b2634bc · b2634bc
2 parents a55720c + 3d2d897
commit b2634bc
Show file tree

Hide file tree

Showing 4 changed files with 77 additions and 6 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/kore/src/main/java/org/kframework/utils/errorsystem/KEMException.java b/kore/src/main/java/org/kframework/utils/errorsystem/KEMException.java
@@ -2,6 +2,7 @@
 package org.kframework.utils.errorsystem;
 
 import java.util.Objects;
+import java.util.Optional;
 import org.kframework.attributes.HasLocation;
 import org.kframework.attributes.Location;
 import org.kframework.attributes.Source;
@@ -96,6 +97,17 @@ public static KEMException internalError(String message, Throwable e, HasLocatio
         node.source().orElse(null));
   }
 
+  public static KEMException internalError(
+      String message, Throwable e, Optional<Location> location, Optional<Source> source) {
+    return create(
+        ExceptionType.ERROR,
+        KExceptionGroup.INTERNAL,
+        message,
+        e,
+        location.orElse(null),
+        source.orElse(null));
+  }
+
   public static KEMException compilerError(String message) {
     return create(ExceptionType.ERROR, KExceptionGroup.COMPILER, message, null, null, null);
   }
@@ -124,6 +136,17 @@ public static KEMException compilerError(String message, Throwable e, HasLocatio
         node.source().orElse(null));
   }
 
+  public static KEMException compilerError(
+      String message, Throwable e, Optional<Location> location, Optional<Source> source) {
+    return create(
+        ExceptionType.ERROR,
+        KExceptionGroup.COMPILER,
+        message,
+        e,
+        location.orElse(null),
+        source.orElse(null));
+  }
+
   public static KEMException innerParserError(String message) {
     return create(ExceptionType.ERROR, KExceptionGroup.INNER_PARSER, message, null, null, null);
   }

diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
@@ -8,18 +8,23 @@
 import java.util.Collections;
 import java.util.HashSet;
 import java.util.List;
+import java.util.Optional;
 import java.util.Set;
 import org.apache.commons.io.FileUtils;
 import org.apache.commons.lang3.mutable.MutableInt;
 import org.kframework.attributes.Att;
+import org.kframework.attributes.Location;
+import org.kframework.attributes.Source;
 import org.kframework.backend.kore.KoreBackend;
 import org.kframework.backend.llvm.matching.Matching;
+import org.kframework.backend.llvm.matching.MatchingException;
 import org.kframework.compile.Backend;
 import org.kframework.kompile.KompileOptions;
 import org.kframework.main.GlobalOptions;
 import org.kframework.main.Tool;
 import org.kframework.utils.Stopwatch;
 import org.kframework.utils.errorsystem.KEMException;
+import org.kframework.utils.errorsystem.KException;
 import org.kframework.utils.errorsystem.KException.ExceptionType;
 import org.kframework.utils.errorsystem.KExceptionManager;
 import org.kframework.utils.file.FileUtil;
@@ -66,8 +71,9 @@ public void accept(Backend.Holder h) {
         globalOptions.includesExceptionType(ExceptionType.USELESS_RULE),
         options.enableSearch,
         ex -> {
-          kem.addKException(ex);
-          if (globalOptions.includesExceptionType(ex.getType())) {
+          var translated = translateError(ex);
+          kem.addKException(translated);
+          if (globalOptions.includesExceptionType(translated.getType())) {
             warnings.increment();
           }
           return null;
@@ -176,6 +182,48 @@ private void llvmKompile(String type, String executable) {
     sw.printIntermediate("  \u2514" + executable + ": " + type);
   }
 
+  private Optional<Source> getSource(MatchingException ex) {
+    return ex.getSource().map(s -> new Source(s.getSource()));
+  }
+
+  private Optional<Location> getLocation(MatchingException ex) {
+    return ex.getLocation()
+        .map(
+            l ->
+                new Location(
+                    l.getStartLine(), l.getEndLine(), l.getStartColumn(), l.getEndColumn()));
+  }
+
+  private KException translateError(MatchingException ex) {
+    switch (ex.getType()) {
+      case USELESS_RULE -> {
+        return new KException(
+            ExceptionType.USELESS_RULE,
+            KException.KExceptionGroup.COMPILER,
+            ex.getMessage(),
+            getSource(ex).orElse(null),
+            getLocation(ex).orElse(null));
+      }
+
+      case NON_EXHAUSTIVE_MATCH -> {
+        return new KException(
+            ExceptionType.NON_EXHAUSTIVE_MATCH,
+            KException.KExceptionGroup.COMPILER,
+            ex.getMessage(),
+            getSource(ex).orElse(null),
+            getLocation(ex).orElse(null));
+      }
+
+      case INTERNAL_ERROR -> throw KEMException.internalError(
+          ex.getMessage(), ex, getLocation(ex), getSource(ex));
+
+      case COMPILER_ERROR -> throw KEMException.compilerError(
+          ex.getMessage(), ex, getLocation(ex), getSource(ex));
+    }
+
+    throw KEMException.criticalError("Unhandled pattern matching exception", ex);
+  }
+
   private String getThreshold() {
     if (!options.iterated && !kompileOptions.optimize3) {
       return "0";

diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend