Merge remote-tracking branch 'origin/main' into proofReordering

Author: FliegendeWurst

.gitlab-ci.yml

@@ -18,7 +18,6 @@ cache:
 variables:
   GRADLE_OPTS:  "-Dorg.gradle.daemon=false -Dorg.gradle.parallel=true -Dorg.gradle.workers.max=2 -Dorg.gradle.configureondemand=true"
   GIT_DEPTH: 0
-  SONAR_SCANNER_OPTS: -Xmx8G
 
 before_script:
   #  - echo `pwd` # debug

build.gradle

@@ -17,8 +17,6 @@ plugins {
     //Some Licenses requires an entry in the credits (MIT, BSD)
     id "com.github.hierynomus.license-report" version "0.16.1"
 
-    id "org.sonarqube" version "4.1.0.3113"
-
     // Gives `gradle dependencyUpdate` to show which dependency has a newer version
     // id "com.github.ben-manes.versions" version "0.39.0"
 
@@ -54,14 +52,6 @@ def build = System.env.BUILD_NUMBER == null ? "" : "-${System.env.BUILD_NUMBER}"
 group = "org.key_project"
 version = "2.11.0$build"
 
-sonarqube {
-    properties {
-        property "sonar.projectKey", "key-main"
-        property "sonar.organization", "keyproject"
-        property "sonar.host.url", "https://sonarcloud.io"
-    }
-}
-
 subprojects {
     apply plugin: "java"
     apply plugin: "java-library"

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java

@@ -3780,16 +3780,6 @@ public static boolean isBaseHeap(Operator op, HeapLDT heapLDT) {
         return op == heapLDT.getHeapForName(HeapLDT.BASE_HEAP_NAME);
     }
 
-    /**
-     * Returns the path to the source file defined by the given {@link PositionInfo}.
-     *
-     * @param posInfo The {@link PositionInfo} to extract source file from.
-     * @return The source file name or {@code null} if not available.
-     */
-    public static String getSourcePath(PositionInfo posInfo) {
-        return MiscTools.getSourcePath(posInfo);
-    }
-
     /**
      * Checks if the given {@link Term} is a select on a heap.
      *

key.core/src/main/java/de/uka/ilkd/key/java/ParseExceptionInFile.java

@@ -41,13 +41,13 @@ public Location getLocation() throws MalformedURLException {
         // This kind of exception has a filename but no line/col information
         // Retrieve the latter from the cause. location remains null if
         // no line/col is available in cause.
-        Location location = null;
         if (getCause() != null) {
-            location = ExceptionTools.getLocation(getCause());
-            if (location != null) {
-                location = new Location(getFilename(), location.getPosition());
+            var location = ExceptionTools.getLocation(getCause());
+            if (location.isEmpty()) {
+                return null;
             }
+            return Location.fromFileName(getFilename(), location.get().getPosition());
         }
-        return location;
+        return null;
     }
 }

key.core/src/main/java/de/uka/ilkd/key/java/PosConvertException.java

@@ -76,6 +76,6 @@ public Location getLocation() throws MalformedURLException {
                 this.file = dataloc.substring(dataloc.indexOf(':') + 1);
             }
         }
-        return new Location(file, position);
+        return Location.fromFileName(file, position);
     }
 }

key.core/src/main/java/de/uka/ilkd/key/java/PositionInfo.java

@@ -1,7 +1,11 @@
 package de.uka.ilkd.key.java;
 
+import java.net.MalformedURLException;
 import java.net.URI;
+import java.net.URL;
 import java.nio.file.Paths;
+import java.util.Optional;
+import javax.annotation.Nullable;
 
 import recoder.java.SourceElement;
 
@@ -13,6 +17,7 @@
 public class PositionInfo {
     /** Unknown URI (enables us to always have a non-null value for fileURI) */
     public static final URI UNKNOWN_URI = URI.create("UNKNOWN://unknown");
+    public static final URI UNKNOWN_URII = URI.create("urn:UNKNOWN:unknown");
 
     /** PositionInfo with undefined positions. */
     public static final PositionInfo UNDEFINED = new PositionInfo();
@@ -29,9 +34,9 @@ public class PositionInfo {
     private final Position endPos;
 
     /**
-     * The URI of the resource this location refers to. Either a meaningful value or
-     * {@link #UNKNOWN_URI}, but never null.
+     * The URI of the resource this location refers to. Either a meaningful value or null.
      */
+    @Nullable
     private final URI fileURI;
 
     /**
@@ -44,7 +49,7 @@ private PositionInfo() {
         this.relPos = SourceElement.Position.UNDEFINED;
         this.startPos = Position.UNDEFINED;
         this.endPos = Position.UNDEFINED;
-        fileURI = UNKNOWN_URI;
+        fileURI = null;
     }
 
     /**
@@ -58,7 +63,7 @@ public PositionInfo(SourceElement.Position relPos, Position startPos, Position e
         this.relPos = relPos;
         this.startPos = startPos;
         this.endPos = endPos;
-        fileURI = UNKNOWN_URI;
+        fileURI = null;
     }
 
     /**
@@ -75,8 +80,11 @@ public PositionInfo(SourceElement.Position relPos, Position startPos, Position e
         this.startPos = startPos;
         this.endPos = endPos;
         if (fileURI == null) {
-            this.fileURI = UNKNOWN_URI; // fileURI must not be null!
+            this.fileURI = null;
         } else {
+            if (fileURI.toString().contains("unknown")) {
+                int i = 0;
+            }
             this.fileURI = fileURI.normalize();
         }
     }
@@ -116,7 +124,7 @@ public String getParentClass() {
      */
     @Deprecated // only kept for compatibility reasons
     public String getFileName() {
-        if (fileURI.getScheme().equals("file")) {
+        if (fileURI != null && fileURI.getScheme().equals("file")) {
             return Paths.get(fileURI).toString();
         }
         return null;
@@ -126,8 +134,12 @@ public URI getParentClassURI() {
         return parentClassURI;
     }
 
-    public URI getURI() {
-        return fileURI;
+    public Optional<URI> getURI() {
+        return Optional.ofNullable(fileURI);
+    }
+
+    public Optional<URL> getURL() throws MalformedURLException {
+        return fileURI == null ? Optional.empty() : Optional.of(fileURI.toURL());
     }
 
     public SourceElement.Position getRelativePosition() {
@@ -183,7 +195,8 @@ public static PositionInfo join(PositionInfo p1, PositionInfo p2) {
             end = p2.endPos;
         }
         // TODO: join relative position as well
-        return new PositionInfo(SourceElement.Position.UNDEFINED, start, end, p1.getURI());
+        return new PositionInfo(SourceElement.Position.UNDEFINED, start, end,
+            p1.getURI().orElse(null));
     }
 
     /**
@@ -201,7 +214,7 @@ public String toString() {
         if (this == PositionInfo.UNDEFINED) {
             return "UNDEFINED";
         } else {
-            return ((fileURI == UNKNOWN_URI ? "" : fileURI) + " rel. Pos: " + relPos
+            return ((fileURI == null ? "" : fileURI) + " rel. Pos: " + relPos
                 + " start Pos: " + startPos + " end Pos: " + endPos);
         }
     }

key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java

@@ -1,6 +1,7 @@
 package de.uka.ilkd.key.java;
 
 import java.io.*;
+import java.net.MalformedURLException;
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Paths;
 import java.util.*;
@@ -21,6 +22,7 @@
 import de.uka.ilkd.key.util.*;
 import de.uka.ilkd.key.util.LinkedHashMap;
 import de.uka.ilkd.key.util.Pair;
+import de.uka.ilkd.key.util.parsing.HasLocation;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
@@ -1203,6 +1205,7 @@ private static String trim(String s, int length) {
     /**
      * tries to parse recoders exception position information
      */
+    @Nullable
     private static Pair<String, Position> extractPositionInfo(String errorMessage) {
         if (errorMessage == null || errorMessage.indexOf('@') == -1) {
             return null;
@@ -1255,17 +1258,31 @@ public static void reportError(String message, Throwable t) {
             throw (PosConvertException) cause;
         }
 
-        Pair<String, Position> pos = extractPositionInfo(cause.toString());
-        if (pos != null) {
-            reportErrorWithPositionInFile(message, cause, pos.second, pos.first);
-        } else {
-            reportErrorWithPositionInFile(message, cause, null, null);
+        Position pos = null;
+        String file = null;
+        if (cause instanceof HasLocation) {
+            try {
+                var location = ((HasLocation) cause).getLocation();
+                if (location != null) {
+                    pos = location.getPosition();
+                    file = location.getFileURI().toString();
+                }
+            } catch (MalformedURLException ignored) {
+            }
+        }
+        if (pos == null) {
+            Pair<String, Position> info = extractPositionInfo(cause.toString());
+            if (info != null) {
+                pos = info.second;
+                file = info.first;
+            }
         }
+        reportErrorWithPositionInFile(message, cause, pos, file);
     }
 
     public static void reportErrorWithPositionInFile(String message, Throwable cause,
             @Nullable Position pos,
-            String file) {
+            @Nullable String file) {
         final RuntimeException rte;
         if (pos != null) {
             rte = new PosConvertException(message, pos, file);

key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java

@@ -89,7 +89,7 @@ public IProgramMethod processDefaultConstructor(recoder.abstraction.DefaultConst
 
     public CompilationUnit processCompilationUnit(recoder.java.CompilationUnit cu,
             DataLocation context) {
-        currentClassURI = MiscTools.extractURI(context);
+        currentClassURI = MiscTools.extractURI(context).orElse(null);
         Object result = process(cu);
         currentClassURI = null;
 
@@ -1467,7 +1467,7 @@ public MethodReference convert(recoder.java.reference.MethodReference mr) {
                         ? ((recoder.java.CompilationUnit) tdc).getOriginalDataLocation()
                         : null;
 
-                currentClassURI = MiscTools.extractURI(loc);
+                currentClassURI = MiscTools.extractURI(loc).orElse(null);
                 pm = convert((recoder.java.declaration.MethodDeclaration) method);
                 // because of cycles when reading recursive programs
                 currentClassURI = oldCurrent;