Per backend code support in stdlibs

.github/workflows/standard-libraries.yml

@@ -15,7 +15,7 @@ jobs:
 
   build:
     needs: check-deep-tests
-    runs-on: ubuntu-latest
+    runs-on: macos-latest
 
     steps:
       - name: Checkout Dafny
@@ -30,7 +30,7 @@ jobs:
       - name: Build Dafny
         run: dotnet build Source/Dafny.sln
       - name: Get Z3
-        run: make z3-ubuntu
+        run: make z3-mac
       - run: npm install bignumber.js
       - name: Test DafnyStandardLibraries
         run: make -C Source/DafnyStandardLibraries all

Source/DafnyCore/AST/ShouldCompileOrVerify.cs

@@ -24,6 +24,14 @@ public static bool ShouldCompile(this ModuleDefinition module, CompilationData p
       // https://github.com/dafny-lang/dafny/issues/4009
       return true;
     }
+
+    if (program.Options.Backend?.TargetId != "lib") {
+      bool compileIt = true;
+      if (Attributes.ContainsBool(module.Attributes, "compile", ref compileIt) && !compileIt) {
+        return false;
+      }
+    }
+
     return program.UrisToCompile.Contains(module.Tok.Uri);
   }
 

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -99,6 +99,9 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimeCsharp", wr, false);
       }
+      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+        EmitRuntimeSource("DafnyStandardLibraries_cs", wr, false);
+      }
 
       if (Options.Get(CommonOptionBag.ExecutionCoverageReport) != null) {
         EmitCoverageReportInstrumentation(program, wr);

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -69,6 +69,9 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimeGo", wr);
       }
+      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+        EmitRuntimeSource("DafnyStandardLibraries_go", wr);
+      }
     }
 
     private string DafnyTypeDescriptor => $"{HelperModulePrefix}TypeDescriptor";

Source/DafnyCore/Compilers/Java/Compiler-java.cs

@@ -303,6 +303,9 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimeJava", wr);
       }
+      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+        EmitRuntimeSource("DafnyStandardLibraries_java", wr);
+      }
       wr.WriteLine($"// Dafny program {program.Name} compiled into Java");
       ModuleName = program.MainMethod != null ? "main" : Path.GetFileNameWithoutExtension(program.Name);
       wr.WriteLine();

Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs

@@ -47,6 +47,9 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimeJs", wr, false);
       }
+      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+        EmitRuntimeSource("DafnyStandardLibraries_js", wr, false);
+      }
     }
 
     public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -62,6 +62,9 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       if (Options.IncludeRuntime) {
         EmitRuntimeSource("DafnyRuntimePython", wr);
       }
+      if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
+        EmitRuntimeSource("DafnyStandardLibraries_py", wr);
+      }
 
       Imports.Add(DafnyRuntimeModule);
       EmitImports(null, wr);

Source/DafnyDriver/Commands/DafnyCli.cs

@@ -31,6 +31,7 @@ public static class DafnyCli {
   private const string ToolchainDebuggingHelpName = "--help-internal";
   private static readonly RootCommand RootCommand = new("The Dafny CLI enables working with Dafny, a verification-aware programming language. Use 'dafny -?' to see help for the previous CLI format.");
 
+  private static readonly string StandardLibrariesDooUriBase = "dllresource://DafnyPipeline/DafnyStandardLibraries";
   private static readonly Uri StandardLibrariesDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries.doo");
   private static readonly Uri StandardLibrariesArithmeticDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries-arithmetic.doo");
 
@@ -488,6 +489,13 @@ public static ExitValue GetDafnyFiles(DafnyOptions options,
     // only because if they are added first, one might be used as the program name,
     // which is not handled well.
     if (options.Get(CommonOptionBag.UseStandardLibraries)) {
+      if (options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {
+        var targetName = options.CompilerName ?? "notarget";
+        var stdlibDooUri = new Uri($"{StandardLibrariesDooUriBase}-{targetName}.doo");
+        options.CliRootSourceUris.Add(stdlibDooUri);
+        dafnyFiles.Add(new DafnyFile(options, stdlibDooUri));
+      }
+
       options.CliRootSourceUris.Add(StandardLibrariesDooUri);
       dafnyFiles.Add(new DafnyFile(options, StandardLibrariesDooUri));
 

Source/DafnyPipeline/DafnyPipeline.csproj

@@ -32,6 +32,51 @@
   we may be able to get away with only embedding these files inside this assembly.
   -->
   <ItemGroup>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\binaries\DafnyStandardLibraries-notarget.doo">
+      <LogicalName>DafnyStandardLibraries-notarget.doo</LogicalName>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\binaries\DafnyStandardLibraries-java.doo">
+      <LogicalName>DafnyStandardLibraries-java.doo</LogicalName>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\binaries\DafnyStandardLibraries-cs.doo">
+      <LogicalName>DafnyStandardLibraries-cs.doo</LogicalName>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\binaries\DafnyStandardLibraries-js.doo">
+      <LogicalName>DafnyStandardLibraries-js.doo</LogicalName>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\binaries\DafnyStandardLibraries-go.doo">
+      <LogicalName>DafnyStandardLibraries-go.doo</LogicalName>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\binaries\DafnyStandardLibraries-py.doo">
+      <LogicalName>DafnyStandardLibraries-py.doo</LogicalName>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\src\**\*.cs">
+      <LinkBase>DafnyStandardLibraries_cs</LinkBase>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\src\**\*.java">
+      <LinkBase>DafnyStandardLibraries_java</LinkBase>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\src\**\*.js">
+      <LinkBase>DafnyStandardLibraries_js</LinkBase>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\src\**\*.go">
+      <LinkBase>DafnyStandardLibraries_go</LinkBase>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+    <EmbeddedResource Include="..\DafnyStandardLibraries\src\**\*.py">
+      <LinkBase>DafnyStandardLibraries_py</LinkBase>
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </EmbeddedResource>
+
     <EmbeddedResource Include="..\DafnyStandardLibraries\binaries\DafnyStandardLibraries.doo">
       <LogicalName>DafnyStandardLibraries.doo</LogicalName>
       <CopyToOutputDirectory>Always</CopyToOutputDirectory>

Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go

@@ -521,6 +521,14 @@ func SeqOfChars(values ...Char) Sequence {
   return SeqFromArray(arr, true)
 }
 
+func SeqOfBytes(values []byte) Sequence {
+  arr := make([]interface{}, len(values))
+  for i, v := range values {
+    arr[i] = v
+  }
+  return SeqFromArray(arr, false)
+}
+
 // SeqOfString converts the given string into a sequence of characters.
 // The given string must contain only ASCII characters!
 func SeqOfString(str string) Sequence {
@@ -672,6 +680,25 @@ func (seq *LazySequence) EqualsGeneric(x interface{}) bool {
   return ok && Companion_Sequence_.Equal(seq, other)
 }
 
+func (seq *ArraySequence) ToByteArray() []byte {
+  return ToByteArray(seq)
+}
+func (seq *ConcatSequence) ToByteArray() []byte {
+  return ToByteArray(seq)
+}
+func (seq *LazySequence) ToByteArray() []byte {
+  return ToByteArray(seq)
+}
+
+func ToByteArray(x Sequence) []byte {
+  nativeArray := x.ToArray().(GoNativeArray)
+  arr := make([]byte, len(nativeArray.contents))
+  for i, v := range nativeArray.contents {
+    arr[i] = v.(byte)
+  }
+  return arr
+}
+
 /******************************************************************************
  * Arrays
  ******************************************************************************/

Source/DafnyStandardLibraries/CONTRIBUTING.md

@@ -37,11 +37,9 @@ to check things are provable are reasonable,
 and it's fine if `dafny test` only ends up checking that verification succeeds,
 but avoid non-ghost code that cannot be compiled.
 
-The support for measuring runtime test coverage of Dafny code
-is not complete enough to be applied easily to this project,
-but will be added as soon as possible.
-In the meantime, please ensure your testing coverage
-is at least greater than 0%!
+To see the runtime coverage of the examples and tests,
+run `make coverage` and then open the 
+`build/testcoverage/<most recent timestamp>/index_tests_actual.html` file.
 
 ### Documentation
 
@@ -65,19 +63,39 @@ The build process applies `dafny format` to all source.
 
 ### Packaging
 
-For now all standard libraries are built together into a single `DafnyStandardLibraries.doo` file,
-which is included as an embedded resource in `DafnyPipeline.dll`.
-That will likely need to change as more libraries are imported,
-in particular https://github.com/dafny-lang/libraries/tree/master/src/NonlinearArithmetic
-which needs to build with `--disable-nonlinear-arithmetic`.
-It will be fairly straightforward to build multiple `.doo` files that are all added
-with the `--standard-libraries` option, but the build process will need to be tweaked to support that.
+The standard libraries are built together into multiple `DafnyStandardLibraries*.doo` files,
+which are included as embedded resources in `DafnyPipeline.dll`.
+These are then added as additional implicit source files when `--standard-libraries` is switched on.
+Having multiple `.doo` files allows each of them to be verified with different flags,
+such as `--disable-nonlinear-arithmetic`.
+This doesn't affect the end user experience, as Dafny checks that each `.doo` file
+is compatible with the current set of options independently,
+and the source of the definitions doesn't matter to the code consuming them.
+
+Some standard libraries depend on `{:extern}`-ally implemented functionality, such as `FileIO`.
+Because the `{:extern}` attribute needs to be defined differently for different backends,
+the build creates a `DafnyStandardLibraries-<target id>.doo` file
+for each supported target language.
+Each is included only when compiling to that target language, 
+using the `build`, `translate`, `run` or `test` Dafny CLI commands
+(or the equivalent modes of the legacy CLI).
+
+There is also a `DafnyStandardLibraries-notarget.doo` file used when NOT compiling,
+which provides only the bodyless interface declaration.
+Each of the `.doo` files for the target languages
+replace the bodyless declarations with the actual implementations, backed by externs.
+The current approach is sound but will not scale well in the future,
+since it repeatedly verifies the common code that consumes the abstract interface
+for each target language.
+A [pending language enhancement](https://github.com/dafny-lang/dafny/pull/4681) will likely address this point.
+
+All target language files in this project are also embedded in the `DafnyPipeline.dll`.
+When `--standard-libraries` is switched on,
+these source files are automatically emitted when compiling,
+just like the contents of each backend's runtime.
+
+See [Makefile](Makefile) and [src/DafnyStdLibs/TargetSpecific/Makefile](src/DafnyStdLibs/TargetSpecific/Makefile) for more details.
 
-### External code
-
-Several standard libraries will need to depend on `{:extern}`-ally implemented functionality.
-The plan is to include such code in each backend's runtime,
-but adding this to the build process is currently blocked on https://github.com/dafny-lang/dafny/issues/511.
 
 ### On brittleness
 
@@ -118,7 +136,7 @@ inflict on consumers.
 ## Importing from dafny-lang/libraries
 
 There are a couple of things to watch out for when importing libraries from the
-[dafny-lang/libraries]() repository:
+[dafny-lang/libraries](https://github.com/dafny-lang/libraries) repository:
 
 * Several libraries have two copies in `dafny-lang/libraries`: one under `src`,
   and one under `src/dafny`. The latter is a copy refactored to nest all modules under a top-level

Source/DafnyStandardLibraries/Makefile

@@ -25,31 +25,33 @@ check-binary: build-binary
 	unzip -o ${DOO_FILE_ARITHMETIC_SOURCE} -d build/current-arithmetic
 	unzip -o ${DOO_FILE_ARITHMETIC_TARGET} -d build/rebuilt-arithmetic
 	diff build/current-arithmetic build/rebuilt-arithmetic
+	make -C src/DafnyStdLibs/TargetSpecific check-binary-all
 
 update-binary: build-binary
 	cp ${DOO_FILE_SOURCE} ${DOO_FILE_TARGET}
 	cp ${DOO_FILE_ARITHMETIC_SOURCE} ${DOO_FILE_ARITHMETIC_TARGET}
+	make -C src/DafnyStdLibs/TargetSpecific update-binary-all
+# Rebuild Dafny to pick up the new embedded assets
+	dotnet build ../Dafny.sln
 
 # For now we only have examples and no dedicated tests.
 # We will likely want a test directory as well,
 # with deeper coverage of module functionality.
-build-examples:
-	$(DAFNY) build -t:lib examples/dfyconfig.toml --output:build/stdlibexamples.doo
 
-test-cs: build-examples
-	$(DAFNY) test -t:cs build/stdlibexamples.doo examples/BoundedInts/NonDefault.cs --output:build/stdlibexamples --coverage-report:build/testcoverage
+test-cs:
+	$(DAFNY) test -t:cs examples/dfyconfig.toml examples/BoundedInts/NonDefault.cs --output:build/stdlibexamples --coverage-report:build/testcoverage
 
-test-java: build-examples
-	$(DAFNY) test -t:java build/stdlibexamples.doo examples/BoundedInts/Externs/NonDefault.java --output:build/stdlibexamples
+test-java:
+	$(DAFNY) test -t:java examples/dfyconfig.toml examples/BoundedInts/Externs/NonDefault.java --output:build/stdlibexamples
 
-test-go: build-examples
-	$(DAFNY) test -t:go build/stdlibexamples.doo examples/BoundedInts/NonDefault.go --output:build/stdlibexamples
+test-go:
+	$(DAFNY) test -t:go examples/dfyconfig.toml examples/BoundedInts/NonDefault.go --output:build/stdlibexamples
 
-test-py: build-examples
-	$(DAFNY) test -t:py build/stdlibexamples.doo examples/BoundedInts/NonDefault.py --output:build/stdlibexamples
+test-py:
+	$(DAFNY) test -t:py examples/dfyconfig.toml examples/BoundedInts/NonDefault.py --output:build/stdlibexamples
 
-test-js: build-examples
-	$(DAFNY) test -t:js build/stdlibexamples.doo examples/BoundedInts/NonDefault.js --output:build/stdlibexamples
+test-js:
+	$(DAFNY) test -t:js examples/dfyconfig.toml examples/BoundedInts/NonDefault.js --output:build/stdlibexamples
 
 test: test-cs test-java test-go test-py test-js
 

Source/DafnyStandardLibraries/README.md

@@ -30,6 +30,13 @@ When using this option with commands like `dafny translate`, `dafny build`, or `
 the contents of the standard libraries will be automatically included in the translated source code as well.
 We do not yet provide any separately-compiled artifacts with this code.
 
+Some libraries are dependent on target language utilities, such as `FileIO`.
+When `--standard-libraries` is on,
+the translation process will also include some additional supporting target language source files,
+just as the runtime source is emitted unless `--include-runtime` is off.
+These libraries may not be available for all supported languages,
+and are simply not defined when translating to those languages.
+
 Because the standard libraries are already pre-verified, `--standard-libraries` is not compatible with all options,
 since mixing and matching some options that affect verification across different components is not always safe.
 In particular, `--standard-libraries` currently cannot be used together with `--unicode-char:false`.

Source/DafnyStandardLibraries/examples/FileIO/ReadBytesFromFile.dfy

@@ -0,0 +1,36 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+module ReadBytesFromFile {
+  import DafnyStdLibs.FileIO
+
+  method {:test} Test() {
+    // TODO: extern function for the expected error prefix
+    theMain("examples/FileIO/../FileIO/data.txt", "");
+  }
+
+  method theMain(dataPath: string, expectedErrorPrefix: string) {
+
+      // 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;
+    }
+  }
+}