feat: add basic file I/O to runtimes

[alex-chew]

This PR adds basic file I/O facilities (read bytes from a file, write bytes to a file) to the C#, Java, Javascript, and Python runtimes. These facilities are a prerequisite for implementing file I/O in the libraries repo, as requested here: dafny-lang/libraries#50

(See Test/runtime/file-io/README.md for a description of the test files and the structure/purpose of the wrapping modules.)

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[davidcok]

Having to write something like Test/runtime/file-io/FileIO.java.dfy in order to do I/O is not a great user experience. Is it possible to have a single (target-independent) .dfy file in the library or natively part of the core language that links with whatever runtime is included for that target?

[alex-chew]

Having to write something like Test/runtime/file-io/FileIO.java.dfy in order to do I/O is not a great user experience. Is it possible to have a single (target-independent) .dfy file in the library or natively part of the core language that links with whatever runtime is included for that target?

I agree that needing to include target-dependent files in order to do I/O, isn't a great user experience (even if those files are defined in the libraries and not here, as is planned after the runtime changes are merged). As far as @robin-aws and I could come up with, there isn't a good way to define a single target-independent .dfy file in the library that links with each target's runtime (mainly due to naming differences in the targets' runtimes). We opted not to define file I/O as part of the language like the way print is - after discussing with Robin and Rustan, we concluded that print is a special convenience for debugging and should not be considered a precedent for implementing proper I/O support.

[davidcok]

OK. So, it would be OK if your intent is to have the same API but different files to be included from the library, with file names per target language (e.g. FileIO-java.dfy).

[davidcok]

But still - it looks like java and CS# could be combined. And the module names do not have to be different. Make it as easy as possible to switch between target languages.

I'd even argue for allowing extern declarations that are activated by a target language and allowing multiple such externs.

[alex-chew]

OK. So, it would be OK if your intent is to have the same API but different files to be included from the library, with file names per target language (e.g. FileIO-java.dfy).

Yes, that's mostly the approach I took here - a singular API defined as an abstract module, with concrete refining modules per target language that differ in the include-d filename (and also in the imported module name).

But still - it looks like java and CS# could be combined.

That's not true because Java uses dafny.Helpers (lowercase "dafny") whereas C# uses Dafny.Helpers (uppercase "Dafny"). Actually, it's possible for the Javascript and Python (and even Go, once other blocker(s) are resolved) to be combined since they all share the _dafny interface. But in my opinion it's less confusing to always have a different concrete module per target, than to have some targets be distinct and some targets be shared. (The ideal of one concrete module for all targets is not feasible as explained before.)

And the module names do not have to be different. Make it as easy as possible to switch between target languages.

That's a good point. I've simplified the module names so that the concrete modules can all be imported under the same name, and only the include-d filename needs to differ per-target.

I'd even argue for allowing extern declarations that are activated by a target language and allowing multiple such externs.

I agree, and there is discussion about such a feature here: #2397. But we opted to keep that out of scope for this initial file I/O support, which is intentionally basic. If/when that feature is added then we can simplify these modules accordingly.

[davidcok]

1. Do you intend to swallow the exception stack?
2. Please write the FileIO files precisely as they will be in the library -- currently they are test files. Even better would be to put them in a separate folder.
   2a) And then you can, in each FileIO file, document a simple use of the IO methods (i.e. what file to include, what module to import)
3. {:compile false} is unnecessary for method stubs that do not have bodies
4. Did you and Robin decide to just read/write bytes and not read/write strings? The more common use case is to get text, not bytes from files.

[robin-aws]

Just some high-level feedback for now, will probably have more after we split up the test files as I've suggested (assuming that makes sense)

[robin-aws]

Do you have a strong opinion about making this isError rather than isSuccess? I know the idiom in Go is to return ok, which this reminds me of.

[davidcok]

I concur with wondering about the correct sign of this output.

[alex-chew]

I don't have a strong opinion either way, but since this an internal API (users of the file I/O API should never see/use this) I'm not too concerned either way.

[fabiomadge]

I would prefer to keep the runtime as small as possible. Can we move those into a separate file in the file-io directory, until this becomes an actual language feature?

[robin-aws]

@alex-chew and I revisited our reasoning for putting this logic in the runtime, and came to the same conclusion. The original motivation was piggybacking on the existing "distribution" of native code, but I think it's not worth the coupling cost, especially since it forces using refinement to customize the extern declaration per language.

@alex-chew is going to move this to a pure dafny-lang/libraries PR that includes the native code as well. The downside will be needing to manually include a target language artifact like DafnyIO.jar to build and run Dafny code that uses this library, but that pain should go away in the long term as we add better support for Dafny projects and dependencies, especially when you add separate compilation.

[davidcok]

Your call, but for me, including the IO routines in the runtime is well worth not having to scrounge around for the relevant FileIO.xx for each target. At least have dafny run include these extra files automatically.

[alex-chew]

In the new PR there is no implementation in the runtime, so @fabiomadge's original concern in this thread is resolved.

Your call, but for me, including the IO routines in the runtime is well worth not having to scrounge around for the relevant FileIO.xx for each target. At least have dafny run include these extra files automatically.

In my opinion the upsides of keeping the file I/O libraries independent from a particular Dafny version range, and of keeping the runtimes small, outweigh the cost of needing to specify an extra --input libraries/src/FileIO/FileIO.xx flag (or otherwise integrating the file into one's build process, if using separate compilation). But having dafny run include the extra files automatically is an interesting idea and I think it can be implemented later as a non-breaking change.

[alex-chew]

As discussed in discussions here and offline, I'm moving this work out of the Dafny language/runtime and into the libraries repo. I'll respond to the open threads here, but further progress will be made in the new libraries PR: dafny-lang/libraries#60

[alex-chew]

1. Do you intend to swallow the exception stack?

This was not intentional; in this PR exception stack traces were only preserved in C#. In the new PR, all implementations preserve stack traces.

2. Please write the FileIO files precisely as they will be in the library -- currently they are test files. Even better would be to put them in a separate folder.

Good call; I've done this in the new PR.

   2a) And then you can, in each FileIO file, document a simple use of the IO methods (i.e. what file to include, what module to import)

I've noted this as a TODO in the new PR.

3. {:compile false} is unnecessary for method stubs that do not have bodies

Thanks, I've removed these in the new PR.

4. Did you and Robin decide to just read/write bytes and not read/write strings? The more common use case is to get text, not bytes from files.

Yes, we wanted to keep the complexity of handling text encoding out of this MVP. I expect that we'll be able provide APIs that "do the right thing" by default once Dafny strings are Unicode by default. For now, users can encode/decode as needed using the existing Unicode modules in the libraries repo.