Make cross-platform path/URI/charset handling in load/save more robust#3860
Merged
Conversation
URLDecoder decodes the application/x-www-form-urlencoded form, in which a literal '+' denotes a space. A URL path never encodes a space as '+' (it uses %20), so a '+' in url.getPath() is part of the file name. The previous decode turned it into a space, silently mangling any file or directory whose name contains '+' (e.g. "C++Model/", "a+b.key"). Since toURI is the central URL->File converter (toFile/toFileString route through it), this affected all platforms. Protect literal '+' as %2B before decoding the remaining percent-escapes.
readBootClassPath, readClassPath and readJavaPath parsed the stored \bootclasspath / \classpath / \javaSource strings directly with Paths.get. KeY now always writes forward slashes, but proofs saved by older versions on Windows contain backslashes. On POSIX a backslash is a valid file-name character, so such a path is not split into segments and fails to resolve, making legacy Windows proofs unloadable on Linux/macOS. IncludeFinder.addInclude already normalizes separators for \include; this applies the same treatment to the three remaining path kinds via a shared normalizeStoredPath helper. Converting '\' to '/' is safe on all platforms (Windows accepts '/' as a separator).
The constructor counted bytes with new File(url.getFile()).length(). url.getFile() is not percent-decoded and retains the leading '/' of "file:/C:/..." on Windows, so for file URLs containing spaces (%20) or on Windows it pointed at a non-existent file and returned a length of 0. Use Files.size(Paths.get(url.toURI())), matching the existing file() method, and fall back to stream counting on failure. The byte count only drives a progress indicator, but the previous behaviour was platform dependent.
Two problems on Windows: Path.relativize throws IllegalArgumentException when the two paths have different roots (e.g. proof and source on different drives), and the result was returned with native separators (backslashes), which are not portable when written into a proof file. Guard the differing-root case by falling back to the absolute path and normalize all output to forward slashes, mirroring the behaviour of IOUtil.safePathRelativeTo.
The settings file is read as UTF-8 (ParsingFacade.readConfigurationFile -> CharStreams.fromPath defaults to UTF-8) but was written with a plain FileWriter, i.e. the platform-default charset. On a JDK whose default charset is not UTF-8 (e.g. windows-1252 on Windows with older JDKs), non-ASCII content such as umlauts in bookmarked paths or user names is written in one encoding and parsed back in another, corrupting the settings. Make the writer explicitly UTF-8 to match the reader.
unp1
enabled auto-merge
June 24, 2026 06:56
unp1
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Intended Change
While auditing KeY for cross-platform (Linux/macOS/Windows) robustness of
loading and saving, several latent path/URI/charset issues surfaced. This PR
fixes them. Each issue is a separate commit.
IOUtil.toURIcorrupted+in file paths (all platforms).The central
URL → Fileconverter decoded the URL path withURLDecoder, whoseapplication/x-www-form-urlencodedsemantics turn aliteral
+into a space. URL paths never encode a space as+(they use%20), so any file or directory whose name contains+(e.g.C++Model/,a+b.key) was silently mangled. The+is now protected before decoding.Loader did not normalize backslashes — legacy Windows proofs failed on POSIX.
KeYFile.readBootClassPath/readClassPath/readJavaPathparsed the storedpath strings directly with
Paths.get. Newer proofs are written with forwardslashes, but proofs saved by older KeY versions on Windows contain
backslashes; on POSIX a backslash is a valid file-name character, so the path
was not split into segments and could not be resolved. The three readers now
normalize separators, matching what
IncludeFinder.addIncludealready doesfor
\include.UrlRuleSourcereported the wrong file size on Windows / for spaced paths.The constructor used
new File(url.getFile()).length();url.getFile()isnot percent-decoded and keeps the leading
/offile:/C:/…on Windows, sofor paths with spaces (
%20) or on Windows it pointed at a non-existent fileand returned
0. It now resolves viaPaths.get(url.toURI()), matching theclass's own
file()method, with a stream-counting fallback.Filenames.makeFilenameRelativewas not cross-platform safe.Path.relativizethrowsIllegalArgumentExceptionwhen the two paths havedifferent roots (e.g. different drive letters on Windows), and the result was
returned with native separators. It now guards the differing-root case and
normalizes output to forward slashes, mirroring
IOUtil.safePathRelativeTo.Proof-independent settings JSON was written with the platform-default charset.
The settings file is read as UTF-8 (
CharStreams.fromPath) but was writtenwith a plain
FileWriter. On a JDK whose default charset is not UTF-8 (olderJDKs on Windows), non-ASCII content (umlauts in bookmarked paths, user names)
was written in one encoding and parsed back in another. The writer is now
explicitly UTF-8.
Type of pull request
Ensuring quality
Additional information and contact(s)
This PR has been done with AI tooling.
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.