feat: Standard library support + DafnyStdLibs.Wrappers

.github/workflows/standard-libraries.yml

@@ -0,0 +1,37 @@
+name: Build and Test Dafny Standard Libraries
+
+on:
+ workflow_dispatch:
+ pull_request:
+ branches: [ master, main-* ]
+
+concurrency:
+ group: ${{ github.workflow }}-${{ github.ref }}
+ cancel-in-progress: true
+
+jobs:
+ check-deep-tests:
+ uses: ./.github/workflows/check-deep-tests-reusable.yml
+
+ build:
+ needs: check-deep-tests
+ runs-on: ubuntu-latest
+
+ steps:
+ - name: Checkout Dafny
+ uses: actions/checkout@v3
+ with:
+ submodules: true
+ - name: Set up JDK 18
+ uses: actions/setup-java@v3
+ with:
+ java-version: 18
+ distribution: corretto
+ - name: Build Dafny
+ run: dotnet build Source/Dafny.sln
+ - name: Get Z3
+ run: make z3-ubuntu
+ - run: npm install bignumber.js
+ - name: Test DafnyStandardLibraries
+ run: make -C Source/DafnyStandardLibraries all
+

.gitignore

@@ -58,6 +58,9 @@ Source/.vs
 # Generated by VS Code
 .vscode/*
 
+# Generated by Dafny tooling
+/Source/DafnyStandardLibraries/build
+
 # Generated by Java tools (gradle/javac/etc)
 
 /Source/DafnyRuntime/DafnyRuntimeJava/.gradle
@@ -70,3 +73,5 @@ package-lock.json
 docs/dev/*.fix
 docs/dev/*.feat
 docs/dev/*.break
+
+

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -1236,6 +1236,7 @@ public void PrintStatement(Statement stmt, int indent) {
  } else if (expectStmt != null && expectStmt.Message != null) {
  wr.Write(", ");
  PrintExpression(expectStmt.Message, true);
+ wr.Write(";");
  } else {
  wr.Write(";");
  }

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -35,11 +35,12 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
  CancellationToken cancellationToken) {
  var options = errorReporter.Options;
  var builtIns = new SystemModuleManager(options);
- var defaultModule = new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList());
+ var defaultModule = new DefaultModuleDefinition();
 
+ var rootSourceUris = files.Select(f => f.Uri).ToList();
  var verifiedRoots = files.Where(df => df.IsPreverified).Select(df => df.Uri).ToHashSet();
  var compiledRoots = files.Where(df => df.IsPrecompiled).Select(df => df.Uri).ToHashSet();
- var compilation = new CompilationData(errorReporter, defaultModule.Includes, defaultModule.RootSourceUris, verifiedRoots,
+ var compilation = new CompilationData(errorReporter, defaultModule.Includes, rootSourceUris, verifiedRoots,
  compiledRoots);
  var program = new Program(
  programName,

Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs

@@ -6,16 +6,13 @@ namespace Microsoft.Dafny;
 
 public class DefaultModuleDefinition : ModuleDefinition, ICloneable<DefaultModuleDefinition> {
  public List<Include> Includes { get; } = new();
- public IList<Uri> RootSourceUris { get; }
 
  public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original) : base(cloner, original, original.NameNode) {
- RootSourceUris = original.RootSourceUris;
  }
 
- public DefaultModuleDefinition(IList<Uri> rootSourceUris)
+ public DefaultModuleDefinition()
  : base(RangeToken.NoToken, new Name("_module"), new List<IToken>(), false, false,
  null, null, null) {
- RootSourceUris = rootSourceUris;
  }
 
  public override bool IsDefaultModule => true;

Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs

@@ -18,7 +18,7 @@ static PrintStmt() {
 
  DooFile.RegisterLibraryChecks(
  checks: new Dictionary<Option, DooFile.OptionCheck> {
- { TrackPrintEffectsOption, DooFile.CheckOptionMatches }
+ { TrackPrintEffectsOption, DooFile.CheckOptionLocalImpliesLibrary }
  });
  }
 

Source/DafnyCore/Compilers/Library/LibraryBackend.cs

@@ -31,6 +31,9 @@ public override string TargetBaseDir(string dafnyProgramName) =>
  Feature.LegacyCLI
  };
 
+ // Necessary since Compiler is null
+ public override string ModuleSeparator => ".";
+
  protected override SinglePassCompiler CreateCompiler() {
  return null;
  }

Source/DafnyCore/DafnyFile.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.IO;
+using System.Reflection;
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
 using DafnyCore;
@@ -10,6 +11,7 @@ namespace Microsoft.Dafny;
 
 public class DafnyFile {
  public string FilePath { get; private set; }
+ public string Extension { get; private set; }
  public string CanonicalPath { get; private set; }
  public string BaseName { get; private set; }
  public bool IsPreverified { get; set; }
@@ -23,29 +25,33 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
  Origin = origin;
  var filePath = uri.LocalPath;
 
- var extension = ".dfy";
+ Extension = ".dfy";
  if (uri.IsFile) {
- extension = Path.GetExtension(uri.LocalPath).ToLower();
+ Extension = Path.GetExtension(uri.LocalPath).ToLower();
  BaseName = Path.GetFileName(uri.LocalPath);
- }
- if (uri.Scheme == "stdin") {
+ // Normalizing symbolic links appears to be not
+ // supported in .Net APIs, because it is very difficult in general
+ // So we will just use the absolute path, lowercased for all file systems.
+ // cf. IncludeComparer.CompareTo
+ CanonicalPath = Canonicalize(filePath).LocalPath;
+ } else if (uri.Scheme == "stdin") {
  getContentOverride = () => options.Input;
  BaseName = "<stdin>";
+ CanonicalPath = "<stdin>";
+ } else if (uri.Scheme == "dllresource") {
+ Extension = Path.GetExtension(uri.LocalPath).ToLower();
+ BaseName = uri.LocalPath;
+ CanonicalPath = uri.ToString();
  }
 
- // Normalizing symbolic links appears to be not
- // supported in .Net APIs, because it is very difficult in general
- // So we will just use the absolute path, lowercased for all file systems.
- // cf. IncludeComparer.CompareTo
- CanonicalPath = getContentOverride == null ? Canonicalize(filePath).LocalPath : "<stdin>";
  FilePath = CanonicalPath;
 
  var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath;
  if (getContentOverride != null) {
  IsPreverified = false;
  IsPrecompiled = false;
  GetContent = getContentOverride;
- } else if (extension == ".dfy" || extension == ".dfyi") {
+ } else if (Extension == ".dfy" || Extension == ".dfyi") {
  IsPreverified = false;
  IsPrecompiled = false;
  if (!File.Exists(filePath)) {
@@ -61,15 +67,30 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
  } else {
  GetContent = () => new StreamReader(filePath);
  }
- } else if (extension == ".doo") {
+ } else if (Extension == ".doo") {
  IsPreverified = true;
  IsPrecompiled = false;
 
- if (!File.Exists(filePath)) {
- options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
- throw new IllegalDafnyFile(true);
+ DooFile dooFile;
+ if (uri.Scheme == "dllresource") {
+ var assembly = Assembly.Load(uri.Host);
+ // Skip the leading "/"
+ var resourceName = uri.LocalPath[1..];
+ using var stream = assembly.GetManifestResourceStream(resourceName);
+ if (stream is null) {
+ throw new Exception($"Cannot find embedded resource: {resourceName}");
+ }
+
+ dooFile = DooFile.Read(stream);
+ } else {
+ if (!File.Exists(filePath)) {
+ options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
+ throw new IllegalDafnyFile(true);
+ }
+
+ dooFile = DooFile.Read(filePath);
  }
- var dooFile = DooFile.Read(filePath);
+
  if (!dooFile.Validate(filePathForErrors, options, options.CurrentCommand)) {
  throw new IllegalDafnyFile(true);
  }
@@ -81,7 +102,7 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
  // the DooFile class should encapsulate the serialization logic better
  // and expose a Program instead of the program text.
  GetContent = () => new StringReader(dooFile.ProgramText);
- } else if (extension == ".dll") {
+ } else if (Extension == ".dll") {
  IsPreverified = true;
  // Technically only for C#, this is for backwards compatability
  IsPrecompiled = true;

Source/DafnyCore/DooFile.cs

@@ -69,9 +69,18 @@ public void Write(TextWriter writer) {
  private static DafnyOptions ProgramSerializationOptions => DafnyOptions.Default;
 
  public static DooFile Read(string path) {
+ using var archive = ZipFile.Open(path, ZipArchiveMode.Read);
+ return Read(archive);
+ }
+
+ public static DooFile Read(Stream stream) {
+ using var archive = new ZipArchive(stream);
+ return Read(archive);
+ }
+
+ private static DooFile Read(ZipArchive archive) {
  var result = new DooFile();
 
- using var archive = ZipFile.Open(path, ZipArchiveMode.Read);
  var manifestEntry = archive.GetEntry(ManifestFileEntry);
  if (manifestEntry == null) {
  throw new ArgumentException(".doo file missing manifest entry");
@@ -119,12 +128,12 @@ public bool Validate(string filePath, DafnyOptions options, Command currentComma
  }
 
  var success = true;
- var revelantOptions = currentCommand.Options.ToHashSet();
+ var relevantOptions = currentCommand.Options.ToHashSet();
  foreach (var (option, check) in OptionChecks) {
  // It's important to only look at the options the current command uses,
  // because other options won't be initialized to the correct default value.
  // See CommandRegistry.Create().
- if (!revelantOptions.Contains(option)) {
+ if (!relevantOptions.Contains(option)) {
  continue;
  }
 
@@ -212,6 +221,30 @@ public static bool CheckOptionMatches(DafnyOptions options, Option option, objec
  return false;
  }
 
+ /// Checks that the library option ==> the local option.
+ /// E.g. --no-verify: the only incompatibility is if it's on in the library but not locally.
+ /// Generally the right check for options that weaken guarantees.
+ public static bool CheckOptionLibraryImpliesLocal(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue) {
+ if (OptionValuesImplied(option, libraryValue, localValue)) {
+ return true;
+ }
+
+ options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: Cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
+ return false;
+ }
+
+ /// Checks that the local option ==> the library option.
+ /// E.g. --track-print-effects: the only incompatibility is if it's on locally but not in the library.
+ /// Generally the right check for options that strengthen guarantees.
+ public static bool CheckOptionLocalImpliesLibrary(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue) {
+ if (OptionValuesImplied(option, localValue, libraryValue)) {
+ return true;
+ }
+
+ options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: Cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
+ return false;
+ }
+
  private static bool OptionValuesEqual(Option option, object first, object second) {
  if (first.Equals(second)) {
  return true;
@@ -224,6 +257,12 @@ private static bool OptionValuesEqual(Option option, object first, object second
  return false;
  }
 
+ private static bool OptionValuesImplied(Option option, object first, object second) {
+ var lhs = (bool)first;
+ var rhs = (bool)second;
+ return !lhs || rhs;
+ }
+
  private static string OptionValueToString(Option option, object value) {
  if (option.ValueType == typeof(IEnumerable<string>)) {
  var values = (IEnumerable<string>)value;

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -136,7 +136,7 @@ static BoogieOptionBag() {
  new Dictionary<Option, DooFile.OptionCheck> {
  { BoogieArguments, DooFile.CheckOptionMatches },
  { BoogieFilter, DooFile.CheckOptionMatches },
- { NoVerify, DooFile.CheckOptionMatches },
+ { NoVerify, DooFile.CheckOptionLibraryImpliesLocal },
  }
  );
  DooFile.RegisterNoChecksNeeded(

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -258,6 +258,13 @@ public enum DefaultFunctionOpacityOptions {
 `opaque` means functions are always opaque so the opaque keyword is not needed, and functions must be revealed everywhere needed for a proof.".TrimStart()) {
  };
 
+ public static readonly Option<bool> UseStandardLibraries = new("--standard-libraries", () => false,
+ @"
+Allow Dafny code to depend on the standard libraries included with the Dafny distribution.
+See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for more information.
+Not compatible with the --unicode-char:false option.
+");
+
  static CommonOptionBag() {
  DafnyOptions.RegisterLegacyUi(Target, DafnyOptions.ParseString, "Compilation options", "compileTarget", @"
 cs (default) - Compile to .NET via C#.
@@ -438,18 +445,9 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
  DooFile.RegisterLibraryChecks(
  new Dictionary<Option, DooFile.OptionCheck>() {
  { UnicodeCharacters, DooFile.CheckOptionMatches },
- { EnforceDeterminism, DooFile.CheckOptionMatches },
- { RelaxDefiniteAssignment, DooFile.CheckOptionMatches },
- // Ideally this feature shouldn't affect separate compilation,
- // because it's automatically disabled on {:extern} signatures.
- // Realistically though, we don't have enough strong mechanisms to stop
- // target language code from referencing compiled internal code,
- // so to be conservative we flag this as not compatible in general.
- { OptimizeErasableDatatypeWrapper, DooFile.CheckOptionMatches },
- // Similarly this shouldn't matter if external code ONLY refers to {:extern}s,
- // but in practice it does.
- { AddCompileSuffix, DooFile.CheckOptionMatches },
- { ReadsClausesOnMethods, DooFile.CheckOptionMatches },
+ { EnforceDeterminism, DooFile.CheckOptionLocalImpliesLibrary },
+ { RelaxDefiniteAssignment, DooFile.CheckOptionLibraryImpliesLocal },
+ { ReadsClausesOnMethods, DooFile.CheckOptionLocalImpliesLibrary },
  }
  );
  DooFile.RegisterNoChecksNeeded(
@@ -485,7 +483,10 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
  WarnRedundantAssumptions,
  VerificationCoverageReport,
  NoTimeStampForCoverageReport,
- DefaultFunctionOpacity
+ DefaultFunctionOpacity,
+ UseStandardLibraries,
+ OptimizeErasableDatatypeWrapper,
+ AddCompileSuffix
  );
  }
 

Source/DafnyCore/Options/DafnyCommands.cs

@@ -85,7 +85,8 @@ static DafnyCommands() {
  CommonOptionBag.TypeSystemRefresh,
  CommonOptionBag.TypeInferenceDebug,
  CommonOptionBag.NewTypeInferenceDebug,
- CommonOptionBag.ReadsClausesOnMethods
+ CommonOptionBag.ReadsClausesOnMethods,
+ CommonOptionBag.UseStandardLibraries
  });
 
  public static IReadOnlyList<Option> ResolverOptions = new List<Option>(new Option[] {

Source/DafnyDriver/Commands/DafnyCli.cs

@@ -31,6 +31,8 @@ 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 Uri StandardLibrariesDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries.doo");
+
  public static int Main(string[] args) {
  return MainWithWriters(Console.Out, Console.Error, Console.In, args);
  }
@@ -481,6 +483,14 @@ public static ExitValue GetDafnyFiles(DafnyOptions options,
  return ExitValue.PREPROCESSING_ERROR;
  }
 
+ // Add standard library .doo files after explicitly provided source files,
+ // 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)) {
+ options.CliRootSourceUris.Add(StandardLibrariesDooUri);
+ dafnyFiles.Add(new DafnyFile(options, StandardLibrariesDooUri));
+ }
+
  return ExitValue.SUCCESS;
  }