Standard lib support in dafny server

Source/DafnyCore/AST/Grammar/IFileSystem.cs

@@ -1,5 +1,9 @@
 using System;
+using System.Collections.Generic;
 using System.IO;
+using System.Linq;
+using DafnyCore.Options;
+using Microsoft.Dafny.LanguageServer.Workspace;
 using Microsoft.Extensions.FileSystemGlobbing.Abstractions;
 
 namespace Microsoft.Dafny;
@@ -11,6 +15,32 @@ public interface IFileSystem {
  DirectoryInfoBase GetDirectoryInfoBase(string root);
 }
 
+public class InMemoryFileSystem : IFileSystem {
+ private readonly IReadOnlyDictionary<Uri, string> files;
+
+ public InMemoryFileSystem(IReadOnlyDictionary<Uri, string> files) {
+ this.files = files;
+ }
+
+ public TextReader ReadFile(Uri uri) {
+ if (files.TryGetValue(uri, out var entry)) {
+ return new StringReader(entry);
+ }
+
+ return OnDiskFileSystem.Instance.ReadFile(uri);
+ }
+
+ public bool Exists(Uri path) {
+ return files.ContainsKey(path) || OnDiskFileSystem.Instance.Exists(path);
+ }
+
+ public DirectoryInfoBase GetDirectoryInfoBase(string root) {
+ var inMemoryFiles = files.Keys.Select(openFileUri => openFileUri.LocalPath);
+ var inMemory = new InMemoryDirectoryInfoFromDotNet8(root, inMemoryFiles);
+ return new CombinedDirectoryInfo(new[] { inMemory, OnDiskFileSystem.Instance.GetDirectoryInfoBase(root) });
+ }
+}
+
 public class OnDiskFileSystem : IFileSystem {
  public static readonly IFileSystem Instance = new OnDiskFileSystem();
 

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -1,5 +1,6 @@
 using System;
 using System.Collections.Generic;
+using System.Collections.Immutable;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
@@ -255,14 +256,7 @@ CancellationToken cancellationToken
  }
 
  private DafnyFile IncludeToDafnyFile(SystemModuleManager systemModuleManager, ErrorReporter errorReporter, Include include) {
- try {
- return new DafnyFile(systemModuleManager.Options, include.IncludedFilename, include.tok,
- () => fileSystem.ReadFile(include.IncludedFilename));
- } catch (IllegalDafnyFile) {
- errorReporter.Error(MessageSource.Parser, include.tok,
- $"Unable to open the include {include.IncludedFilename}.");
- return null;
- }
+ return DafnyFile.CreateAndValidate(errorReporter, fileSystem, systemModuleManager.Options, include.IncludedFilename, include.tok);
  }
 
  ///<summary>
@@ -317,7 +311,9 @@ private static Parser SetupParser(bool parseAsDooFile, string s /*!*/, Uri uri /
  }
 
  public Program Parse(string source, Uri uri, ErrorReporter reporter) {
- var files = new[] { new DafnyFile(reporter.Options, uri, null, () => new StringReader(source)) };
+ var fs = new InMemoryFileSystem(ImmutableDictionary<Uri, string>.Empty.Add(uri, source));
+ var file = DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken);
+ var files = file == null ? Array.Empty<DafnyFile>() : new[] { file };
  return ParseFiles(uri.ToString(), files, reporter, CancellationToken.None);
  }
 }

Source/DafnyCore/AST/Tokens.cs

@@ -57,6 +57,7 @@ public class Token : IToken {
 
  public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normally null at the end of parsing
  public static readonly Token NoToken = new Token();
+ public static readonly Token Cli = new Token();
  public Token() : this(0, 0) { }
 
  public Token(int linenum, int colnum) {
@@ -193,6 +194,10 @@ public int CompareTo(IToken other) {
 public static class TokenExtensions {
 
  public static string TokenToString(this IToken tok, DafnyOptions options) {
+ if (tok == Token.Cli) {
+ return "CLI";
+ }
+
  if (tok.Uri == null) {
  return $"({tok.line},{tok.col - 1})";
  }

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -68,7 +68,8 @@ private string GetFileLine(Uri uri, int lineIndex) {
  try {
  // Note: This is not guaranteed to be the same file that Dafny parsed. To ensure that, Dafny should keep
  // an in-memory version of each file it parses.
- var reader = new DafnyFile(options, uri).GetContent();
+ var file = DafnyFile.CreateAndValidate(new ErrorReporterSink(options), OnDiskFileSystem.Instance, options, uri, Token.NoToken);
+ var reader = file.GetContent();
  lines = Util.Lines(reader).ToList();
  } catch (Exception) {
  lines = new List<string>();

Source/DafnyCore/DafnyFile.cs

@@ -10,9 +10,9 @@
 namespace Microsoft.Dafny;
 
 public class DafnyFile {
- public string FilePath { get; private set; }
+ public string FilePath => CanonicalPath;
  public string Extension { get; private set; }
- public string CanonicalPath { get; private set; }
+ public string CanonicalPath { get; }
  public string BaseName { get; private set; }
  public bool IsPreverified { get; set; }
  public bool IsPrecompiled { get; set; }
@@ -21,56 +21,62 @@ public class DafnyFile {
  public Uri Uri { get; }
  [CanBeNull] public IToken Origin { get; }
 
- public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null, Func<TextReader> getContentOverride = null) {
- Uri = uri;
- Origin = origin;
+ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
+ DafnyOptions options, Uri uri, IToken origin) {
  var filePath = uri.LocalPath;
 
- Extension = ".dfy";
+ origin ??= Token.NoToken;
+
+ string canonicalPath;
+ string baseName;
+ Func<TextReader> getContent = null;
+ bool isPreverified;
+ bool isPrecompiled;
+ var isPrerefined = false;
+ var extension = ".dfy";
  if (uri.IsFile) {
- Extension = Path.GetExtension(uri.LocalPath).ToLower();
- BaseName = Path.GetFileName(uri.LocalPath);
+ extension = Path.GetExtension(uri.LocalPath).ToLower();
+ baseName = Path.GetFileName(uri.LocalPath);
  // 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;
+ canonicalPath = Canonicalize(filePath).LocalPath;
  } else if (uri.Scheme == "stdin") {
- getContentOverride = () => options.Input;
- BaseName = "<stdin>";
- CanonicalPath = "<stdin>";
+ getContent = () => options.Input;
+ baseName = "<stdin>";
+ canonicalPath = "<stdin>";
  } else if (uri.Scheme == "dllresource") {
- Extension = Path.GetExtension(uri.LocalPath).ToLower();
- BaseName = uri.LocalPath;
- CanonicalPath = uri.ToString();
+ extension = Path.GetExtension(uri.LocalPath).ToLower();
+ baseName = uri.LocalPath;
+ canonicalPath = uri.ToString();
+ } else {
+ canonicalPath = "";
+ baseName = "";
  }
 
- 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") {
- IsPreverified = false;
- IsPrecompiled = false;
- if (!File.Exists(filePath)) {
+ if (getContent != null) {
+ isPreverified = false;
+ isPrecompiled = false;
+ } else if (uri.Scheme == "untitled" || extension == ".dfy" || extension == ".dfyi") {
+ isPreverified = false;
+ isPrecompiled = false;
+ if (!fileSystem.Exists(uri)) {
  if (0 < options.VerifySnapshots) {
  // For snapshots, we first create broken DafnyFile without content,
  // then look for the real files and create DafnuFiles for them.
- // TODO prevent creating the broken DafnyFiles for snapshots
- return;
+ return new DafnyFile(extension, canonicalPath, baseName, null, uri, origin);
  }
 
- options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
- throw new IllegalDafnyFile(true);
- } else {
- GetContent = () => new StreamReader(filePath);
+ reporter.Error(MessageSource.Project, origin, $"file {filePathForErrors} not found");
+ return null;
  }
- } else if (Extension == ".doo") {
- IsPreverified = true;
- IsPrecompiled = false;
+
+ getContent = () => fileSystem.ReadFile(uri);
+ } else if (extension == ".doo") {
+ isPreverified = true;
+ isPrecompiled = false;
 
  DooFile dooFile;
  if (uri.Scheme == "dllresource") {
@@ -84,16 +90,16 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
 
  dooFile = DooFile.Read(stream);
  } else {
- if (!File.Exists(filePath)) {
- options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found");
- throw new IllegalDafnyFile(true);
+ if (!fileSystem.Exists(uri)) {
+ reporter.Error(MessageSource.Project, origin, $"file {filePathForErrors} not found");
+ return null;
  }
 
  dooFile = DooFile.Read(filePath);
  }
 
- if (!dooFile.Validate(filePathForErrors, options, options.CurrentCommand)) {
- throw new IllegalDafnyFile(true);
+ if (!dooFile.Validate(reporter, filePathForErrors, options, options.CurrentCommand, origin)) {
+ return null;
  }
 
  // For now it's simpler to let the rest of the pipeline parse the
@@ -102,19 +108,37 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
  // more efficiently inside a .doo file, at which point
  // the DooFile class should encapsulate the serialization logic better
  // and expose a Program instead of the program text.
- GetContent = () => new StringReader(dooFile.ProgramText);
- IsPrerefined = true;
- } else if (Extension == ".dll") {
- IsPreverified = true;
+ getContent = () => new StringReader(dooFile.ProgramText);
+ isPrerefined = true;
+ } else if (extension == ".dll") {
+ isPreverified = true;
  // Technically only for C#, this is for backwards compatability
- IsPrecompiled = true;
+ isPrecompiled = true;
 
  var sourceText = GetDafnySourceAttributeText(filePath);
- if (sourceText == null) { throw new IllegalDafnyFile(); }
- GetContent = () => new StringReader(sourceText);
+ if (sourceText == null) {
+ return null;
+ }
+ getContent = () => new StringReader(sourceText);
  } else {
- throw new IllegalDafnyFile();
+ return null;
  }
+
+ return new DafnyFile(extension, canonicalPath, baseName, getContent, uri, origin) {
+ IsPrecompiled = isPrecompiled,
+ IsPreverified = isPreverified,
+ IsPrerefined = isPrerefined
+ };
+ }
+
+ protected DafnyFile(string extension, string canonicalPath, string baseName,
+ Func<TextReader> getContent, Uri uri, [CanBeNull] IToken origin) {
+ Extension = extension;
+ CanonicalPath = canonicalPath;
+ BaseName = baseName;
+ GetContent = getContent;
+ Uri = uri;
+ Origin = origin;
  }
 
  // Returns a canonical string for the given file path, namely one which is the same
@@ -155,7 +179,7 @@ public static List<string> FileNames(IReadOnlyList<DafnyFile> dafnyFiles) {
 
  private static string GetDafnySourceAttributeText(string dllPath) {
  if (!File.Exists(dllPath)) {
- throw new IllegalDafnyFile();
+ return null;
  }
  using var dllFs = new FileStream(dllPath, FileMode.Open, FileAccess.Read, FileShare.ReadWrite);
  using var dllPeReader = new PEReader(dllFs);

Source/DafnyCore/DafnyMain.cs

@@ -21,15 +21,10 @@
 
 namespace Microsoft.Dafny {
 
- public class IllegalDafnyFile : Exception {
- public bool ProcessingError { get; }
-
- public IllegalDafnyFile(bool processingError = false) {
- this.ProcessingError = processingError;
- }
- }
-
  public class DafnyMain {
+ public static readonly string StandardLibrariesDooUriBase = "dllresource://DafnyPipeline/DafnyStandardLibraries";
+ public static readonly Uri StandardLibrariesDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries.doo");
+ public static readonly Uri StandardLibrariesArithmeticDooUri = new("dllresource://DafnyPipeline/DafnyStandardLibraries-arithmetic.doo");
 
  public static void MaybePrintProgram(Program program, string filename, bool afterResolver) {
  if (filename == null) {

Source/DafnyCore/DooFile.cs

@@ -116,14 +116,17 @@ public DooFile(Program dafnyProgram) {
  private DooFile() {
  }
 
- public bool Validate(string filePath, DafnyOptions options, Command currentCommand) {
+ public bool Validate(ErrorReporter reporter, string filePath, DafnyOptions options, Command currentCommand,
+ IToken origin) {
  if (currentCommand == null) {
- options.Printer.ErrorWriteLine(Console.Out, $"Cannot load {filePath}: .doo files cannot be used with the legacy CLI");
+ reporter.Error(MessageSource.Project, origin,
+ $"Cannot load {filePath}: .doo files cannot be used with the legacy CLI");
  return false;
  }
 
  if (options.VersionNumber != Manifest.DafnyVersion) {
- options.Printer.ErrorWriteLine(Console.Out, $"Cannot load {filePath}: it was built with Dafny {Manifest.DafnyVersion}, which cannot be used by Dafny {options.VersionNumber}");
+ reporter.Error(MessageSource.Project, origin,
+ $"cannot load {filePath}: it was built with Dafny {Manifest.DafnyVersion}, which cannot be used by Dafny {options.VersionNumber}");
  return false;
  }
 
@@ -141,15 +144,15 @@ public bool Validate(string filePath, DafnyOptions options, Command currentComma
 
  object libraryValue = null;
  if (Manifest.Options.TryGetValue(option.Name, out var manifestValue)) {
- if (!TomlUtil.TryGetValueFromToml(Console.Out, null,
+ if (!TomlUtil.TryGetValueFromToml(reporter, origin, null,
  option.Name, option.ValueType, manifestValue, out libraryValue)) {
  return false;
  }
  } else if (option.ValueType == typeof(IEnumerable<string>)) {
  // This can happen because Tomlyn will drop aggregate properties with no values.
  libraryValue = Array.Empty<string>();
  }
- success = success && check(options, option, localValue, filePath, libraryValue);
+ success = success && check(reporter, origin, option, localValue, filePath, libraryValue);
  }
  return success;
  }
@@ -208,40 +211,39 @@ public void Write(string path) {
  // more difficult to completely categorize, which is the main reason the LibraryBackend
  // is restricted to only the new CLI.
 
- public delegate bool OptionCheck(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue);
+ public delegate bool OptionCheck(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue);
  private static readonly Dictionary<Option, OptionCheck> OptionChecks = new();
  private static readonly HashSet<Option> NoChecksNeeded = new();
 
- public static bool CheckOptionMatches(DafnyOptions options, Option option, object localValue, string libraryFile, object libraryValue) {
+ public static bool CheckOptionMatches(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
  if (OptionValuesEqual(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)}");
+ reporter.Error(MessageSource.Project, origin, $"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 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) {
+ public static bool CheckOptionLibraryImpliesLocal(ErrorReporter reporter, IToken origin, 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)}");
+ reporter.Error(MessageSource.Project, origin, $"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) {
+ public static bool CheckOptionLocalImpliesLibrary(ErrorReporter reporter, IToken origin, 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)}");
+ reporter.Error(MessageSource.Project, origin, $"cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
  return false;
  }