Windows file system shims are missing

[RalfJung]

Miri supports accessing the file system (opening, reading, writing files; listing directories) on Unix systems, but not on Windows. This is probably the biggest remaining gap in our Windows support.

If you run into this, try cargo miri test --target x86_64-unknown-linux-gnu. This works even on a Windows host (without installing anything extra) and interprets programs on a well-supported Linux target -- file system access should generally work then. If it doesn't please file an issue (do not comment on this issue, instead file a new one).

Nobody on the Miri team is very knowledgeable in Windows APIs, and a reasonable work-around exists for Windows users, so this is unlikely to be on our agenda any time soon. Contributions are always welcome though. :)

[mbyt]

Thanks again for your fast response.

What I currently do, is that I run the complete unittest suite on windows and skip the tests which (i) access the filesystem or (ii) a foreign function. This works actually quite well and thanks to miri I already found a few places of undefined behavior. That's marvelous!

With this ticket I could also run the tests which access the filesystem and would only need to skip the tests with the foreign function.

Regarding external C dependencies: Is this the topic of #2365?

[RalfJung]

Okay, so the problem is getting the build scripts to shut up and do nothing so that you can use --target x86_64-unknown-linux-gnu. On Windows the external dependencies will be built and linked even in Miri, which is useless but harmless. With a cross-target then it is not harmless any more, it causes the build to fail. I can see how disabling those build scripts could become tricky. Might still be simpler than implementing the Windows FS shims though. ;)

Regarding external C dependencies: Is this the topic of #2365?

Yes.

This works actually quite well and thanks to miri I already found a few places of undefined behavior. That's marvelous!

Awesome. :)

If these bugs have a public track record / issue / PR somewhere, we always appreciate PRs that add more bugs to the "bugs found with Miri" list in the readme. :D

[mbyt]

Thanks again for your fast response and help. This is really a great project!

If these bugs have a public track record / issue / PR somewhere, we always appreciate PRs that add more bugs to the "bugs found with Miri" list in the readme. :D

Unfortunately the issues are in the closed source components, thus I cannot share. However, if interesting for you here the error messages of the discovered errors:

• error: Undefined Behavior: accessing memory based on pointer with alignment 1, but alignment 4 is required
• error: memory leaked: alloc288778 (C heap, size: 824, align: 16), allocated here:
• error: casting references to a bigger memory layout than the backing allocation is undefined behavior, even if the reference is unused