diff --git a/.github/workflows/standard-libraries.yml b/.github/workflows/standard-libraries.yml index 37848e4cbeb..1b3f67aed61 100644 --- a/.github/workflows/standard-libraries.yml +++ b/.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 diff --git a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs index 103c57e39d6..edf31aae0d9 100644 --- a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs +++ b/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); } diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index c0dcd391747..7b8e0d61f0f 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/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); diff --git a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs index 43aae8a70ce..ea506f6cae8 100644 --- a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs +++ b/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"; diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index f41a92e9196..2ea7506832e 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/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(); diff --git a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs index 8d08c2cdd32..249c8395a61 100644 --- a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs +++ b/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) { diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs index ba5e59ed0ae..4c9718b0990 100644 --- a/Source/DafnyCore/Compilers/Python/Compiler-python.cs +++ b/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); diff --git a/Source/DafnyDriver/Commands/DafnyCli.cs b/Source/DafnyDriver/Commands/DafnyCli.cs index ed7a6fd6754..a8da490ff95 100644 --- a/Source/DafnyDriver/Commands/DafnyCli.cs +++ b/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)); diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj index 8d047e8f784..2ca70976e14 100644 --- a/Source/DafnyPipeline/DafnyPipeline.csproj +++ b/Source/DafnyPipeline/DafnyPipeline.csproj @@ -32,6 +32,51 @@ we may be able to get away with only embedding these files inside this assembly. --> + + DafnyStandardLibraries-notarget.doo + Always + + + DafnyStandardLibraries-java.doo + Always + + + DafnyStandardLibraries-cs.doo + Always + + + DafnyStandardLibraries-js.doo + Always + + + DafnyStandardLibraries-go.doo + Always + + + DafnyStandardLibraries-py.doo + Always + + + DafnyStandardLibraries_cs + Always + + + DafnyStandardLibraries_java + Always + + + DafnyStandardLibraries_js + Always + + + DafnyStandardLibraries_go + Always + + + DafnyStandardLibraries_py + Always + + DafnyStandardLibraries.doo Always diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go index 6cb755e1f8b..d9929d627ad 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go +++ b/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 ******************************************************************************/ diff --git a/Source/DafnyStandardLibraries/CONTRIBUTING.md b/Source/DafnyStandardLibraries/CONTRIBUTING.md index 992f7c275dd..0cebdd373d3 100644 --- a/Source/DafnyStandardLibraries/CONTRIBUTING.md +++ b/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//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-.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 diff --git a/Source/DafnyStandardLibraries/Makefile b/Source/DafnyStandardLibraries/Makefile index 7669cd5692e..84ef10037f2 100644 --- a/Source/DafnyStandardLibraries/Makefile +++ b/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 diff --git a/Source/DafnyStandardLibraries/README.md b/Source/DafnyStandardLibraries/README.md index 557dc9f03ca..dcb609dd54a 100644 --- a/Source/DafnyStandardLibraries/README.md +++ b/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`. diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo index 8d909f67490..0143118541b 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo new file mode 100644 index 00000000000..e95bb0ff007 Binary files /dev/null and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo new file mode 100644 index 00000000000..17f46c91cbe Binary files /dev/null and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo new file mode 100644 index 00000000000..0f660948aea Binary files /dev/null and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo new file mode 100644 index 00000000000..166218e2752 Binary files /dev/null and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo new file mode 100644 index 00000000000..2b00cf91a37 Binary files /dev/null and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo new file mode 100644 index 00000000000..da51e2a02ed Binary files /dev/null and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index a325a4b773e..4ca146ea331 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo differ diff --git a/Source/DafnyStandardLibraries/examples/FileIO/ReadBytesFromFile.dfy b/Source/DafnyStandardLibraries/examples/FileIO/ReadBytesFromFile.dfy new file mode 100644 index 00000000000..702ce5cfd90 --- /dev/null +++ b/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; + } + } +} diff --git a/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy b/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy new file mode 100644 index 00000000000..2013c447dbb --- /dev/null +++ b/Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy @@ -0,0 +1,56 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module WriteBytesToFile { + import DafnyStdLibs.FileIO + + method {:test} Test() { + // TODO: extern function for the expected error prefix + theMain("build/../build/fileioexamples", ""); + } + + method {:rlimit 2000} theMain(outputDir: string, expectedErrorPrefix: string) { + + // 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: . + // 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 := [ + // "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; + } + } +} diff --git a/Source/DafnyStandardLibraries/examples/FileIO/data.txt b/Source/DafnyStandardLibraries/examples/FileIO/data.txt new file mode 100644 index 00000000000..03acd5d37a3 --- /dev/null +++ b/Source/DafnyStandardLibraries/examples/FileIO/data.txt @@ -0,0 +1,2 @@ +Hello world +Goodbye diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIO-notarget-java-cs-js-go-py.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIO-notarget-java-cs-js-go-py.dfy new file mode 100644 index 00000000000..63395a682cb --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIO-notarget-java-cs-js-go-py.dfy @@ -0,0 +1,50 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/** + * 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. + * + * File path symbols including . and .. are allowed. + */ +module DafnyStdLibs.FileIO { + import opened Wrappers + import FileIOInternalExterns + + 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, string>) { + var isError, bytesRead, errorMsg := FileIOInternalExterns.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) returns (res: Result<(), string>) { + var isError, errorMsg := FileIOInternalExterns.INTERNAL_WriteBytesToFile(path, bytes); + return if isError then Failure(errorMsg) else Success(()); + } +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-go.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-go.dfy new file mode 100644 index 00000000000..bb03f26ba7b --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-go.dfy @@ -0,0 +1,27 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/* + * Private API - these should not be used elsewhere + */ +module +// This attribute isn't strictly necessary because it's possible +// to split the implementation of a Dafny module +// across multiple Go files under the same path. +// But it makes debugging the translated output a little clearer. +{:compile false} +{:extern "DafnyStdLibs_FileIOInternalExterns"} +{:dummyImportMember "INTERNAL__ReadBytesFromFile", false} +DafnyStdLibs.FileIOInternalExterns { + method + {:extern} + INTERNAL_ReadBytesFromFile(path: string) + returns (isError: bool, bytesRead: seq, errorMsg: string) + + method + {:extern} + INTERNAL_WriteBytesToFile(path: string, bytes: seq) + returns (isError: bool, errorMsg: string) +} \ No newline at end of file diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy new file mode 100644 index 00000000000..ee5afc4b546 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy @@ -0,0 +1,19 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/* + * Private API - these should not be used elsewhere + */ +module DafnyStdLibs.FileIOInternalExterns { + method + {:extern "DafnyStdLibsExterns.FileIO", "INTERNAL_ReadBytesFromFile"} + INTERNAL_ReadBytesFromFile(path: string) + returns (isError: bool, bytesRead: seq, errorMsg: string) + + method + {:extern "DafnyStdLibsExterns.FileIO", "INTERNAL_WriteBytesToFile"} + INTERNAL_WriteBytesToFile(path: string, bytes: seq) + returns (isError: bool, errorMsg: string) +} \ No newline at end of file diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy new file mode 100644 index 00000000000..2d883d601e2 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy @@ -0,0 +1,17 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/* + * Private API - these should not be used elsewhere + */ +module DafnyStdLibs.FileIOInternalExterns { + method + INTERNAL_ReadBytesFromFile(path: string) + returns (isError: bool, bytesRead: seq, errorMsg: string) + + method + INTERNAL_WriteBytesToFile(path: string, bytes: seq) + returns (isError: bool, errorMsg: string) +} \ No newline at end of file diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-py.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-py.dfy new file mode 100644 index 00000000000..47f0a9efec9 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-py.dfy @@ -0,0 +1,22 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +/* + * Private API - these should not be used elsewhere + */ +// {:compile false} is necessary here since otherwise the translation to Python +// will create a DafnyStdLibs_FileIOInternalExterns.py source file as well, +// which the embedded version can't easily override. +module {:compile false} DafnyStdLibs.FileIOInternalExterns { + method + {:extern} + INTERNAL_ReadBytesFromFile(path: string) + returns (isError: bool, bytesRead: seq, errorMsg: string) + + method + {:extern} + INTERNAL_WriteBytesToFile(path: string, bytes: seq) + returns (isError: bool, errorMsg: string) +} \ No newline at end of file diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/Makefile b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/Makefile new file mode 100644 index 00000000000..cb0f35989f6 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/Makefile @@ -0,0 +1,43 @@ + +# This Makefile builds the individual DafnyStandardLibraries-.doo +# binary files, containing libraries that are defined differently for +# different target languages. +# Currently this is only FileIO, but the source file naming pattern +# used here should work for others as well. +# DafnyStandardLibraries-notarget is used for non-compiled contexts +# such as `dafny verify`. + +# Invoking the CLI this way just to stay platform-independent +DAFNY = dotnet run --project ../../../../Dafny --no-build -- + +DOO_FILE_SOURCE=../../../build/DafnyStandardLibraries-${TARGETLANG}.doo +DOO_FILE_TARGET=../../../binaries/DafnyStandardLibraries-${TARGETLANG}.doo + +build-binary: + $(DAFNY) build -t:lib dfyconfig.toml \ + `find . -name '*-${TARGETLANG}*.dfy'` \ + --output:${DOO_FILE_SOURCE} + +check-binary: build-binary + unzip -o ${DOO_FILE_SOURCE} -d ../../../build/current-${TARGETLANG} + unzip -o ${DOO_FILE_TARGET} -d ../../../build/rebuilt-${TARGETLANG} + diff ../../../build/current-${TARGETLANG} ../../../build/rebuilt-${TARGETLANG} + +check-binary-all: + make check-binary TARGETLANG=notarget + make check-binary TARGETLANG=cs + make check-binary TARGETLANG=java + make check-binary TARGETLANG=js + make check-binary TARGETLANG=go + make check-binary TARGETLANG=py + +update-binary: build-binary + cp ${DOO_FILE_SOURCE} ${DOO_FILE_TARGET} + +update-binary-all: + make update-binary TARGETLANG=notarget + make update-binary TARGETLANG=cs + make update-binary TARGETLANG=java + make update-binary TARGETLANG=js + make update-binary TARGETLANG=go + make update-binary TARGETLANG=py diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/README.md b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/README.md new file mode 100644 index 00000000000..d92e021c198 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/README.md @@ -0,0 +1,14 @@ +# File I/O + +The `FileIO` module provides basic file I/O operations. +Right now, these are limited to reading bytes from a file, and writing bytes to a file. +The API is intentionally limited in scope and will be expanded later. + +The `examples/FileIO` directory contains more detailed examples of how to use the `FileIO` module. + +Note that because this module is implemented with target-language utilities, +it is only defined for a subset of the Dafny backends: +currently C#, Java, JavaScript, Go and Python. +For other backends, the `FileIO` module is simply not defined, +so attempting to compile code that uses it to them will result +in resolution errors. diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/dfyconfig.toml b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/dfyconfig.toml new file mode 100644 index 00000000000..07ec5a99d80 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/dfyconfig.toml @@ -0,0 +1,22 @@ + +# The Makefile has its own non-trivial logic for determining which files +# to include in which mode. +includes = [] + +[options] +# Options that help support more values of consuming context options +# (mostly turning on any more restrictive verification) +track-print-effects = true +enforce-determinism = true +reads-clauses-on-methods = true + +# Options important for sustainable development +# of the libraries themselves. +resource-limit = 1000 +warn-as-errors = true +warn-redundant-assumptions = true +warn-contradictory-assumptions = true + +library = [ + "../Wrappers.dfy" +] diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.cs b/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.cs new file mode 100644 index 00000000000..d3b59d9710e --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.cs @@ -0,0 +1,94 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +namespace DafnyStdLibsExterns { + using System; + using System.IO; + + using Dafny; + + public class FileIO { + /// + /// Attempts to read all bytes from the file at the given path, and outputs the following values: + /// + /// + /// isError + /// + /// true iff an exception was thrown during path string conversion or when reading the file + /// + /// + /// + /// bytesRead + /// + /// the sequence of bytes read from the file, or an empty sequence if isError is true + /// + /// + /// + /// errorMsg + /// + /// the error message of the thrown exception if isError is true, or an empty sequence otherwise + /// + /// + /// + /// + /// 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. + /// + public static void INTERNAL_ReadBytesFromFile(ISequence path, out bool isError, out ISequence bytesRead, + out ISequence errorMsg) { + isError = true; + bytesRead = Sequence.Empty; + errorMsg = Sequence.Empty; + try { + bytesRead = Helpers.SeqFromArray(File.ReadAllBytes(path?.ToVerbatimString(false))); + isError = false; + } catch (Exception e) { + errorMsg = Sequence.UnicodeFromString(e.ToString()); + } + } + + /// + /// Attempts to write all given bytes to the file at the given path, creating nonexistent parent directories as necessary, + /// and outputs the following values: + /// + /// + /// isError + /// + /// true iff an exception was thrown during path string conversion or when writing to the file + /// + /// + /// + /// errorMsg + /// + /// the error message of the thrown exception if isError is true, or an empty sequence otherwise + /// + /// + /// + /// + /// 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. + /// + public static void INTERNAL_WriteBytesToFile(ISequence path, ISequence bytes, out bool isError, out ISequence errorMsg) { + isError = true; + errorMsg = Sequence.Empty; + try { + string pathStr = path?.ToVerbatimString(false); + CreateParentDirs(pathStr); + File.WriteAllBytes(pathStr, bytes.CloneAsArray()); + isError = false; + } catch (Exception e) { + errorMsg = Sequence.UnicodeFromString(e.ToString()); + } + } + + /// + /// Creates the nonexistent parent directory(-ies) of the given path. + /// + private static void CreateParentDirs(string path) { + string parentDir = Path.GetDirectoryName(Path.GetFullPath(path)); + Directory.CreateDirectory(parentDir); + } + } +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.java b/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.java new file mode 100644 index 00000000000..60f0bb6292e --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.java @@ -0,0 +1,102 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +package DafnyStdLibsExterns; + +import java.io.IOException; +import java.io.PrintWriter; +import java.io.StringWriter; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; + +import dafny.CodePoint; +import dafny.DafnySequence; +import dafny.Tuple2; +import dafny.Tuple3; +import dafny.TypeDescriptor; + +public class FileIO { + /** + * Attempts to read all bytes from the file at {@code path}, and returns a tuple of the following values: + *
+ *
{@code isError}
+ *
true iff an exception was thrown during path string conversion or when reading the file
+ *
{@code bytesRead}
+ *
the sequence of bytes read from the file, or an empty sequence if {@code isError} is true
+ *
{@code errorMsg}
+ *
the error message of the thrown exception if {@code isError} is true, or an empty sequence otherwise
+ *
+ *

+ * We return these values individually because {@code Result} is not defined in the runtime but instead in library code. + * It is the responsibility of library code to construct an equivalent {@code Result} value. + */ + public static Tuple3, DafnySequence> + INTERNAL_ReadBytesFromFile(DafnySequence path) { + try { + final Path pathObj = dafnyStringToPath(path); + final DafnySequence readBytes = DafnySequence.fromBytes(Files.readAllBytes(pathObj)); + return Tuple3.create(false, readBytes, DafnySequence.empty(TypeDescriptor.UNICODE_CHAR)); + } catch (Exception ex) { + return Tuple3.create(true, DafnySequence.empty(TypeDescriptor.BYTE), stackTraceToDafnyString(ex)); + } + } + + /** + * Attempts to write {@code bytes} to the file at {@code path}, creating nonexistent parent directories as necessary, + * and returns a tuple of the following values: + *

+ *
{@code isError}
+ *
true iff an exception was thrown during path string conversion or when writing to the file
+ *
{@code errorMsg}
+ *
the error message of the thrown exception if {@code isError} is true, or an empty sequence otherwise
+ *
+ *

+ * We return these values individually because {@code Result} is not defined in the runtime but instead in library code. + * It is the responsibility of library code to construct an equivalent {@code Result} value. + */ + public static Tuple2> + INTERNAL_WriteBytesToFile(DafnySequence path, DafnySequence bytes) { + try { + final Path pathObj = dafnyStringToPath(path); + createParentDirs(pathObj); + + // It's safe to cast `bytes` to `DafnySequence` since the cast value is immediately consumed + @SuppressWarnings("unchecked") + final byte[] byteArr = DafnySequence.toByteArray((DafnySequence) bytes); + + Files.write(pathObj, byteArr); + return Tuple2.create(false, DafnySequence.empty(TypeDescriptor.UNICODE_CHAR)); + } catch (Exception ex) { + return Tuple2.create(true, stackTraceToDafnyString(ex)); + } + } + + /** + * Returns a Path constructed from the given Dafny string. + */ + private static final Path dafnyStringToPath(final DafnySequence path) { + return Paths.get(path.verbatimString()); + } + + /** + * Creates the nonexistent parent directory(-ies) of the given path. + */ + private static final void createParentDirs(final Path path) throws IOException { + final Path parentDir = path.toAbsolutePath().getParent(); + if (parentDir == null) { + return; + } + Files.createDirectories(parentDir); + } + + private static final DafnySequence stackTraceToDafnyString(final Throwable t) { + final StringWriter stringWriter = new StringWriter(); + final PrintWriter printWriter = new PrintWriter(stringWriter); + t.printStackTrace(printWriter); + final String str = stringWriter.toString(); + return DafnySequence.asUnicodeString(str); + } +} diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.js b/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.js new file mode 100644 index 00000000000..3465ed07259 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.js @@ -0,0 +1,70 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +var DafnyStdLibsExterns = DafnyStdLibsExterns || {}; +DafnyStdLibsExterns.FileIO = (function() { + const buffer = require("buffer"); + const fs = require("fs"); + const nodePath = require("path"); + + let $module = {}; + + /** + * Attempts to read all bytes from the file at the given `path`, and returns an array of the following values: + * + * - `isError`: true iff an error was thrown during path string conversion or when reading the file + * - `bytesRead`: the sequence of bytes from the file, or an empty sequence if `isError` is true + * - `errorMsg`: the error message of the thrown error if `isError` is true, or an empty sequence otherwise + * + * We return 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. + */ + $module.INTERNAL_ReadBytesFromFile = function(path) { + const emptySeq = _dafny.Seq.of(); + try { + const readOpts = { encoding: null }; // read as buffer, not string + const pathStr = path.toVerbatimString(false) + const buf = fs.readFileSync(pathStr, readOpts); + const readBytes = _dafny.Seq.from(buf.valueOf(), byte => new BigNumber(byte)); + return [false, readBytes, emptySeq]; + } catch (e) { + const errorMsg = _dafny.Seq.UnicodeFromString(e.stack); + return [true, emptySeq, errorMsg]; + } + } + + /** + * Attempts to write all given `bytes` to the file at the given `path`, creating nonexistent parent directories as necessary, + * and returns an array of the following values: + * + * - `isError`: true iff an error was thrown during path string conversion or when writing to the file + * - `errorMsg`: the error message of the thrown error if `isError` is true, or an empty sequence otherwise + * + * We return 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. + */ + $module.INTERNAL_WriteBytesToFile = function(path, bytes) { + try { + const buf = buffer.Buffer.from(bytes); + const pathStr = path.toVerbatimString(false) + createParentDirs(pathStr); + fs.writeFileSync(pathStr, buf); // no need to specify encoding because data is a Buffer + return [false, _dafny.Seq.of()]; + } catch (e) { + const errorMsg = _dafny.Seq.from(e.stack); + return [true, errorMsg]; + } + } + + /** + * Creates the nonexistent parent directory(-ies) of the given path. + */ + const createParentDirs = function(path) { + const parentDir = nodePath.dirname(nodePath.normalize(path)); + fs.mkdirSync(parentDir, { recursive: true }); + }; + + return $module; +})(); diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns.py b/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns.py new file mode 100644 index 00000000000..bfb78fb55d9 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns.py @@ -0,0 +1,38 @@ +# Module: DafnyStdLibs_FileIOInternalExterns + +import traceback +import os +import os.path +import pathlib +import _dafny + +class default__: + @staticmethod + def INTERNAL__ReadBytesFromFile(path): + path_str = path.VerbatimString(False) + try: + with open(path_str, mode="rb") as file: + contents = file.read() + contents_seq = _dafny.Seq(contents) + return (False, contents_seq, _dafny.Seq()) + except: + exc_str = traceback.format_exc() + exc_seq = _dafny.Seq(exc_str) + return (True, _dafny.Seq(), exc_seq) + + @staticmethod + def INTERNAL__WriteBytesToFile(path, contents): + path_str = path.VerbatimString(False) + contents_bytes = bytes(contents) + + try: + pathlib.Path(path_str).parent.mkdir(parents=True, exist_ok=True) + + with open(path_str, mode="wb") as file: + contents = file.write(contents_bytes) + return (False, _dafny.Seq()) + except: + exc_str = traceback.format_exc() + exc_seq = _dafny.Seq(exc_str) + return (True, exc_seq) + diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns/DafnyStdLibs_FileIOInternalExterns.go b/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns/DafnyStdLibs_FileIOInternalExterns.go new file mode 100644 index 00000000000..11e794b3f45 --- /dev/null +++ b/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns/DafnyStdLibs_FileIOInternalExterns.go @@ -0,0 +1,33 @@ +package DafnyStdLibs_FileIOInternalExterns + +import ( + _dafny "dafny" + os "os" + filepath "path/filepath" +) + +func INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) { + p := _dafny.SequenceVerbatimString(path, false) + dat, err := os.ReadFile(p) + if err != nil { + errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error()) + return true, _dafny.EmptySeq, errAsSequence + } + datAsSequence := _dafny.SeqOfBytes(dat) + return false, datAsSequence, _dafny.EmptySeq +} + +func INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) { + p := _dafny.SequenceVerbatimString(path, false) + + // Create directories + os.MkdirAll(filepath.Dir(p), os.ModePerm) + + bytesArray := _dafny.ToByteArray(bytes) + err := os.WriteFile(p, bytesArray, 0644) + if err != nil { + errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error()) + return true, errAsSequence + } + return false, _dafny.EmptySeq +} diff --git a/Source/DafnyStandardLibraries/src/dfyconfig.toml b/Source/DafnyStandardLibraries/src/dfyconfig.toml index 04205750646..f5178c20475 100644 --- a/Source/DafnyStandardLibraries/src/dfyconfig.toml +++ b/Source/DafnyStandardLibraries/src/dfyconfig.toml @@ -1,6 +1,11 @@ -# *Nonlinear.dfy in Arithmetic/Internals/ are subject to the options here -excludes = ["**/Arithmetic/*.dfy", "**/Arithmetic/**/*Internals.dfy"] + +excludes = [ + # *Nonlinear.dfy in Arithmetic/Internals/ are subject to the options here + "**/Arithmetic/*.dfy", "**/Arithmetic/**/*Internals.dfy", + # Built per-target language instead + "**/TargetSpecific/*.dfy" +] [options] # Options that help support more values of consuming context options diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect index c06276e5700..b605c419f6d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect @@ -4,6 +4,7 @@ Dafny program verifier finished with 1 verified, 0 errors Dafny program verifier finished with 1 verified, 0 errors StandardLibraries_Errors.dfy(20,29): Error: module DafnyStdLibs does not exist (position 0 in path DafnyStdLibs.Wrappers) 1 resolution/type errors detected in StandardLibraries_Errors.dfy -*** Error: Cannot load DafnyStandardLibraries.doo: --unicode-char is set locally to False, but the library was built with True +*** Error: Cannot load DafnyStandardLibraries-notarget.doo: --unicode-char is set locally to False, but the library was built with True +Please use the '--check' and/or '--print' option as doo files cannot be formatted in place. Please use the '--check' and/or '--print' option as doo files cannot be formatted in place. Please use the '--check' and/or '--print' option as doo files cannot be formatted in place. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy new file mode 100644 index 00000000000..eecb3119553 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy @@ -0,0 +1,10 @@ +// This test just asserts what happens when you try to use a library +// that isn't available for all backends (see .check files). +// Full testing of such libraries is handled in the DafnyStandardLibraries +// project rather than here. + +// RUN: %testDafnyForEachCompiler "%s" -- --standard-libraries:true + +module UsesFileIO { + import DafnyStdLibs.FileIO +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.cpp.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.cpp.check new file mode 100644 index 00000000000..73c3a21186e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.cpp.check @@ -0,0 +1 @@ +CHECK-L: StandardLibraries_TargetSpecific.dfy(9,22): Error: module FileIO does not exist (position 1 in path DafnyStdLibs.FileIO) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.dfy.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.dfy.check new file mode 100644 index 00000000000..73c3a21186e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.dfy.check @@ -0,0 +1 @@ +CHECK-L: StandardLibraries_TargetSpecific.dfy(9,22): Error: module FileIO does not exist (position 1 in path DafnyStdLibs.FileIO) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.expect new file mode 100644 index 00000000000..e69de29bb2d diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.rs.check new file mode 100644 index 00000000000..73c3a21186e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_TargetSpecific.dfy.rs.check @@ -0,0 +1 @@ +CHECK-L: StandardLibraries_TargetSpecific.dfy(9,22): Error: module FileIO does not exist (position 1 in path DafnyStdLibs.FileIO)