From ca40e6cb6308ca057b371f1760f0e49ae65abb05 Mon Sep 17 00:00:00 2001 From: Alen Jo <45494246+joalen@users.noreply.github.com> Date: Sun, 15 Dec 2024 11:34:15 -0600 Subject: [PATCH] Added model classes for java.nio.file and java.nio.charset packages #429 (#506) * Found Potential Fix for #429 Seems like there needs to be model classes in the file and charset packages for java.nio. These are as small as I could make them * Create NullCharsetTest.java Developed UnitTest to address the error from #429 * Update NullCharsetTest.java Should be "iae" and not "e" * Fixed Failing Tests for NullCharSet It turns out my implementation of Charset affected the behavior of underlying Gradle JPF tests. Removed this custom Charset implementation and instead kept four files to fix the root cause: - FileSystem.java - FileSystems.java - Pathy.java - spi/FileSystemProvider.java All other files in the initial commit to PR were redundant. --- .../java.base/java/nio/files/FileSystem.java | 11 ++ .../java.base/java/nio/files/FileSystems.java | 186 ++++++++++++++++++ .../java.base/java/nio/files/Path.java | 25 +++ .../nio/files/spi/FileSystemProvider.java | 19 ++ src/tests/NullCharsetTest.java | 23 +++ 5 files changed, 264 insertions(+) create mode 100644 src/classes/modules/java.base/java/nio/files/FileSystem.java create mode 100644 src/classes/modules/java.base/java/nio/files/FileSystems.java create mode 100644 src/classes/modules/java.base/java/nio/files/Path.java create mode 100644 src/classes/modules/java.base/java/nio/files/spi/FileSystemProvider.java create mode 100644 src/tests/NullCharsetTest.java diff --git a/src/classes/modules/java.base/java/nio/files/FileSystem.java b/src/classes/modules/java.base/java/nio/files/FileSystem.java new file mode 100644 index 00000000..243f33ba --- /dev/null +++ b/src/classes/modules/java.base/java/nio/files/FileSystem.java @@ -0,0 +1,11 @@ +package java.nio.file; + +import java.nio.file.spi.FileSystemProvider; + +public abstract class FileSystem { + protected FileSystem() {} + + public abstract Path getPath(String first, String... more); + + public abstract FileSystemProvider provider(); +} \ No newline at end of file diff --git a/src/classes/modules/java.base/java/nio/files/FileSystems.java b/src/classes/modules/java.base/java/nio/files/FileSystems.java new file mode 100644 index 00000000..da321b15 --- /dev/null +++ b/src/classes/modules/java.base/java/nio/files/FileSystems.java @@ -0,0 +1,186 @@ +package java.nio.file; + +import java.nio.file.spi.FileSystemProvider; +import java.net.URI; +import java.util.Map; +import java.util.HashMap; + +public class FileSystems { + private static volatile FileSystem defaultFileSystem; + + static { + defaultFileSystem = new FileSystem() { + private final FileSystemProvider provider = new FileSystemProvider() { + @Override + public FileSystem newFileSystem(URI uri, Map env) { + return this.getFileSystem(); + } + + @Override + public String getScheme() { + return "file"; + } + + @Override + public FileSystem getFileSystem() { + return defaultFileSystem; + } + }; + + @Override + public Path getPath(String first, String... more) { + return new Path() { + private final String path; + private final String[] segments; + + { + StringBuilder sb = new StringBuilder(first); + if (more != null) { + for (String s : more) { + if (s != null && !s.isEmpty()) { + if (sb.length() > 0 && sb.charAt(sb.length() - 1) != '/') { + sb.append('/'); + } + sb.append(s); + } + } + } + path = sb.toString(); + segments = path.split("/"); + } + + @Override + public FileSystem getFileSystem() { + return defaultFileSystem; + } + + @Override + public boolean isAbsolute() { + return path.startsWith("/"); + } + + @Override + public Path getRoot() { + return isAbsolute() ? getFileSystem().getPath("/") : null; + } + + @Override + public Path getFileName() { + if (path.isEmpty()) return null; + return getFileSystem().getPath(segments[segments.length - 1]); + } + + @Override + public Path getParent() { + int lastSep = path.lastIndexOf('/'); + return lastSep > 0 ? getFileSystem().getPath(path.substring(0, lastSep)) : null; + } + + @Override + public int getNameCount() { + if (path.isEmpty()) return 0; + if (path.equals("/")) return 0; + int count = segments.length; + if (path.startsWith("/")) count--; + if (path.endsWith("/")) count--; + return count; + } + + @Override + public Path getName(int index) { + if (index < 0 || index >= getNameCount()) { + throw new IllegalArgumentException(); + } + return getFileSystem().getPath(segments[path.startsWith("/") ? index + 1 : index]); + } + + @Override + public Path subpath(int beginIndex, int endIndex) { + if (beginIndex < 0 || beginIndex >= getNameCount() || + endIndex > getNameCount() || beginIndex >= endIndex) { + throw new IllegalArgumentException(); + } + + StringBuilder result = new StringBuilder(); + int start = path.startsWith("/") ? beginIndex + 1 : beginIndex; + for (int i = start; i < start + (endIndex - beginIndex); i++) { + if (result.length() > 0) result.append('/'); + result.append(segments[i]); + } + return getFileSystem().getPath(result.toString()); + } + + @Override + public boolean startsWith(Path other) { + return path.startsWith(other.toString()); + } + + @Override + public boolean endsWith(Path other) { + return path.endsWith(other.toString()); + } + + @Override + public Path normalize() { + return this; // Simplified implementation + } + + @Override + public Path resolve(Path other) { + return getFileSystem().getPath(path + "/" + other.toString()); + } + + @Override + public Path relativize(Path other) { + return other; // Simplified implementation + } + + @Override + public URI toUri() { + try { + return new URI("file", null, path, null); + } catch (Exception e) { + return null; + } + } + + @Override + public Path toAbsolutePath() { + if (isAbsolute()) return this; + return getFileSystem().getPath("/" + path); + } + + @Override + public Path toRealPath(LinkOption... options) { + return toAbsolutePath(); + } + + @Override + public String toString() { + return path; + } + + @Override + public int compareTo(Path other) { + return path.compareTo(other.toString()); + } + }; + } + + @Override + public FileSystemProvider provider() { + return provider; + } + }; + } + + public static FileSystem getDefault() { + return defaultFileSystem; + } + + public static FileSystem newFileSystem(URI uri, Map env, ClassLoader loader) { + if (uri == null) + throw new NullPointerException(); + return defaultFileSystem; + } +} \ No newline at end of file diff --git a/src/classes/modules/java.base/java/nio/files/Path.java b/src/classes/modules/java.base/java/nio/files/Path.java new file mode 100644 index 00000000..11200435 --- /dev/null +++ b/src/classes/modules/java.base/java/nio/files/Path.java @@ -0,0 +1,25 @@ +package java.nio.file; +import java.net.URI; + +public interface Path extends Comparable { + FileSystem getFileSystem(); + boolean isAbsolute(); + Path getRoot(); + Path getFileName(); + Path getParent(); + int getNameCount(); + Path getName(int index); + Path subpath(int beginIndex, int endIndex); + boolean startsWith(Path other); + boolean endsWith(Path other); + Path normalize(); + Path resolve(Path other); + Path relativize(Path other); + URI toUri(); + Path toAbsolutePath(); + Path toRealPath(LinkOption... options); + + static Path of(String first, String... more) { + return FileSystems.getDefault().getPath(first, more); + } +} \ No newline at end of file diff --git a/src/classes/modules/java.base/java/nio/files/spi/FileSystemProvider.java b/src/classes/modules/java.base/java/nio/files/spi/FileSystemProvider.java new file mode 100644 index 00000000..6e1cacba --- /dev/null +++ b/src/classes/modules/java.base/java/nio/files/spi/FileSystemProvider.java @@ -0,0 +1,19 @@ +package java.nio.file.spi; + +import java.io.IOException; +import java.nio.file.FileSystem; +import java.nio.file.AccessMode; +import java.nio.file.Path; +import java.net.URI; +import java.util.Map; + + +public abstract class FileSystemProvider { + protected FileSystemProvider() {} + + public abstract FileSystem newFileSystem(URI uri, Map env); + + public abstract String getScheme(); + + public abstract FileSystem getFileSystem(); +} \ No newline at end of file diff --git a/src/tests/NullCharsetTest.java b/src/tests/NullCharsetTest.java new file mode 100644 index 00000000..4a1d37fd --- /dev/null +++ b/src/tests/NullCharsetTest.java @@ -0,0 +1,23 @@ +import gov.nasa.jpf.util.test.TestJPF; +import org.junit.Test; +import java.nio.file.Path; + +public class NullCharsetTest extends TestJPF +{ + @Test + public void testDirectPathEntry() + { + if (verifyNoPropertyViolation()) + { + try { + Path.of("/tmp"); + } catch (IllegalArgumentException iae) + { + if ("Null charset name".equals(iae.getMessage())) + { + fail("IllegalArgumentException with 'Null charset name' encountered"); + } + } + } + } +} \ No newline at end of file