Implement Windows file read, write, and delete APIs. #4043

CraftSpider · 2024-11-21T06:45:40Z

This also improves how HANDLEs are, well, handled a bit. STDIN/ERR/OUT are now proper pseudo-handles. The invalid handle is added and encode/decodes to exactly 0xFFFFFFFF correctly.

Unix shims require changes to hoist FdTable up, so that Windows can share most of its implementation.

RalfJung · 2024-11-21T06:57:10Z

Thanks for the PR!

This is a huge PR. It will take a while until I have enough time to take a look at such a big change. If there is any way to stage this as a series of smaller changes, that would be much appreciated.

CraftSpider · 2024-11-21T07:04:38Z

I could possibly further split this down by first PRing the FdMap move, and the handle changes, as their own PRs. In that format, both of those would basically be refactors with no/minimal functional changes, then this PR would just add the shims. It would still be a good bit of stuff, just because even a minimal test needs 4 or 5 shims, but it would be notably smaller hopefully.

RalfJung · 2024-11-21T07:21:09Z

That sounds like a good plan. You can keep this PR open (maybe mark it as draft); it can serve as good context for why you want to refactor things the way you suggest.

RalfJung · 2024-11-21T07:24:10Z

Also, I know very little about the Windows API... @ChrisDenton @beepster4096 if you have any chance at taking a look at the windows-specific parts here and check whether they look sensible, that would be great. :)

cgettys-microsoft · 2024-11-21T21:51:54Z

@sivadeilra - here's one of the PRs related to adding Miri support for Windows FS APIs, RE: #3482

bors · 2024-11-21T22:30:02Z

☔ The latest upstream changes (presumably #4046) made this pull request unmergeable. Please resolve the merge conflicts.

ChrisDenton · 2024-11-21T22:36:56Z

src/shims/windows/handle.rs

+    Stdin,
+    Stdout,
+    Stderr,


Note that the handles returned by GetStdHandle are proper file handles and not pseudo-handles. This differs from posix where the fds have fixed values. I realise that miri does want to track the difference but I worry about confusing the terminology.

Hm, some ideas on paths forwards:

Leave it as-is, but add documentation about the terminology here

Try to merge stdin/out into Handle::File as normal FileDescription (basically what unix does)

This will require some more changes to the FileDescription trait. Its read and write methods are a bit tailored towards unix flavor currently, you may notice I have some hacky code in here to work around that. I'd like to fix it eventually anyways, but it adds more friction to MVP

Make Handle::File hold an enum like enum FileHandle { Stdin, Stdout, File(i32) }

Its read and write methods are a bit tailored towards unix flavor currently, you may notice I have some hacky code in here to work around that. I'd like to fix it eventually anyways, but it adds more friction to MVP

Is it even worth using the same trait for Unix and Windows? The trait is indeed very tailored towards Unix, deliberately so. Knowing nothing about the Windows APIs, I expected they would need their own trait anyway.

I haven't looked yet at those hacks. Can you write a high-level summary of the pros and cons of using the same vs a different trait?

So, the main pro of reusing the trait at all is because we need a common base trait so long as we don't intend to have two different 'open file maps', one for Windows-like systems and one for Unix-like systems. And most of the FdMap code works well for this purpose - map of numbers to open files is actually a pretty good abstraction for both platforms. The read/write/seek parts of the trait aren't very file-system dependent already, as they're closer to abstractions over the File interface than the syscalls.

To use an entirely different trait, we'd have to somehow support two different dyn Trait in the file code. They also actually would be nearly identical - I think I can remove the main hack I was talking about, looking at it again with fresh eyes.

I expected we'd have two different open file maps, yeah.

But if there's stuff that can be usefully shared between Windows and Unix, even better! I just want to make sure we can keep evolving the Unix side without being held back by constraints or lack of knowledge about what happens on the Windows side.

CraftSpider · 2024-12-01T20:58:29Z

Rebased on top of #4045

bors · 2024-12-01T22:57:12Z

☔ The latest upstream changes (presumably #4045) made this pull request unmergeable. Please resolve the merge conflicts.

- consistent handling, invalid handles are always an abort - Helper for reading handles that does the checking and machine stop - Use real handle types more places - Adds `File` and `Invalid` types of handle. File support will be added next

… enough to get file metadata.

STDIN/ERR/OUT are now proper pseudo-handles.

…handling

RalfJung · 2024-12-06T06:49:27Z

src/shims/files.rs

@@ -402,10 +411,21 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
        &mut self,
        actual_write_size: usize,
        dest: &MPlaceTy<'tcx>,
-    ) -> InterpResult<'tcx> {
+    ) -> InterpResult<'tcx, Result<(), io::ErrorKind>> {


If you have to completely change how we do error handling for IO functions on Unix, please make that a separate PR.

Will do. I wanted to make the change to this branch first to ensure it would work well and pass local tests with both the existing unix code, and my new Windows shims. I already intended to split this change off and merge it separately.

CraftSpider marked this pull request as draft November 21, 2024 07:50

CraftSpider mentioned this pull request Nov 21, 2024

Move FdTable to a common location and split off Unix behavior #4045

Merged

ChrisDenton reviewed Nov 21, 2024

View reviewed changes

sivadeilra mentioned this pull request Nov 21, 2024

Windows file system shims are missing #3482

Open

RalfJung changed the title ~~Implement file metadata, read, and write APIs.~~ Implement Windows file metadata, read, and write APIs. Nov 25, 2024

RalfJung added S-waiting-on-author Status: Waiting for the PR author to address review comments S-blocked Status: blocked on something happening somewhere else and removed S-waiting-on-author Status: Waiting for the PR author to address review comments labels Dec 1, 2024

CraftSpider force-pushed the windows-files-simple branch from ea07bef to 37140af Compare December 1, 2024 20:57

CraftSpider force-pushed the windows-files-simple branch from 37140af to 85d4f2e Compare December 2, 2024 01:06

CraftSpider added 2 commits December 1, 2024 19:27

Refactor Handle slightly

9b61c05

- consistent handling, invalid handles are always an abort - Helper for reading handles that does the checking and machine stop - Use real handle types more places - Adds `File` and `Invalid` types of handle. File support will be added next

Implement trivial file operations - opening and closing handles. Just…

ab0e138

… enough to get file metadata.

CraftSpider mentioned this pull request Dec 2, 2024

Support getting file metadata on Windows #4067

Open

CraftSpider added 4 commits December 1, 2024 19:55

Fix MAIN_THREAD handle in windows_join_main

e19deaa

Try fix for Windows paths on non-Windows machines

f1bb77d

Implement file read, write, and delete APIs.

d8720c9

STDIN/ERR/OUT are now proper pseudo-handles.

Less hacky read/write

19acb93

CraftSpider force-pushed the windows-files-simple branch from 85d4f2e to 19acb93 Compare December 2, 2024 05:48

CraftSpider changed the title ~~Implement Windows file metadata, read, and write APIs.~~ Implement Windows file read, write, and delete APIs. Dec 2, 2024

CraftSpider added 2 commits December 5, 2024 20:40

Proper error handling for Windows. Requires one-off changes to Linux …

296d806

…handling

Fix path reading

f230bb9

RalfJung reviewed Dec 6, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement Windows file read, write, and delete APIs. #4043

Implement Windows file read, write, and delete APIs. #4043

CraftSpider commented Nov 21, 2024

RalfJung commented Nov 21, 2024

CraftSpider commented Nov 21, 2024

RalfJung commented Nov 21, 2024

RalfJung commented Nov 21, 2024

cgettys-microsoft commented Nov 21, 2024

bors commented Nov 21, 2024

ChrisDenton Nov 21, 2024

CraftSpider Nov 21, 2024

This comment was marked as outdated.

RalfJung Nov 22, 2024

CraftSpider Nov 22, 2024

RalfJung Nov 24, 2024

CraftSpider commented Dec 1, 2024

bors commented Dec 1, 2024

RalfJung Dec 6, 2024

CraftSpider Dec 6, 2024

Implement Windows file read, write, and delete APIs. #4043

Are you sure you want to change the base?

Implement Windows file read, write, and delete APIs. #4043

Conversation

CraftSpider commented Nov 21, 2024

RalfJung commented Nov 21, 2024

CraftSpider commented Nov 21, 2024

RalfJung commented Nov 21, 2024

RalfJung commented Nov 21, 2024

cgettys-microsoft commented Nov 21, 2024

bors commented Nov 21, 2024

ChrisDenton Nov 21, 2024

Choose a reason for hiding this comment

CraftSpider Nov 21, 2024

Choose a reason for hiding this comment

This comment was marked as outdated.

RalfJung Nov 22, 2024

Choose a reason for hiding this comment

CraftSpider Nov 22, 2024

Choose a reason for hiding this comment

RalfJung Nov 24, 2024

Choose a reason for hiding this comment

CraftSpider commented Dec 1, 2024

bors commented Dec 1, 2024

RalfJung Dec 6, 2024

Choose a reason for hiding this comment

CraftSpider Dec 6, 2024

Choose a reason for hiding this comment