fixing relative java path

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java

@@ -37,7 +37,7 @@ public GZipProofSaver(Proof proof, String fileName, String internalVersion) {
     @Override
     protected void save(Path file) throws IOException {
         try (var out = new GZIPOutputStream(Files.newOutputStream(file))) {
-            save(out);
+            save(file.getParent(), out);
         }
     }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java

@@ -22,6 +22,7 @@
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.IPersistablePO;
+import de.uka.ilkd.key.proof.init.KeYUserProblemFile;
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.init.ProofOblInput;
 import de.uka.ilkd.key.proof.io.IProofFileParser.ProofElementID;
@@ -62,6 +63,8 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import static org.key_project.util.java.IOUtil.safePathRelativeTo;
+
 /**
  * Saves a proof to a given {@link OutputStream}.
  *
@@ -84,19 +87,6 @@ public class OutputStreamProofSaver {
     protected final boolean saveProofSteps;
 
 
-    /**
-     * Extracts java source directory from {@link Proof#header()}, if it exists.
-     *
-     * @param proof the Proof
-     * @return the location of the java source code or null if no such exists
-     */
-    public static @Nullable File getJavaSourceLocation(Proof proof) {
-        KeyAst.@Nullable Declarations header = proof.header();
-        if (header == null)
-            return null;
-        return header.getJavaSourceLocation();
-    }
-
     public OutputStreamProofSaver(Proof proof) {
         this(proof, KeYConstants.INTERNAL_VERSION);
     }
@@ -153,7 +143,7 @@ public String writeSettings(ProofSettings ps) {
         return String.format("\\settings %s \n", ps.settingsToString());
     }
 
-    public void save(OutputStream out) throws IOException {
+    public void save(Path basePath, OutputStream out) throws IOException {
         CopyReferenceResolver.copyCachedGoals(proof, null, null, null);
         try (var ps = new PrintWriter(out, true, StandardCharsets.UTF_8)) {
             final ProofOblInput po =
@@ -179,7 +169,7 @@ public void save(OutputStream out) throws IOException {
 
 
             var header = proof.header();
-            String headerStr = makePathsRelative(header);
+            String headerStr = makePathsRelative(basePath, header);
             ps.print(headerStr);
 
             proof.printSymbols(ps);
@@ -214,14 +204,6 @@ public void save(OutputStream out) throws IOException {
         }
     }
 
-    protected @Nullable Path getBasePath() throws IOException {
-        File javaSourceLocation = getJavaSourceLocation(proof);
-        if (javaSourceLocation != null) {
-            return javaSourceLocation.toPath().toAbsolutePath();
-        } else {
-            return null;
-        }
-    }
 
     /// Searches in the header for absolute paths to Java files and tries to replace them by paths
     /// relative to the proof file to be saved.
@@ -239,13 +221,12 @@ public void save(OutputStream out) throws IOException {
     ///
     /// @see KeYUserProblemFile#getProblemHeader()
     /// @see de.uka.ilkd.key.proof.init.InitConfig#getProblemHeader()
-    private String makePathsRelative(KeyAst.@Nullable Declarations header) throws IOException {
+    private String makePathsRelative(Path basePath, KeyAst.@Nullable Declarations header) throws IOException {
         if (header == null) {
             return "";
         }
         StringWriter sw = new StringWriter();
         PrintWriter out = new PrintWriter(sw, true);
-        Path basePath = getBasePath();
 
         header.printDefinitions(out);
 
@@ -259,20 +240,20 @@ private String makePathsRelative(KeyAst.@Nullable Declarations header) throws IO
         var classPath = jm.getClassPath();
         if (classPath != null && !classPath.isEmpty()) {
             for (Path path : classPath) {
-                out.printf("\\classpath \"%s\";\\n", IOUtil.safePathRelativeTo(path, basePath));
+                out.printf("\\classpath \"%s\";\\n", safePathRelativeTo(path, basePath));
             }
         }
 
         var javaSource = jm.getModelDir();
         if (javaSource != null) {
-            out.printf("\\javaSource \"%s\";\n", IOUtil.safePathRelativeTo(javaSource, basePath));
+            out.printf("\\javaSource \"%s\";\n", safePathRelativeTo(javaSource, basePath));
         }
 
         var includedFiles = jm.getIncludedFiles();
         if (includedFiles != null && !includedFiles.isEmpty()) {
             for (var includedFile : includedFiles) {
                 out.printf("\\include \"%s\";\n",
-                    IOUtil.safePathRelativeTo(includedFile, basePath));
+                    safePathRelativeTo(includedFile, basePath));
             }
         }
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java

@@ -54,7 +54,8 @@ protected void save(Path file) throws IOException {
         String proofFileName = MiscTools.toValidFileName(proof.name() + ".proof");
 
         // save the proof file to the FileRepo (stream is closed by the save method!)
-        save(repo.createOutputStream(Paths.get(proofFileName)));
+        final var path = Paths.get(proofFileName);
+        save(path.toAbsolutePath().getParent(), repo.createOutputStream(path));
 
         // save proof bundle with the help of the FileRepo
         ((AbstractFileRepo) repo).saveProof(file);

key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java

@@ -117,7 +117,7 @@ public ProofSaver(Proof proof, Path file, String internalVersion, boolean savePr
      */
     protected void save(Path file) throws IOException {
         try (var out = Files.newOutputStream(file)) {
-            save(out);
+            save(file.getParent(), out);
         }
     }
 
@@ -141,23 +141,6 @@ public String save() {
         return errorMsg;
     }
 
-    @Override
-    protected Path getBasePath() throws IOException {
-        return computeBasePath(file);
-    }
-
-    /**
-     * Computes the base path of the given proof {@link File}.
-     * <p>
-     * This method is used by {@link #getBasePath()} and by the Eclipse integration.
-     *
-     * @param proofFile The proof {@link File}.
-     * @return The computed base path of the given proof {@link File}.
-     */
-    public static Path computeBasePath(Path proofFile) {
-        return proofFile.toAbsolutePath().getParent().toAbsolutePath();
-    }
-
     /**
      * Adds the {@link ProofSaverListener}.
      *

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java

@@ -11,6 +11,8 @@
 import java.nio.charset.Charset;
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
 import java.util.LinkedList;
 import java.util.List;
 import java.util.zip.ZipEntry;
@@ -23,6 +25,7 @@
 import de.uka.ilkd.key.core.KeYMediator;
 import de.uka.ilkd.key.gui.IssueDialog;
 import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
@@ -32,6 +35,7 @@
 import de.uka.ilkd.key.util.KeYConstants;
 import de.uka.ilkd.key.util.KeYResourceManager;
 
+import org.jspecify.annotations.Nullable;
 import org.key_project.util.Streams;
 import org.key_project.util.java.IOUtil;
 
@@ -69,6 +73,19 @@ private static String serializeStackTrace(Throwable t) {
         return sw.toString();
     }
 
+    /**
+     * Extracts java source directory from {@link Proof#header()}, if it exists.
+     *
+     * @param proof the Proof
+     * @return the location of the java source code or null if no such exists
+     */
+    public static @Nullable File getJavaSourceLocation(Proof proof) {
+        KeyAst.@Nullable Declarations header = proof.header();
+        if (header == null)
+            return null;
+        return header.getJavaSourceLocation();
+    }
+
     private static abstract class SendFeedbackItem implements ActionListener {
 
         final String displayName;
@@ -213,7 +230,7 @@ byte[] retrieveFileData() throws IOException {
             Proof proof = mediator.getSelectedProof();
             OutputStreamProofSaver saver = new OutputStreamProofSaver(proof);
             ByteArrayOutputStream stream = new ByteArrayOutputStream();
-            saver.save(stream);
+            saver.save(Paths.get(".").toAbsolutePath(), stream);
             return stream.toByteArray();
         }
 
@@ -302,7 +319,7 @@ public JavaSourceItem() {
         boolean isEnabled() {
             try {
                 Proof proof = MainWindow.getInstance().getMediator().getSelectedProof();
-                File javaSourceLocation = OutputStreamProofSaver.getJavaSourceLocation(proof);
+                File javaSourceLocation = getJavaSourceLocation(proof);
                 return javaSourceLocation != null;
             } catch (Exception e) {
                 return false;
@@ -322,7 +339,7 @@ private void getJavaFilesRecursively(File directory, List<File> list) {
         @Override
         void appendDataToZipOutputStream(ZipOutputStream stream) throws IOException {
             Proof proof = MainWindow.getInstance().getMediator().getSelectedProof();
-            File javaSourceLocation = OutputStreamProofSaver.getJavaSourceLocation(proof);
+            File javaSourceLocation = getJavaSourceLocation(proof);
             List<File> javaFiles = new LinkedList<>();
             getJavaFilesRecursively(javaSourceLocation, javaFiles);
             for (File f : javaFiles) {

key.util/src/main/java/org/key_project/util/java/IOUtil.java

@@ -826,6 +826,10 @@ public static String safePath(Path path) {
     }
 
 
+    /// Returns a string, representing the given path to `source` relatively to `basePath`.
+    /// @param source   a path
+    /// @param basePath a directory
+    /// @return a string that is printable (escaped) for KeY files
     public static String safePathRelativeTo(Path source, Path basePath) {
         var abs = source.toAbsolutePath();
         return safePath(basePath.relativize(abs));