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);
+ var files = file == null ? Array.Empty<DafnyFile>() : new[] { file };
  return ParseFiles(uri.ToString(), files, reporter, CancellationToken.None);
  }
 }

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);
+ 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,63 @@ 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, [CanBeNull] IToken origin = null) {
  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 null;
  }
 
- 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 +91,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 +109,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 +180,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,9 @@
 
 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 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,7 +144,7 @@ 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;
  }

Source/DafnyLanguageServer/Workspace/CombinedDirectoryInfo.cs → Source/DafnyCore/Generic/CombinedDirectoryInfo.cs

@@ -1,3 +1,4 @@
+#nullable enable
 using System;
 using System.Collections.Generic;
 using System.IO;
@@ -11,7 +12,7 @@ namespace Microsoft.Dafny.LanguageServer.Workspace;
 /// The order in which the filesystems are given matters,
 /// when multiple filesystem contain the same file, the first containing filesystem returns it.
 /// </summary>
-class CombinedDirectoryInfo : DirectoryInfoBase {
+public class CombinedDirectoryInfo : DirectoryInfoBase {
  public DirectoryInfoBase[] Parts { get; }
 
  public CombinedDirectoryInfo(DirectoryInfoBase[] parts) {

Source/DafnyCore/Generic/Reporting.cs

@@ -13,7 +13,7 @@ public enum ErrorLevel {
  }
 
  public enum MessageSource {
- Parser, Cloner, RefinementTransformer, Rewriter, Resolver, Translator, Verifier, Compiler, Documentation, TestGeneration
+ Project, Parser, Cloner, RefinementTransformer, Rewriter, Resolver, Translator, Verifier, Compiler, Documentation, TestGeneration
  }
 
  public record DafnyRelatedInformation(IToken Token, string Message);

Source/DafnyCore/Generic/TomlUtil.cs

@@ -2,23 +2,26 @@
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
+using Microsoft.Dafny;
 using Tomlyn.Model;
+using Type = System.Type;
 
 namespace DafnyCore.Generic;
 
 public static class TomlUtil {
 
- public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir, string tomlPath, Type type, object tomlValue, out object value) {
+ public static bool TryGetValueFromToml(ErrorReporter reporter, IToken origin, string sourceDir, string tomlPath,
+ Type type, object tomlValue, out object value) {
  if (tomlValue == null) {
  value = null;
  return false;
  }
 
  if (type.IsAssignableFrom(typeof(List<string>))) {
- return TryGetListValueFromToml<string>(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
+ return TryGetListValueFromToml<string>(reporter, origin, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
  }
  if (type.IsAssignableFrom(typeof(List<FileInfo>))) {
- return TryGetListValueFromToml<FileInfo>(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
+ return TryGetListValueFromToml<FileInfo>(reporter, origin, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
  }
 
  if (tomlValue is string tomlString) {
@@ -46,8 +49,7 @@ public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir,
  value = tomlValue.ToString();
  return true;
  }
- errorWriter.WriteLine(
- $"Error: property '{tomlPath}' is of type '{tomlValue.GetType()}' but should be of type '{type}'");
+ reporter.Error(MessageSource.Project, origin, $"property '{tomlPath}' is of type '{tomlValue.GetType()}' but should be of type '{type}'");
  value = null;
  return false;
  }
@@ -56,10 +58,10 @@ public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir,
  return true;
  }
 
- private static bool TryGetListValueFromToml<T>(TextWriter errorWriter, string sourceDir, string tomlPath, TomlArray tomlValue, out object value) {
+ private static bool TryGetListValueFromToml<T>(ErrorReporter reporter, IToken origin, string sourceDir, string tomlPath, TomlArray tomlValue, out object value) {
  var success = true;
  value = tomlValue.Select((e, i) => {
- if (TryGetValueFromToml(errorWriter, sourceDir, $"{tomlPath}[{i}]", typeof(T), e, out var elementValue)) {
+ if (TryGetValueFromToml(reporter, origin, sourceDir, $"{tomlPath}[{i}]", typeof(T), e, out var elementValue)) {
  return (T)elementValue;
  }
  success = false;