feat: add basic file I/O implementations

.github/workflows/tests.yml

@@ -16,11 +16,14 @@ jobs:
       - name: Install Dafny
         uses: dafny-lang/setup-dafny-action@v1
         with:
-          dafny-version: "3.4.2"
+          dafny-version: "3.9.1"
 
-      - name: Install lit 
+      - name: Install lit
         run: pip install lit OutputCheck
 
+      - name: Set up JS dependencies
+        run: npm install bignumber.js
+
       - name: Verify Dafny Code
         run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' .
 

examples/FileIO/ReadBytesFromFile.dfy

@@ -0,0 +1,45 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+// RUN: %dafny /compile:0 "%s"
+// RUN: echo -n > "%t"
+// RUN: %baredafny run --no-verify --target:cs "%s" --input "%S/../../src/FileIO/FileIO.cs" -- "%S/data.txt" "System.ArgumentException:" >> "%t"
+// RUN: %baredafny run --no-verify --target:java "%s" --input "%S/../../src/FileIO/FileIO.java" -- "%S/data.txt" "java.io.IOException:" >> "%t"
+// RUN: %baredafny run --no-verify --target:js "%s" --input "%S/../../src/FileIO/FileIO.js" -- "%S/data.txt" "Error: ENOENT" >> "%t"
+// TODO: %baredafny run --no-verify --target:py "%s" --input "%S/../../src/FileIO/FileIO.py" -- "%S/data.txt" "[Errno 2]" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "../../src/FileIO/FileIO.dfy"
+
+module ReadBytesFromFile {
+  import FileIO
+
+  method Main(args: seq<string>) {
+    expect |args| > 0;
+    expect |args| == 3, "usage: " + args[0] + " DATA_PATH EXPECTED_ERROR_PREFIX";
+    var dataPath := args[1];
+    var expectedErrorPrefix := args[2];
+
+    // Happy path: read from the data file, and check that we see the expected content.
+    {
+      var expectedStr := "Hello world\nGoodbye\n";
+      // This conversion is safe only for ASCII values. For Unicode conversions, see the Unicode modules.
+      var expectedBytes := seq(|expectedStr|, i requires 0 <= i < |expectedStr| => expectedStr[i] as int);
+
+      var res := FileIO.ReadBytesFromFile(dataPath);
+      expect res.Success?, "unexpected failure: " + res.error;
+
+      var readBytes := seq(|res.value|, i requires 0 <= i < |res.value| => res.value[i] as int);
+      expect readBytes == expectedBytes, "read unexpected byte sequence";
+    }
+
+    // Failure path: attempting to read from a blank file path should never work.
+    {
+      var res := FileIO.ReadBytesFromFile("");
+      expect res.Failure?, "unexpected success";
+      expect expectedErrorPrefix <= res.error, "unexpected error message: " + res.error;
+    }
+  }
+}

examples/FileIO/ReadBytesFromFile.dfy.expect

@@ -0,0 +1,6 @@
+
+Dafny program verifier did not attempt verification
+
+Dafny program verifier did not attempt verification
+
+Dafny program verifier did not attempt verification

examples/FileIO/WriteBytesToFile.dfy

@@ -0,0 +1,79 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+// RUN: %dafny /compile:0 "%s"
+// RUN: echo -n > "%t"
+// RUN: %baredafny run --no-verify --target:cs "%s" --input "%S/../../src/FileIO/FileIO.cs" -- "%t_cs" "System.ArgumentException:" >> "%t"
+// RUN: %baredafny run --no-verify --target:java "%s" --input "%S/../../src/FileIO/FileIO.java" -- "%t_java" "java.nio.file.FileSystemException:" >> "%t"
+// RUN: %baredafny run --no-verify --target:js "%s" --input "%S/../../src/FileIO/FileIO.js" -- "%t_js" "Error: ENOENT" >> "%t"
+// TODO: %baredafny run --no-verify --target:py "%s" --input "%S/../../src/FileIO/FileIO.py" -- "%t_py" "[Errno 2]" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+//// Check that written files match expectations
+// RUN: %diff "data.txt" "%t_cs/output_plain"
+// RUN: %diff "data.txt" "%t_cs/foo/bar/output_nested"
+// RUN: %diff "data.txt" "%t_cs/foo/output_up"
+// RUN: %diff "data.txt" "%t_java/output_plain"
+// RUN: %diff "data.txt" "%t_java/foo/bar/output_nested"
+// RUN: %diff "data.txt" "%t_java/foo/output_up"
+// RUN: %diff "data.txt" "%t_js/output_plain"
+// RUN: %diff "data.txt" "%t_js/foo/bar/output_nested"
+// RUN: %diff "data.txt" "%t_js/foo/output_up"
+// TODO: %diff "data.txt" "%t_py/output_plain"
+// TODO: %diff "data.txt" "%t_py/foo/bar/output_nested"
+// TODO: %diff "data.txt" "%t_py/foo/output_up"
+
+include "../../src/FileIO/FileIO.dfy"
+
+module WriteBytesToFile {
+  import FileIO
+
+  method Main(args: seq<string>) {
+    expect |args| > 0;
+    expect |args| == 3, "usage: " + args[0] + " OUTPUT_DIR EXPECTED_ERROR_PREFIX";
+    var outputDir := args[1];
+    var expectedErrorPrefix := args[2];
+
+    // Happy paths: write files to the output dir. (The %diff LIT commands check that we wrote the correct content.)
+    {
+      // Ideally we would define `str` as a constant and compute `bytes` automatically.
+      // To do so, we would need to convert each `char` in `str` to a `bv8` value, by using `as bv8`.
+      // But that triggers a bug in the Java compiler: <https://github.com/dafny-lang/dafny/issues/2942>.
+      // So for now we settle for manually writing out the desired `bytes`,
+      // and statically verifying that these values match the characters of `str`.
+      ghost var str := "Hello world\nGoodbye\n";
+      var bytes: seq<bv8> := [
+        // "Hello world\n"
+        0x48, 0x65, 0x6c, 0x6c, 0x6f, 0x20, 0x77, 0x6f, 0x72, 0x6c, 0x64, 0x0a,
+        // "Goodbye\n"
+        0x47, 0x6f, 0x6f, 0x64, 0x62, 0x79, 0x65, 0x0a
+      ];
+      assert forall i | 0 <= i < |bytes| :: bytes[i] as int == str[i] as int;
+
+      // Write directly into the output directory
+      {
+        var res := FileIO.WriteBytesToFile(outputDir + "/output_plain", bytes);
+        expect res.Success?, "unexpected failure writing to output_plain: " + res.error;
+      }
+      // Ensure that nonexistent parent directories are created as necessary
+      {
+        var res := FileIO.WriteBytesToFile(outputDir + "/foo/bar/output_nested", bytes);
+        expect res.Success?, "unexpected failure writing to output_nested: " + res.error;
+      }
+      // Ensure that file paths with .. are handled correctly
+      {
+        var res := FileIO.WriteBytesToFile(outputDir + "/foo/bar/../output_up", bytes);
+        expect res.Success?, "unexpected failure writing to output_up: " + res.error;
+      }
+    }
+
+    // Failure path: attempting to write to a blank file path should never work.
+    {
+      var res := FileIO.WriteBytesToFile("", []);
+      expect res.Failure?, "unexpected success";
+      expect expectedErrorPrefix <= res.error, "unexpected error message: " + res.error;
+    }
+  }
+}

examples/FileIO/WriteBytesToFile.dfy.expect

@@ -0,0 +1,6 @@
+
+Dafny program verifier did not attempt verification
+
+Dafny program verifier did not attempt verification
+
+Dafny program verifier did not attempt verification

examples/FileIO/data.txt

@@ -0,0 +1,2 @@
+Hello world
+Goodbye

src/FileIO/FileIO.cs

@@ -0,0 +1,94 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+namespace DafnyLibraries {
+  using System;
+  using System.IO;
+
+  using Dafny;
+
+  public class FileIO {
+    /// <summary>
+    /// Attempts to read all bytes from the file at the given path, and outputs the following values:
+    /// <list>
+    ///   <item>
+    ///     <term>isError</term>
+    ///     <description>
+    ///       true iff an exception was thrown during path string conversion or when reading the file
+    ///     </description>
+    ///   </item>
+    ///   <item>
+    ///     <term>bytesRead</term>
+    ///     <description>
+    ///       the sequence of bytes read from the file, or an empty sequence if <c>isError</c> is true
+    ///     </description>
+    ///   </item>
+    ///   <item>
+    ///     <term>errorMsg</term>
+    ///     <description>
+    ///       the error message of the thrown exception if <c>isError</c> is true, or an empty sequence otherwise
+    ///     </description>
+    ///   </item>
+    /// </list>
+    ///
+    /// We output these values individually because Result is not defined in the runtime but instead in library code.
+    /// It is the responsibility of library code to construct an equivalent Result value.
+    /// </summary>
+    public static void INTERNAL_ReadBytesFromFile(ISequence<char> path, out bool isError, out ISequence<byte> bytesRead,
+      out ISequence<char> errorMsg) {
+      isError = true;
+      bytesRead = Sequence<byte>.Empty;
+      errorMsg = Sequence<char>.Empty;
+      try {
+        bytesRead = Helpers.SeqFromArray(File.ReadAllBytes(path?.ToString()));
+        isError = false;
+      } catch (Exception e) {
+        errorMsg = Helpers.SeqFromArray(e.ToString().ToCharArray());
+      }
+    }
+
+    /// <summary>
+    /// Attempts to write all given bytes to the file at the given path, creating nonexistent parent directories as necessary,
+    /// and outputs the following values:
+    /// <list>
+    ///   <item>
+    ///     <term>isError</term>
+    ///     <description>
+    ///       true iff an exception was thrown during path string conversion or when writing to the file
+    ///     </description>
+    ///   </item>
+    ///   <item>
+    ///     <term>errorMsg</term>
+    ///     <description>
+    ///       the error message of the thrown exception if <c>isError</c> is true, or an empty sequence otherwise
+    ///     </description>
+    ///   </item>
+    /// </list>
+    ///
+    /// We output these values individually because Result is not defined in the runtime but instead in library code.
+    /// It is the responsibility of library code to construct an equivalent Result value.
+    /// </summary>
+    public static void INTERNAL_WriteBytesToFile(ISequence<char> path, ISequence<byte> bytes, out bool isError, out ISequence<char> errorMsg) {
+      isError = true;
+      errorMsg = Sequence<char>.Empty;
+      try {
+        string pathStr = path?.ToString();
+        CreateParentDirs(pathStr);
+        File.WriteAllBytes(pathStr, bytes.CloneAsArray());
+        isError = false;
+      } catch (Exception e) {
+        errorMsg = Helpers.SeqFromArray(e.ToString().ToCharArray());
+      }
+    }
+
+    /// <summary>
+    /// Creates the nonexistent parent directory(-ies) of the given path.
+    /// </summary>
+    private static void CreateParentDirs(string path) {
+      string parentDir = Path.GetDirectoryName(Path.GetFullPath(path));
+      Directory.CreateDirectory(parentDir);
+    }
+  }
+}

src/FileIO/FileIO.dfy

@@ -0,0 +1,66 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+// RUN: %dafny /compile:0 "%s"
+
+include "../Wrappers.dfy"
+
+/**
+ * This module provides basic file I/O operations: reading and writing bytes from/to a file.
+ * The provided API is intentionally limited in scope and will be expanded later.
+ *
+ * Where the API accepts file paths as strings, there are some limitations.
+ * File paths containing only ASCII characters work identically across languages and platforms;
+ * non-ASCII Unicode codepoints may cause different language- or platform-specific behavior.
+ */
+module FileIO {
+  import opened Wrappers
+
+  export provides ReadBytesFromFile, WriteBytesToFile, Wrappers
+
+  /*
+   * Public API
+   */
+
+  /**
+   * Attempts to read all bytes from the file at the given file path.
+   * If an error occurs, a `Result.Failure` value is returned containing an implementation-specific
+   * error message (which may also contain a stack trace).
+   *
+   * NOTE: See the module description for limitations on the path argument.
+   */
+  method ReadBytesFromFile(path: string) returns (res: Result<seq<bv8>, string>) {
+    var isError, bytesRead, errorMsg := INTERNAL_ReadBytesFromFile(path);
+    return if isError then Failure(errorMsg) else Success(bytesRead);
+  }
+
+  /**
+   * Attempts to write the given bytes to the file at the given file path,
+   * creating nonexistent parent directories as necessary.
+   * If an error occurs, a `Result.Failure` value is returned containing an implementation-specific
+   * error message (which may also contain a stack trace).
+   *
+   * NOTE: See the module description for limitations on the path argument.
+   */
+  method WriteBytesToFile(path: string, bytes: seq<bv8>) returns (res: Result<(), string>)
+  {
+    var isError, errorMsg := INTERNAL_WriteBytesToFile(path, bytes);
+    return if isError then Failure(errorMsg) else Success(());
+  }
+
+  /*
+   * Private API - these are intentionally not exported from the module and should not be used elsewhere
+   */
+
+  method
+    {:extern "DafnyLibraries.FileIO", "INTERNAL_ReadBytesFromFile"}
+    INTERNAL_ReadBytesFromFile(path: string)
+    returns (isError: bool, bytesRead: seq<bv8>, errorMsg: string)
+
+  method
+    {:extern "DafnyLibraries.FileIO", "INTERNAL_WriteBytesToFile"}
+    INTERNAL_WriteBytesToFile(path: string, bytes: seq<bv8>)
+    returns (isError: bool, errorMsg: string)
+}