From 148a2fdd459d72b2bf140cb594f3e2d8adac6d35 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 22 May 2023 10:53:19 +0200 Subject: [PATCH 01/68] Remove verify and compile fields from modules to enable caching parsing --- Source/DafnyCore.Test/DooFileTest.cs | 2 +- Source/DafnyCore/AST/BuiltIns.cs | 2 +- Source/DafnyCore/AST/Cloner.cs | 4 +- Source/DafnyCore/AST/DafnyAst.cs | 16 ++- Source/DafnyCore/AST/Grammar/Printer.cs | 109 ++++++++-------- .../AST/Grammar/SourcePreprocessor.cs | 53 ++++++-- .../AST/Grammar/TokenNewIndentCollector.cs | 6 +- Source/DafnyCore/AST/IncludeHandler.cs | 28 ---- Source/DafnyCore/AST/ShouldCompileOrVerify.cs | 101 +++++++++++++++ Source/DafnyCore/AST/TopLevelDeclarations.cs | 16 +-- Source/DafnyCore/Auditor/AuditReport.cs | 2 +- .../DafnyCore/Compilers/Java/Compiler-java.cs | 6 +- .../DafnyCore/Compilers/SinglePassCompiler.cs | 2 +- Source/DafnyCore/Dafny.atg | 44 +++---- Source/DafnyCore/DafnyFile.cs | 120 ++++++++++-------- Source/DafnyCore/DafnyMain.cs | 48 +++---- Source/DafnyCore/DafnyOptions.cs | 4 +- Source/DafnyCore/Generic/Reporting.cs | 2 +- Source/DafnyCore/Generic/Util.cs | 6 + Source/DafnyCore/Options/ProjectFile.cs | 2 +- Source/DafnyCore/Resolver/Resolver.cs | 12 +- .../Rewriters/IncludedLemmaBodyRemover.cs | 2 +- .../DafnyCore/Rewriters/PrecedenceLinter.cs | 2 +- Source/DafnyCore/Verifier/Translator.cs | 8 +- .../DafnyDriver/Commands/CommandRegistry.cs | 10 +- Source/DafnyDriver/Commands/RunCommand.cs | 4 +- Source/DafnyDriver/DafnyDriver.cs | 30 ++--- .../Unit/GhostStateDiagnosticCollectorTest.cs | 2 +- .../Language/DafnyLangParser.cs | 10 +- .../Symbols/SignatureAndCompletionTable.cs | 2 +- .../DafnyPipeline.Test/FormatterBaseTest.cs | 4 +- Source/DafnyPipeline.Test/TranslatorTest.cs | 2 +- Source/DafnyServer/DafnyHelper.cs | 4 +- .../SignatureAndCompletionTable.cs | 10 +- Source/DafnyTestGeneration/DafnyInfo.cs | 4 +- Source/DafnyTestGeneration/Utils.cs | 4 +- Test/auditor/TestAuditor.dfy | 4 +- Test/dafny0/formatting2.dfy.expect | 5 +- 38 files changed, 387 insertions(+), 305 deletions(-) delete mode 100644 Source/DafnyCore/AST/IncludeHandler.cs create mode 100644 Source/DafnyCore/AST/ShouldCompileOrVerify.cs diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs index d63f76baf38..2fb4a01cae0 100644 --- a/Source/DafnyCore.Test/DooFileTest.cs +++ b/Source/DafnyCore.Test/DooFileTest.cs @@ -38,6 +38,6 @@ private static Program ParseProgram(string dafnyProgramText, DafnyOptions option var errorReporter = new ConsoleErrorReporter(options, outerModule); var parseResult = Parser.Parse(dafnyProgramText, rootUri, module, builtIns, errorReporter); Assert.Equal(0, parseResult); - return new Program(fullFilePath, module, builtIns, errorReporter); + return new Program(fullFilePath, module, builtIns, errorReporter, Sets.Empty(), Sets.Empty()); } } diff --git a/Source/DafnyCore/AST/BuiltIns.cs b/Source/DafnyCore/AST/BuiltIns.cs index 39840f64175..9c889d67b17 100644 --- a/Source/DafnyCore/AST/BuiltIns.cs +++ b/Source/DafnyCore/AST/BuiltIns.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny; public class BuiltIns { public DafnyOptions Options { get; } - public readonly ModuleDefinition SystemModule = new ModuleDefinition(RangeToken.NoToken, new Name("_System"), new List(), false, false, null, null, null, true, true, true); + public readonly ModuleDefinition SystemModule = new ModuleDefinition(RangeToken.NoToken, new Name("_System"), new List(), false, false, null, null, null, true); internal readonly Dictionary arrayTypeDecls = new Dictionary(); public readonly Dictionary ArrowTypeDecls = new Dictionary(); public readonly Dictionary PartialArrowTypeDecls = new Dictionary(); // same keys as arrowTypeDecl diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 22a34bc5432..6fa6f4f321f 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -32,11 +32,11 @@ public Cloner(bool cloneResolvedFields = false) { public virtual ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) { ModuleDefinition nw; if (m is DefaultModuleDefinition defaultModuleDefinition) { - nw = new DefaultModuleDefinition(defaultModuleDefinition.RootUris); + nw = new DefaultModuleDefinition(defaultModuleDefinition.RootSourceUris); } else { nw = new ModuleDefinition(Range(m.RangeToken), name, m.PrefixIds, m.IsAbstract, m.IsFacade, m.RefinementQId, m.EnclosingModule, CloneAttributes(m.Attributes), - true, m.IsToBeVerified, m.IsToBeCompiled); + true); } foreach (var d in m.TopLevelDecls) { nw.TopLevelDecls.Add(CloneDeclaration(d, nw)); diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 6beee38f5a7..5b6da191136 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -39,7 +39,14 @@ void ObjectInvariant() { Contract.Invariant(DefaultModule != null); } + public ISet AlreadyVerifiedRoots; + public ISet AlreadyCompiledRoots; + public List Includes => DefaultModuleDef.Includes; + [FilledInDuringResolution] + public ISet UrisToVerify; + [FilledInDuringResolution] + public ISet UrisToCompile; public readonly string FullName; [FilledInDuringResolution] public Dictionary ModuleSigs; @@ -55,7 +62,8 @@ void ObjectInvariant() { public DafnyOptions Options => Reporter.Options; public ErrorReporter Reporter { get; set; } - public Program(string name, [Captured] LiteralModuleDecl module, [Captured] BuiltIns builtIns, ErrorReporter reporter) { + public Program(string name, [Captured] LiteralModuleDecl module, [Captured] BuiltIns builtIns, ErrorReporter reporter, + ISet alreadyVerifiedRoots, ISet alreadyCompiledRoots) { Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(reporter != null); @@ -64,6 +72,8 @@ public Program(string name, [Captured] LiteralModuleDecl module, [Captured] Buil DefaultModuleDef = (DefaultModuleDefinition)((LiteralModuleDecl)module).ModuleDef; BuiltIns = builtIns; this.Reporter = reporter; + AlreadyVerifiedRoots = alreadyVerifiedRoots; + AlreadyCompiledRoots = alreadyCompiledRoots; ModuleSigs = new Dictionary(); CompileModules = new List(); } @@ -126,16 +136,14 @@ public class Include : TokenNode, IComparable { public Uri IncluderFilename { get; } public string IncludedFilename { get; } public string CanonicalPath { get; } - public bool CompileIncludedCode { get; } public bool ErrorReported; - public Include(IToken tok, Uri includer, string theFilename, bool compileIncludedCode) { + public Include(IToken tok, Uri includer, string theFilename) { this.tok = tok; this.IncluderFilename = includer; this.IncludedFilename = theFilename; this.CanonicalPath = DafnyFile.Canonicalize(theFilename).LocalPath; this.ErrorReported = false; - CompileIncludedCode = compileIncludedCode; } public int CompareTo(object obj) { diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index 949963038bf..665e76fb7bf 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -153,16 +153,6 @@ public static string MethodSignatureToString(DafnyOptions options, Method m) { } } - public static string ModuleDefinitionToString(DafnyOptions options, ModuleDefinition m, PrintModes printMode = PrintModes.Everything) { - Contract.Requires(m != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr, options, printMode); - pr.PrintModuleDefinition(m, m.VisibilityScope, 0, null, null); - return ToStringWithoutNewline(wr); - } - } - - /// /// Returns a string for all attributes on the list "a". Each attribute is /// followed by a space. @@ -211,7 +201,7 @@ public void PrintProgram(Program prog, bool afterResolver) { if (options.DafnyPrintResolvedFile != null && options.PrintMode == PrintModes.Everything) { wr.WriteLine(); wr.WriteLine("/*"); - PrintModuleDefinition(prog.BuiltIns.SystemModule, null, 0, null, Path.GetFullPath(options.DafnyPrintResolvedFile)); + PrintModuleDefinition(prog, prog.BuiltIns.SystemModule, null, 0, null, Path.GetFullPath(options.DafnyPrintResolvedFile)); wr.Write("// bitvector types in use:"); foreach (var w in prog.BuiltIns.Bitwidths) { wr.Write(" bv{0}", w); @@ -221,10 +211,10 @@ public void PrintProgram(Program prog, bool afterResolver) { } wr.WriteLine(); PrintCallGraph(prog.DefaultModuleDef, 0); - PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0, null, Path.GetFullPath(prog.FullName)); + PrintTopLevelDecls(prog, prog.DefaultModuleDef.TopLevelDecls, 0, null, Path.GetFullPath(prog.FullName)); foreach (var tup in prog.DefaultModuleDef.PrefixNamedModules) { var decls = new List() { tup.Item2 }; - PrintTopLevelDecls(decls, 0, tup.Item1, Path.GetFullPath(prog.FullName)); + PrintTopLevelDecls(prog, decls, 0, tup.Item1, Path.GetFullPath(prog.FullName)); } wr.Flush(); } @@ -270,7 +260,7 @@ public void PrintCallGraph(ModuleDefinition module, int indent) { } } - public void PrintTopLevelDecls(List decls, int indent, List/*?*/ prefixIds, string fileBeingPrinted) { + public void PrintTopLevelDecls(Program program, List decls, int indent, List/*?*/ prefixIds, string fileBeingPrinted) { Contract.Requires(decls != null); int i = 0; foreach (TopLevelDecl d in decls) { @@ -322,35 +312,10 @@ public void PrintTopLevelDecls(List decls, int indent, List decls, int indent, List decls, int indent, List decls, int indent, List decls, int indent, List decls, int indent, List { (TopLevelDecl)id.Decl }, indent + IndentAmount, null, fileBeingPrinted); + PrintTopLevelDecls(program, new List { (TopLevelDecl)id.Decl }, indent + IndentAmount, null, fileBeingPrinted); } else if (id.Decl is MemberDecl) { PrintMembers(new List { (MemberDecl)id.Decl }, indent + IndentAmount, fileBeingPrinted); } @@ -562,7 +559,7 @@ void PrintModuleExportDecl(ModuleExportDecl m, int indent, string fileBeingPrint } } - public void PrintModuleDefinition(ModuleDefinition module, VisibilityScope scope, int indent, List/*?*/ prefixIds, string fileBeingPrinted) { + public void PrintModuleDefinition(Program program, ModuleDefinition module, VisibilityScope scope, int indent, List/*?*/ prefixIds, string fileBeingPrinted) { Contract.Requires(module != null); Contract.Requires(0 <= indent); Type.PushScope(scope); @@ -586,14 +583,14 @@ public void PrintModuleDefinition(ModuleDefinition module, VisibilityScope scope } else { wr.WriteLine("{"); PrintCallGraph(module, indent + IndentAmount); - PrintTopLevelDeclsOrExportedView(module, indent, fileBeingPrinted); + PrintTopLevelDeclsOrExportedView(program, module, indent, fileBeingPrinted); Indent(indent); wr.WriteLine("}"); } Type.PopScope(scope); } - void PrintTopLevelDeclsOrExportedView(ModuleDefinition module, int indent, string fileBeingPrinted) { + void PrintTopLevelDeclsOrExportedView(Program program, ModuleDefinition module, int indent, string fileBeingPrinted) { var decls = module.TopLevelDecls; // only filter based on view name after resolver. if (afterResolver && options.DafnyPrintExportedViews.Count != 0) { @@ -606,10 +603,10 @@ void PrintTopLevelDeclsOrExportedView(ModuleDefinition module, int indent, strin } } } - PrintTopLevelDecls(decls, indent + IndentAmount, null, fileBeingPrinted); + PrintTopLevelDecls(program, decls, indent + IndentAmount, null, fileBeingPrinted); foreach (var tup in module.PrefixNamedModules) { decls = new List() { tup.Item2 }; - PrintTopLevelDecls(decls, indent + IndentAmount, tup.Item1, fileBeingPrinted); + PrintTopLevelDecls(program, decls, indent + IndentAmount, tup.Item1, fileBeingPrinted); } } @@ -654,7 +651,7 @@ private void PrintIteratorClass(IteratorDecl iter, int indent, string fileBeingP Indent(indent); wr.WriteLine("}"); Contract.Assert(iter.NonNullTypeDecl != null); - PrintTopLevelDecls(new List { iter.NonNullTypeDecl }, indent, null, fileBeingPrinted); + PrintSubsetTypeDecl(iter.NonNullTypeDecl, indent); } public void PrintClass(ClassDecl c, int indent, string fileBeingPrinted) { @@ -686,7 +683,7 @@ public void PrintClass(ClassDecl c, int indent, string fileBeingPrinted) { if (!printingExportSet) { Indent(indent); wr.WriteLine("/*-- non-null type"); } - PrintTopLevelDecls(new List { c.NonNullTypeDecl }, indent, null, fileBeingPrinted); + PrintSubsetTypeDecl(c.NonNullTypeDecl, indent); if (!printingExportSet) { Indent(indent); wr.WriteLine("*/"); } diff --git a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs index 1de95abfbea..31db67415f1 100644 --- a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs +++ b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs @@ -56,20 +56,11 @@ private static bool IfdefConditionSaysToInclude(string arg, List /*!*/ d return defines.Contains(arg) == sense; } - public static string ProcessDirectives(Stream stream, List /*!*/ defines, string newline) { - Contract.Requires(stream != null); - Contract.Requires(cce.NonNullElements(defines)); - Contract.Ensures(Contract.Result() != null); - StreamReader /*!*/ - reader = new StreamReader(stream); - var o = stream.CanSeek; - return ProcessDirectives(reader, defines, newline); - } - - public static string ProcessDirectives(TextReader reader, List /*!*/ defines, string newline) { + public static string ProcessDirectives(TextReader reader, List /*!*/ defines) { Contract.Requires(reader != null); Contract.Requires(cce.NonNullElements(defines)); Contract.Ensures(Contract.Result() != null); + string newline = null; StringBuilder sb = new StringBuilder(); List /*!*/ ifDirectiveStates = new List(); // readState.Count is the current nesting level of #if's @@ -78,7 +69,12 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def while (true) //invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count; { - string line = reader.ReadLine(); + string line; + if (newline == null) { + line = ReadLineAndDetermineNewline(reader, out newline); + } else { + line = reader.ReadLine(); + } if (line == null) { if (ifDirectiveStates.Count != 0) { sb.AppendLine("#MalformedInput: missing #endif"); @@ -165,6 +161,39 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def return sb.ToString(); } + public static string ReadLineAndDetermineNewline(TextReader reader, out string newline) { + + StringBuilder sb = new StringBuilder(); + newline = null; + while (true) { + int ch = reader.Read(); + if (ch == -1) { + break; + } + + if (ch == '\r' || ch == '\n') { + if (ch == '\r') { + if (reader.Peek() == '\n') { + newline = "\r\n"; + reader.Read(); + } else { + newline = "\r"; + } + } else { + newline = "\n"; + } + + return sb.ToString(); + } + sb.Append((char)ch); + } + if (sb.Length > 0) { + return sb.ToString(); + } + + return null; + } + /// /// Returns the newline style used in the given file /// diff --git a/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs b/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs index 998d4ec67c7..ca0597ec551 100644 --- a/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs +++ b/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs @@ -231,7 +231,7 @@ public static bool IsFollowedByNewline(IToken token) { // 'inline' is the hypothetical indentation of this token if it was on its own line // 'below' is the hypothetical indentation of a comment after that token, and of the next token if it does not have a set indentation public void SetIndentations(IToken token, int above = -1, int inline = -1, int below = -1) { - if (token.WasIncluded(program) || (token.line == 0 && token.col == 0)) { + if (token.FromIncludeDirective(program) || (token.line == 0 && token.col == 0)) { // Just ignore this token. return; } @@ -401,7 +401,7 @@ public void SetStatementIndentation(Statement statement) { } public void SetDeclIndentation(TopLevelDecl topLevelDecl, int indent) { - if (topLevelDecl.tok.WasIncluded(program)) { + if (topLevelDecl.tok.FromIncludeDirective(program)) { return; } @@ -422,7 +422,7 @@ public void SetDeclIndentation(TopLevelDecl topLevelDecl, int indent) { var initialMemberIndent = declWithMembers.tok.line == 0 ? indent : indent2; foreach (var member in declWithMembers.PreResolveChildren) { - if (member.Tok.WasIncluded(program)) { + if (member.Tok.FromIncludeDirective(program)) { continue; } diff --git a/Source/DafnyCore/AST/IncludeHandler.cs b/Source/DafnyCore/AST/IncludeHandler.cs deleted file mode 100644 index bbc124c6ad7..00000000000 --- a/Source/DafnyCore/AST/IncludeHandler.cs +++ /dev/null @@ -1,28 +0,0 @@ -using System; -using System.IO; -using System.Linq; - -namespace Microsoft.Dafny; - -public static class IncludeHandler { - public static bool WasIncluded(this IToken token, DefaultModuleDefinition outerModule) { - if (token is RefinementToken) { - return false; - } - - if (token == Token.NoToken) { - return false; - } - - var files = outerModule.RootUris; - if (files.Contains(token.Uri)) { - return false; - } - - return true; - } - - public static bool WasIncluded(this IToken token, Program program) { - return token.WasIncluded(program.DefaultModuleDef); - } -} \ No newline at end of file diff --git a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs new file mode 100644 index 00000000000..eae9cbf80a4 --- /dev/null +++ b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs @@ -0,0 +1,101 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; + +namespace Microsoft.Dafny; + +public static class ShouldCompileOrVerify { + + public static bool ShouldCompile(this ModuleDefinition module, Program program) { + if (program.UrisToCompile == null) { + program.UrisToCompile = ComputeUrisToCompile(program); + } + + if (module.FullName == "_System") { + return true; + } + + if (module is DefaultModuleDefinition) { + // If things from precompiled files live in the default module, that can cause downstream compilation issues: + // https://github.com/dafny-lang/dafny/issues/4009 + return true; + } + return program.UrisToCompile.Contains(module.Tok.Uri); + } + + public static bool ShouldVerify(this INode declaration, Program program) { + if (declaration.Tok == Token.NoToken) { + // Required for DefaultModuleDefinition. + return true; + } + if (program.UrisToVerify == null) { + program.UrisToVerify = ComputeUrisToVerify(program); + } + if (!program.UrisToVerify.Contains(declaration.Tok.Uri)) { + return false; + } + + if (program.Options.VerifyAllModules) { + return true; + } + + return !declaration.Tok.FromIncludeDirective(program); + } + + public static bool FromIncludeDirective(this IToken token, DefaultModuleDefinition outerModule) { + if (token is RefinementToken) { + return false; + } + + if (token == Token.NoToken) { + return false; + } + + var files = outerModule.RootSourceUris; + if (files.Contains(token.Uri)) { + return false; + } + + return true; + } + + public static bool FromIncludeDirective(this IToken token, Program program) { + return token.FromIncludeDirective(program.DefaultModuleDef); + } + + private static ISet ComputeUrisToCompile(Program program) { + var compiledRoots = program.AlreadyCompiledRoots; + return GetReachableUris(program, compiledRoots); + } + + private static ISet ComputeUrisToVerify(Program program) { + var verifiedRoots = program.AlreadyVerifiedRoots; + return GetReachableUris(program, verifiedRoots); + } + + private static ISet GetReachableUris(Program program, ISet stopUris) { + var toVisit = new Stack(program.DefaultModuleDef.RootSourceUris); + + var visited = new HashSet(); + var edges = program.Includes.GroupBy(i => i.IncluderFilename) + .ToDictionary(g => g.Key, g => g.Select(i => new Uri(i.IncludedFilename)).ToList()); + while (toVisit.Any()) { + var uri = toVisit.Pop(); + if (stopUris.Contains(uri)) { + continue; + } + + if (!visited.Add(uri)) { + continue; + } + + foreach (var included in edges.GetOrDefault(uri, Enumerable.Empty)) { + toVisit.Push(included); + } + } + + return visited; + } + +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 0bdb7885c97..de2184d949d 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -849,6 +849,7 @@ public string FullName { public ModuleQualifiedId RefinementQId; // full qualified ID of the refinement parent, null if no refinement base public bool SuccessfullyResolved; // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved + // TODO move to Program once this list is no longer mutated by parsing. public List Includes; [FilledInDuringResolution] public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that, except for the addition of prefix-named modules, which happens in the resolver @@ -858,8 +859,6 @@ public string FullName { public readonly bool IsAbstract; public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface) private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled. - public readonly bool IsToBeVerified; - public readonly bool IsToBeCompiled; public int? ResolvedHash { get; set; } @@ -870,8 +869,7 @@ void ObjectInvariant() { } public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool isAbstract, bool isFacade, - ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, bool isBuiltinName, - bool isToBeVerified, bool isToBeCompiled) : base(tok) { + ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, bool isBuiltinName) : base(tok) { Contract.Requires(tok != null); Contract.Requires(name != null); this.NameNode = name; @@ -883,8 +881,6 @@ public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool this.IsFacade = isFacade; this.Includes = new List(); this.IsBuiltinName = isBuiltinName; - this.IsToBeVerified = isToBeVerified; - this.IsToBeCompiled = isToBeCompiled; } VisibilityScope visibilityScope; @@ -1160,10 +1156,10 @@ public override IEnumerable Assumptions(Declaration decl) { public class DefaultModuleDefinition : ModuleDefinition { - public IList RootUris { get; } - public DefaultModuleDefinition(IList rootUris) - : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, null, null, null, true, true, true) { - RootUris = rootUris; + public IList RootSourceUris { get; } + public DefaultModuleDefinition(IList rootSourceUris) + : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, null, null, null, true) { + RootSourceUris = rootSourceUris; } public override bool IsDefaultModule => true; diff --git a/Source/DafnyCore/Auditor/AuditReport.cs b/Source/DafnyCore/Auditor/AuditReport.cs index b75d341b5d3..90de25eda0b 100644 --- a/Source/DafnyCore/Auditor/AuditReport.cs +++ b/Source/DafnyCore/Auditor/AuditReport.cs @@ -190,7 +190,7 @@ public static AuditReport BuildReport(Program program) { continue; } foreach (var decl in topLevelDeclWithMembers.Members) { - if (decl.tok.WasIncluded(program)) { + if (decl.tok.FromIncludeDirective(program)) { // Don't audit included code continue; } diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index a1bc2aa3efb..4c56016a0a5 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -74,9 +74,7 @@ string FormatTypeDescriptorVariable(TypeParameter tp) => //RootImportWriter writes additional imports to the main file. private ConcreteSyntaxTree RootImportWriter; - private struct Import { - public string Name, Path; - } + private record Import(string Name, string Path); protected override bool UseReturnStyleOuts(Method m, int nonGhostOutCount) => true; @@ -365,7 +363,7 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef } var pkgName = libraryName ?? IdProtect(moduleName); var path = pkgName.Replace('.', '/'); - var import = new Import { Name = moduleName, Path = path }; + var import = new Import(moduleName, path); ModuleName = IdProtect(moduleName); ModulePath = path; ModuleImport = import; diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index d90ab21f4e9..a518e8f5b08 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs @@ -1343,7 +1343,7 @@ public void Compile(Program program, ConcreteSyntaxTree wrx) { // the purpose of an abstract module is to skip compilation continue; } - if (!m.IsToBeCompiled) { + if (!m.ShouldCompile(program)) { continue; } var moduleIsExtern = false; diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 708a7b987cb..8ca56aa9aee 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -28,8 +28,6 @@ readonly Statement/*!*/ dummyStmt; readonly Statement/*!*/ dummyIfStmt; readonly ModuleDecl theModule; readonly BuiltIns theBuiltIns; -readonly bool theVerifyThisFile; -readonly bool theCompileThisFile; DafnyOptions theOptions; int anonymousIds = 0; @@ -148,37 +146,29 @@ bool IsAssumeTypeKeyword(IToken la) { /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// -public static int Parse (TextReader fileReaderOverride, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true, bool compileThisFile=true) /* throws System.IO.IOException */ { +public static int Parse(TextReader reader, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors) /* throws System.IO.IOException */ { Contract.Requires(uri != null); Contract.Requires(module != null); - string s; - if (fileReaderOverride != null) { - s = Microsoft.Dafny.SourcePreprocessor.ProcessDirectives(fileReaderOverride, new List(), Environment.NewLine); - return Parse(s, uri, module, builtIns, errors, verifyThisFile, compileThisFile); - } else { - var newline = SourcePreprocessor.GetNewlineStyle(uri.LocalPath); - using (System.IO.StreamReader reader = new System.IO.StreamReader(uri.LocalPath)) { - s = Microsoft.Dafny.SourcePreprocessor.ProcessDirectives(reader, new List(), newline); - return Parse(s, uri, module, builtIns, errors, verifyThisFile, compileThisFile); - } - } + var text = Microsoft.Dafny.SourcePreprocessor.ProcessDirectives(reader, new List()); + return Parse(text, uri, module, builtIns, errors); } + /// /// Parses top-level things (modules, classes, datatypes, class members) /// and appends them in appropriate form to "module". /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// -public static int Parse(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, ErrorReporter reporter, bool verifyThisFile=true, bool compileThisFile=true) { +public static int Parse(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, ErrorReporter reporter) { Contract.Requires(s != null); Contract.Requires(uri != null); Contract.Requires(module != null); Errors errors = new Errors(reporter); - return Parse(s, uri, module, builtIns, errors, verifyThisFile, compileThisFile); + return Parse(s, uri, module, builtIns, errors); } public static Parser SetupParser(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, - BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true, bool compileThisFile=true) { + BuiltIns builtIns, Errors/*!*/ errors) { Contract.Requires(s != null); Contract.Requires(uri != null); Contract.Requires(module != null); @@ -195,12 +185,12 @@ public static Parser SetupParser(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, firstToken = new Token(); // It's an included file } Scanner scanner = new Scanner(ms, errors, uri, firstToken: firstToken); - return new Parser(scanner, errors, module, builtIns, verifyThisFile, compileThisFile); + return new Parser(scanner, errors, module, builtIns); } public static Expression ParseExpression(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, - BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true, bool compileThisFile=true) { - Parser parser = SetupParser(s, uri, module, builtIns, errors, verifyThisFile, compileThisFile); + BuiltIns builtIns, Errors/*!*/ errors) { + Parser parser = SetupParser(s, uri, module, builtIns, errors); parser.la = new Token(); parser.la.val = ""; parser.Get(); @@ -253,14 +243,14 @@ public void ApplyOptionsFromAttributes(Attributes attrs) { /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner with the given Errors sink. /// -public static int Parse (string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, - BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true, bool compileThisFile=true) { - Parser parser = SetupParser(s, uri, module, builtIns, errors, verifyThisFile, compileThisFile); +public static int Parse(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, + BuiltIns builtIns, Errors/*!*/ errors) { + Parser parser = SetupParser(s, uri, module, builtIns, errors); parser.Parse(); return parser.errors.ErrorCount; } -public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true, bool compileThisFile=true) +public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns) : this(scanner, errors) // the real work { // initialize readonly fields @@ -272,8 +262,6 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, Built dummyIfStmt = new IfStmt(Token.NoToken.ToRange(), false, null, dummyBlockStmt, null); theModule = module; theBuiltIns = builtIns; - theVerifyThisFile = verifyThisFile; - theCompileThisFile = compileThisFile; theOptions = new DafnyOptions(builtIns.Options); } @@ -1031,7 +1019,7 @@ Dafny string basePath = Path.GetDirectoryName(parsedFile.LocalPath); includedFile = Path.Combine(basePath, includedFile); } - var oneInclude = new Include(t, parsedFile, includedFile, theCompileThisFile); + var oneInclude = new Include(t, parsedFile, includedFile); oneInclude.RangeToken = new RangeToken(startToken, t); defaultModule.Includes.Add(oneInclude); } @@ -1136,7 +1124,7 @@ ModuleDefinition() { "file:\\", "file:/", "file:" }; - foreach (var potentialPrefix in potentialPrefixes) { - if (filePath.StartsWith(potentialPrefix)) { - var withoutPrefix = filePath.Substring(potentialPrefix.Length); - var tentativeURI = "file:///" + withoutPrefix.Replace("\\", "/"); - if (Uri.IsWellFormedUriString(tentativeURI, UriKind.RelativeOrAbsolute)) { - return new Uri(tentativeURI); - } - // Recovery mechanisms for the language server - return new Uri(filePath.Substring(potentialPrefix.Length)); - } - } - return new Uri(filePath.Substring("file:".Length)); - } - public static List FileNames(IList dafnyFiles) { - var sourceFiles = new List(); - foreach (DafnyFile f in dafnyFiles) { - sourceFiles.Add(f.FilePath); - } - return sourceFiles; - } - public DafnyFile(DafnyOptions options, string filePath, bool useStdin = false) { - UseStdin = useStdin; - Uri = useStdin ? new Uri("stdin:///") : new Uri(filePath); - BaseName = useStdin ? "" : Path.GetFileName(filePath); - - var extension = useStdin ? ".dfy" : Path.GetExtension(filePath); + public TextReader Content { get; } + public Uri Uri { get; } + public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverride = null) { + UseStdin = contentOverride != null; + Uri = contentOverride != null ? new Uri("stdin:///") : new Uri(filePath); + BaseName = contentOverride != null ? "" : Path.GetFileName(filePath); + + var extension = contentOverride != null ? ".dfy" : Path.GetExtension(filePath); if (extension != null) { extension = extension.ToLower(); } // 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 = !useStdin ? Canonicalize(filePath).LocalPath : ""; + CanonicalPath = contentOverride == null ? Canonicalize(filePath).LocalPath : ""; filePath = CanonicalPath; - if (extension == ".dfy" || extension == ".dfyi") { + if (contentOverride != null) { + IsPreverified = false; + IsPrecompiled = false; + Content = contentOverride; + } else if (extension == ".dfy" || extension == ".dfyi") { IsPreverified = false; IsPrecompiled = false; - SourceFilePath = filePath; + if (!File.Exists(filePath)) { + 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; + } + + options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePath} not found"); + throw new IllegalDafnyFile(true); + } else { + Content = new StreamReader(filePath); + } } else if (extension == ".doo") { IsPreverified = true; IsPrecompiled = false; @@ -88,10 +68,7 @@ public DafnyFile(DafnyOptions options, string filePath, bool useStdin = false) { // 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. - SourceFilePath = Path.GetTempFileName(); - Uri = new Uri(SourceFilePath); - File.WriteAllText(SourceFilePath, dooFile.ProgramText); - + Content = new StringReader(dooFile.ProgramText); } else if (extension == ".dll") { IsPreverified = true; // Technically only for C#, this is for backwards compatability @@ -99,15 +76,48 @@ public DafnyFile(DafnyOptions options, string filePath, bool useStdin = false) { var sourceText = GetDafnySourceAttributeText(filePath); if (sourceText == null) { throw new IllegalDafnyFile(); } - SourceFilePath = Path.GetTempFileName(); - Uri = new Uri(SourceFilePath); - File.WriteAllText(SourceFilePath, sourceText); - + Content = new StringReader(sourceText); } else { throw new IllegalDafnyFile(); } } + // Returns a canonical string for the given file path, namely one which is the same + // for all paths to a given file and different otherwise. The best we can do is to + // make the path absolute -- detecting case and canonicalizing symbolic and hard + // links are difficult across file systems (which may mount parts of other filesystems, + // with different characteristics) and is not supported by .Net libraries + public static Uri Canonicalize(string filePath) { + if (filePath == null || !filePath.StartsWith("file:")) { + return new Uri(Path.GetFullPath(filePath)); + } + + if (Uri.IsWellFormedUriString(filePath, UriKind.RelativeOrAbsolute)) { + return new Uri(filePath); + } + + var potentialPrefixes = new List() { "file:\\", "file:/", "file:" }; + foreach (var potentialPrefix in potentialPrefixes) { + if (filePath.StartsWith(potentialPrefix)) { + var withoutPrefix = filePath.Substring(potentialPrefix.Length); + var tentativeURI = "file:///" + withoutPrefix.Replace("\\", "/"); + if (Uri.IsWellFormedUriString(tentativeURI, UriKind.RelativeOrAbsolute)) { + return new Uri(tentativeURI); + } + // Recovery mechanisms for the language server + return new Uri(filePath.Substring(potentialPrefix.Length)); + } + } + return new Uri(filePath.Substring("file:".Length)); + } + public static List FileNames(IList dafnyFiles) { + var sourceFiles = new List(); + foreach (DafnyFile f in dafnyFiles) { + sourceFiles.Add(f.FilePath); + } + return sourceFiles; + } + private static string GetDafnySourceAttributeText(string dllPath) { if (!File.Exists(dllPath)) { throw new IllegalDafnyFile(); diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index 3f0f5f98a16..c7a7d51a761 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -79,27 +79,24 @@ public static string Parse(TextReader stdIn, IList files, string prog options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath); } - var include = dafnyFile.IsPrecompiled - ? new Include(new Token() { - Uri = dafnyFile.Uri, - col = 1, - line = 0 - }, null, dafnyFile.SourceFilePath, false) - : null; + // We model a precompiled file, a library, as an include + var include = dafnyFile.IsPrecompiled ? new Include(new Token { + Uri = dafnyFile.Uri, + col = 1, + line = 0 + }, new Uri("cli://"), dafnyFile.FilePath) : null; if (include != null) { + // TODO this can be removed once the include error message in ErrorReporter.Error is removed. module.ModuleDef.Includes.Add(include); } - - var err = ParseFile(stdIn, dafnyFile, include, module, builtIns, new Errors(reporter), !dafnyFile.IsPreverified, - !dafnyFile.IsPrecompiled); + var err = ParseFile(dafnyFile, null, module, builtIns, new Errors(reporter)); if (err != null) { return err; } } if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) { - string errString = ParseIncludesDepthFirstNotCompiledFirst(stdIn, module, builtIns, - files.Select(f => f.SourceFilePath).ToHashSet(), new Errors(reporter)); + string errString = ParseIncludes(module, builtIns, files.Select(f => f.FilePath).ToHashSet(), new Errors(reporter)); if (errString != null) { return errString; } @@ -111,7 +108,9 @@ public static string Parse(TextReader stdIn, IList files, string prog dmap.PrintMap(options); } - program = new Program(programName, module, builtIns, reporter); + var verifiedRoots = files.Where(df => df.IsPreverified).Select(df => df.Uri).ToHashSet(); + var compiledRoots = files.Where(df => df.IsPrecompiled).Select(df => df.Uri).ToHashSet(); + program = new Program(programName, module, builtIns, reporter, verifiedRoots, compiledRoots); MaybePrintProgram(program, options.DafnyPrintFile, false); @@ -148,28 +147,15 @@ public int Compare(Include x, Include y) { } } - public static string ParseIncludesDepthFirstNotCompiledFirst(TextReader stdIn, ModuleDecl module, - BuiltIns builtIns, ISet excludeFiles, Errors errs) { + public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, ISet excludeFiles, Errors errs) { var includesFound = new SortedSet(new IncludeComparer()); var allIncludes = ((LiteralModuleDecl)module).ModuleDef.Includes; - var notCompiledRoots = allIncludes.Where(include => !include.CompileIncludedCode).ToList(); - var compiledRoots = allIncludes.Where(include => include.CompileIncludedCode).ToList(); - allIncludes.Clear(); - allIncludes.AddRange(notCompiledRoots); var notCompiledResult = TraverseIncludesFrom(0); if (notCompiledResult != null) { return notCompiledResult; } - var notCompiledIncludeCount = allIncludes.Count; - allIncludes.AddRange(compiledRoots); - - var compiledResult = TraverseIncludesFrom(notCompiledIncludeCount); - if (compiledResult != null) { - return compiledResult; - } - if (builtIns.Options.PrintIncludesMode != DafnyOptions.IncludesModes.None) { var dependencyMap = new DependencyMap(); dependencyMap.AddIncludes(allIncludes); @@ -206,7 +192,7 @@ string TraverseIncludesFrom(int startingIndex) { return ($"Include of file \"{include.IncludedFilename}\" failed."); } - string result = ParseFile(stdIn, file, include, module, builtIns, errs, false, include.CompileIncludedCode); + string result = ParseFile(file, include, module, builtIns, errs); if (result != null) { return result; } @@ -216,12 +202,10 @@ string TraverseIncludesFrom(int startingIndex) { } } - private static string ParseFile(TextReader stdIn, DafnyFile dafnyFile, Include include, ModuleDecl module, - BuiltIns builtIns, Errors errs, bool verifyThisFile = true, bool compileThisFile = true) { + private static string ParseFile(DafnyFile dafnyFile, Include include, ModuleDecl module, BuiltIns builtIns, Errors errs) { var fn = builtIns.Options.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath; try { - int errorCount = Dafny.Parser.Parse(dafnyFile.UseStdin ? stdIn : null, dafnyFile.Uri, module, builtIns, errs, - verifyThisFile, compileThisFile); + int errorCount = Parser.Parse(dafnyFile.Content, dafnyFile.Uri, module, builtIns, errs); if (errorCount != 0) { return $"{errorCount} parse errors detected in {fn}"; } diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index fc8517917e4..650d9add549 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -39,7 +39,7 @@ public class DafnyOptions : Bpl.CommandLineOptions { public TextReader Input { get; } public static readonly DafnyOptions Default = new(TextReader.Null, TextWriter.Null, TextWriter.Null); - public IList CliRootUris = new List(); + public IList CliRootSourceUris = new List(); public ProjectFile ProjectFile { get; set; } public Command CurrentCommand { get; set; } @@ -150,7 +150,7 @@ public void Set(Option option, T value) { } protected override void AddFile(string file, Bpl.CommandLineParseState ps) { - this.CliRootUris.Add(new Uri(Path.GetFullPath(file))); + this.CliRootSourceUris.Add(new Uri(Path.GetFullPath(file))); base.AddFile(file, ps); } diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index 6bbea88f725..00021c34bc1 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -46,7 +46,7 @@ public void Error(MessageSource source, IToken tok, string msg) { public virtual void Error(MessageSource source, string errorId, IToken tok, string msg) { Contract.Requires(tok != null); Contract.Requires(msg != null); - if (tok.WasIncluded(OuterModule) && OuterModule != null) { + if (tok.FromIncludeDirective(OuterModule) && OuterModule != null) { var include = OuterModule.Includes.First(i => new Uri(i.IncludedFilename).LocalPath == tok.ActualFilename); if (!include.ErrorReported) { Message(source, ErrorLevel.Error, null, include.tok, "the included file " + Path.GetFileName(tok.ActualFilename) + " contains error(s)"); diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index c896bfccbd5..e0d14888b84 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -14,6 +14,12 @@ using Microsoft.Boogie; namespace Microsoft.Dafny { + + public static class Sets { + public static ISet Empty() { + return new HashSet(); + } + } public static class Util { public static Task SelectMany(this Task task, Func> f) { diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index b31d71248e0..2ecc79bcfe4 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -63,7 +63,7 @@ public void AddFilesToOptions(DafnyOptions options) { var result = matcher.Execute(new DirectoryInfoWrapper(new DirectoryInfo(root!))); var files = result.Files.Select(f => Path.Combine(root, f.Path)); foreach (var file in files) { - options.CliRootUris.Add(new Uri(Path.GetFullPath(file))); + options.CliRootSourceUris.Add(new Uri(Path.GetFullPath(file))); } } diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 6f38b32d777..024791598de 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -535,7 +535,7 @@ public void ResolveProgram(Program prog) { if (good && reporter.ErrorCount == preResolveErrorCount) { // Check that the module export gives a self-contained view of the module. - CheckModuleExportConsistency(m); + CheckModuleExportConsistency(prog, m); } var tempVis = new VisibilityScope(); @@ -1158,7 +1158,7 @@ private void ResolveModuleExport(LiteralModuleDecl literalDecl, ModuleSignature //check for export consistency by resolving internal modules //this should be effect-free, as it only operates on clones - private void CheckModuleExportConsistency(ModuleDefinition m) { + private void CheckModuleExportConsistency(Program program, ModuleDefinition m) { var oldModuleInfo = moduleInfo; foreach (var exportDecl in m.TopLevelDecls.OfType()) { @@ -1195,7 +1195,7 @@ private void CheckModuleExportConsistency(ModuleDefinition m) { var wr = Options.OutputWriter; wr.WriteLine("/* ===== export set {0}", exportDecl.FullName); var pr = new Printer(wr, Options); - pr.PrintTopLevelDecls(exportView.TopLevelDecls, 0, null, null); + pr.PrintTopLevelDecls(program, exportView.TopLevelDecls, 0, null, null); wr.WriteLine("*/"); } @@ -1310,8 +1310,7 @@ private ModuleBindings BindModuleNames(ModuleDefinition moduleDecl, ModuleBindin var name = entry.Key; var prefixNamedModules = entry.Value; var tok = prefixNamedModules.First().Item1[0]; - var modDef = new ModuleDefinition(tok.ToRange(), new Name(tok.ToRange(), name), new List(), false, false, null, moduleDecl, null, false, - true, true); + var modDef = new ModuleDefinition(tok.ToRange(), new Name(tok.ToRange(), name), new List(), false, false, null, moduleDecl, null, false); // Every module is expected to have a default class, so we create and add one now var defaultClass = new DefaultClassDecl(modDef, new List()); modDef.TopLevelDecls.Add(defaultClass); @@ -2014,8 +2013,7 @@ private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, in var errCount = reporter.Count(ErrorLevel.Error); var mod = new ModuleDefinition(RangeToken.NoToken, new Name(Name + ".Abs"), new List(), true, true, null, null, null, - false, - p.ModuleDef.IsToBeVerified, p.ModuleDef.IsToBeCompiled); + false); mod.Height = Height; bool hasDefaultClass = false; foreach (var kv in p.TopLevels) { diff --git a/Source/DafnyCore/Rewriters/IncludedLemmaBodyRemover.cs b/Source/DafnyCore/Rewriters/IncludedLemmaBodyRemover.cs index 302e6b25502..e041cf8a36f 100644 --- a/Source/DafnyCore/Rewriters/IncludedLemmaBodyRemover.cs +++ b/Source/DafnyCore/Rewriters/IncludedLemmaBodyRemover.cs @@ -22,7 +22,7 @@ public IncludedLemmaBodyRemover(Program program, ErrorReporter reporter) internal override void PostResolve(ModuleDefinition moduleDefinition) { foreach (var method in moduleDefinition.TopLevelDecls.OfType(). SelectMany(withMembers => withMembers.Members.OfType())) { - if (method.Body != null && method.IsLemmaLike && method.Tok.WasIncluded(program)) { + if (method.Body != null && method.IsLemmaLike && method.Tok.FromIncludeDirective(program)) { method.Body = EmptyBody; } } diff --git a/Source/DafnyCore/Rewriters/PrecedenceLinter.cs b/Source/DafnyCore/Rewriters/PrecedenceLinter.cs index 952b7a0e124..2565ad63582 100644 --- a/Source/DafnyCore/Rewriters/PrecedenceLinter.cs +++ b/Source/DafnyCore/Rewriters/PrecedenceLinter.cs @@ -243,7 +243,7 @@ void VisitRhsComponent(IToken errorToken, Expression expr, string what) { } void VisitRhsComponent(IToken errorToken, Expression expr, int rightMargin, string what) { - if (expr is ParensExpression || errorToken.WasIncluded(program)) { + if (expr is ParensExpression || errorToken.FromIncludeDirective(program)) { VisitIndependentComponent(expr); } else { var st = new LeftMargin(rightMargin); diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index fb92f8486f6..59ab2f2c27c 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -169,7 +169,7 @@ bool RevealedInScope(RevealableTypeDecl d) { [Pure] bool InVerificationScope(Declaration d) { Contract.Requires(d != null); - if (!options.VerifyAllModules && d.tok.WasIncluded(program)) { + if (!d.ShouldVerify(program)) { return false; } @@ -839,8 +839,8 @@ private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { } // Don't verify modules which only contain other modules - private static bool ShouldVerifyModule(DafnyOptions options, ModuleDefinition m) { - if (!m.IsToBeVerified && !options.VerifyAllModules) { + private static bool ShouldVerifyModule(Program program, ModuleDefinition m) { + if (!m.ShouldVerify(program)) { return false; } @@ -857,7 +857,7 @@ private static bool ShouldVerifyModule(DafnyOptions options, ModuleDefinition m) } public static IEnumerable VerifiableModules(Program p) { - return p.RawModules().Where(m => ShouldVerifyModule(p.Options, m)); + return p.RawModules().Where(m => ShouldVerifyModule(p, m)); } public static IEnumerable> Translate(Program p, ErrorReporter reporter, TranslatorFlags flags = null) { diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 4655d6d211b..535676784f5 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -162,7 +162,7 @@ void CommandHandler(InvocationContext context) { foreach (var option in command.Options) { var result = context.ParseResult.FindResultFor(option); object projectFileValue = null; - var hasProjectFileValue = dafnyOptions.ProjectFile?.TryGetValue(option, Console.Error, out projectFileValue) ?? false; + var hasProjectFileValue = dafnyOptions.ProjectFile?.TryGetValue(option, errorWriter, out projectFileValue) ?? false; object value; if (option.Arity.MaximumNumberOfValues <= 1) { // If multiple values aren't allowed, CLI options take precedence over project file options @@ -239,15 +239,15 @@ private static object GetValueForOption(ParseResult result, Option option) { private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) { if (Path.GetExtension(singleFile.FullName) == ".toml") { if (dafnyOptions.ProjectFile != null) { - Console.Error.WriteLine($"Only one project file can be used at a time. Both {dafnyOptions.ProjectFile.Uri.LocalPath} and {singleFile.FullName} were specified"); + dafnyOptions.ErrorWriter.WriteLine($"Only one project file can be used at a time. Both {dafnyOptions.ProjectFile.Uri.LocalPath} and {singleFile.FullName} were specified"); return false; } if (!File.Exists(singleFile.FullName)) { - Console.Error.WriteLine($"Error: file {singleFile.FullName} not found"); + dafnyOptions.ErrorWriter.WriteLine($"Error: file {singleFile.FullName} not found"); return false; } - var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), Console.Error); + var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), dafnyOptions.ErrorWriter); if (projectFile == null) { return false; } @@ -255,7 +255,7 @@ private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) dafnyOptions.ProjectFile = projectFile; projectFile.AddFilesToOptions(dafnyOptions); } else { - dafnyOptions.CliRootUris.Add(new Uri(singleFile.FullName)); + dafnyOptions.CliRootSourceUris.Add(new Uri(singleFile.FullName)); } return true; } diff --git a/Source/DafnyDriver/Commands/RunCommand.cs b/Source/DafnyDriver/Commands/RunCommand.cs index eab2132d125..57393b00f89 100644 --- a/Source/DafnyDriver/Commands/RunCommand.cs +++ b/Source/DafnyDriver/Commands/RunCommand.cs @@ -18,7 +18,7 @@ class RunCommand : ICommandSpec { static RunCommand() { DafnyOptions.RegisterLegacyBinding(Inputs, (options, files) => { foreach (var file in files) { - options.CliRootUris.Add(new Uri(Path.GetFullPath(file))); + options.CliRootSourceUris.Add(new Uri(Path.GetFullPath(file))); } }); @@ -49,7 +49,7 @@ public Command Create() { public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) { dafnyOptions.MainArgs = context.ParseResult.GetValueForArgument(userProgramArguments).ToList(); var inputFile = context.ParseResult.GetValueForArgument(CommandRegistry.FileArgument); - dafnyOptions.CliRootUris.Add(new Uri(Path.GetFullPath(inputFile.FullName))); + dafnyOptions.CliRootSourceUris.Add(new Uri(Path.GetFullPath(inputFile.FullName))); dafnyOptions.Compile = true; dafnyOptions.RunAfterCompile = true; dafnyOptions.ForceCompile = dafnyOptions.Get(BoogieOptionBag.NoVerify); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 1b8d2e85701..be931d518c8 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -120,13 +120,20 @@ public static int MainWithWriters(TextWriter outputWriter, TextWriter errorWrite private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, string[] args) { Contract.Requires(cce.NonNullElements(args)); - var cliArgumentsResult = ProcessCommandLineArguments(outputWriter, errorWriter, inputReader, args, out var dafnyOptions, out var dafnyFiles, out var otherFiles); ExitValue exitValue; switch (cliArgumentsResult) { case CommandLineArgumentsResult.OK: + + if (dafnyOptions.RunLanguageServer) { +#pragma warning disable VSTHRD002 + LanguageServer.Server.Start(dafnyOptions).Wait(); +#pragma warning restore VSTHRD002 + return 0; + } + var driver = new DafnyDriver(dafnyOptions); #pragma warning disable VSTHRD002 exitValue = driver.ProcessFilesAsync(dafnyFiles, otherFiles.AsReadOnly(), dafnyOptions).Result; @@ -140,13 +147,6 @@ private static int ThreadMain(TextWriter outputWriter, TextWriter errorWriter, T throw new ArgumentOutOfRangeException(); } - if (dafnyOptions.RunLanguageServer) { -#pragma warning disable VSTHRD002 - LanguageServer.Server.Start(dafnyOptions).Wait(); -#pragma warning restore VSTHRD002 - return 0; - } - dafnyOptions.XmlSink?.Close(); if (dafnyOptions.VerificationLoggerConfigs.Any()) { @@ -242,10 +242,10 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter } if (options.UseStdin) { - options.CliRootUris.Add(new Uri("stdin:///")); - dafnyFiles.Add(new DafnyFile(options, "", true)); - } else if (options.CliRootUris.Count == 0 && !options.Format) { - options.Printer.ErrorWriteLine(Console.Error, "*** Error: No input files were specified in command-line " + string.Join("|", args) + "."); + options.CliRootSourceUris.Add(new Uri("stdin:///")); + dafnyFiles.Add(new DafnyFile(options, "", inputReader)); + } else if (options.CliRootSourceUris.Count == 0 && !options.Format) { + options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: No input files were specified in command-line " + string.Join("|", args) + "."); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } if (options.XmlSink != null) { @@ -265,7 +265,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter } ISet filesSeen = new HashSet(); - foreach (var file in options.CliRootUris.Where(u => u.IsFile).Select(u => u.LocalPath). + foreach (var file in options.CliRootSourceUris.Where(u => u.IsFile).Select(u => u.LocalPath). Concat(SplitOptionValueIntoFiles(options.LibraryFiles))) { Contract.Assert(file != null); string extension = Path.GetExtension(file); @@ -391,13 +391,13 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny return exitValue; } - if (0 <= options.VerifySnapshots && lookForSnapshots) { + if (0 < options.VerifySnapshots && lookForSnapshots) { var snapshotsByVersion = ExecutionEngine.LookForSnapshots(dafnyFileNames); foreach (var s in snapshotsByVersion) { var snapshots = new List(); foreach (var f in s) { snapshots.Add(new DafnyFile(options, f)); - options.CliRootUris.Add(new Uri(Path.GetFullPath(f))); + options.CliRootSourceUris.Add(new Uri(Path.GetFullPath(f))); } var ev = await ProcessFilesAsync(snapshots, new List().AsReadOnly(), options, false, programId); if (exitValue != ev && ev != ExitValue.SUCCESS) { diff --git a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs index e6ed3d57b10..ce4f4d6c0ef 100644 --- a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs @@ -63,7 +63,7 @@ public void EnsureResilienceAgainstErrors() { var rootUri = new Uri(Directory.GetCurrentDirectory()); var dummyModuleDecl = new DummyModuleDecl(new List() { rootUri }); var reporter = new CollectingErrorReporter(options, (DefaultModuleDefinition)dummyModuleDecl.ModuleDef); - var program = new Dafny.Program("dummy", dummyModuleDecl, null, reporter); + var program = new Dafny.Program("dummy", dummyModuleDecl, null, reporter, Sets.Empty(), Sets.Empty()); var ghostDiagnostics = ghostStateDiagnosticCollector.GetGhostStateDiagnostics( new SignatureAndCompletionTable(null!, new CompilationUnit(rootUri, program), null!, null!, new IntervalTree(), true) diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index ff342e00ee2..e34315f203a 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -92,7 +92,7 @@ private Dafny.Program NewDafnyProgram(TextDocumentItem document, ErrorReporter e new LiteralModuleDecl(errorReporter.OuterModule, null), // BuiltIns cannot be initialized without Type.ResetScopes() before. new BuiltIns(errorReporter.Options), - errorReporter + errorReporter, Sets.Empty(), Sets.Empty() ); } @@ -114,7 +114,7 @@ CancellationToken cancellationToken // A HashSet must not be used here since equals treats A included by B not equal to A included by C. // In contrast, the compareTo-Method treats them as the same. var resolvedIncludes = new SortedSet(); - resolvedIncludes.Add(new Include(Token.NoToken, root.ToUri(), root.ToString(), false)); + resolvedIncludes.Add(new Include(Token.NoToken, root.ToUri(), root.ToString())); bool newIncludeParsed = true; while (newIncludeParsed) { @@ -140,13 +140,11 @@ private bool TryParseInclude(Include include, ModuleDecl module, BuiltIns builtI try { var dafnyFile = new DafnyFile(builtIns.Options, include.IncludedFilename); int errorCount = Parser.Parse( - (TextReader)null!, + dafnyFile.Content, dafnyFile.Uri, module, builtIns, - errors, - verifyThisFile: false, - compileThisFile: false + errors ); if (errorCount != 0) { return false; diff --git a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs b/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs index 0164627b458..759d7341b82 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs @@ -52,7 +52,7 @@ public static SignatureAndCompletionTable Empty(DafnyOptions options, DocumentTe new LiteralModuleDecl(outerModule, null), // BuiltIns cannot be initialized without Type.ResetScopes() before. new BuiltIns(options), // TODO creating a BuiltIns is a heavy operation - errorReporter + errorReporter, Sets.Empty(), Sets.Empty() )), new Dictionary(), new Dictionary(), diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index aab142263fd..0af51e22af4 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -60,7 +60,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString Microsoft.Dafny.Type.ResetScopes(); BuiltIns builtIns = new BuiltIns(options); Parser.Parse(programNotIndented, uri, module, builtIns, reporter); - var dafnyProgram = new Program("programName", module, builtIns, reporter); + var dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; @@ -99,7 +99,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString Microsoft.Dafny.Type.ResetScopes(); builtIns = new BuiltIns(options); Parser.Parse(reprinted, uri, module, builtIns, reporter); - dafnyProgram = new Program("programName", module, builtIns, reporter); + dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); var newReporter = (BatchErrorReporter)dafnyProgram.Reporter; Assert.Equal(initErrorCount, newReporter.ErrorCount); diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index 93e6190a14c..6249374202b 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -79,7 +79,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption var module = new LiteralModuleDecl(defaultModuleDefinition, null); BatchErrorReporter reporter = new BatchErrorReporter(options, defaultModuleDefinition); var builtIns = new BuiltIns(options); - var dafnyProgram = new Program("programName", module, builtIns, reporter); + var dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); Parser.Parse(program, uri, module, builtIns, reporter); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 51ddc093398..d4e6c4313ae 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -45,9 +45,9 @@ private bool Parse() { reporter = new ConsoleErrorReporter(options, defaultModuleDefinition); BuiltIns builtIns = new BuiltIns(options); var success = (Parser.Parse(source, uri, module, builtIns, new Errors(reporter)) == 0 && - DafnyMain.ParseIncludesDepthFirstNotCompiledFirst(Console.In, module, builtIns, new HashSet(), new Errors(reporter)) == null); + DafnyMain.ParseIncludes(module, builtIns, new HashSet(), new Errors(reporter)) == null); if (success) { - dafnyProgram = new Program(fname, module, builtIns, reporter); + dafnyProgram = new Program(fname, module, builtIns, reporter, Sets.Empty(), Sets.Empty()); } return success; } diff --git a/Source/DafnyServer/SignatureAndCompletionTable.cs b/Source/DafnyServer/SignatureAndCompletionTable.cs index 88ee1c4f0e6..b4d163853fe 100644 --- a/Source/DafnyServer/SignatureAndCompletionTable.cs +++ b/Source/DafnyServer/SignatureAndCompletionTable.cs @@ -30,7 +30,7 @@ public List CalculateSymbols() { private void AddMethods(ModuleDefinition module, List information) { foreach (var clbl in ModuleDefinition.AllCallables(module.TopLevelDecls). - Where(e => e != null && !e.Tok.WasIncluded(_dafnyProgram))) { + Where(e => e != null && !e.Tok.FromIncludeDirective(_dafnyProgram))) { if (clbl is Predicate) { var predicate = clbl as Predicate; @@ -87,7 +87,7 @@ private void AddMethods(ModuleDefinition module, List informa private void AddFields(ModuleDefinition module, List information) { foreach (var fs in ModuleDefinition.AllFields(module.TopLevelDecls). - Where(e => e != null && !e.Tok.WasIncluded(_dafnyProgram))) { + Where(e => e != null && !e.Tok.FromIncludeDirective(_dafnyProgram))) { var fieldSymbol = new SymbolInformation { Module = fs.EnclosingClass.EnclosingModuleDefinition.Name, @@ -108,7 +108,7 @@ private void AddFields(ModuleDefinition module, List informat private void AddClasses(ModuleDefinition module, List information) { foreach (var cs in ModuleDefinition.AllClasses(module.TopLevelDecls). - Where(cl => !cl.Tok.WasIncluded(_dafnyProgram))) { + Where(cl => !cl.Tok.FromIncludeDirective(_dafnyProgram))) { if (cs.EnclosingModuleDefinition != null && cs.tok != null) { var classSymbol = new SymbolInformation { Module = cs.EnclosingModuleDefinition.Name, @@ -255,7 +255,7 @@ private List FindFieldReferencesInternal(string fieldName, foreach (var module in _dafnyProgram.Modules()) { foreach (var clbl in ModuleDefinition.AllCallables(module.TopLevelDecls). - Where(e => !e.Tok.WasIncluded(_dafnyProgram))) { + Where(e => !e.Tok.FromIncludeDirective(_dafnyProgram))) { if (!(clbl is Method)) { continue; } @@ -274,7 +274,7 @@ private List FindMethodReferencesInternal(string methodToF foreach (var module in _dafnyProgram.Modules()) { foreach (var clbl in ModuleDefinition.AllCallables(module.TopLevelDecls). - Where(e => !e.Tok.WasIncluded(_dafnyProgram))) { + Where(e => !e.Tok.FromIncludeDirective(_dafnyProgram))) { if (!(clbl is Method)) { continue; } diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs index 70095f6b375..a4e3a68d5fc 100644 --- a/Source/DafnyTestGeneration/DafnyInfo.cs +++ b/Source/DafnyTestGeneration/DafnyInfo.cs @@ -140,7 +140,7 @@ private uint GetTestInlineAttributeValue(MemberDecl callable) { while (attributes != null) { if (attributes.Name == TestGenerationOptions.TestInlineAttribute) { if (attributes.Args.Count != 1) { - Options.Printer.ErrorWriteLine(Console.Error, + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: :{TestGenerationOptions.TestInlineAttribute} " + $"attribute must be followed by a positive integer to specify " + $"the recursion unrolling limit (one means no unrolling)"); @@ -150,7 +150,7 @@ private uint GetTestInlineAttributeValue(MemberDecl callable) { if (uint.TryParse(attributes.Args.First().ToString(), out uint result) && result > 0) { return result; } - Options.Printer.ErrorWriteLine(Console.Error, + Options.Printer.ErrorWriteLine(Options.ErrorWriter, $"*** Error: {TestGenerationOptions.TestInlineAttribute} value " + $"on {callable.FullName} must be a positive integer"); SetNonZeroExitCode = true; diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 7f82b966cfd..8ca6392701d 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -80,9 +80,9 @@ public static Type CopyWithReplacements(Type type, List from, List var builtIns = new BuiltIns(options); var reporter = new BatchErrorReporter(options, defaultModuleDefinition); var success = Parser.Parse(source, uri, module, builtIns, - new Errors(reporter)) == 0 && DafnyMain.ParseIncludesDepthFirstNotCompiledFirst(options.Input, module, builtIns, + new Errors(reporter)) == 0 && DafnyMain.ParseIncludes(module, builtIns, new HashSet(), new Errors(reporter)) == null; - var program = new Program(uri.LocalPath, module, builtIns, reporter); + var program = new Program(uri.LocalPath, module, builtIns, reporter, Sets.Empty(), Sets.Empty()); if (!resolve) { return program; diff --git a/Test/auditor/TestAuditor.dfy b/Test/auditor/TestAuditor.dfy index 3cdb6373673..09f0b55df21 100644 --- a/Test/auditor/TestAuditor.dfy +++ b/Test/auditor/TestAuditor.dfy @@ -2,11 +2,11 @@ // RUN: %baredafny audit --report-file "%t.md" --compare-report "%s" // RUN: %baredafny audit --report-file "%t.html" "%s" // RUN: %baredafny audit --report-file "%t-ietf.md" --report-format markdown-ietf "%s" -// RUN: %baredafny audit --use-basename-for-filename "%s" > "%t.expect" +// RUN: %baredafny audit --use-basename-for-filename "%s" > "%t" // RUN: %diff "%s.md.expect" "%t.md" // RUN: %diff "%s-ietf.md.expect" "%t-ietf.md" // RUN: %diff "%s.html.expect" "%t.html" -// RUN: %diff "%s.expect" %t.expect" +// RUN: %diff "%s.expect" %t" include "IgnoredAssumptions.dfy" diff --git a/Test/dafny0/formatting2.dfy.expect b/Test/dafny0/formatting2.dfy.expect index 37ea122d24b..598a0ecd8ac 100644 --- a/Test/dafny0/formatting2.dfy.expect +++ b/Test/dafny0/formatting2.dfy.expect @@ -1,4 +1 @@ -(0,-1): Error: Unable to open included file - -1 file failed to parse: - unexisting.dfy +*** Error: file /unexisting.dfy not found From c9c071d04614db9461dec9a17d8c3a687c324dd5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 22 May 2023 11:11:07 +0200 Subject: [PATCH 02/68] Fix test --- Test/dafny0/formatting2.dfy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Test/dafny0/formatting2.dfy b/Test/dafny0/formatting2.dfy index 17a57e4f54d..d266761ff07 100644 --- a/Test/dafny0/formatting2.dfy +++ b/Test/dafny0/formatting2.dfy @@ -1,4 +1,5 @@ -// RUN: %exits-with 2 %baredafny format --use-basename-for-filename --print "unexisting.dfy" > "%t" +// RUN: %exits-with 1 %baredafny format --use-basename-for-filename --print "%S/unexisting.dfy" > "%t.raw" +// RUN: %sed 's#%S##g' "%t.raw" > "%t" // RUN: %diff "%s.expect" "%t" module A { From 1b1908b77b4b69dfbba58148790ceaaf0195ee3d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 22 May 2023 11:13:25 +0200 Subject: [PATCH 03/68] Add TODOs --- Source/DafnyCore/AST/DafnyAst.cs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 5b6da191136..9f5a2c755a9 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -39,12 +39,16 @@ void ObjectInvariant() { Contract.Invariant(DefaultModule != null); } + // TODO move to Compilation once that's used by the CLI public ISet AlreadyVerifiedRoots; + // TODO move to Compilation once that's used by the CLI public ISet AlreadyCompiledRoots; public List Includes => DefaultModuleDef.Includes; + // TODO move to DocumentAfterParsing once that's used by the CLI [FilledInDuringResolution] public ISet UrisToVerify; + // TODO move to DocumentAfterParsing once that's used by the CLI [FilledInDuringResolution] public ISet UrisToCompile; From 3f0b3c5a72443a9a80f45f6efbfb7c92d8127324 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 22 May 2023 14:58:52 +0200 Subject: [PATCH 04/68] Return a module after parsing, insteadf of mutating one --- Source/DafnyCore.Test/DooFileTest.cs | 2 +- Source/DafnyCore/AST/BuiltIns.cs | 2 +- Source/DafnyCore/AST/Cloner.cs | 18 +-- Source/DafnyCore/AST/DafnyAst.cs | 18 +-- Source/DafnyCore/AST/FileModuleDefinition.cs | 14 ++ Source/DafnyCore/AST/Grammar/ParseUtils.cs | 87 +++++++++++ Source/DafnyCore/AST/ShouldCompileOrVerify.cs | 2 +- Source/DafnyCore/AST/Tokens.cs | 2 +- Source/DafnyCore/AST/TopLevelDeclarations.cs | 56 +++++-- Source/DafnyCore/Dafny.atg | 118 ++------------- Source/DafnyCore/DafnyFile.cs | 2 + Source/DafnyCore/DafnyMain.cs | 13 +- Source/DafnyCore/Generic/Reporting.cs | 2 +- .../DafnyDriver/Commands/CommandRegistry.cs | 2 +- .../Lookup/DefinitionTest.cs | 3 +- .../Language/DafnyLangParser.cs | 137 ++++++++++++------ .../Workspace/SymbolTable.cs | 6 +- .../DafnyPipeline.Test/FormatterBaseTest.cs | 4 +- Source/DafnyPipeline.Test/TranslatorTest.cs | 2 +- Source/DafnyServer/DafnyHelper.cs | 2 +- Source/DafnyTestGeneration/Utils.cs | 3 +- 21 files changed, 284 insertions(+), 211 deletions(-) create mode 100644 Source/DafnyCore/AST/FileModuleDefinition.cs create mode 100644 Source/DafnyCore/AST/Grammar/ParseUtils.cs diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs index 2fb4a01cae0..fbbbfb9c3c5 100644 --- a/Source/DafnyCore.Test/DooFileTest.cs +++ b/Source/DafnyCore.Test/DooFileTest.cs @@ -36,7 +36,7 @@ private static Program ParseProgram(string dafnyProgramText, DafnyOptions option Microsoft.Dafny.Type.ResetScopes(); var builtIns = new BuiltIns(options); var errorReporter = new ConsoleErrorReporter(options, outerModule); - var parseResult = Parser.Parse(dafnyProgramText, rootUri, module, builtIns, errorReporter); + var parseResult = ParseUtils.Parse(dafnyProgramText, rootUri, module, builtIns, errorReporter); Assert.Equal(0, parseResult); return new Program(fullFilePath, module, builtIns, errorReporter, Sets.Empty(), Sets.Empty()); } diff --git a/Source/DafnyCore/AST/BuiltIns.cs b/Source/DafnyCore/AST/BuiltIns.cs index 9c889d67b17..0fc489c0e54 100644 --- a/Source/DafnyCore/AST/BuiltIns.cs +++ b/Source/DafnyCore/AST/BuiltIns.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny; public class BuiltIns { public DafnyOptions Options { get; } - public readonly ModuleDefinition SystemModule = new ModuleDefinition(RangeToken.NoToken, new Name("_System"), new List(), false, false, null, null, null, true); + public readonly ModuleDefinition SystemModule = new(RangeToken.NoToken, new Name("_System"), new List(), false, false, null, null, null, true); internal readonly Dictionary arrayTypeDecls = new Dictionary(); public readonly Dictionary ArrowTypeDecls = new Dictionary(); public readonly Dictionary PartialArrowTypeDecls = new Dictionary(); // same keys as arrowTypeDecl diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 6fa6f4f321f..15e9b8af2a0 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -30,23 +30,11 @@ public Cloner(bool cloneResolvedFields = false) { } public virtual ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) { - ModuleDefinition nw; if (m is DefaultModuleDefinition defaultModuleDefinition) { - nw = new DefaultModuleDefinition(defaultModuleDefinition.RootSourceUris); - } else { - nw = new ModuleDefinition(Range(m.RangeToken), name, m.PrefixIds, m.IsAbstract, m.IsFacade, - m.RefinementQId, m.EnclosingModule, CloneAttributes(m.Attributes), - true); - } - foreach (var d in m.TopLevelDecls) { - nw.TopLevelDecls.Add(CloneDeclaration(d, nw)); + return new DefaultModuleDefinition(this, defaultModuleDefinition); } - foreach (var tup in m.PrefixNamedModules) { - var newTup = new Tuple, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)CloneDeclaration(tup.Item2, nw)); - nw.PrefixNamedModules.Add(newTup); - } - nw.Height = m.Height; - return nw; + + return new ModuleDefinition(this, m, name); } public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) { diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 9f5a2c755a9..177ebb7084b 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -39,16 +39,13 @@ void ObjectInvariant() { Contract.Invariant(DefaultModule != null); } - // TODO move to Compilation once that's used by the CLI public ISet AlreadyVerifiedRoots; - // TODO move to Compilation once that's used by the CLI public ISet AlreadyCompiledRoots; + // TODO remove? public List Includes => DefaultModuleDef.Includes; - // TODO move to DocumentAfterParsing once that's used by the CLI [FilledInDuringResolution] public ISet UrisToVerify; - // TODO move to DocumentAfterParsing once that's used by the CLI [FilledInDuringResolution] public ISet UrisToCompile; @@ -110,13 +107,14 @@ public string Name { /// Get the first token that is in the same file as the DefaultModule.RootToken.FileName /// (skips included tokens) public IToken GetFirstTopLevelToken() { - if (DefaultModule.RootToken.Next == null) { + var rootToken = DefaultModule.RangeToken.StartToken; + if (rootToken.Next == null) { return null; } - var firstToken = DefaultModule.RootToken.Next; + var firstToken = rootToken.Next; // We skip all included files - while (firstToken is { Next: { } } && firstToken.Next.Filepath != DefaultModule.RootToken.Filepath) { + while (firstToken is { Next: { } } && firstToken.Next.Filepath != rootToken.Filepath) { firstToken = firstToken.Next; } @@ -138,15 +136,15 @@ public override IEnumerable Assumptions(Declaration decl) { public class Include : TokenNode, IComparable { public Uri IncluderFilename { get; } - public string IncludedFilename { get; } + public Uri IncludedFilename { get; } public string CanonicalPath { get; } public bool ErrorReported; - public Include(IToken tok, Uri includer, string theFilename) { + public Include(IToken tok, Uri includer, Uri theFilename) { this.tok = tok; this.IncluderFilename = includer; this.IncludedFilename = theFilename; - this.CanonicalPath = DafnyFile.Canonicalize(theFilename).LocalPath; + this.CanonicalPath = DafnyFile.Canonicalize(theFilename.LocalPath).LocalPath; this.ErrorReported = false; } diff --git a/Source/DafnyCore/AST/FileModuleDefinition.cs b/Source/DafnyCore/AST/FileModuleDefinition.cs new file mode 100644 index 00000000000..70c204b5e9b --- /dev/null +++ b/Source/DafnyCore/AST/FileModuleDefinition.cs @@ -0,0 +1,14 @@ +using System.Collections.Generic; + +namespace Microsoft.Dafny; + +public class FileModuleDefinition : ModuleDefinition { + public List Includes { get; } = new(); + + public FileModuleDefinition() : + base(RangeToken.NoToken, new Name("_module"), new List(), + false, false, null, null, null, true) { + { + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs new file mode 100644 index 00000000000..cb4746c03ef --- /dev/null +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -0,0 +1,87 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.IO; +using System.Text; + +namespace Microsoft.Dafny; + +public record DfyParseResult(int ErrorCount, FileModuleDefinition Module); + +public class ParseUtils { + + /// + /// Parses top-level things (modules, classes, datatypes, class members) from "filename" + /// and appends them in appropriate form to "module". + /// Returns the number of parsing errors encountered. + /// Note: first initialize the Scanner. + /// + public static DfyParseResult Parse(TextReader reader, Uri /*!*/ uri, BuiltIns builtIns, + Errors /*!*/ errors) /* throws System.IO.IOException */ { + Contract.Requires(uri != null); + var text = SourcePreprocessor.ProcessDirectives(reader, new List()); + return Parse(text, uri, builtIns, errors); + } + + /// + /// Parses top-level things (modules, classes, datatypes, class members) + /// and appends them in appropriate form to "module". + /// Returns the number of parsing errors encountered. + /// Note: first initialize the Scanner. + /// + public static DfyParseResult Parse(string /*!*/ s, Uri /*!*/ uri, BuiltIns builtIns, ErrorReporter reporter) { + Contract.Requires(s != null); + Contract.Requires(uri != null); + Errors errors = new Errors(reporter); + return Parse(s, uri, builtIns, errors); + } + + /// + /// Parses top-level things (modules, classes, datatypes, class members) + /// and appends them in appropriate form to "module". + /// Returns the number of parsing errors encountered. + /// Note: first initialize the Scanner with the given Errors sink. + /// + public static DfyParseResult Parse(string /*!*/ s, Uri /*!*/ uri, + BuiltIns builtIns, Errors /*!*/ errors) { + Parser parser = SetupParser(s, uri, builtIns, errors); + parser.Parse(); + + if (parser.theModule.DefaultClass.Members.Count == 0 && parser.theModule.Includes.Count == 0 && parser.theModule.TopLevelDecls.Count == 1 + && (parser.theModule.PrefixNamedModules == null || parser.theModule.PrefixNamedModules.Count == 0)) { + errors.Warning(new Token(1, 1) { Uri = uri }, "File contains no code"); + } + + return new DfyParseResult(parser.errors.ErrorCount, parser.theModule); + } + + public static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, + BuiltIns builtIns, Errors /*!*/ errors) { + Contract.Requires(s != null); + Contract.Requires(uri != null); + Contract.Requires(errors != null); + System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle); + System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ResolutionErrors).TypeHandle); + byte[] /*!*/ + buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s)); + MemoryStream ms = new MemoryStream(buffer, false); + var firstToken = new Token { + Uri = uri + }; + + // if ((module.RootToken.Filepath ?? "") == "") { + // // This is the first module + // module.RootToken.Uri = uri; + // firstToken = module.RootToken; + // } else { + // firstToken = new Token(); // It's an included file + // } + + Scanner scanner = new Scanner(ms, errors, uri, firstToken: firstToken); + return new Parser(scanner, errors, builtIns); + } + + public static int Parse(string source, Uri uri, LiteralModuleDecl builtIns, BuiltIns reporter, ErrorReporter errorReporter) { + throw new NotImplementedException(); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs index eae9cbf80a4..b77edbad58a 100644 --- a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs +++ b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs @@ -79,7 +79,7 @@ private static ISet GetReachableUris(Program program, ISet stopUris) { var visited = new HashSet(); var edges = program.Includes.GroupBy(i => i.IncluderFilename) - .ToDictionary(g => g.Key, g => g.Select(i => new Uri(i.IncludedFilename)).ToList()); + .ToDictionary(g => g.Key, g => g.Select(x => x.IncludedFilename).ToList()); while (toVisit.Any()) { var uri = toVisit.Pop(); if (stopUris.Contains(uri)) { diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index 0c8cf0f57be..54f9e522a14 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -56,7 +56,7 @@ string Boogie.IToken.filename { public class Token : IToken { public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normallly null at the end of parsing - public static readonly IToken NoToken = new Token(); + public static readonly Token NoToken = new Token(); static Token() { NoToken.Next = NoToken; diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index de2184d949d..b00a2f29411 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -4,6 +4,7 @@ using System.Diagnostics.Contracts; using System.Numerics; using System.Linq; +using System.Xml; using Microsoft.Dafny.Auditor; namespace Microsoft.Dafny; @@ -387,7 +388,6 @@ public virtual ModuleSignature AccessibleSignature() { return Signature; } public int Height; - public Token RootToken = new Token(); public readonly bool Opened; @@ -849,9 +849,6 @@ public string FullName { public ModuleQualifiedId RefinementQId; // full qualified ID of the refinement parent, null if no refinement base public bool SuccessfullyResolved; // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved - // TODO move to Program once this list is no longer mutated by parsing. - public List Includes; - [FilledInDuringResolution] public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that, except for the addition of prefix-named modules, which happens in the resolver [FilledInDuringResolution] public readonly List, LiteralModuleDecl>> PrefixNamedModules = new List, LiteralModuleDecl>>(); // filled in by the parser; emptied by the resolver [FilledInDuringResolution] public readonly Graph CallGraph = new Graph(); @@ -860,14 +857,24 @@ public string FullName { public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface) private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled. - public int? ResolvedHash { get; set; } - [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(TopLevelDecls)); Contract.Invariant(CallGraph != null); } + public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : base(cloner, original) { + NameNode = name; + foreach (var d in original.TopLevelDecls) { + TopLevelDecls.Add(cloner.CloneDeclaration(d, this)); + } + foreach (var tup in original.PrefixNamedModules) { + var newTup = new Tuple, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)cloner.CloneDeclaration(tup.Item2, this)); + PrefixNamedModules.Add(newTup); + } + Height = original.Height; + } + public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool isAbstract, bool isFacade, ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, bool isBuiltinName) : base(tok) { Contract.Requires(tok != null); @@ -879,10 +886,16 @@ public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool this.RefinementQId = refinementQId; this.IsAbstract = isAbstract; this.IsFacade = isFacade; - this.Includes = new List(); this.IsBuiltinName = isBuiltinName; + + if (Name != "_System") { + DefaultClass = new DefaultClassDecl(this, new List()); + TopLevelDecls.Add(DefaultClass); + } } + public DefaultClassDecl DefaultClass { get; set; } + VisibilityScope visibilityScope; public VisibilityScope VisibilityScope => visibilityScope ??= new VisibilityScope(this.SanitizedName); @@ -1111,7 +1124,7 @@ public IToken GetFirstTopLevelToken() { includes[0].OwnedTokens.Any()) { return includes[0].OwnedTokens.First(); } - IEnumerable topTokens = TopLevelDecls.SelectMany(decl => { + IEnumerable topTokens = TopLevelDecls.SelectMany(decl => { if (decl.StartToken.line > 0) { return new List() { decl.StartToken }; } else if (decl is TopLevelDeclWithMembers declWithMembers) { @@ -1137,8 +1150,11 @@ public IToken GetFirstTopLevelToken() { private IEnumerable preResolveTopLevelDecls; private IEnumerable preResolvePrefixNamedModules; + public override IEnumerable PreResolveChildren => - Includes.Concat(Attributes != null ? + //Includes. + Enumerable.Empty(). // TODO refactor + Concat(Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat(preResolveTopLevelDecls ?? TopLevelDecls).Concat( (preResolvePrefixNamedModules ?? PrefixNamedModules.Select(tuple => tuple.Item2))); @@ -1156,7 +1172,14 @@ public override IEnumerable Assumptions(Declaration decl) { public class DefaultModuleDefinition : ModuleDefinition { + // TODO remove??? + public List Includes { get; } = new(); public IList RootSourceUris { get; } + + public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original) : base(cloner, original, original.NameNode) { + RootSourceUris = original.RootSourceUris; + } + public DefaultModuleDefinition(IList rootSourceUris) : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, null, null, null, true) { RootSourceUris = rootSourceUris; @@ -1274,10 +1297,11 @@ public virtual bool IsEssentiallyEmpty() { public abstract class TopLevelDeclWithMembers : TopLevelDecl { public readonly List Members; - public readonly ImmutableList MembersBeforeResolution; + // TODO remove this and instead clone the AST after parsing. + public ImmutableList MembersBeforeResolution; // The following fields keep track of parent traits - public readonly List InheritedMembers = new List(); // these are instance members declared in parent traits + public readonly List InheritedMembers = new(); // these are instance members declared in parent traits public readonly List ParentTraits; // these are the types that are parsed after the keyword 'extends'; note, for a successfully resolved program, these are UserDefinedType's where .ResolvedClass is NonNullTypeDecl public readonly Dictionary ParentFormalTypeParametersToActuals = new Dictionary(); // maps parent traits' type parameters to actuals @@ -1338,15 +1362,21 @@ public void Extend(TraitDecl parent, InheritanceInformationClass parentInfo, Dic } } - protected TopLevelDeclWithMembers(RangeToken rangeToken, Name name, ModuleDefinition module, List typeArgs, List members, Attributes attributes, bool isRefining, List/*?*/ traits = null) + protected TopLevelDeclWithMembers(RangeToken rangeToken, Name name, ModuleDefinition module, + List typeArgs, List members, Attributes attributes, + bool isRefining, List/*?*/ traits = null) : base(rangeToken, name, module, typeArgs, attributes, isRefining) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(members)); Members = members; - MembersBeforeResolution = members.ToImmutableList(); ParentTraits = traits ?? new List(); + SetMembersBeforeResolution(); + } + + public void SetMembersBeforeResolution() { + MembersBeforeResolution = Members.ToImmutableList(); } public static List CommonTraits(TopLevelDeclWithMembers a, TopLevelDeclWithMembers b) { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 8ca56aa9aee..5cafea9a7fb 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -26,7 +26,7 @@ readonly AssignmentRhs/*!*/ dummyRhs; readonly FrameExpression/*!*/ dummyFrameExpr; readonly Statement/*!*/ dummyStmt; readonly Statement/*!*/ dummyIfStmt; -readonly ModuleDecl theModule; +public readonly FileModuleDefinition theModule; readonly BuiltIns theBuiltIns; DafnyOptions theOptions; int anonymousIds = 0; @@ -140,65 +140,6 @@ bool IsAssumeTypeKeyword(IToken la) { return la.kind == _assume || la.kind == _assert || la.kind == _expect; } -/// -/// Parses top-level things (modules, classes, datatypes, class members) from "filename" -/// and appends them in appropriate form to "module". -/// Returns the number of parsing errors encountered. -/// Note: first initialize the Scanner. -/// -public static int Parse(TextReader reader, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors) /* throws System.IO.IOException */ { - Contract.Requires(uri != null); - Contract.Requires(module != null); - var text = Microsoft.Dafny.SourcePreprocessor.ProcessDirectives(reader, new List()); - return Parse(text, uri, module, builtIns, errors); -} - -/// -/// Parses top-level things (modules, classes, datatypes, class members) -/// and appends them in appropriate form to "module". -/// Returns the number of parsing errors encountered. -/// Note: first initialize the Scanner. -/// -public static int Parse(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, BuiltIns builtIns, ErrorReporter reporter) { - Contract.Requires(s != null); - Contract.Requires(uri != null); - Contract.Requires(module != null); - Errors errors = new Errors(reporter); - return Parse(s, uri, module, builtIns, errors); -} - -public static Parser SetupParser(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, - BuiltIns builtIns, Errors/*!*/ errors) { - Contract.Requires(s != null); - Contract.Requires(uri != null); - Contract.Requires(module != null); - Contract.Requires(errors != null); - System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle); - System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ResolutionErrors).TypeHandle); - byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s)); - MemoryStream ms = new MemoryStream(buffer,false); - Token firstToken; - if((module.RootToken.Filepath ?? "") == "") { // This is the first module - module.RootToken.Uri = uri; - firstToken = module.RootToken; - } else { - firstToken = new Token(); // It's an included file - } - Scanner scanner = new Scanner(ms, errors, uri, firstToken: firstToken); - return new Parser(scanner, errors, module, builtIns); -} - -public static Expression ParseExpression(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, - BuiltIns builtIns, Errors/*!*/ errors) { - Parser parser = SetupParser(s, uri, module, builtIns, errors); - parser.la = new Token(); - parser.la.val = ""; - parser.Get(); - Expression e; - parser.Expression(out e, true, true, true); - return e; -} - public void ApplyOptionsFromAttributes(Attributes attrs) { var overrides = attrs.AsEnumerable().Where(a => a.Name == "options") .Reverse().Select(a => @@ -237,20 +178,7 @@ public void ApplyOptionsFromAttributes(Attributes attrs) { } } -/// -/// Parses top-level things (modules, classes, datatypes, class members) -/// and appends them in appropriate form to "module". -/// Returns the number of parsing errors encountered. -/// Note: first initialize the Scanner with the given Errors sink. -/// -public static int Parse(string/*!*/ s, Uri/*!*/ uri, ModuleDecl module, - BuiltIns builtIns, Errors/*!*/ errors) { - Parser parser = SetupParser(s, uri, module, builtIns, errors); - parser.Parse(); - return parser.errors.ErrorCount; -} - -public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns) +public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, BuiltIns builtIns) : this(scanner, errors) // the real work { // initialize readonly fields @@ -260,7 +188,8 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, Built dummyStmt = new ReturnStmt(Token.NoToken.ToRange(), null); var dummyBlockStmt = new BlockStmt(Token.NoToken.ToRange(), new List()); dummyIfStmt = new IfStmt(Token.NoToken.ToRange(), false, null, dummyBlockStmt, null); - theModule = module; + + theModule = new FileModuleDefinition(); theBuiltIns = builtIns; theOptions = new DafnyOptions(builtIns.Options); } @@ -1001,12 +930,7 @@ IGNORE cr + lf + tab /*------------------------------------------------------------------------*/ PRODUCTIONS Dafny -= (. List membersDefaultClass = new List(); - // to support multiple files, create a default module only if theModule is null - DefaultModuleDefinition defaultModule = (DefaultModuleDefinition)((LiteralModuleDecl)theModule).ModuleDef; - // theModule should be a DefaultModuleDefinition (actually, the singular DefaultModuleDefinition) - Contract.Assert(defaultModule != null); - IToken startToken = t; += (. IToken startToken = t; .) { "include" (. startToken = t; .) stringToken (. { @@ -1021,30 +945,14 @@ Dafny } var oneInclude = new Include(t, parsedFile, includedFile); oneInclude.RangeToken = new RangeToken(startToken, t); - defaultModule.Includes.Add(oneInclude); + theModule.Includes.Add(oneInclude); } .) } - { TopDecl } + { TopDecl } (. - defaultModule.RangeToken = new RangeToken(startToken, t); - // find the default class in the default module, then append membersDefaultClass to its member list - if (membersDefaultClass.Count == 0 && defaultModule.Includes.Count == 0 && defaultModule.TopLevelDecls.Count == 0 - && (defaultModule.PrefixNamedModules == null || defaultModule.PrefixNamedModules.Count == 0)) { - errors.Warning(new Token(1, 1) { Uri = la.Uri }, "File contains no code"); - } - DefaultClassDecl defaultClass = null; - foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) { - defaultClass = topleveldecl as DefaultClassDecl; - if (defaultClass != null) { - defaultClass.Members.AddRange(membersDefaultClass); - break; - } - } - if (defaultClass == null) { // create the default class here, because it wasn't found - defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass); - defaultModule.TopLevelDecls.Add(defaultClass); - } .) + theModule.RangeToken = new RangeToken(startToken, t); + .) SYNC EOF . @@ -1059,7 +967,7 @@ DeclModifier . /*------------------------------------------------------------------------*/ -TopDecl<. ModuleDefinition module, List membersDefaultClass, bool isTopLevel, bool isAbstract .> +TopDecl<. ModuleDefinition module, bool isTopLevel, bool isAbstract .> = (. DeclModifierData dmod = new DeclModifierData(); ModuleDecl submodule; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter; TraitDecl/*!*/ trait; @@ -1080,7 +988,7 @@ TopDecl<. ModuleDefinition module, List membersDefaultClass, bo | SynonymTypeDecl (. module.TopLevelDecls.Add(td); .) | IteratorDecl (. module.TopLevelDecls.Add(iter); .) | TraitDecl (. module.TopLevelDecls.Add(trait); .) - | ClassMemberDecl + | ClassMemberDecl ) . @@ -1105,7 +1013,6 @@ ModuleDefinition(); - List namedModuleDefaultClassMembers = new List();; List idRefined = null; ModuleDefinition module; submodule = null; // appease compiler @@ -1128,11 +1035,10 @@ ModuleDefinition} + { TopDecl} "}" (. module.RangeToken = new RangeToken(dmod.FirstToken, t); - module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); module.TokenWithTrailingDocString = tokenWithTrailingDocString; submodule = new LiteralModuleDecl(module, parent); submodule.RangeToken = module.RangeToken; diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index 4c0f3b97621..f9e582dcef0 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -16,6 +16,8 @@ public class DafnyFile { public bool IsPrecompiled { get; set; } public TextReader Content { get; } public Uri Uri { get; } + + // TODO take a Uri instead of a filePath public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverride = null) { UseStdin = contentOverride != null; Uri = contentOverride != null ? new Uri("stdin:///") : new Uri(filePath); diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index c7a7d51a761..41a678ae3e3 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -84,10 +84,10 @@ public static string Parse(TextReader stdIn, IList files, string prog Uri = dafnyFile.Uri, col = 1, line = 0 - }, new Uri("cli://"), dafnyFile.FilePath) : null; + }, new Uri("cli://"), dafnyFile.Uri) : null; if (include != null) { // TODO this can be removed once the include error message in ErrorReporter.Error is removed. - module.ModuleDef.Includes.Add(include); + defaultModuleDefinition.Includes.Add(include); } var err = ParseFile(dafnyFile, null, module, builtIns, new Errors(reporter)); if (err != null) { @@ -104,7 +104,7 @@ public static string Parse(TextReader stdIn, IList files, string prog if (options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate) { DependencyMap dmap = new DependencyMap(); - dmap.AddIncludes(module.ModuleDef.Includes); + dmap.AddIncludes(defaultModuleDefinition.Includes); dmap.PrintMap(options); } @@ -149,7 +149,7 @@ public int Compare(Include x, Include y) { public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, ISet excludeFiles, Errors errs) { var includesFound = new SortedSet(new IncludeComparer()); - var allIncludes = ((LiteralModuleDecl)module).ModuleDef.Includes; + var allIncludes = ((DefaultModuleDefinition)((LiteralModuleDecl)module).ModuleDef).Includes; var notCompiledResult = TraverseIncludesFrom(0); if (notCompiledResult != null) { @@ -187,7 +187,7 @@ string TraverseIncludesFrom(int startingIndex) { DafnyFile file; try { - file = new DafnyFile(builtIns.Options, include.IncludedFilename); + file = new DafnyFile(builtIns.Options, include.IncludedFilename.LocalPath); } catch (IllegalDafnyFile) { return ($"Include of file \"{include.IncludedFilename}\" failed."); } @@ -205,7 +205,8 @@ string TraverseIncludesFrom(int startingIndex) { private static string ParseFile(DafnyFile dafnyFile, Include include, ModuleDecl module, BuiltIns builtIns, Errors errs) { var fn = builtIns.Options.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath; try { - int errorCount = Parser.Parse(dafnyFile.Content, dafnyFile.Uri, module, builtIns, errs); + var parseResult = ParseUtils.Parse(dafnyFile.Content, dafnyFile.Uri, builtIns, errs); + var errorCount = parseResult.ErrorCount; if (errorCount != 0) { return $"{errorCount} parse errors detected in {fn}"; } diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index 00021c34bc1..3f6fc8eab6e 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -47,7 +47,7 @@ public virtual void Error(MessageSource source, string errorId, IToken tok, stri Contract.Requires(tok != null); Contract.Requires(msg != null); if (tok.FromIncludeDirective(OuterModule) && OuterModule != null) { - var include = OuterModule.Includes.First(i => new Uri(i.IncludedFilename).LocalPath == tok.ActualFilename); + var include = OuterModule.Includes.First(i => i.IncludedFilename == tok.Uri); if (!include.ErrorReported) { Message(source, ErrorLevel.Error, null, include.tok, "the included file " + Path.GetFileName(tok.ActualFilename) + " contains error(s)"); include.ErrorReported = true; diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 535676784f5..9202670f76e 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -53,7 +53,7 @@ static CommandRegistry() { // This SHOULD find the same method but returns null for some reason: // typeof(ParseResult).GetMethod("GetValueForOption", 1, new[] { typeof(Option<>) }); - foreach (var method in typeof(ParseResult).GetMethods()) { + foreach (var method in typeof(DfyParseResult).GetMethods()) { if (method.Name == "GetValueForOption" && method.GetGenericArguments().Length == 1) { GetValueForOptionMethod = method; } diff --git a/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs b/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs index 659711bbfac..88e8e6f4527 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs @@ -295,7 +295,8 @@ method DoIt() { }".TrimStart(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - Assert.False((await RequestDefinition(documentItem, (2, 14)).AsTask()).Any()); + var locations = await RequestDefinition(documentItem, (2, 14)).AsTask(); + Assert.False(locations.Any()); } [Fact] diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index e34315f203a..76fd6ce50d1 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -4,6 +4,7 @@ using System; using System.Collections.Generic; using System.IO; +using System.Linq; using System.Threading; using Microsoft.Boogie; using OmniSharp.Extensions.LanguageServer.Protocol; @@ -50,20 +51,25 @@ public Dafny.Program Parse(TextDocumentItem document, ErrorReporter errorReporte mutex.Wait(cancellationToken); var program = NewDafnyProgram(document, errorReporter); try { - var parseErrors = Parser.Parse( + var parseResult = ParseUtils.Parse( document.Text, // We use the full path as filename so we can better re-construct the DocumentUri for the definition lookup. document.Uri.ToUri(), - program.DefaultModule, program.BuiltIns, errorReporter ); - if (parseErrors != 0) { - logger.LogDebug("encountered {ErrorCount} errors while parsing {DocumentUri}", parseErrors, document.Uri); + if (parseResult.ErrorCount != 0) { + logger.LogDebug("encountered {ErrorCount} errors while parsing {DocumentUri}", parseResult.ErrorCount, document.Uri); } - if (!TryParseIncludesOfModule(document.Uri, program.DefaultModule, program.BuiltIns, errorReporter, cancellationToken)) { - logger.LogDebug("encountered error while parsing the includes of {DocumentUri}", document.Uri); + AddFileModuleToProgram(parseResult.Module, program); + program.DefaultModule.RangeToken = parseResult.Module.RangeToken; + + var includedModules = TryParseIncludesOfModule(document.Uri, parseResult.Module, + program.BuiltIns, errorReporter, cancellationToken); + + foreach (var module in includedModules) { + AddFileModuleToProgram(module, program); } return program; @@ -84,6 +90,31 @@ public Dafny.Program Parse(TextDocumentItem document, ErrorReporter errorReporte } } + private static void AddFileModuleToProgram(FileModuleDefinition module, Dafny.Program program) + { + foreach (var topLevelDecl in module.TopLevelDecls) + { + if (topLevelDecl is DefaultClassDecl defaultClassDecl) + { + foreach (var member in defaultClassDecl.Members) + { + program.DefaultModuleDef.DefaultClass.Members.Add(member); + } + } + else + { + program.DefaultModuleDef.TopLevelDecls.Add(topLevelDecl); + } + } + + foreach (var include in module.Includes) + { + program.Includes.Add(include); + } + + program.DefaultModuleDef.DefaultClass.SetMembersBeforeResolution(); + } + private Dafny.Program NewDafnyProgram(TextDocumentItem document, ErrorReporter errorReporter) { // Ensure that the statically kept scopes are empty when parsing a new document. Type.ResetScopes(); @@ -102,63 +133,77 @@ public void Dispose() { // TODO The following methods are based on the ones from DafnyPipeline/DafnyMain.cs. // It could be convenient to adapt them in the main-repo so location info could be extracted. - private bool TryParseIncludesOfModule( + private IList TryParseIncludesOfModule( DocumentUri root, - ModuleDecl module, + FileModuleDefinition rootModule, BuiltIns builtIns, ErrorReporter errorReporter, CancellationToken cancellationToken ) { var errors = new Errors(errorReporter); - // Issue #40: - // A HashSet must not be used here since equals treats A included by B not equal to A included by C. - // In contrast, the compareTo-Method treats them as the same. - var resolvedIncludes = new SortedSet(); - resolvedIncludes.Add(new Include(Token.NoToken, root.ToUri(), root.ToString())); - - bool newIncludeParsed = true; - while (newIncludeParsed) { + + var result = new List(); + var resolvedIncludes = new HashSet(); + resolvedIncludes.Add(root.ToUri()); + + var stack = new Stack(); + foreach (var include in rootModule.Includes) { + var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, include); + if (dafnyFile != null) { + stack.Push(dafnyFile); + } + } + + while (stack.Any()) { + var top = stack.Pop(); + if (!resolvedIncludes.Add(top.Uri)) { + continue; + } + cancellationToken.ThrowIfCancellationRequested(); - newIncludeParsed = false; - // Parser.Parse appears to modify the include list; thus, we create a copy to avoid concurrent modifications. - var moduleIncludes = new List(((LiteralModuleDecl)module).ModuleDef.Includes); - foreach (var include in moduleIncludes) { - bool isNewInclude = resolvedIncludes.Add(include); - if (isNewInclude) { - newIncludeParsed = true; - if (!TryParseInclude(include, module, builtIns, errorReporter, errors)) { - return false; - } + var parseIncludeResult = TryParseDocument(top, builtIns, errorReporter, errors); + result.Add(parseIncludeResult.Module); + + foreach (var include in parseIncludeResult.Module.Includes) { + var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, include); + if (dafnyFile != null) { + stack.Push(dafnyFile); } } } - return true; + return result; } - private bool TryParseInclude(Include include, ModuleDecl module, BuiltIns builtIns, ErrorReporter errorReporter, Errors errors) { - try { - var dafnyFile = new DafnyFile(builtIns.Options, include.IncludedFilename); - int errorCount = Parser.Parse( - dafnyFile.Content, - dafnyFile.Uri, - module, - builtIns, - errors - ); - if (errorCount != 0) { - return false; - } - } catch (IllegalDafnyFile e) { + private DafnyFile? IncludeToDafnyFile(BuiltIns builtIns, ErrorReporter errorReporter, Include include) + { + try + { + return new DafnyFile(builtIns.Options, include.IncludedFilename.LocalPath); + } + catch (IllegalDafnyFile e) + { errorReporter.Error(MessageSource.Parser, include.tok, $"Include of file '{include.IncludedFilename}' failed."); logger.LogDebug(e, "encountered include of illegal dafny file {Filename}", include.IncludedFilename); - return false; - } catch (IOException e) { - errorReporter.Error(MessageSource.Parser, include.tok, $"Unable to open the include {include.IncludedFilename}."); + return null; + } + catch (IOException e) + { + errorReporter.Error(MessageSource.Parser, include.tok, + $"Unable to open the include {include.IncludedFilename}."); logger.LogDebug(e, "could not open file {Filename}", include.IncludedFilename); - return false; + return null; } - return true; + } + + private DfyParseResult TryParseDocument(DafnyFile dafnyFile, BuiltIns builtIns, ErrorReporter errorReporter, + Errors errors) { + return ParseUtils.Parse( + dafnyFile.Content, + dafnyFile.Uri, + builtIns, + errors + ); } } } diff --git a/Source/DafnyLanguageServer/Workspace/SymbolTable.cs b/Source/DafnyLanguageServer/Workspace/SymbolTable.cs index fe7cbc4b337..bef9700c60f 100644 --- a/Source/DafnyLanguageServer/Workspace/SymbolTable.cs +++ b/Source/DafnyLanguageServer/Workspace/SymbolTable.cs @@ -21,13 +21,15 @@ private SymbolTable() { public SymbolTable(Document document, IReadOnlyList<(IDeclarationOrUsage usage, IDeclarationOrUsage declaration)> usages) { var safeUsages = usages.Where(k => k.declaration.NameToken.Uri != null).ToList(); - Declarations = safeUsages.DistinctBy(k => k.usage).ToDictionary(k => k.usage, k => k.declaration); + Declarations = safeUsages.DistinctBy(k => k.usage). + ToDictionary(k => k.usage, k => k.declaration); Usages = safeUsages.GroupBy(u => u.declaration).ToDictionary( g => g.Key, g => (ISet)g.Select(k => k.usage).ToHashSet()); NodePositions = new IntervalTree(); var symbols = safeUsages.Select(u => u.declaration).Concat(usages.Select(u => u.usage)). - Where(u => u.NameToken.Uri == document.Uri.ToUri() && !AutoGeneratedToken.Is(u.NameToken)).Distinct(); + Where(u => u.NameToken.Uri == document.Uri.ToUri() + && !AutoGeneratedToken.Is(u.NameToken)).Distinct(); foreach (var symbol in symbols) { var range = symbol.NameToken.GetLspRange(); NodePositions.Add(range.Start, range.End, symbol); diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index 0af51e22af4..ced709de0d8 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -59,7 +59,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString var module = new LiteralModuleDecl(outerModule, null); Microsoft.Dafny.Type.ResetScopes(); BuiltIns builtIns = new BuiltIns(options); - Parser.Parse(programNotIndented, uri, module, builtIns, reporter); + ParseUtils.Parse(programNotIndented, uri, module, builtIns, reporter); var dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); if (reporter.ErrorCount > 0) { @@ -98,7 +98,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString module = new LiteralModuleDecl(new DefaultModuleDefinition(new List() { uri }), null); Microsoft.Dafny.Type.ResetScopes(); builtIns = new BuiltIns(options); - Parser.Parse(reprinted, uri, module, builtIns, reporter); + ParseUtils.Parse(reprinted, uri, module, builtIns, reporter); dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); var newReporter = (BatchErrorReporter)dafnyProgram.Reporter; diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index 6249374202b..c28011ea619 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -80,7 +80,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption BatchErrorReporter reporter = new BatchErrorReporter(options, defaultModuleDefinition); var builtIns = new BuiltIns(options); var dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); - Parser.Parse(program, uri, module, builtIns, reporter); + ParseUtils.Parse(program, uri, module, builtIns, reporter); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index d4e6c4313ae..cffd30eb590 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -44,7 +44,7 @@ private bool Parse() { var module = new LiteralModuleDecl(defaultModuleDefinition, null); reporter = new ConsoleErrorReporter(options, defaultModuleDefinition); BuiltIns builtIns = new BuiltIns(options); - var success = (Parser.Parse(source, uri, module, builtIns, new Errors(reporter)) == 0 && + var success = (ParseUtils.Parse(source, uri, module, builtIns, reporter) == 0 && DafnyMain.ParseIncludes(module, builtIns, new HashSet(), new Errors(reporter)) == null); if (success) { dafnyProgram = new Program(fname, module, builtIns, reporter, Sets.Empty(), Sets.Empty()); diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 8ca6392701d..ae47a6c8c64 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -79,8 +79,7 @@ public static Type CopyWithReplacements(Type type, List from, List var module = new LiteralModuleDecl(defaultModuleDefinition, null); var builtIns = new BuiltIns(options); var reporter = new BatchErrorReporter(options, defaultModuleDefinition); - var success = Parser.Parse(source, uri, module, builtIns, - new Errors(reporter)) == 0 && DafnyMain.ParseIncludes(module, builtIns, + var success = ParseUtils.Parse(source, uri, module, builtIns, reporter) == 0 && DafnyMain.ParseIncludes(module, builtIns, new HashSet(), new Errors(reporter)) == null; var program = new Program(uri.LocalPath, module, builtIns, reporter, Sets.Empty(), Sets.Empty()); From 6201104781f15318740720b260e4bccf366b3ad8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 22 May 2023 17:11:13 +0200 Subject: [PATCH 05/68] 7 server tests fail after merging CLI and server parsing code --- Source/DafnyCore/AST/DafnyAst.cs | 4 + Source/DafnyCore/AST/Grammar/ParseUtils.cs | 192 +++++++++++++++++- Source/DafnyCore/AST/TopLevelDeclarations.cs | 27 --- Source/DafnyCore/DafnyFile.cs | 19 +- Source/DafnyCore/DafnyMain.cs | 151 ++------------ Source/DafnyDriver/DafnyDriver.cs | 19 +- .../Unit/ParserExceptionTest.cs | 3 +- .../Unit/TextDocumentLoaderTest.cs | 4 +- .../Language/DafnyLangParser.cs | 144 +------------ .../Language/IDafnyParser.cs | 3 +- .../Workspace/DocumentTextBuffer.cs | 2 + Source/DafnyServer/DafnyHelper.cs | 11 +- Source/DafnyTestGeneration/Utils.cs | 9 +- 13 files changed, 260 insertions(+), 328 deletions(-) diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 177ebb7084b..80759fb1f84 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -39,13 +39,17 @@ void ObjectInvariant() { Contract.Invariant(DefaultModule != null); } + // TODO move to Compilation once that's used by the CLI public ISet AlreadyVerifiedRoots; + // TODO move to Compilation once that's used by the CLI public ISet AlreadyCompiledRoots; // TODO remove? public List Includes => DefaultModuleDef.Includes; + // TODO move to DocumentAfterParsing once that's used by the CLI [FilledInDuringResolution] public ISet UrisToVerify; + // TODO move to DocumentAfterParsing once that's used by the CLI [FilledInDuringResolution] public ISet UrisToCompile; diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index cb4746c03ef..966284b8567 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -2,7 +2,9 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.IO; +using System.Linq; using System.Text; +using System.Threading; namespace Microsoft.Dafny; @@ -16,11 +18,23 @@ public class ParseUtils { /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// - public static DfyParseResult Parse(TextReader reader, Uri /*!*/ uri, BuiltIns builtIns, - Errors /*!*/ errors) /* throws System.IO.IOException */ { + public static DfyParseResult Parse(TextReader reader, Uri /*!*/ uri, BuiltIns builtIns, ErrorReporter /*!*/ errorReporter) /* throws System.IO.IOException */ { Contract.Requires(uri != null); var text = SourcePreprocessor.ProcessDirectives(reader, new List()); - return Parse(text, uri, builtIns, errors); + try { + return Parse(text, uri, builtIns, errorReporter); + } catch (Exception e) { + var internalErrorDummyToken = new Token { + Uri = uri, + line = 1, + col = 1, + pos = 0, + val = string.Empty + }; + errorReporter.Error(MessageSource.Parser, internalErrorDummyToken, + "[internal error] Parser exception: " + e.Message); + throw; + } } /// @@ -63,7 +77,7 @@ public static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle); System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ResolutionErrors).TypeHandle); byte[] /*!*/ - buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s)); + buffer = cce.NonNull(Encoding.Default.GetBytes(s)); MemoryStream ms = new MemoryStream(buffer, false); var firstToken = new Token { Uri = uri @@ -84,4 +98,174 @@ public static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, public static int Parse(string source, Uri uri, LiteralModuleDecl builtIns, BuiltIns reporter, ErrorReporter errorReporter) { throw new NotImplementedException(); } + + public static Program ParseFiles(string programName, IReadOnlyList files, ErrorReporter errorReporter, + CancellationToken cancellationToken) { + var options = errorReporter.Options; + var builtIns = new BuiltIns(options); + var defaultModule = errorReporter.OuterModule; + foreach (var dafnyFile in files) { + if (options.Trace) { + options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath); + } + + if (options.XmlSink is { IsOpen: true } && dafnyFile.Uri.IsFile) { + options.XmlSink.WriteFileFragment(dafnyFile.Uri.LocalPath); + } + + try { + // We model a precompiled file, a library, as an include + // var include = dafnyFile.IsPrecompiled ? new Include(new Token { + // Uri = dafnyFile.Uri, + // col = 1, + // line = 0 + // }, new Uri("cli://"), dafnyFile.Uri) : null; + // if (include != null) { + // // TODO this can be removed once the include error message in ErrorReporter.Error is removed. + // defaultModuleDefinition.Includes.Add(include); + // } + + var parseResult = Parse( + dafnyFile.Content, + dafnyFile.Uri, + builtIns, + errorReporter + ); + + if (parseResult.ErrorCount != 0) { + // logger.LogDebug("encountered {ErrorCount} errors while parsing {DocumentUri}", parseResult.ErrorCount, document.Uri); + } + + AddFileModuleToProgram(parseResult.Module, defaultModule); + if (defaultModule.RangeToken == null) { + defaultModule.RangeToken = parseResult.Module.RangeToken; + } + + } catch (Exception) { + // ignored + } + } + + if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) { + var includedModules = TryParseIncludes(defaultModule.Includes.ToList(), + builtIns, errorReporter, cancellationToken); + + foreach (var module in includedModules) { + AddFileModuleToProgram(module, defaultModule); + } + } + + if (options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate) { + var dependencyMap = new DependencyMap(); + dependencyMap.AddIncludes(defaultModule.Includes); + dependencyMap.PrintMap(options); + } + + 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 program = new Program( + programName, + new LiteralModuleDecl(errorReporter.OuterModule, null), + builtIns, + errorReporter, verifiedRoots, compiledRoots + ); + + DafnyMain.MaybePrintProgram(program, options.DafnyPrintFile, false); + return program; + } + + public static void AddFileModuleToProgram(FileModuleDefinition module, DefaultModuleDefinition defaultModule) + { + foreach (var topLevelDecl in module.TopLevelDecls) + { + if (topLevelDecl is DefaultClassDecl defaultClassDecl) + { + foreach (var member in defaultClassDecl.Members) + { + defaultModule.DefaultClass.Members.Add(member); + } + } + else + { + defaultModule.TopLevelDecls.Add(topLevelDecl); + } + } + + foreach (var include in module.Includes) + { + defaultModule.Includes.Add(include); + } + + defaultModule.DefaultClass.SetMembersBeforeResolution(); + } + + // TODO The following methods are based on the ones from DafnyPipeline/DafnyMain.cs. + // It could be convenient to adapt them in the main-repo so location info could be extracted. + public static IList TryParseIncludes( + IEnumerable roots, + BuiltIns builtIns, + ErrorReporter errorReporter, + CancellationToken cancellationToken + ) + { + var stack = new Stack(); + var result = new List(); + var resolvedIncludes = new HashSet(); + foreach (var root in roots) { + resolvedIncludes.Add(root.IncluderFilename); + + var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, root); + if (dafnyFile != null) { + stack.Push(dafnyFile); + } + } + + while (stack.Any()) { + var top = stack.Pop(); + if (!resolvedIncludes.Add(top.Uri)) { + continue; + } + + cancellationToken.ThrowIfCancellationRequested(); + try { + var parseIncludeResult = Parse( + top.Content, + top.Uri, + builtIns, + errorReporter + ); + result.Add(parseIncludeResult.Module); + + foreach (var include in parseIncludeResult.Module.Includes) { + var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, include); + if (dafnyFile != null) { + stack.Push(dafnyFile); + } + } + } catch (Exception e) { + // ignored + } + } + + return result; + } + + private static DafnyFile? IncludeToDafnyFile(BuiltIns builtIns, ErrorReporter errorReporter, Include include) + { + try + { + return new DafnyFile(builtIns.Options, include.IncludedFilename.LocalPath); + } + catch (IllegalDafnyFile e) + { + errorReporter.Error(MessageSource.Parser, include.tok, $"Include of file '{include.IncludedFilename}' failed."); + return null; + } + catch (IOException e) + { + errorReporter.Error(MessageSource.Parser, include.tok, + $"Unable to open the include {include.IncludedFilename}."); + return null; + } + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index b00a2f29411..44e38dfa164 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -1116,32 +1116,6 @@ public bool IsEssentiallyEmptyModuleBody() { return TopLevelDecls.All(decl => decl.IsEssentiallyEmpty()); } - public IToken GetFirstTopLevelToken() { - if (StartToken.line > 0) { - return StartToken; - } - if (this is DefaultModuleDefinition { Includes: { Count: > 0 } includes } && - includes[0].OwnedTokens.Any()) { - return includes[0].OwnedTokens.First(); - } - IEnumerable topTokens = TopLevelDecls.SelectMany(decl => { - if (decl.StartToken.line > 0) { - return new List() { decl.StartToken }; - } else if (decl is TopLevelDeclWithMembers declWithMembers) { - return declWithMembers.Members.Where( - member => member.tok.line > 0) - .Select(member => member.StartToken); - } else if (decl is LiteralModuleDecl literalModuleDecl) { - return literalModuleDecl.ModuleDef.PrefixNamedModules.Select(module => - module.Item2.ModuleDef.GetFirstTopLevelToken()).Where((IToken t) => t is { line: > 0 }); - } else { - return new List() { }; - } - }); - - return topTokens.MinBy(token => token.pos); - } - public IToken NameToken => tok; public override IEnumerable Children => (Attributes != null ? new List { Attributes } : @@ -1164,7 +1138,6 @@ public void PreResolveSnapshotForFormatter() { preResolvePrefixNamedModules = PrefixNamedModules.Select(tuple => tuple.Item2).ToImmutableList(); } - public override IEnumerable Assumptions(Declaration decl) { return TopLevelDecls.SelectMany(m => m.Assumptions(decl)); } diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index f9e582dcef0..f8a079de765 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.IO; +using System.Linq; using System.Reflection.Metadata; using System.Reflection.PortableExecutable; using DafnyCore; @@ -8,20 +9,26 @@ namespace Microsoft.Dafny; public class DafnyFile { - public bool UseStdin { get; private set; } public string FilePath => Uri.LocalPath; public string CanonicalPath { get; private set; } public string BaseName { get; private set; } public bool IsPreverified { get; set; } public bool IsPrecompiled { get; set; } - public TextReader Content { get; } + public TextReader Content { get; set; } public Uri Uri { get; } - + + // TODO take a Uri instead of a filePath - public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverride = null) { - UseStdin = contentOverride != null; + public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverride = null) : this(options, contentOverride != null ? new Uri("stdin:///") : new Uri(filePath)) { Uri = contentOverride != null ? new Uri("stdin:///") : new Uri(filePath); BaseName = contentOverride != null ? "" : Path.GetFileName(filePath); + } + + public DafnyFile(DafnyOptions options, Uri uri, TextReader contentOverride = null) { + Uri = uri; + var filePath = uri.LocalPath; + // TODO fix + BaseName = uri.IsFile ? Path.GetFileName(uri.LocalPath) : ""; var extension = contentOverride != null ? ".dfy" : Path.GetExtension(filePath); if (extension != null) { extension = extension.ToLower(); } @@ -112,7 +119,7 @@ public static Uri Canonicalize(string filePath) { } return new Uri(filePath.Substring("file:".Length)); } - public static List FileNames(IList dafnyFiles) { + public static List FileNames(IReadOnlyList dafnyFiles) { var sourceFiles = new List(); foreach (DafnyFile f in dafnyFiles) { sourceFiles.Add(f.FilePath); diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index 41a678ae3e3..91d0feafab9 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -40,11 +40,11 @@ public static void MaybePrintProgram(Program program, string filename, bool afte /// /// Returns null on success, or an error string otherwise. /// - public static string ParseCheck(TextReader stdIn, IList /*!*/ files, string /*!*/ programName, + public static string ParseCheck(TextReader stdIn, IReadOnlyList /*!*/ files, string /*!*/ programName, DafnyOptions options, out Program program) //modifies Bpl.options.XmlSink.*; { - string err = Parse(stdIn, files, programName, options, out program); + string err = Parse(files, programName, options, out program); if (err != null) { return err; } @@ -52,7 +52,7 @@ public static string ParseCheck(TextReader stdIn, IList /*!*/ f return Resolve(program); } - public static string Parse(TextReader stdIn, IList files, string programName, DafnyOptions options, + public static string Parse(IReadOnlyList files, string programName, DafnyOptions options, out Program program) { Contract.Requires(programName != null); Contract.Requires(files != null); @@ -66,55 +66,8 @@ public static string Parse(TextReader stdIn, IList files, string prog _ => throw new ArgumentOutOfRangeException() }; - LiteralModuleDecl module = new LiteralModuleDecl(defaultModuleDefinition, null); - BuiltIns builtIns = new BuiltIns(options); - - foreach (DafnyFile dafnyFile in files) { - Contract.Assert(dafnyFile != null); - if (options.XmlSink is { IsOpen: true } && !dafnyFile.UseStdin) { - options.XmlSink.WriteFileFragment(dafnyFile.FilePath); - } - - if (options.Trace) { - options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath); - } - - // We model a precompiled file, a library, as an include - var include = dafnyFile.IsPrecompiled ? new Include(new Token { - Uri = dafnyFile.Uri, - col = 1, - line = 0 - }, new Uri("cli://"), dafnyFile.Uri) : null; - if (include != null) { - // TODO this can be removed once the include error message in ErrorReporter.Error is removed. - defaultModuleDefinition.Includes.Add(include); - } - var err = ParseFile(dafnyFile, null, module, builtIns, new Errors(reporter)); - if (err != null) { - return err; - } - } - - if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) { - string errString = ParseIncludes(module, builtIns, files.Select(f => f.FilePath).ToHashSet(), new Errors(reporter)); - if (errString != null) { - return errString; - } - } - - if (options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate) { - DependencyMap dmap = new DependencyMap(); - dmap.AddIncludes(defaultModuleDefinition.Includes); - dmap.PrintMap(options); - } - - var verifiedRoots = files.Where(df => df.IsPreverified).Select(df => df.Uri).ToHashSet(); - var compiledRoots = files.Where(df => df.IsPrecompiled).Select(df => df.Uri).ToHashSet(); - program = new Program(programName, module, builtIns, reporter, verifiedRoots, compiledRoots); - - MaybePrintProgram(program, options.DafnyPrintFile, false); - - return null; // success + program = ParseUtils.ParseFiles(programName, files, reporter, CancellationToken.None); + return null; } private static readonly TaskScheduler largeThreadScheduler = @@ -140,84 +93,22 @@ public static string Resolve(Program program) { return null; // success } - // Lower-case file names before comparing them, since Windows uses case-insensitive file names - private class IncludeComparer : IComparer { - public int Compare(Include x, Include y) { - return x.CompareTo(y); - } - } - - public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, ISet excludeFiles, Errors errs) { - var includesFound = new SortedSet(new IncludeComparer()); - var allIncludes = ((DefaultModuleDefinition)((LiteralModuleDecl)module).ModuleDef).Includes; - - var notCompiledResult = TraverseIncludesFrom(0); - if (notCompiledResult != null) { - return notCompiledResult; - } - - if (builtIns.Options.PrintIncludesMode != DafnyOptions.IncludesModes.None) { - var dependencyMap = new DependencyMap(); - dependencyMap.AddIncludes(allIncludes); - dependencyMap.PrintMap(builtIns.Options); - } - - return null; // Success - - string TraverseIncludesFrom(int startingIndex) { - var includeIndex = startingIndex; - var stack = new Stack(); - - while (true) { - var addedItems = allIncludes.Skip(includeIndex); - foreach (var addedItem in addedItems.Reverse()) { - stack.Push(addedItem); - } - - includeIndex = allIncludes.Count; - - if (stack.Count == 0) { - break; - } - - var include = stack.Pop(); - if (!includesFound.Add(include) || excludeFiles.Contains(include.CanonicalPath)) { - continue; - } - - DafnyFile file; - try { - file = new DafnyFile(builtIns.Options, include.IncludedFilename.LocalPath); - } catch (IllegalDafnyFile) { - return ($"Include of file \"{include.IncludedFilename}\" failed."); - } - - string result = ParseFile(file, include, module, builtIns, errs); - if (result != null) { - return result; - } - } - - return null; - } - } - - private static string ParseFile(DafnyFile dafnyFile, Include include, ModuleDecl module, BuiltIns builtIns, Errors errs) { - var fn = builtIns.Options.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath; - try { - var parseResult = ParseUtils.Parse(dafnyFile.Content, dafnyFile.Uri, builtIns, errs); - var errorCount = parseResult.ErrorCount; - if (errorCount != 0) { - return $"{errorCount} parse errors detected in {fn}"; - } - } catch (IOException e) { - IToken tok = include == null ? Token.NoToken : include.tok; - errs.SemErr(tok, "Unable to open included file"); - return $"Error opening file \"{fn}\": {e.Message}"; - } - - return null; // Success - } + // private static string ParseFile(DafnyFile dafnyFile, Include include, BuiltIns builtIns, ErrorReporter errorReporter) { + // var fn = builtIns.Options.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath; + // try { + // var parseResult = ParseUtils.Parse(dafnyFile.Content, dafnyFile.Uri, builtIns, errorReporter); + // var errorCount = parseResult.ErrorCount; + // if (errorCount != 0) { + // return $"{errorCount} parse errors detected in {fn}"; + // } + // } catch (IOException e) { + // IToken tok = include == null ? Token.NoToken : include.tok; + // errorReporter.Error(MessageSource.Parser, tok, "Unable to open included file"); + // return $"Error opening file \"{fn}\": {e.Message}"; + // } + // + // return null; // Success + // } public static async Task<(PipelineOutcome Outcome, PipelineStatistics Statistics)> BoogieOnce( DafnyOptions options, diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index be931d518c8..8c0e895a4dc 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -18,16 +18,12 @@ using System; using System.Collections.Generic; using System.Collections.ObjectModel; -using System.CommandLine; -using System.CommandLine.IO; using System.Diagnostics.Contracts; using System.IO; using System.Linq; using Microsoft.Boogie; using Bpl = Microsoft.Boogie; using System.Diagnostics; -using System.Threading; -using DafnyCore; using Microsoft.Dafny.Plugins; namespace Microsoft.Dafny { @@ -353,7 +349,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter return CommandLineArgumentsResult.OK; } - private async Task ProcessFilesAsync(IList/*!*/ dafnyFiles, + private async Task ProcessFilesAsync(IReadOnlyList/*!*/ dafnyFiles, ReadOnlyCollection otherFileNames, DafnyOptions options, bool lookForSnapshots = true, string programId = null) { Contract.Requires(cce.NonNullElements(dafnyFiles)); @@ -452,7 +448,7 @@ private async Task ProcessFilesAsync(IList/*!*/ dafny return exitValue; } - private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions options, string programName, TextWriter errorWriter) { + private static ExitValue DoFormatting(IReadOnlyList dafnyFiles, DafnyOptions options, string programName, TextWriter errorWriter) { var exitValue = ExitValue.SUCCESS; Contract.Assert(dafnyFiles.Count > 0 || options.FoldersToFormat.Count > 0); dafnyFiles = dafnyFiles.Concat(options.FoldersToFormat.SelectMany(folderPath => { @@ -468,24 +464,23 @@ private static ExitValue DoFormatting(IList dafnyFiles, DafnyOptions var neededFormatting = 0; foreach (var file in dafnyFiles) { var dafnyFile = file; - if (dafnyFile.UseStdin && !doCheck && !doPrint) { + if (!dafnyFile.Uri.IsFile && !doCheck && !doPrint) { errorWriter.WriteLine("Please use the --check and/or --print option as stdin cannot be formatted in place."); exitValue = ExitValue.PREPROCESSING_ERROR; continue; } string tempFileName = null; - if (dafnyFile.UseStdin) { + if (!dafnyFile.Uri.IsFile) { tempFileName = Path.GetTempFileName() + ".dfy"; WriteFile(tempFileName, Console.In.ReadToEnd()); dafnyFile = new DafnyFile(options, tempFileName); } + var originalText = dafnyFile.Content.ReadToEnd(); + dafnyFile.Content = new StringReader(originalText); // Might not be totally optimized but let's do that for now - var err = DafnyMain.Parse(options.Input, new List { dafnyFile }, programName, options, out var dafnyProgram); - var originalText = dafnyFile.UseStdin ? Console.In.ReadToEnd() : - File.Exists(dafnyFile.FilePath) ? - File.ReadAllText(dafnyFile.FilePath) : null; + var err = DafnyMain.Parse(new List { dafnyFile }, programName, options, out var dafnyProgram); if (err != null) { exitValue = ExitValue.DAFNY_ERROR; errorWriter.WriteLine(err); diff --git a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs index 99b23a347af..699afb28fa3 100644 --- a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using Microsoft.Dafny.LanguageServer.Language; using System.IO; +using Microsoft.Dafny.LanguageServer.Workspace; using Microsoft.Extensions.Logging; using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; @@ -30,7 +31,7 @@ public void DocumentWithParserExceptionDisplaysIt() { var uri = new Uri("file:///" + TestFilePath); var outerModule = new DefaultModuleDefinition(new List { uri }); var errorReporter = new ParserExceptionSimulatingErrorReporter(options, outerModule); - parser.Parse(documentItem, errorReporter, default); + parser.Parse(new DocumentTextBuffer(documentItem), errorReporter, default); Assert.Equal($"encountered an exception while parsing {uri}", lastDebugLogger.LastDebugMessage); Assert.Equal($"/{TestFilePath}(1,0): Error: [internal error] Parser exception: Simulated parser internal error", errorReporter.LastMessage); } diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 67d4097e263..0bcd53bdfae 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -58,7 +58,7 @@ private static DocumentTextBuffer CreateTestDocument() { [Fact] public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { var source = new CancellationTokenSource(); - parser.Setup(p => p.Parse(It.IsAny(), + parser.Setup(p => p.Parse(It.IsAny(), It.IsAny(), It.IsAny())).Callback(() => source.Cancel()) .Throws(); @@ -75,7 +75,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { [Fact] public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() { - parser.Setup(p => p.Parse(It.IsAny(), It.IsAny(), It.IsAny())) + parser.Setup(p => p.Parse(It.IsAny(), It.IsAny(), It.IsAny())) .Throws(); var task = textDocumentLoader.LoadAsync(DafnyOptions.Default, CreateTestDocument(), default); try { diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index 76fd6ce50d1..8e210d2e22c 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -7,6 +7,7 @@ using System.Linq; using System.Threading; using Microsoft.Boogie; +using Microsoft.Dafny.LanguageServer.Workspace; using OmniSharp.Extensions.LanguageServer.Protocol; namespace Microsoft.Dafny.LanguageServer.Language { @@ -47,74 +48,22 @@ public Dafny.Program CreateUnparsed(TextDocumentItem document, ErrorReporter err } } - public Dafny.Program Parse(TextDocumentItem document, ErrorReporter errorReporter, CancellationToken cancellationToken) { + public Dafny.Program Parse(DocumentTextBuffer document, ErrorReporter errorReporter, CancellationToken cancellationToken) { mutex.Wait(cancellationToken); - var program = NewDafnyProgram(document, errorReporter); - try { - var parseResult = ParseUtils.Parse( - document.Text, - // We use the full path as filename so we can better re-construct the DocumentUri for the definition lookup. - document.Uri.ToUri(), - program.BuiltIns, - errorReporter - ); - if (parseResult.ErrorCount != 0) { - logger.LogDebug("encountered {ErrorCount} errors while parsing {DocumentUri}", parseResult.ErrorCount, document.Uri); - } - - AddFileModuleToProgram(parseResult.Module, program); - program.DefaultModule.RangeToken = parseResult.Module.RangeToken; - - var includedModules = TryParseIncludesOfModule(document.Uri, parseResult.Module, - program.BuiltIns, errorReporter, cancellationToken); - foreach (var module in includedModules) { - AddFileModuleToProgram(module, program); - } - - return program; - } catch (Exception e) { - logger.LogDebug(e, "encountered an exception while parsing {DocumentUri}", document.Uri); - var internalErrorDummyToken = new Token { - Uri = document.Uri.ToUri(), - line = 1, - col = 1, - pos = 0, - val = string.Empty - }; - errorReporter.Error(MessageSource.Parser, internalErrorDummyToken, "[internal error] Parser exception: " + e.Message); - return program; + try { + return ParseUtils.ParseFiles(document.Uri.ToString(), + new DafnyFile[] + { + new(errorReporter.Options, document.Uri.ToUri(), document.Content) + }, + errorReporter, cancellationToken); } finally { mutex.Release(); } } - private static void AddFileModuleToProgram(FileModuleDefinition module, Dafny.Program program) - { - foreach (var topLevelDecl in module.TopLevelDecls) - { - if (topLevelDecl is DefaultClassDecl defaultClassDecl) - { - foreach (var member in defaultClassDecl.Members) - { - program.DefaultModuleDef.DefaultClass.Members.Add(member); - } - } - else - { - program.DefaultModuleDef.TopLevelDecls.Add(topLevelDecl); - } - } - - foreach (var include in module.Includes) - { - program.Includes.Add(include); - } - - program.DefaultModuleDef.DefaultClass.SetMembersBeforeResolution(); - } - private Dafny.Program NewDafnyProgram(TextDocumentItem document, ErrorReporter errorReporter) { // Ensure that the statically kept scopes are empty when parsing a new document. Type.ResetScopes(); @@ -130,80 +79,5 @@ private Dafny.Program NewDafnyProgram(TextDocumentItem document, ErrorReporter e public void Dispose() { mutex.Dispose(); } - - // TODO The following methods are based on the ones from DafnyPipeline/DafnyMain.cs. - // It could be convenient to adapt them in the main-repo so location info could be extracted. - private IList TryParseIncludesOfModule( - DocumentUri root, - FileModuleDefinition rootModule, - BuiltIns builtIns, - ErrorReporter errorReporter, - CancellationToken cancellationToken - ) { - var errors = new Errors(errorReporter); - - var result = new List(); - var resolvedIncludes = new HashSet(); - resolvedIncludes.Add(root.ToUri()); - - var stack = new Stack(); - foreach (var include in rootModule.Includes) { - var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, include); - if (dafnyFile != null) { - stack.Push(dafnyFile); - } - } - - while (stack.Any()) { - var top = stack.Pop(); - if (!resolvedIncludes.Add(top.Uri)) { - continue; - } - - cancellationToken.ThrowIfCancellationRequested(); - var parseIncludeResult = TryParseDocument(top, builtIns, errorReporter, errors); - result.Add(parseIncludeResult.Module); - - foreach (var include in parseIncludeResult.Module.Includes) { - var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, include); - if (dafnyFile != null) { - stack.Push(dafnyFile); - } - } - } - - return result; - } - - private DafnyFile? IncludeToDafnyFile(BuiltIns builtIns, ErrorReporter errorReporter, Include include) - { - try - { - return new DafnyFile(builtIns.Options, include.IncludedFilename.LocalPath); - } - catch (IllegalDafnyFile e) - { - errorReporter.Error(MessageSource.Parser, include.tok, $"Include of file '{include.IncludedFilename}' failed."); - logger.LogDebug(e, "encountered include of illegal dafny file {Filename}", include.IncludedFilename); - return null; - } - catch (IOException e) - { - errorReporter.Error(MessageSource.Parser, include.tok, - $"Unable to open the include {include.IncludedFilename}."); - logger.LogDebug(e, "could not open file {Filename}", include.IncludedFilename); - return null; - } - } - - private DfyParseResult TryParseDocument(DafnyFile dafnyFile, BuiltIns builtIns, ErrorReporter errorReporter, - Errors errors) { - return ParseUtils.Parse( - dafnyFile.Content, - dafnyFile.Uri, - builtIns, - errors - ); - } } } diff --git a/Source/DafnyLanguageServer/Language/IDafnyParser.cs b/Source/DafnyLanguageServer/Language/IDafnyParser.cs index a5be6125b0e..f1d3fc393d3 100644 --- a/Source/DafnyLanguageServer/Language/IDafnyParser.cs +++ b/Source/DafnyLanguageServer/Language/IDafnyParser.cs @@ -1,5 +1,6 @@ using OmniSharp.Extensions.LanguageServer.Protocol.Models; using System.Threading; +using Microsoft.Dafny.LanguageServer.Workspace; namespace Microsoft.Dafny.LanguageServer.Language { /// @@ -29,6 +30,6 @@ public interface IDafnyParser { /// The parsed document represented as a dafny program. /// Thrown when the cancellation was requested before completion. /// Thrown if the cancellation token was disposed before the completion. - Dafny.Program Parse(TextDocumentItem textDocument, ErrorReporter errorReporter, CancellationToken cancellationToken); + Dafny.Program Parse(DocumentTextBuffer textDocument, ErrorReporter errorReporter, CancellationToken cancellationToken); } } diff --git a/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs b/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs index b3b5b705821..c28f12da43b 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs @@ -1,3 +1,4 @@ +using System.IO; using System.Net.Mime; using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; @@ -37,4 +38,5 @@ public string Extract(Range range) { public int? Version => TextDocumentItem.Version; public int NumberOfLines => Buffer.Lines.Count; + public TextReader Content => new StringReader(Text); } \ No newline at end of file diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index cffd30eb590..76f83e35318 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -7,6 +7,7 @@ using System.Linq; using System.Runtime.Serialization.Json; using System.Text; +using System.Threading; using Microsoft.Boogie; using DafnyServer; using Bpl = Microsoft.Boogie; @@ -41,13 +42,13 @@ public bool Verify() { private bool Parse() { var uri = new Uri("transcript:///" + fname); var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); - var module = new LiteralModuleDecl(defaultModuleDefinition, null); reporter = new ConsoleErrorReporter(options, defaultModuleDefinition); - BuiltIns builtIns = new BuiltIns(options); - var success = (ParseUtils.Parse(source, uri, module, builtIns, reporter) == 0 && - DafnyMain.ParseIncludes(module, builtIns, new HashSet(), new Errors(reporter)) == null); + var program = ParseUtils.ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri.LocalPath, new StringReader(source))}, + reporter, CancellationToken.None); + + var success = reporter.ErrorCount == 0; if (success) { - dafnyProgram = new Program(fname, module, builtIns, reporter, Sets.Empty(), Sets.Empty()); + dafnyProgram = program; } return success; } diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index ae47a6c8c64..90285c98391 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -3,6 +3,7 @@ using System.Collections.Generic; using System.IO; using System.Linq; +using System.Threading; using DafnyServer.CounterexampleGeneration; using Microsoft.Boogie; using Microsoft.Dafny; @@ -76,12 +77,10 @@ public static Type CopyWithReplacements(Type type, List from, List public static Program/*?*/ Parse(DafnyOptions options, string source, bool resolve = true, Uri uri = null) { uri ??= new Uri(Path.GetTempPath()); var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); - var module = new LiteralModuleDecl(defaultModuleDefinition, null); - var builtIns = new BuiltIns(options); var reporter = new BatchErrorReporter(options, defaultModuleDefinition); - var success = ParseUtils.Parse(source, uri, module, builtIns, reporter) == 0 && DafnyMain.ParseIncludes(module, builtIns, - new HashSet(), new Errors(reporter)) == null; - var program = new Program(uri.LocalPath, module, builtIns, reporter, Sets.Empty(), Sets.Empty()); + + var program = ParseUtils.ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri.LocalPath, new StringReader(source))}, + reporter, CancellationToken.None); if (!resolve) { return program; From 8bc4492285c076cc0425982167d8ad43c9b5fb52 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 23 May 2023 11:17:56 +0200 Subject: [PATCH 06/68] Only one failing integration test --- Source/DafnyCore/AST/DafnyAst.cs | 2 +- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 12 ++++++------ Source/DafnyCore/Coco/Parser.frame | 9 +++------ Source/DafnyCore/Coco/Scanner.frame | 3 +++ Source/DafnyCore/Dafny.atg | 2 +- Source/DafnyCore/Generic/Reporting.cs | 1 + .../DafnyLanguageServer.Test/_plugins/PluginsTest.cs | 4 ++-- 7 files changed, 17 insertions(+), 16 deletions(-) diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 80759fb1f84..9e5e86414c4 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -74,7 +74,7 @@ public Program(string name, [Captured] LiteralModuleDecl module, [Captured] Buil Contract.Requires(reporter != null); FullName = name; DefaultModule = module; - DefaultModuleDef = (DefaultModuleDefinition)((LiteralModuleDecl)module).ModuleDef; + DefaultModuleDef = (DefaultModuleDefinition)module.ModuleDef; BuiltIns = builtIns; this.Reporter = reporter; AlreadyVerifiedRoots = alreadyVerifiedRoots; diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index 966284b8567..084f0143fe3 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -69,7 +69,7 @@ public static DfyParseResult Parse(string /*!*/ s, Uri /*!*/ uri, return new DfyParseResult(parser.errors.ErrorCount, parser.theModule); } - public static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, + private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, BuiltIns builtIns, Errors /*!*/ errors) { Contract.Requires(s != null); Contract.Requires(uri != null); @@ -137,7 +137,7 @@ public static Program ParseFiles(string programName, IReadOnlyList fi } AddFileModuleToProgram(parseResult.Module, defaultModule); - if (defaultModule.RangeToken == null) { + if (defaultModule.RangeToken.StartToken.Uri == null) { defaultModule.RangeToken = parseResult.Module.RangeToken; } @@ -242,7 +242,7 @@ CancellationToken cancellationToken stack.Push(dafnyFile); } } - } catch (Exception e) { + } catch (Exception) { // ignored } } @@ -250,18 +250,18 @@ CancellationToken cancellationToken return result; } - private static DafnyFile? IncludeToDafnyFile(BuiltIns builtIns, ErrorReporter errorReporter, Include include) + private static DafnyFile IncludeToDafnyFile(BuiltIns builtIns, ErrorReporter errorReporter, Include include) { try { return new DafnyFile(builtIns.Options, include.IncludedFilename.LocalPath); } - catch (IllegalDafnyFile e) + catch (IllegalDafnyFile) { errorReporter.Error(MessageSource.Parser, include.tok, $"Include of file '{include.IncludedFilename}' failed."); return null; } - catch (IOException e) + catch (IOException) { errorReporter.Error(MessageSource.Parser, include.tok, $"Unable to open the include {include.IncludedFilename}."); diff --git a/Source/DafnyCore/Coco/Parser.frame b/Source/DafnyCore/Coco/Parser.frame index e52f57599d6..b21adbad0f1 100644 --- a/Source/DafnyCore/Coco/Parser.frame +++ b/Source/DafnyCore/Coco/Parser.frame @@ -55,10 +55,8 @@ public class Parser { public Parser(Scanner scanner, Errors errors) { this.scanner = scanner; this.errors = errors; - Token tok = new Token(); - tok.val = ""; - this.la = tok; - this.t = new Token(); // just to satisfy its non-null constraint + this.la = scanner.FirstToken; + this.t = scanner.FirstToken; // just to satisfy its non-null constraint } void SynErr (int n) { @@ -145,8 +143,7 @@ public class Parser { -->productions public void Parse() { - la = new Token(); - la.val = ""; + la = scanner.FirstToken; Get(); -->parseRoot } diff --git a/Source/DafnyCore/Coco/Scanner.frame b/Source/DafnyCore/Coco/Scanner.frame index 77b7cdaa30c..a98d10d01a7 100644 --- a/Source/DafnyCore/Coco/Scanner.frame +++ b/Source/DafnyCore/Coco/Scanner.frame @@ -306,6 +306,7 @@ public class Scanner { bool triviaTrailing = false; // The first trivia is always leading int triviaNewlines = 0; // How many newlines in the trivia so far bool lastWasCr = false; // if the last newline character was \r + public Token FirstToken { get; } private Errors/*!*/ errorHandler; @@ -324,6 +325,7 @@ public class Scanner { if(firstToken.Uri == null) { firstToken.Uri = uri; } + this.FirstToken = firstToken; pt = tokens = firstToken ?? new Token(); // first token is a dummy t = firstToken ?? new Token(); // dummy because t is a non-null field try { @@ -344,6 +346,7 @@ public class Scanner { if(firstToken.Uri == null) { firstToken.Uri = uri; } + this.FirstToken = firstToken; pt = tokens = firstToken ?? new Token(); // first token is a dummy t = firstToken ?? new Token(); // dummy because t is a non-null field this._buffer = new Buffer(s, true); diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 5cafea9a7fb..2d49511324b 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -943,7 +943,7 @@ Dafny string basePath = Path.GetDirectoryName(parsedFile.LocalPath); includedFile = Path.Combine(basePath, includedFile); } - var oneInclude = new Include(t, parsedFile, includedFile); + var oneInclude = new Include(t, parsedFile, new Uri(includedFile)); oneInclude.RangeToken = new RangeToken(startToken, t); theModule.Includes.Add(oneInclude); } diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index 3f6fc8eab6e..3bbf053a094 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -46,6 +46,7 @@ public void Error(MessageSource source, IToken tok, string msg) { public virtual void Error(MessageSource source, string errorId, IToken tok, string msg) { Contract.Requires(tok != null); Contract.Requires(msg != null); + // TODO move this out of ErrorReporter together with OuterModule. Let Program have a list of FileModuleDefinitions as constructor input and create its default module there. if (tok.FromIncludeDirective(OuterModule) && OuterModule != null) { var include = OuterModule.Includes.First(i => i.IncludedFilename == tok.Uri); if (!include.ErrorReported) { diff --git a/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs b/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs index 06744a75af1..6e651b8380a 100644 --- a/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs +++ b/Source/DafnyLanguageServer.Test/_plugins/PluginsTest.cs @@ -21,8 +21,8 @@ public ErrorRewriter(ErrorReporter reporter, TestConfiguration configuration) : this.configuration = configuration; } - public override void PostResolve(ModuleDefinition moduleDefinition) { - Reporter.Error(MessageSource.Resolver, moduleDefinition.GetFirstTopLevelToken(), "Impossible to continue " + configuration.Argument); + public override void PostResolve(Program program) { + Reporter.Error(MessageSource.Resolver, program.GetFirstTopLevelToken(), "Impossible to continue " + configuration.Argument); } } From 7b878b31f66a24e0dcf6c5c1b7f13d9402a96736 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 23 May 2023 11:30:33 +0200 Subject: [PATCH 07/68] Get last language server test to pass --- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 13 +++++++++---- .../Unit/ParserExceptionTest.cs | 1 - 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index 084f0143fe3..01d5f4b9963 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -141,8 +141,15 @@ public static Program ParseFiles(string programName, IReadOnlyList fi defaultModule.RangeToken = parseResult.Module.RangeToken; } - } catch (Exception) { - // ignored + } catch (Exception e) { + var internalErrorDummyToken = new Token { + Uri = dafnyFile.Uri, + line = 1, + col = 1, + pos = 0, + val = string.Empty + }; + errorReporter.Error(MessageSource.Parser, internalErrorDummyToken, "[internal error] Parser exception: " + e.Message); } } @@ -199,8 +206,6 @@ public static void AddFileModuleToProgram(FileModuleDefinition module, DefaultMo defaultModule.DefaultClass.SetMembersBeforeResolution(); } - // TODO The following methods are based on the ones from DafnyPipeline/DafnyMain.cs. - // It could be convenient to adapt them in the main-repo so location info could be extracted. public static IList TryParseIncludes( IEnumerable roots, BuiltIns builtIns, diff --git a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs index 699afb28fa3..0087708f48f 100644 --- a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs @@ -32,7 +32,6 @@ public void DocumentWithParserExceptionDisplaysIt() { var outerModule = new DefaultModuleDefinition(new List { uri }); var errorReporter = new ParserExceptionSimulatingErrorReporter(options, outerModule); parser.Parse(new DocumentTextBuffer(documentItem), errorReporter, default); - Assert.Equal($"encountered an exception while parsing {uri}", lastDebugLogger.LastDebugMessage); Assert.Equal($"/{TestFilePath}(1,0): Error: [internal error] Parser exception: Simulated parser internal error", errorReporter.LastMessage); } From fef7ae1e0302e59616c6fd4985285a414161cf86 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 23 May 2023 11:38:56 +0200 Subject: [PATCH 08/68] Test fixes --- Source/DafnyCore.Test/DooFileTest.cs | 8 +++----- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 5 +++-- Source/DafnyPipeline.Test/FormatterBaseTest.cs | 11 +++-------- Source/DafnyPipeline.Test/TranslatorTest.cs | 6 ++---- Source/DafnyTestGeneration/Utils.cs | 2 +- 5 files changed, 12 insertions(+), 20 deletions(-) diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs index fbbbfb9c3c5..8465dffa97f 100644 --- a/Source/DafnyCore.Test/DooFileTest.cs +++ b/Source/DafnyCore.Test/DooFileTest.cs @@ -32,12 +32,10 @@ private static Program ParseProgram(string dafnyProgramText, DafnyOptions option const string fullFilePath = "untitled:foo"; var rootUri = new Uri(fullFilePath); var outerModule = new DefaultModuleDefinition(new List { rootUri }); - var module = new LiteralModuleDecl(outerModule, null); Microsoft.Dafny.Type.ResetScopes(); - var builtIns = new BuiltIns(options); var errorReporter = new ConsoleErrorReporter(options, outerModule); - var parseResult = ParseUtils.Parse(dafnyProgramText, rootUri, module, builtIns, errorReporter); - Assert.Equal(0, parseResult); - return new Program(fullFilePath, module, builtIns, errorReporter, Sets.Empty(), Sets.Empty()); + var program = ParseUtils.Parse(dafnyProgramText, rootUri, errorReporter); + Assert.Equal(0, errorReporter.ErrorCount); + return program; } } diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index 01d5f4b9963..8e9966ad997 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -95,8 +95,9 @@ private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, return new Parser(scanner, errors, builtIns); } - public static int Parse(string source, Uri uri, LiteralModuleDecl builtIns, BuiltIns reporter, ErrorReporter errorReporter) { - throw new NotImplementedException(); + public static Program Parse(string source, Uri uri, ErrorReporter reporter) { + var files = new[] { new DafnyFile(reporter.Options, uri, new StringReader(source)) }; + return ParseFiles(uri.ToString(), files, reporter, CancellationToken.None); } public static Program ParseFiles(string programName, IReadOnlyList files, ErrorReporter errorReporter, diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index ced709de0d8..94806575833 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -56,11 +56,9 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString var uri = new Uri("virtual:virtual"); var outerModule = new DefaultModuleDefinition(new List() { uri }); BatchErrorReporter reporter = new BatchErrorReporter(options, outerModule); - var module = new LiteralModuleDecl(outerModule, null); Microsoft.Dafny.Type.ResetScopes(); - BuiltIns builtIns = new BuiltIns(options); - ParseUtils.Parse(programNotIndented, uri, module, builtIns, reporter); - var dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); + + var dafnyProgram = ParseUtils.Parse(programNotIndented, uri, reporter); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; @@ -95,11 +93,8 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString var initErrorCount = reporter.ErrorCount; // Verify that the formatting is stable. - module = new LiteralModuleDecl(new DefaultModuleDefinition(new List() { uri }), null); Microsoft.Dafny.Type.ResetScopes(); - builtIns = new BuiltIns(options); - ParseUtils.Parse(reprinted, uri, module, builtIns, reporter); - dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); + dafnyProgram = ParseUtils.Parse(reprinted, uri, reporter);; var newReporter = (BatchErrorReporter)dafnyProgram.Reporter; Assert.Equal(initErrorCount, newReporter.ErrorCount); diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index c28011ea619..c7e9c98a3c7 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -76,11 +76,9 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption options = options ?? new DafnyOptions(TextReader.Null, TextWriter.Null, TextWriter.Null); var uri = new Uri("virtual:///virtual"); var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); - var module = new LiteralModuleDecl(defaultModuleDefinition, null); BatchErrorReporter reporter = new BatchErrorReporter(options, defaultModuleDefinition); - var builtIns = new BuiltIns(options); - var dafnyProgram = new Program("programName", module, builtIns, reporter, Sets.Empty(), Sets.Empty()); - ParseUtils.Parse(program, uri, module, builtIns, reporter); + var dafnyProgram = ParseUtils.Parse(program, uri, reporter); + ParseUtils.Parse(program, uri, reporter); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 90285c98391..e91d1a04265 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -79,7 +79,7 @@ public static Type CopyWithReplacements(Type type, List from, List var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); var reporter = new BatchErrorReporter(options, defaultModuleDefinition); - var program = ParseUtils.ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri.LocalPath, new StringReader(source))}, + var program = ParseUtils.ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source))}, reporter, CancellationToken.None); if (!resolve) { From 234423efa17f230272b9ef1dd4007b3a6f05278e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 23 May 2023 11:59:29 +0200 Subject: [PATCH 09/68] Test generation tests now pass --- Source/DafnyCore/AST/FileModuleDefinition.cs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Source/DafnyCore/AST/FileModuleDefinition.cs b/Source/DafnyCore/AST/FileModuleDefinition.cs index 70c204b5e9b..7e9900ba6ad 100644 --- a/Source/DafnyCore/AST/FileModuleDefinition.cs +++ b/Source/DafnyCore/AST/FileModuleDefinition.cs @@ -11,4 +11,6 @@ public FileModuleDefinition() : { } } + + public override bool IsDefaultModule => true; } \ No newline at end of file From d43a210b100d4cf435218bac89070228d927716d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 23 May 2023 12:19:37 +0200 Subject: [PATCH 10/68] Fix bug and correctly set parent relationships when merging FileModuleDefinition into Program --- Source/DafnyCore/AST/FileModuleDefinition.cs | 2 -- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 5 +++++ Source/DafnyCore/AST/TopLevelDeclarations.cs | 2 +- Source/DafnyDriver/Commands/CommandRegistry.cs | 4 +++- 4 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Source/DafnyCore/AST/FileModuleDefinition.cs b/Source/DafnyCore/AST/FileModuleDefinition.cs index 7e9900ba6ad..70c204b5e9b 100644 --- a/Source/DafnyCore/AST/FileModuleDefinition.cs +++ b/Source/DafnyCore/AST/FileModuleDefinition.cs @@ -11,6 +11,4 @@ public FileModuleDefinition() : { } } - - public override bool IsDefaultModule => true; } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index 8e9966ad997..0411e610cb0 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -186,11 +186,16 @@ public static void AddFileModuleToProgram(FileModuleDefinition module, DefaultMo { foreach (var topLevelDecl in module.TopLevelDecls) { + topLevelDecl.EnclosingModuleDefinition = defaultModule; + if (topLevelDecl is LiteralModuleDecl literalModuleDecl) { + literalModuleDecl.ModuleDef.EnclosingModule = defaultModule; + } if (topLevelDecl is DefaultClassDecl defaultClassDecl) { foreach (var member in defaultClassDecl.Members) { defaultModule.DefaultClass.Members.Add(member); + member.EnclosingClass = defaultModule.DefaultClass; } } else diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 44e38dfa164..79f80f5436f 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -1163,7 +1163,7 @@ public DefaultModuleDefinition(IList rootSourceUris) public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType { public abstract string WhatKind { get; } - public readonly ModuleDefinition EnclosingModuleDefinition; + public ModuleDefinition EnclosingModuleDefinition; public readonly List TypeArgs; [ContractInvariantMethod] void ObjectInvariant() { diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 9202670f76e..c5a112c2db0 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -7,6 +7,7 @@ using System.CommandLine.Invocation; using System.CommandLine.IO; using System.CommandLine.Parsing; +using System.Diagnostics; using System.IO; using System.Linq; using System.Reflection; @@ -53,11 +54,12 @@ static CommandRegistry() { // This SHOULD find the same method but returns null for some reason: // typeof(ParseResult).GetMethod("GetValueForOption", 1, new[] { typeof(Option<>) }); - foreach (var method in typeof(DfyParseResult).GetMethods()) { + foreach (var method in typeof(ParseResult).GetMethods()) { if (method.Name == "GetValueForOption" && method.GetGenericArguments().Length == 1) { GetValueForOptionMethod = method; } } + Debug.Assert(GetValueForOptionMethod != null); } public static Argument FileArgument { get; } From 71411544b8eb0d90e7e3c968a8f9cd27891aab60 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 23 May 2023 14:18:07 +0200 Subject: [PATCH 11/68] Fix clone method of ModuleDefinition --- Source/DafnyCore/AST/FileModuleDefinition.cs | 6 ++++++ Source/DafnyCore/AST/TopLevelDeclarations.cs | 1 + 2 files changed, 7 insertions(+) diff --git a/Source/DafnyCore/AST/FileModuleDefinition.cs b/Source/DafnyCore/AST/FileModuleDefinition.cs index 70c204b5e9b..9df8e3de08c 100644 --- a/Source/DafnyCore/AST/FileModuleDefinition.cs +++ b/Source/DafnyCore/AST/FileModuleDefinition.cs @@ -2,6 +2,12 @@ namespace Microsoft.Dafny; +/// +/// This is a temporary container of everything declared at the top level of a file, including include directives. +/// After parsing, the contents of this 'module' are moved into the default module. +/// In the future, files may declare implicit modules and then this class will play a non-temporary role: +/// https://github.com/dafny-lang/dafny/issues/3027 +/// public class FileModuleDefinition : ModuleDefinition { public List Includes { get; } = new(); diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 79f80f5436f..a0a37a6d43e 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -865,6 +865,7 @@ void ObjectInvariant() { public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : base(cloner, original) { NameNode = name; + IsBuiltinName = original.IsBuiltinName; foreach (var d in original.TopLevelDecls) { TopLevelDecls.Add(cloner.CloneDeclaration(d, this)); } From 42041b632b2512e9f9a901645891c7eab0ff5640 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 23 May 2023 14:23:48 +0200 Subject: [PATCH 12/68] Complete ModuleDefinition clone function --- Source/DafnyCore/AST/TopLevelDeclarations.cs | 21 ++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index a0a37a6d43e..935caab293e 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -849,8 +849,8 @@ public string FullName { public ModuleQualifiedId RefinementQId; // full qualified ID of the refinement parent, null if no refinement base public bool SuccessfullyResolved; // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved - [FilledInDuringResolution] public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that, except for the addition of prefix-named modules, which happens in the resolver - [FilledInDuringResolution] public readonly List, LiteralModuleDecl>> PrefixNamedModules = new List, LiteralModuleDecl>>(); // filled in by the parser; emptied by the resolver + [FilledInDuringResolution] public readonly List TopLevelDecls = new(); // filled in by the parser; readonly after that, except for the addition of prefix-named modules, which happens in the resolver + [FilledInDuringResolution] public readonly List, LiteralModuleDecl>> PrefixNamedModules = new(); // filled in by the parser; emptied by the resolver [FilledInDuringResolution] public readonly Graph CallGraph = new Graph(); [FilledInDuringResolution] public int Height; // height in the topological sorting of modules; public readonly bool IsAbstract; @@ -866,14 +866,23 @@ void ObjectInvariant() { public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : base(cloner, original) { NameNode = name; IsBuiltinName = original.IsBuiltinName; + PrefixIds = original.PrefixIds.Select(cloner.Tok).ToList(); + IsFacade = original.IsFacade; + Attributes = original.Attributes; + IsAbstract = original.IsAbstract; + RefinementQId = original.RefinementQId; + EnclosingModule = original.EnclosingModule; foreach (var d in original.TopLevelDecls) { TopLevelDecls.Add(cloner.CloneDeclaration(d, this)); } - foreach (var tup in original.PrefixNamedModules) { - var newTup = new Tuple, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)cloner.CloneDeclaration(tup.Item2, this)); - PrefixNamedModules.Add(newTup); + + if (cloner.CloneResolvedFields) { + Height = original.Height; + foreach (var tup in original.PrefixNamedModules) { + var newTup = new Tuple, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)cloner.CloneDeclaration(tup.Item2, this)); + PrefixNamedModules.Add(newTup); + } } - Height = original.Height; } public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool isAbstract, bool isFacade, From 087b5fcd85b7ccf80d32945a879fc9465fbaae5f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 23 May 2023 15:02:14 +0200 Subject: [PATCH 13/68] Lots of changes to resolve issues around the default class --- Source/DafnyCore/AST/BuiltIns.cs | 16 ++--- Source/DafnyCore/AST/Cloner.cs | 4 +- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 16 ++--- Source/DafnyCore/AST/Grammar/Printer.cs | 8 +-- Source/DafnyCore/AST/TopLevelDeclarations.cs | 69 ++++++++----------- Source/DafnyCore/Dafny.atg | 14 ++-- Source/DafnyCore/Generic/Util.cs | 2 +- Source/DafnyCore/Resolver/Resolver.cs | 27 +++----- .../Rewriters/RefinementTransformer.cs | 39 ++++++----- Source/DafnyCore/Verifier/Translator.cs | 2 +- Source/DafnyPipeline.Test/Trivia.cs | 16 +++-- .../SignatureAndCompletionTable.cs | 2 +- Source/DafnyTestGeneration/DafnyInfo.cs | 5 +- Source/DafnyTestGeneration/Utils.cs | 4 +- 14 files changed, 107 insertions(+), 117 deletions(-) diff --git a/Source/DafnyCore/AST/BuiltIns.cs b/Source/DafnyCore/AST/BuiltIns.cs index 0fc489c0e54..dbd2e64720d 100644 --- a/Source/DafnyCore/AST/BuiltIns.cs +++ b/Source/DafnyCore/AST/BuiltIns.cs @@ -34,7 +34,7 @@ public BuiltIns(DafnyOptions options) { var str = new TypeSynonymDecl(RangeToken.NoToken, new Name("string"), new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false), new List(), SystemModule, new SeqType(new CharType()), null); - SystemModule.TopLevelDecls.Add(str); + SystemModule.SourceDecls.Add(str); // create subset type 'nat' var bvNat = new BoundVar(Token.NoToken, "x", Type.Int); var natConstraint = Expression.CreateAtMost(Expression.CreateIntLiteral(Token.NoToken, 0), Expression.CreateIdentExpr(bvNat)); @@ -42,10 +42,10 @@ public BuiltIns(DafnyOptions options) { NatDecl = new SubsetTypeDecl(RangeToken.NoToken, new Name("nat"), new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false), new List(), SystemModule, bvNat, natConstraint, SubsetTypeDecl.WKind.CompiledZero, null, ax); - SystemModule.TopLevelDecls.Add(NatDecl); + SystemModule.SourceDecls.Add(NatDecl); // create trait 'object' ObjectDecl = new TraitDecl(RangeToken.NoToken, new Name("object"), SystemModule, new List(), new List(), DontCompile(), false, null); - SystemModule.TopLevelDecls.Add(ObjectDecl); + SystemModule.SourceDecls.Add(ObjectDecl); // add one-dimensional arrays, since they may arise during type checking // Arrays of other dimensions may be added during parsing as the parser detects the need for these UserDefinedType tmp = ArrayType(1, Type.Int, true); @@ -87,7 +87,7 @@ public UserDefinedType ArrayType(IToken tok, int dims, List optTypeArgs, b arrayClass.Members.Add(len); } arrayTypeDecls.Add(dims, arrayClass); - SystemModule.TopLevelDecls.Add(arrayClass); + SystemModule.SourceDecls.Add(arrayClass); CreateArrowTypeDecl(dims); // also create an arrow type with this arity, since it may be used in an initializing expression for the array } UserDefinedType udt = new UserDefinedType(tok, arrayName, optTypeArgs); @@ -145,7 +145,7 @@ Function createMember(string name, Type resultType, Function readsFunction = nul var arrowDecl = new ArrowTypeDecl(tps, req, reads, SystemModule, DontCompile()); ArrowTypeDecls.Add(arity, arrowDecl); - SystemModule.TopLevelDecls.Add(arrowDecl); + SystemModule.SourceDecls.Add(arrowDecl); // declaration of read-effect-free arrow-type, aka heap-independent arrow-type, aka partial-function arrow-type tps = Util.Map(Enumerable.Range(0, arity + 1), @@ -158,7 +158,7 @@ Function createMember(string name, Type resultType, Function readsFunction = nul new TypeParameter.TypeParameterCharacteristics(false), tps, SystemModule, id, ArrowSubtypeConstraint(tok, tok.ToRange(), id, reads, tps, false), SubsetTypeDecl.WKind.Special, null, DontCompile()); PartialArrowTypeDecls.Add(arity, partialArrow); - SystemModule.TopLevelDecls.Add(partialArrow); + SystemModule.SourceDecls.Add(partialArrow); // declaration of total arrow-type @@ -172,7 +172,7 @@ Function createMember(string name, Type resultType, Function readsFunction = nul new TypeParameter.TypeParameterCharacteristics(false), tps, SystemModule, id, ArrowSubtypeConstraint(tok, tok.ToRange(), id, req, tps, true), SubsetTypeDecl.WKind.Special, null, DontCompile()); TotalArrowTypeDecls.Add(arity, totalArrow); - SystemModule.TopLevelDecls.Add(totalArrow); + SystemModule.SourceDecls.Add(totalArrow); } /// @@ -263,7 +263,7 @@ public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType } tupleTypeDecls.Add(argumentGhostness, tt); - SystemModule.TopLevelDecls.Add(tt); + SystemModule.SourceDecls.Add(tt); } return tt; } diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 15e9b8af2a0..5b7d7cfa3bf 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -771,7 +771,7 @@ public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name } } - basem.TopLevelDecls.RemoveAll(t => { + basem.SourceDecls.RemoveAll(t => { // TODO What about the prefix ones? if (t is AliasModuleDecl aliasModuleDecl) { var def = aliasModuleDecl.Signature.ModuleDef; return def != null && vismap[def].IsEmpty(); @@ -871,7 +871,7 @@ public AbstractSignatureCloner(VisibilityScope scope) public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Name name) { var basem = base.CloneModuleDefinition(m, name); - basem.TopLevelDecls.RemoveAll(t => t is ModuleExportDecl); + basem.SourceDecls.RemoveAll(t => t is ModuleExportDecl); // TODO What about the prefix ones? return basem; } diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index 0411e610cb0..1e99c97182d 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -61,7 +61,7 @@ public static DfyParseResult Parse(string /*!*/ s, Uri /*!*/ uri, Parser parser = SetupParser(s, uri, builtIns, errors); parser.Parse(); - if (parser.theModule.DefaultClass.Members.Count == 0 && parser.theModule.Includes.Count == 0 && parser.theModule.TopLevelDecls.Count == 1 + if (parser.theModule.DefaultClass.Members.Count == 0 && parser.theModule.Includes.Count == 0 && !parser.theModule.SourceDecls.Any() && (parser.theModule.PrefixNamedModules == null || parser.theModule.PrefixNamedModules.Count == 0)) { errors.Warning(new Token(1, 1) { Uri = uri }, "File contains no code"); } @@ -182,15 +182,15 @@ public static Program ParseFiles(string programName, IReadOnlyList fi return program; } - public static void AddFileModuleToProgram(FileModuleDefinition module, DefaultModuleDefinition defaultModule) + public static void AddFileModuleToProgram(FileModuleDefinition fileModule, DefaultModuleDefinition defaultModule) { - foreach (var topLevelDecl in module.TopLevelDecls) + foreach (var declToMove in fileModule.TopLevelDecls) { - topLevelDecl.EnclosingModuleDefinition = defaultModule; - if (topLevelDecl is LiteralModuleDecl literalModuleDecl) { + declToMove.EnclosingModuleDefinition = defaultModule; + if (declToMove is LiteralModuleDecl literalModuleDecl) { literalModuleDecl.ModuleDef.EnclosingModule = defaultModule; } - if (topLevelDecl is DefaultClassDecl defaultClassDecl) + if (declToMove is DefaultClassDecl defaultClassDecl) { foreach (var member in defaultClassDecl.Members) { @@ -200,11 +200,11 @@ public static void AddFileModuleToProgram(FileModuleDefinition module, DefaultMo } else { - defaultModule.TopLevelDecls.Add(topLevelDecl); + defaultModule.SourceDecls.Add(declToMove); } } - foreach (var include in module.Includes) + foreach (var include in fileModule.Includes) { defaultModule.Includes.Add(include); } diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index 665e76fb7bf..8cf6ed4f837 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -260,7 +260,7 @@ public void PrintCallGraph(ModuleDefinition module, int indent) { } } - public void PrintTopLevelDecls(Program program, List decls, int indent, List/*?*/ prefixIds, string fileBeingPrinted) { + public void PrintTopLevelDecls(Program program, IEnumerable decls, int indent, List/*?*/ prefixIds, string fileBeingPrinted) { Contract.Requires(decls != null); int i = 0; foreach (TopLevelDecl d in decls) { @@ -576,9 +576,9 @@ public void PrintModuleDefinition(Program program, ModuleDefinition module, Visi } wr.Write("{0} ", module.Name); if (module.RefinementQId != null) { - wr.Write("refines {0} ", module.RefinementQId.ToString()); + wr.Write("refines {0} ", module.RefinementQId); } - if (module.TopLevelDecls.Count == 0) { + if (!module.TopLevelDecls.Any()) { wr.WriteLine("{ }"); } else { wr.WriteLine("{"); @@ -591,7 +591,7 @@ public void PrintModuleDefinition(Program program, ModuleDefinition module, Visi } void PrintTopLevelDeclsOrExportedView(Program program, ModuleDefinition module, int indent, string fileBeingPrinted) { - var decls = module.TopLevelDecls; + var decls = module.TopLevelDecls.ToList(); // only filter based on view name after resolver. if (afterResolver && options.DafnyPrintExportedViews.Count != 0) { decls = new List(); diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 935caab293e..92aa04dde44 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -848,15 +848,25 @@ public string FullName { Attributes IAttributeBearingDeclaration.Attributes => Attributes; public ModuleQualifiedId RefinementQId; // full qualified ID of the refinement parent, null if no refinement base public bool SuccessfullyResolved; // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved - - [FilledInDuringResolution] public readonly List TopLevelDecls = new(); // filled in by the parser; readonly after that, except for the addition of prefix-named modules, which happens in the resolver - [FilledInDuringResolution] public readonly List, LiteralModuleDecl>> PrefixNamedModules = new(); // filled in by the parser; emptied by the resolver - [FilledInDuringResolution] public readonly Graph CallGraph = new Graph(); - [FilledInDuringResolution] public int Height; // height in the topological sorting of modules; public readonly bool IsAbstract; public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface) private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled. + public DefaultClassDecl DefaultClass { get; set; } + + public readonly List SourceDecls = new(); + [FilledInDuringResolution] + public readonly List ResolvedPrefixNamedModules = new(); + [FilledInDuringResolution] + public readonly List, LiteralModuleDecl>> PrefixNamedModules = new(); // filled in by the parser; emptied by the resolver + public IEnumerable TopLevelDecls => (DefaultClass == null ? Enumerable.Empty() : new TopLevelDecl[] {DefaultClass}). + Concat(SourceDecls).Concat(ResolvedPrefixNamedModules); + + [FilledInDuringResolution] + public readonly Graph CallGraph = new(); + [FilledInDuringResolution] + public int Height; // height in the topological sorting of modules; + [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(TopLevelDecls)); @@ -872,10 +882,12 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : b IsAbstract = original.IsAbstract; RefinementQId = original.RefinementQId; EnclosingModule = original.EnclosingModule; - foreach (var d in original.TopLevelDecls) { - TopLevelDecls.Add(cloner.CloneDeclaration(d, this)); + foreach (var d in original.SourceDecls) { + SourceDecls.Add(cloner.CloneDeclaration(d, this)); } + DefaultClass = (DefaultClassDecl)cloner.CloneDeclaration(original.DefaultClass, this); + if (cloner.CloneResolvedFields) { Height = original.Height; foreach (var tup in original.PrefixNamedModules) { @@ -900,21 +912,14 @@ public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool if (Name != "_System") { DefaultClass = new DefaultClassDecl(this, new List()); - TopLevelDecls.Add(DefaultClass); } } - public DefaultClassDecl DefaultClass { get; set; } - - VisibilityScope visibilityScope; + private VisibilityScope visibilityScope; public VisibilityScope VisibilityScope => visibilityScope ??= new VisibilityScope(this.SanitizedName); - public virtual bool IsDefaultModule { - get { - return false; - } - } + public virtual bool IsDefaultModule => false; private string sanitizedName = null; @@ -1004,13 +1009,11 @@ public static IEnumerable AllFunctions(List declarations } } - public static IEnumerable AllFields(List declarations) { + public static IEnumerable AllFields(IEnumerable declarations) { foreach (var d in declarations) { - var cl = d as TopLevelDeclWithMembers; - if (cl != null) { + if (d is TopLevelDeclWithMembers cl) { foreach (var member in cl.Members) { - var fn = member as Field; - if (fn != null) { + if (member is Field fn) { yield return fn; } } @@ -1018,14 +1021,6 @@ public static IEnumerable AllFields(List declarations) { } } - public static IEnumerable AllClasses(List declarations) { - foreach (var d in declarations) { - if (d is ClassDecl cl) { - yield return cl; - } - } - } - public static IEnumerable AllTypesWithMembers(List declarations) { foreach (var d in declarations) { if (d is TopLevelDeclWithMembers cl) { @@ -1042,7 +1037,7 @@ public static IEnumerable AllTypesWithMembers(List - public static IEnumerable AllCallables(List declarations) { + public static IEnumerable AllCallables(IEnumerable declarations) { foreach (var d in declarations) { if (d is TopLevelDeclWithMembers cl) { foreach (var member in cl.Members.Where(member => member is ICallable and not ConstantField)) { @@ -1059,7 +1054,7 @@ public static IEnumerable AllCallables(List declaration /// Yields all functions and methods that are members of some type in the given list of /// declarations, including prefix lemmas and prefix predicates. /// - public static IEnumerable AllCallablesIncludingPrefixDeclarations(List declarations) { + public static IEnumerable AllCallablesIncludingPrefixDeclarations(IEnumerable declarations) { foreach (var decl in AllCallables(declarations)) { yield return decl; if (decl is ExtremeLemma extremeLemma) { @@ -1074,7 +1069,7 @@ public static IEnumerable AllCallablesIncludingPrefixDeclarations(Lis /// Yields all functions and methods that are members of some non-iterator type in the given /// list of declarations, as well as any IteratorDecl's in that list. /// - public static IEnumerable AllItersAndCallables(List declarations) { + public static IEnumerable AllItersAndCallables(IEnumerable declarations) { foreach (var d in declarations) { if (d is IteratorDecl) { yield return (IteratorDecl)d; @@ -1089,19 +1084,11 @@ public static IEnumerable AllItersAndCallables(List dec } } - public static IEnumerable AllIteratorDecls(List declarations) { - foreach (var d in declarations) { - if (d is IteratorDecl iter) { - yield return iter; - } - } - } - /// /// Emits the declarations in "declarations", but for each such declaration that is a class with /// a corresponding non-null type, also emits that non-null type *after* the class declaration. /// - public static IEnumerable AllDeclarationsAndNonNullTypeDecls(List declarations) { + public static IEnumerable AllDeclarationsAndNonNullTypeDecls(IEnumerable declarations) { foreach (var d in declarations) { yield return d; if (d is ClassDecl { NonNullTypeDecl: { } } cl) { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 2d49511324b..3b68e1f44f4 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -979,15 +979,15 @@ TopDecl<. ModuleDefinition module, bool isTopLevel, bool isAbstract .> var tup = new Tuple, LiteralModuleDecl>(litmod.ModuleDef.PrefixIds, litmod); module.PrefixNamedModules.Add(tup); } else { - module.TopLevelDecls.Add(submodule); + module.SourceDecls.Add(submodule); } .) - | ClassDecl (. module.TopLevelDecls.Add(td); .) - | DatatypeDecl (. module.TopLevelDecls.Add(dt); .) - | NewtypeDecl (. module.TopLevelDecls.Add(td); .) - | SynonymTypeDecl (. module.TopLevelDecls.Add(td); .) - | IteratorDecl (. module.TopLevelDecls.Add(iter); .) - | TraitDecl (. module.TopLevelDecls.Add(trait); .) + | ClassDecl (. module.SourceDecls.Add(td); .) + | DatatypeDecl (. module.SourceDecls.Add(dt); .) + | NewtypeDecl (. module.SourceDecls.Add(td); .) + | SynonymTypeDecl (. module.SourceDecls.Add(td); .) + | IteratorDecl (. module.SourceDecls.Add(iter); .) + | TraitDecl (. module.SourceDecls.Add(trait); .) | ClassMemberDecl ) . diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index e0d14888b84..6785b23b10e 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -717,7 +717,7 @@ public bool Traverse(ModuleDefinition moduleDefinition) { return Traverse(moduleDefinition.TopLevelDecls); } - public bool Traverse(List topLevelDecls) { + public bool Traverse(IEnumerable topLevelDecls) { if (topLevelDecls == null) { return false; } diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 024791598de..07629c48e0c 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -276,7 +276,7 @@ public Resolver(Program prog) { new List() { TypeParameter.TPVarianceSyntax.Covariant_Permissive , TypeParameter.TPVarianceSyntax.Covariant_Strict }, t => t.IsIMapType, typeArgs => new MapType(false, typeArgs[0], typeArgs[1])) }; - builtIns.SystemModule.TopLevelDecls.AddRange(valuetypeDecls); + builtIns.SystemModule.SourceDecls.AddRange(valuetypeDecls); // Resolution error handling relies on being able to get to the 0-tuple declaration builtIns.TupleType(Token.NoToken, 0, true); @@ -677,7 +677,7 @@ public void ResolveProgram(Program prog) { } foreach (var module in prog.Modules()) { - foreach (var iter in ModuleDefinition.AllIteratorDecls(module.TopLevelDecls)) { + foreach (var iter in module.TopLevelDecls.OfType()) { reporter.Info(MessageSource.Resolver, iter.tok, Printer.IteratorClassToString(Reporter.Options, iter)); } } @@ -1311,12 +1311,9 @@ private ModuleBindings BindModuleNames(ModuleDefinition moduleDecl, ModuleBindin var prefixNamedModules = entry.Value; var tok = prefixNamedModules.First().Item1[0]; var modDef = new ModuleDefinition(tok.ToRange(), new Name(tok.ToRange(), name), new List(), false, false, null, moduleDecl, null, false); - // Every module is expected to have a default class, so we create and add one now - var defaultClass = new DefaultClassDecl(modDef, new List()); - modDef.TopLevelDecls.Add(defaultClass); // Add the new module to the top-level declarations of its parent and then bind its names as usual var subdecl = new LiteralModuleDecl(modDef, moduleDecl); - moduleDecl.TopLevelDecls.Add(subdecl); + moduleDecl.ResolvedPrefixNamedModules.Add(subdecl); BindModuleName_LiteralModuleDecl(subdecl, prefixNamedModules.ConvertAll(ShortenPrefix), bindings); } @@ -1366,7 +1363,7 @@ private void BindModuleName_LiteralModuleDecl(LiteralModuleDecl litmod, litmod.ModuleDef; // change the parent, now that we have found the right parent module for the prefix-named module var sm = new LiteralModuleDecl(tup.Item2.ModuleDef, litmod.ModuleDef); // this will create a ModuleDecl with the right parent - litmod.ModuleDef.TopLevelDecls.Add(sm); + litmod.ModuleDef.ResolvedPrefixNamedModules.Add(sm); } else { litmod.ModuleDef.PrefixNamedModules.Add(tup); } @@ -1696,13 +1693,11 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport sig.VisibilityScope = new VisibilityScope(); sig.VisibilityScope.Augment(moduleDef.VisibilityScope); - List declarations = moduleDef.TopLevelDecls; - // This is solely used to detect duplicates amongst the various e Dictionary toplevels = new Dictionary(); // Now add the things present var anonymousImportCount = 0; - foreach (TopLevelDecl d in declarations) { + foreach (TopLevelDecl d in moduleDef.TopLevelDecls) { Contract.Assert(d != null); if (d is RevealableTypeDecl) { @@ -1879,7 +1874,7 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport } // Now, for each class, register its possibly-null type - foreach (TopLevelDecl d in declarations) { + foreach (TopLevelDecl d in moduleDef.TopLevelDecls) { if ((d as ClassDecl)?.NonNullTypeDecl != null) { var name = d.Name + "?"; TopLevelDecl prev; @@ -2018,15 +2013,15 @@ private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, in bool hasDefaultClass = false; foreach (var kv in p.TopLevels) { hasDefaultClass = kv.Value is DefaultClassDecl || hasDefaultClass; - if (!(kv.Value is NonNullTypeDecl)) { + if (!(kv.Value is NonNullTypeDecl or DefaultClassDecl)) { var clone = CloneDeclaration(p.VisibilityScope, kv.Value, mod, mods, Name, compilationModuleClones); - mod.TopLevelDecls.Add(clone); + mod.SourceDecls.Add(clone); } } if (!hasDefaultClass) { - DefaultClassDecl cl = new DefaultClassDecl(mod, p.StaticMembers.Values.ToList()); - mod.TopLevelDecls.Add(CloneDeclaration(p.VisibilityScope, cl, mod, mods, Name, compilationModuleClones)); + var defaultClassDecl = new DefaultClassDecl(mod, p.StaticMembers.Values.ToList()); + mod.DefaultClass = (DefaultClassDecl)CloneDeclaration(p.VisibilityScope, defaultClassDecl, mod, mods, Name, compilationModuleClones); } var sig = RegisterTopLevelDecls(mod, true); @@ -2171,7 +2166,7 @@ public bool ResolveExport(ModuleDecl alias, ModuleDefinition parent, ModuleQuali return true; } - public void RevealAllInScope(List declarations, VisibilityScope scope) { + public void RevealAllInScope(IEnumerable declarations, VisibilityScope scope) { foreach (TopLevelDecl d in declarations) { d.AddVisibilityScope(scope, false); if (d is TopLevelDeclWithMembers) { diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index 2ce1dd60dd6..013476bdec0 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -177,8 +177,8 @@ internal override void PreResolve(ModuleDefinition m) { Contract.Assert(RefinedSig.ModuleDef != null); Contract.Assert(m.RefinementQId.Def == RefinedSig.ModuleDef); // check that the openness in the imports between refinement and its base matches - List declarations = m.TopLevelDecls; - List baseDeclarations = m.RefinementQId.Def.TopLevelDecls; + var declarations = m.TopLevelDecls; + var baseDeclarations = m.RefinementQId.Def.TopLevelDecls.ToList(); foreach (var im in declarations) { // TODO: this is a terribly slow algorithm; use the symbol table instead foreach (var bim in baseDeclarations) { @@ -222,8 +222,9 @@ void PreResolveWorker(ModuleDefinition m) { // Create a simple name-to-decl dictionary. Ignore any duplicates at this time. var declaredNames = new Dictionary(); - for (int i = 0; i < m.TopLevelDecls.Count; i++) { - var d = m.TopLevelDecls[i]; + var topLevelDecls = m.TopLevelDecls.ToList(); + for (int i = 0; i < topLevelDecls.Count; i++) { + var d = topLevelDecls[i]; if (!declaredNames.ContainsKey(d.Name)) { declaredNames.Add(d.Name, i); } @@ -232,12 +233,12 @@ void PreResolveWorker(ModuleDefinition m) { // Merge the declarations of prev into the declarations of m List processedDecl = new List(); foreach (var d in prev.TopLevelDecls) { - int index; processedDecl.Add(d.Name); - if (!declaredNames.TryGetValue(d.Name, out index)) { - m.TopLevelDecls.Add(refinementCloner.CloneDeclaration(d, m)); + if (!declaredNames.TryGetValue(d.Name, out var index)) { + var clone = refinementCloner.CloneDeclaration(d, m); + m.SourceDecls.Add(clone); } else { - var nw = m.TopLevelDecls[index]; + var nw = topLevelDecls[index]; if (d.Name == "_default" || nw.IsRefining || d is AbstractTypeDecl) { MergeTopLevelDecls(m, nw, d, index); } else if (nw is TypeSynonymDecl) { @@ -254,10 +255,9 @@ void PreResolveWorker(ModuleDefinition m) { // Merge the imports of prev var prevTopLevelDecls = RefinedSig.TopLevels.Values; foreach (var d in prevTopLevelDecls) { - int index; - if (!processedDecl.Contains(d.Name) && declaredNames.TryGetValue(d.Name, out index)) { + if (!processedDecl.Contains(d.Name) && declaredNames.TryGetValue(d.Name, out var index)) { // if it is redefined, we need to merge them. - var nw = m.TopLevelDecls[index]; + var nw = topLevelDecls[index]; MergeTopLevelDecls(m, nw, d, index); } } @@ -266,7 +266,7 @@ void PreResolveWorker(ModuleDefinition m) { Contract.Assert(moduleUnderConstruction == m); // this should be as it was set earlier in this method } - private void CheckSuperfluousRefiningMarks(List topLevelDecls, List excludeList) { + private void CheckSuperfluousRefiningMarks(IEnumerable topLevelDecls, List excludeList) { Contract.Requires(topLevelDecls != null); Contract.Requires(excludeList != null); foreach (var d in topLevelDecls) { @@ -280,7 +280,7 @@ private void CheckSuperfluousRefiningMarks(List topLevelDecls, Lis /// Give unresolved newtypes a reasonable default type (int), to avoid having to support `null` in the /// rest of the resolution pipeline. /// - private void AddDefaultBaseTypeToUnresolvedNewtypes(List topLevelDecls) { + private void AddDefaultBaseTypeToUnresolvedNewtypes(IEnumerable topLevelDecls) { foreach (var d in topLevelDecls) { if (d is NewtypeDecl { IsRefining: true, BaseType: null } decl) { Reporter.Info(MessageSource.RefinementTransformer, decl.tok, $"defaulting to 'int' for unspecified base type of '{decl.Name}'"); @@ -300,6 +300,7 @@ private void MergeModuleExports(ModuleExportDecl nw, ModuleExportDecl d) { private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDecl d, int index) { var commonMsg = "a {0} declaration ({1}) in a refinement module can only refine a {0} declaration or replace an abstract type declaration"; + var topLevelDecls = m.TopLevelDecls.ToList(); if (d is ModuleDecl) { if (!(nw is ModuleDecl)) { @@ -371,7 +372,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec } } if (nw is TopLevelDeclWithMembers) { - m.TopLevelDecls[index] = MergeClass((TopLevelDeclWithMembers)nw, od); + topLevelDecls[index] = MergeClass((TopLevelDeclWithMembers)nw, od); } else if (od.Members.Count != 0) { Reporter.Error(MessageSource.RefinementTransformer, nw, "a {0} ({1}) cannot declare members, so it cannot refine an abstract type with members", @@ -387,7 +388,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec var (dd, nwd) = ((DatatypeDecl)d, (DatatypeDecl)nw); Contract.Assert(!nwd.Ctors.Any()); nwd.Ctors.AddRange(dd.Ctors.Select(refinementCloner.CloneCtor)); - m.TopLevelDecls[index] = MergeClass((DatatypeDecl)nw, (DatatypeDecl)d); + topLevelDecls[index] = MergeClass((DatatypeDecl)nw, (DatatypeDecl)d); } else if (nw is DatatypeDecl) { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } else if (d is NewtypeDecl && nw is NewtypeDecl) { @@ -399,25 +400,25 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec nwn.Constraint = dn.Constraint == null ? null : refinementCloner.CloneExpr(dn.Constraint); nwn.WitnessKind = dn.WitnessKind; nwn.Witness = dn.Witness == null ? null : refinementCloner.CloneExpr(dn.Witness); - m.TopLevelDecls[index] = MergeClass((NewtypeDecl)nw, (NewtypeDecl)d); + topLevelDecls[index] = MergeClass((NewtypeDecl)nw, (NewtypeDecl)d); } else if (nw is NewtypeDecl) { // `.Basetype` will be set in AddDefaultBaseTypeToUnresolvedNewtypes Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } else if (nw is IteratorDecl) { if (d is IteratorDecl) { - m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d); + topLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name); } } else if (nw is TraitDecl) { if (d is TraitDecl) { - m.TopLevelDecls[index] = MergeClass((TraitDecl)nw, (TraitDecl)d); + topLevelDecls[index] = MergeClass((TraitDecl)nw, (TraitDecl)d); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } } else if (nw is ClassDecl) { if (d is ClassDecl && !(d is TraitDecl)) { - m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d); + topLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 59ab2f2c27c..4077e826cc8 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -794,7 +794,7 @@ private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { mods.Insert(0, forModule); foreach (ModuleDefinition m in mods) { - foreach (TopLevelDecl d in m.TopLevelDecls.FindAll(VisibleInScope)) { + foreach (TopLevelDecl d in m.TopLevelDecls.Where(VisibleInScope)) { currentDeclaration = d; if (d is AbstractTypeDecl) { var dd = (AbstractTypeDecl)d; diff --git a/Source/DafnyPipeline.Test/Trivia.cs b/Source/DafnyPipeline.Test/Trivia.cs index d67c093591b..a28b8291d19 100644 --- a/Source/DafnyPipeline.Test/Trivia.cs +++ b/Source/DafnyPipeline.Test/Trivia.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.IO; +using System.Linq; using System.Text.RegularExpressions; using DafnyTestGeneration; using Bpl = Microsoft.Boogie; @@ -80,13 +81,14 @@ ensures true var dafnyProgram = Utils.Parse(options, programString, false); var reporter = dafnyProgram.Reporter; Assert.Equal(0, reporter.ErrorCount); - Assert.Equal(6, dafnyProgram.DefaultModuleDef.TopLevelDecls.Count); - var moduleTest = dafnyProgram.DefaultModuleDef.TopLevelDecls[0] as LiteralModuleDecl; - var trait1 = dafnyProgram.DefaultModuleDef.TopLevelDecls[1]; - var trait2 = dafnyProgram.DefaultModuleDef.TopLevelDecls[2]; - var subsetType = dafnyProgram.DefaultModuleDef.TopLevelDecls[3]; - var class1 = dafnyProgram.DefaultModuleDef.TopLevelDecls[4] as ClassDecl; - var defaultClass = dafnyProgram.DefaultModuleDef.TopLevelDecls[5] as ClassDecl; + var topLevelDecls = dafnyProgram.DefaultModuleDef.TopLevelDecls.ToList(); + Assert.Equal(6, topLevelDecls.Count()); + var moduleTest = topLevelDecls[0] as LiteralModuleDecl; + var trait1 = topLevelDecls[1]; + var trait2 = topLevelDecls[2]; + var subsetType = topLevelDecls[3]; + var class1 = topLevelDecls[4] as ClassDecl; + var defaultClass = topLevelDecls[5] as ClassDecl; Assert.NotNull(moduleTest); Assert.NotNull(class1); Assert.NotNull(defaultClass); diff --git a/Source/DafnyServer/SignatureAndCompletionTable.cs b/Source/DafnyServer/SignatureAndCompletionTable.cs index b4d163853fe..bf1596bd9a4 100644 --- a/Source/DafnyServer/SignatureAndCompletionTable.cs +++ b/Source/DafnyServer/SignatureAndCompletionTable.cs @@ -107,7 +107,7 @@ private void AddFields(ModuleDefinition module, List informat } private void AddClasses(ModuleDefinition module, List information) { - foreach (var cs in ModuleDefinition.AllClasses(module.TopLevelDecls). + foreach (var cs in module.TopLevelDecls.OfType(). Where(cl => !cl.Tok.FromIncludeDirective(_dafnyProgram))) { if (cs.EnclosingModuleDefinition != null && cs.tok != null) { var classSymbol = new SymbolInformation { diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs index a4e3a68d5fc..5c72ae0eb14 100644 --- a/Source/DafnyTestGeneration/DafnyInfo.cs +++ b/Source/DafnyTestGeneration/DafnyInfo.cs @@ -484,7 +484,10 @@ private void Visit(LiteralModuleDecl d) { } else if (d.FullDafnyName != "") { info.ToImportAs[d.FullDafnyName] = d.Name; } - d.ModuleDef.TopLevelDecls.ForEach(Visit); + + foreach (var topLevelDecl in d.ModuleDef.TopLevelDecls) { + Visit(topLevelDecl); + } } private void Visit(IndDatatypeDecl d) { diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index e91d1a04265..97cdd03051e 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -137,7 +137,9 @@ internal void PreResolve(Program program) { private static void AddByMethod(TopLevelDecl d) { if (d is LiteralModuleDecl moduleDecl) { - moduleDecl.ModuleDef.TopLevelDecls.ForEach(AddByMethod); + foreach (var topLevelDecl in moduleDecl.ModuleDef.TopLevelDecls) { + AddByMethod(topLevelDecl); + } } else if (d is TopLevelDeclWithMembers withMembers) { withMembers.Members.OfType().Iter(AddByMethod); } From 0dbd1ce83f96ff0d2b7e3acd68bceb9cb0decc3b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 23 May 2023 16:54:20 +0200 Subject: [PATCH 14/68] Bugfixes --- Source/DafnyCore/AST/TopLevelDeclarations.cs | 18 ++++++++++++++---- .../Compilers/Cplusplus/Compiler-cpp.cs | 2 +- Source/DafnyCore/Resolver/Resolver.cs | 11 ++++------- 3 files changed, 19 insertions(+), 12 deletions(-) diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 92aa04dde44..b3264fea5b5 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -859,9 +859,15 @@ public string FullName { public readonly List ResolvedPrefixNamedModules = new(); [FilledInDuringResolution] public readonly List, LiteralModuleDecl>> PrefixNamedModules = new(); // filled in by the parser; emptied by the resolver - public IEnumerable TopLevelDecls => (DefaultClass == null ? Enumerable.Empty() : new TopLevelDecl[] {DefaultClass}). - Concat(SourceDecls).Concat(ResolvedPrefixNamedModules); - + public virtual IEnumerable TopLevelDecls => SourceDecls. + Concat(DefaultClasses). + Concat(ResolvedPrefixNamedModules); + + protected IEnumerable DefaultClasses + { + get { return DefaultClass == null ? Enumerable.Empty() : new TopLevelDecl[] {DefaultClass}; } + } + [FilledInDuringResolution] public readonly Graph CallGraph = new(); [FilledInDuringResolution] @@ -875,7 +881,7 @@ void ObjectInvariant() { public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : base(cloner, original) { NameNode = name; - IsBuiltinName = original.IsBuiltinName; + IsBuiltinName = true; PrefixIds = original.PrefixIds.Select(cloner.Tok).ToList(); IsFacade = original.IsFacade; Attributes = original.Attributes; @@ -1155,6 +1161,10 @@ public DefaultModuleDefinition(IList rootSourceUris) RootSourceUris = rootSourceUris; } + // TODO added to get similar compilation behavior. Probably not useful. + public override IEnumerable TopLevelDecls => + DefaultClasses.Concat(SourceDecls).Concat(ResolvedPrefixNamedModules); + public override bool IsDefaultModule => true; } diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs index 181df1ce6d0..5d3bdcd5425 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs @@ -159,7 +159,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a } protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) { - var s = string.Format("namespace {0} ", IdProtect(moduleName)); + var s = $"namespace {IdProtect(moduleName)} "; string footer = "// end of " + s + " declarations"; this.modDeclWr = this.modDeclsWr.NewBlock(s, footer); string footer1 = "// end of " + s + " datatype declarations"; diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 07629c48e0c..e53993910df 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -559,7 +559,8 @@ public void ResolveProgram(Program prog) { if (reporter.ErrorCount == errorCount && !m.IsAbstract) { // compilation should only proceed if everything is good, including the signature (which preResolveErrorCount does not include); CompilationCloner cloner = new CompilationCloner(compilationModuleClones); - var nw = cloner.CloneModuleDefinition(m, new Name(m.NameNode.RangeToken, m.GetCompileName(Options) + "_Compile")); + var compileName = new Name(m.NameNode.RangeToken, m.GetCompileName(Options) + "_Compile"); + var nw = cloner.CloneModuleDefinition(m, compileName); compilationModuleClones.Add(m, nw); var oldErrorsOnly = reporter.ErrorsOnly; reporter.ErrorsOnly = true; // turn off warning reporting for the clone @@ -2010,19 +2011,15 @@ private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, in var mod = new ModuleDefinition(RangeToken.NoToken, new Name(Name + ".Abs"), new List(), true, true, null, null, null, false); mod.Height = Height; - bool hasDefaultClass = false; foreach (var kv in p.TopLevels) { - hasDefaultClass = kv.Value is DefaultClassDecl || hasDefaultClass; if (!(kv.Value is NonNullTypeDecl or DefaultClassDecl)) { var clone = CloneDeclaration(p.VisibilityScope, kv.Value, mod, mods, Name, compilationModuleClones); mod.SourceDecls.Add(clone); } } - if (!hasDefaultClass) { - var defaultClassDecl = new DefaultClassDecl(mod, p.StaticMembers.Values.ToList()); - mod.DefaultClass = (DefaultClassDecl)CloneDeclaration(p.VisibilityScope, defaultClassDecl, mod, mods, Name, compilationModuleClones); - } + var defaultClassDecl = new DefaultClassDecl(mod, p.StaticMembers.Values.ToList()); + mod.DefaultClass = (DefaultClassDecl)CloneDeclaration(p.VisibilityScope, defaultClassDecl, mod, mods, Name, compilationModuleClones); var sig = RegisterTopLevelDecls(mod, true); sig.Refines = p.Refines; From 8b205270c272981233f1b616dc2f71872635f3c8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 13:03:22 +0200 Subject: [PATCH 15/68] Several bugfixes and workarounds --- Source/DafnyCore.Test/DooFileTest.cs | 2 +- Source/DafnyCore/AST/BuiltIns.cs | 3 ++- Source/DafnyCore/AST/DafnyAst.cs | 2 +- Source/DafnyCore/AST/FileModuleDefinition.cs | 2 +- Source/DafnyCore/AST/TopLevelDeclarations.cs | 27 ++++++++++++------- Source/DafnyCore/Dafny.atg | 2 +- Source/DafnyCore/DafnyMain.cs | 7 ++++- .../Unit/DafnyLangSymbolResolverTest.cs | 2 +- .../Unit/GhostStateDiagnosticCollectorTest.cs | 2 +- .../Unit/ParserExceptionTest.cs | 2 +- .../Symbols/SignatureAndCompletionTable.cs | 2 +- .../Workspace/TextDocumentLoader.cs | 2 +- .../DafnyPipeline.Test/FormatterBaseTest.cs | 2 +- Source/DafnyPipeline.Test/TranslatorTest.cs | 2 +- Source/DafnyServer/DafnyHelper.cs | 2 +- Source/DafnyTestGeneration/Utils.cs | 2 +- Test/allocated1/dafny0/Definedness.dfy | 2 +- Test/allocated1/dafny0/DirtyLoops.dfy | 2 +- Test/allocated1/dafny0/LetExpr.dfy | 2 +- 19 files changed, 42 insertions(+), 27 deletions(-) diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs index 8465dffa97f..3c9eee0a2e0 100644 --- a/Source/DafnyCore.Test/DooFileTest.cs +++ b/Source/DafnyCore.Test/DooFileTest.cs @@ -31,7 +31,7 @@ public void UnknownManifestEntries() { private static Program ParseProgram(string dafnyProgramText, DafnyOptions options) { const string fullFilePath = "untitled:foo"; var rootUri = new Uri(fullFilePath); - var outerModule = new DefaultModuleDefinition(new List { rootUri }); + var outerModule = new DefaultModuleDefinition(new List { rootUri }, false); Microsoft.Dafny.Type.ResetScopes(); var errorReporter = new ConsoleErrorReporter(options, outerModule); var program = ParseUtils.Parse(dafnyProgramText, rootUri, errorReporter); diff --git a/Source/DafnyCore/AST/BuiltIns.cs b/Source/DafnyCore/AST/BuiltIns.cs index dbd2e64720d..63a2f8620d4 100644 --- a/Source/DafnyCore/AST/BuiltIns.cs +++ b/Source/DafnyCore/AST/BuiltIns.cs @@ -8,7 +8,8 @@ namespace Microsoft.Dafny; public class BuiltIns { public DafnyOptions Options { get; } - public readonly ModuleDefinition SystemModule = new(RangeToken.NoToken, new Name("_System"), new List(), false, false, null, null, null, true); + public readonly ModuleDefinition SystemModule = new(RangeToken.NoToken, new Name("_System"), new List(), + false, false, null, null, null, true, false); internal readonly Dictionary arrayTypeDecls = new Dictionary(); public readonly Dictionary ArrowTypeDecls = new Dictionary(); public readonly Dictionary PartialArrowTypeDecls = new Dictionary(); // same keys as arrowTypeDecl diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 9e5e86414c4..b4f37ca0d5d 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -116,7 +116,7 @@ public IToken GetFirstTopLevelToken() { return null; } - var firstToken = rootToken.Next; + var firstToken = rootToken; // We skip all included files while (firstToken is { Next: { } } && firstToken.Next.Filepath != rootToken.Filepath) { firstToken = firstToken.Next; diff --git a/Source/DafnyCore/AST/FileModuleDefinition.cs b/Source/DafnyCore/AST/FileModuleDefinition.cs index 9df8e3de08c..d5aa4572b1f 100644 --- a/Source/DafnyCore/AST/FileModuleDefinition.cs +++ b/Source/DafnyCore/AST/FileModuleDefinition.cs @@ -13,7 +13,7 @@ public class FileModuleDefinition : ModuleDefinition { public FileModuleDefinition() : base(RangeToken.NoToken, new Name("_module"), new List(), - false, false, null, null, null, true) { + false, false, null, null, null, true, false) { { } } diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 8c1e7f6483d..ddab70c36d8 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -850,6 +850,7 @@ public string FullName { public readonly bool IsAbstract; public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface) private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled. + private readonly bool defaultClassFirst; public DefaultClassDecl DefaultClass { get; set; } @@ -858,9 +859,13 @@ public string FullName { public readonly List ResolvedPrefixNamedModules = new(); [FilledInDuringResolution] public readonly List, LiteralModuleDecl>> PrefixNamedModules = new(); // filled in by the parser; emptied by the resolver - public virtual IEnumerable TopLevelDecls => SourceDecls. - Concat(DefaultClasses). - Concat(ResolvedPrefixNamedModules); + public virtual IEnumerable TopLevelDecls => + defaultClassFirst ? DefaultClasses. + Concat(SourceDecls). + Concat(ResolvedPrefixNamedModules) + : SourceDecls. + Concat(DefaultClasses). + Concat(ResolvedPrefixNamedModules); protected IEnumerable DefaultClasses { get { return DefaultClass == null ? Enumerable.Empty() : new TopLevelDecl[] { DefaultClass }; } @@ -886,6 +891,7 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : b IsAbstract = original.IsAbstract; RefinementQId = original.RefinementQId; EnclosingModule = original.EnclosingModule; + defaultClassFirst = original.defaultClassFirst; foreach (var d in original.SourceDecls) { SourceDecls.Add(cloner.CloneDeclaration(d, this)); } @@ -902,7 +908,8 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : b } public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool isAbstract, bool isFacade, - ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, bool isBuiltinName) : base(tok) { + ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, + bool isBuiltinName, bool defaultClassFirst = false) : base(tok) { Contract.Requires(tok != null); Contract.Requires(name != null); this.NameNode = name; @@ -913,6 +920,7 @@ public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool this.IsAbstract = isAbstract; this.IsFacade = isFacade; this.IsBuiltinName = isBuiltinName; + this.defaultClassFirst = defaultClassFirst; if (Name != "_System") { DefaultClass = new DefaultClassDecl(this, new List()); @@ -1154,14 +1162,15 @@ public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original) RootSourceUris = original.RootSourceUris; } - public DefaultModuleDefinition(IList rootSourceUris) - : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, null, null, null, true) { + public DefaultModuleDefinition(IList rootSourceUris, bool defaultClassFirst) + : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, + null, null, null, true, defaultClassFirst) { RootSourceUris = rootSourceUris; } // TODO added to get similar compilation behavior. Probably not useful. - public override IEnumerable TopLevelDecls => - DefaultClasses.Concat(SourceDecls).Concat(ResolvedPrefixNamedModules); + // public override IEnumerable TopLevelDecls => + // DefaultClasses.Concat(SourceDecls).Concat(ResolvedPrefixNamedModules); public override bool IsDefaultModule => true; } @@ -2087,7 +2096,7 @@ public NoContext(ModuleDefinition module) { public bool AllowsAllocation => true; } -public class AbstractTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat, IHasDocstring { +public class AbstractTypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, ICanFormat, IHasDocstring { public override string WhatKind { get { return "abstract type"; } } public override bool CanBeRevealed() { return true; } public readonly TypeParameter.TypeParameterCharacteristics Characteristics; diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 315f3fd44cd..7d00bdc7650 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1559,7 +1559,7 @@ SynonymTypeDecl ] (. if (td == null) { - if (module is DefaultModuleDefinition) { + if (module is DefaultModuleDefinition or FileModuleDefinition) { // abstract type declarations at the very outermost program scope get an automatic (!new) characteristics.ContainsNoReferenceTypes = true; } diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index 91d0feafab9..84a34a8b270 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -58,8 +58,9 @@ public static string Parse(IReadOnlyList files, string programName, D Contract.Requires(files != null); program = null; + var defaultClassFirst = options.VerifyAllModules; var defaultModuleDefinition = - new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList()); + new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList(), defaultClassFirst); ErrorReporter reporter = options.DiagnosticsFormat switch { DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(options, defaultModuleDefinition), DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(options, defaultModuleDefinition), @@ -67,6 +68,10 @@ public static string Parse(IReadOnlyList files, string programName, D }; program = ParseUtils.ParseFiles(programName, files, reporter, CancellationToken.None); + var errorCount = program.Reporter.ErrorCount; + if (errorCount != 0) { + return $"{errorCount} parse errors detected in {program.Name}"; + } return null; } diff --git a/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs b/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs index b7b87d2c10a..dcd3fcd2ad6 100644 --- a/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs @@ -27,7 +27,7 @@ public CollectingErrorReporter(DafnyOptions options, DefaultModuleDefinition out class DummyModuleDecl : LiteralModuleDecl { public DummyModuleDecl() : base( - new DefaultModuleDefinition(new List()), null) { + new DefaultModuleDefinition(new List(), false), null) { } public override object Dereference() { return this; diff --git a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs index ce4f4d6c0ef..d36131fe201 100644 --- a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs @@ -49,7 +49,7 @@ public CollectingErrorReporter(DafnyOptions options, DefaultModuleDefinition out class DummyModuleDecl : LiteralModuleDecl { public DummyModuleDecl(IList rootUris) : base( - new DefaultModuleDefinition(rootUris), null) { + new DefaultModuleDefinition(rootUris, false), null) { } public override object Dereference() { return this; diff --git a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs index 0087708f48f..609aac1003b 100644 --- a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs @@ -29,7 +29,7 @@ public void DocumentWithParserExceptionDisplaysIt() { var options = new DafnyOptions(DafnyOptions.DefaultImmutableOptions); var documentItem = CreateTestDocument(source, TestFilePath); var uri = new Uri("file:///" + TestFilePath); - var outerModule = new DefaultModuleDefinition(new List { uri }); + var outerModule = new DefaultModuleDefinition(new List { uri }, false); var errorReporter = new ParserExceptionSimulatingErrorReporter(options, outerModule); parser.Parse(new DocumentTextBuffer(documentItem), errorReporter, default); Assert.Equal($"/{TestFilePath}(1,0): Error: [internal error] Parser exception: Simulated parser internal error", errorReporter.LastMessage); diff --git a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs b/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs index 759d7341b82..886ea00a133 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs @@ -43,7 +43,7 @@ public class SignatureAndCompletionTable { private readonly DafnyLangTypeResolver typeResolver; public static SignatureAndCompletionTable Empty(DafnyOptions options, DocumentTextBuffer textDocument) { - var outerModule = new DefaultModuleDefinition(new List() { textDocument.Uri.ToUri() }); + var outerModule = new DefaultModuleDefinition(new List() { textDocument.Uri.ToUri() }, false); var errorReporter = new DiagnosticErrorReporter(options, outerModule, textDocument.Text, textDocument.Uri); return new SignatureAndCompletionTable( NullLogger.Instance, diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index e0d26389fc2..3846d072aa1 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -82,7 +82,7 @@ public async Task LoadAsync(DafnyOptions options, Document private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuffer textDocument, CancellationToken cancellationToken) { - var outerModule = new DefaultModuleDefinition(new List() { textDocument.Uri.ToUri() }); + var outerModule = new DefaultModuleDefinition(new List() { textDocument.Uri.ToUri() }, false); var errorReporter = new DiagnosticErrorReporter(options, outerModule, textDocument.Text, textDocument.Uri); statusPublisher.SendStatusNotification(textDocument, CompilationStatus.Parsing); var program = parser.Parse(textDocument, errorReporter, cancellationToken); diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index 7fd13f86855..423858a7579 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -54,7 +54,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString : removeTrailingNewlineRegex.Replace(programString, ""); var uri = new Uri("virtual:virtual"); - var outerModule = new DefaultModuleDefinition(new List() { uri }); + var outerModule = new DefaultModuleDefinition(new List() { uri }, false); BatchErrorReporter reporter = new BatchErrorReporter(options, outerModule); Microsoft.Dafny.Type.ResetScopes(); diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index c7e9c98a3c7..c7e72bd889e 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -75,7 +75,7 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption Microsoft.Dafny.Type.ResetScopes(); options = options ?? new DafnyOptions(TextReader.Null, TextWriter.Null, TextWriter.Null); var uri = new Uri("virtual:///virtual"); - var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); + var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }, false); BatchErrorReporter reporter = new BatchErrorReporter(options, defaultModuleDefinition); var dafnyProgram = ParseUtils.Parse(program, uri, reporter); ParseUtils.Parse(program, uri, reporter); diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 9809645d865..20ab8ef3b25 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -41,7 +41,7 @@ public bool Verify() { private bool Parse() { var uri = new Uri("transcript:///" + fname); - var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); + var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }, false); reporter = new ConsoleErrorReporter(options, defaultModuleDefinition); var program = ParseUtils.ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri.LocalPath, new StringReader(source)) }, reporter, CancellationToken.None); diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index ec2cad7e280..ec898752927 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -76,7 +76,7 @@ public static Type CopyWithReplacements(Type type, List from, List /// public static Program/*?*/ Parse(DafnyOptions options, string source, bool resolve = true, Uri uri = null) { uri ??= new Uri(Path.GetTempPath()); - var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }); + var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }, false); var reporter = new BatchErrorReporter(options, defaultModuleDefinition); var program = ParseUtils.ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, diff --git a/Test/allocated1/dafny0/Definedness.dfy b/Test/allocated1/dafny0/Definedness.dfy index 99c994c14b2..a8450756d4e 100644 --- a/Test/allocated1/dafny0/Definedness.dfy +++ b/Test/allocated1/dafny0/Definedness.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // ----------------- wellformed specifications ---------------------- diff --git a/Test/allocated1/dafny0/DirtyLoops.dfy b/Test/allocated1/dafny0/DirtyLoops.dfy index f8a1063e2c0..44987813a8c 100644 --- a/Test/allocated1/dafny0/DirtyLoops.dfy +++ b/Test/allocated1/dafny0/DirtyLoops.dfy @@ -1,4 +1,4 @@ // RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t" -// RUN: %exits-with 0 %dafny /verifyAllModules /allocated:1 /noVerify "%t.dprint.dfy" >> "%t" +// RUN: %exits-with 0 %dafny /allocated:1 /noVerify "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" include "../../dafny0/DirtyLoops.dfy" diff --git a/Test/allocated1/dafny0/LetExpr.dfy b/Test/allocated1/dafny0/LetExpr.dfy index a478d95f15c..bd7f568f749 100644 --- a/Test/allocated1/dafny0/LetExpr.dfy +++ b/Test/allocated1/dafny0/LetExpr.dfy @@ -1,4 +1,4 @@ // RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" -// RUN: %dafny /verifyAllModules /allocated:1 /noVerify /compile:0 "%t.dprint.dfy" >> "%t" +// RUN: %dafny /allocated:1 /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" include "../../dafny0/LetExpr.dfy" From 8d0fc92f5f35d0454d56d800be377be5fe0f4f38 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 16:16:49 +0200 Subject: [PATCH 16/68] Cloner and other fixes --- Source/DafnyCore/AST/Cloner.cs | 6 +++++- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 4 ++++ Source/DafnyCore/AST/TopLevelDeclarations.cs | 9 ++++++--- Source/DafnyCore/DafnyFile.cs | 4 +++- 4 files changed, 18 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index b59680035ef..021ab5e5db1 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -683,6 +683,10 @@ public override Expression CloneExpr(Expression expr) { /// This cloner copies the origin module signatures to their cloned declarations /// class DeepModuleSignatureCloner : Cloner { + public DeepModuleSignatureCloner(bool cloneResolvedFields = false) : base(cloneResolvedFields) + { + } + public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) { var dd = base.CloneDeclaration(d, m); if (d is ModuleDecl) { @@ -894,7 +898,7 @@ public override BlockStmt CloneMethodBody(Method m) { class CompilationCloner : DeepModuleSignatureCloner { Dictionary compilationModuleClones; public CompilationCloner(Dictionary compilationModuleClones) - : base() { + : base(true) { this.compilationModuleClones = compilationModuleClones; } diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index c40b9a43909..ae311050c5e 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -202,6 +202,10 @@ public static void AddFileModuleToProgram(FileModuleDefinition fileModule, Defau defaultModule.Includes.Add(include); } + foreach (var prefixNamedModule in fileModule.PrefixNamedModules) { + defaultModule.PrefixNamedModules.Add(prefixNamedModule); + } + defaultModule.DefaultClass.SetMembersBeforeResolution(); } diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index ddab70c36d8..2f7ae6d826c 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -897,12 +897,15 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : b } DefaultClass = (DefaultClassDecl)cloner.CloneDeclaration(original.DefaultClass, this); + foreach (var tup in original.PrefixNamedModules) { + var newTup = new Tuple, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)cloner.CloneDeclaration(tup.Item2, this)); + PrefixNamedModules.Add(newTup); + } if (cloner.CloneResolvedFields) { Height = original.Height; - foreach (var tup in original.PrefixNamedModules) { - var newTup = new Tuple, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)cloner.CloneDeclaration(tup.Item2, this)); - PrefixNamedModules.Add(newTup); + foreach (var tup in original.ResolvedPrefixNamedModules) { + ResolvedPrefixNamedModules.Add(cloner.CloneDeclaration(tup, this)); } } } diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index f8a079de765..6dcc727a656 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -19,7 +19,9 @@ public class DafnyFile { // TODO take a Uri instead of a filePath - public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverride = null) : this(options, contentOverride != null ? new Uri("stdin:///") : new Uri(filePath)) { + public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverride = null) + : this(options, contentOverride != null ? new Uri("stdin:///") : new Uri(filePath), contentOverride) + { Uri = contentOverride != null ? new Uri("stdin:///") : new Uri(filePath); BaseName = contentOverride != null ? "" : Path.GetFileName(filePath); } From bc09b4fee95328e7c330144f9754db259b1d9d74 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 16:25:32 +0200 Subject: [PATCH 17/68] Fix compilation module cloning bug --- Source/DafnyCore/AST/Cloner.cs | 2 +- Source/DafnyCore/AST/TopLevelDeclarations.cs | 12 +++++------- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 021ab5e5db1..0a154f27376 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -898,7 +898,7 @@ public override BlockStmt CloneMethodBody(Method m) { class CompilationCloner : DeepModuleSignatureCloner { Dictionary compilationModuleClones; public CompilationCloner(Dictionary compilationModuleClones) - : base(true) { + : base(false) { this.compilationModuleClones = compilationModuleClones; } diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 2f7ae6d826c..689c9856fff 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -901,12 +901,14 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : b var newTup = new Tuple, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)cloner.CloneDeclaration(tup.Item2, this)); PrefixNamedModules.Add(newTup); } + + // For cloning modules into their compiled variants, we don't want to copy resolved fields, but we do need to copy this. + foreach (var tup in original.ResolvedPrefixNamedModules) { + ResolvedPrefixNamedModules.Add(cloner.CloneDeclaration(tup, this)); + } if (cloner.CloneResolvedFields) { Height = original.Height; - foreach (var tup in original.ResolvedPrefixNamedModules) { - ResolvedPrefixNamedModules.Add(cloner.CloneDeclaration(tup, this)); - } } } @@ -1171,10 +1173,6 @@ public DefaultModuleDefinition(IList rootSourceUris, bool defaultClassFirst RootSourceUris = rootSourceUris; } - // TODO added to get similar compilation behavior. Probably not useful. - // public override IEnumerable TopLevelDecls => - // DefaultClasses.Concat(SourceDecls).Concat(ResolvedPrefixNamedModules); - public override bool IsDefaultModule => true; } From 02f55cc966d0f8e72b79e42a60c8e4f9f50efbbe Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 19:24:16 +0200 Subject: [PATCH 18/68] Fix move declarations bug --- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 9 ++++++++- Source/DafnyCore/AST/Grammar/Printer.cs | 6 +++--- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index ae311050c5e..dbfae4cacf9 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -183,11 +183,18 @@ public static Program ParseFiles(string programName, IReadOnlyList fi } public static void AddFileModuleToProgram(FileModuleDefinition fileModule, DefaultModuleDefinition defaultModule) { - foreach (var declToMove in fileModule.TopLevelDecls) { + foreach (var declToMove in fileModule.TopLevelDecls. + Where(d => d != null) // Can occur when there are parse errors. Error correction is at fault but we workaround it here + ) + { declToMove.EnclosingModuleDefinition = defaultModule; if (declToMove is LiteralModuleDecl literalModuleDecl) { literalModuleDecl.ModuleDef.EnclosingModule = defaultModule; } + + if (declToMove is ClassLikeDecl classDecl) { + classDecl.NonNullTypeDecl.EnclosingModuleDefinition = defaultModule; + } if (declToMove is DefaultClassDecl defaultClassDecl) { foreach (var member in defaultClassDecl.Members) { defaultModule.DefaultClass.Members.Add(member); diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index dec5e06dfe4..e66155fb3b7 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -246,10 +246,10 @@ public void PrintCallGraph(ModuleDefinition module, int indent) { } return string.CompareOrdinal(m.NameRelativeToModule, n.NameRelativeToModule); }); - foreach (var clbl in SCCs) { + foreach (var callable in SCCs) { Indent(indent); - wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativePredecessorCount(clbl)); - var r = module.CallGraph.GetSCC(clbl); + wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativePredecessorCount(callable)); + var r = module.CallGraph.GetSCC(callable); foreach (var m in r) { Indent(indent); var maybeByMethod = m is Method method && method.IsByMethod ? " (by method)" : ""; From 4b9493ff3c4691df78d64ba4e84869b517190fb2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 19:34:30 +0200 Subject: [PATCH 19/68] Change the StartToken of the FileModuleDefinition so it's an actual token --- Source/DafnyCore/Dafny.atg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 7d00bdc7650..bc6642071df 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -951,7 +951,7 @@ Dafny } { TopDecl } (. - theModule.RangeToken = new RangeToken(startToken, t); + theModule.RangeToken = new RangeToken(startToken.Next, t); .) SYNC EOF From acc76d27045940809d99c15a16d09ed931e82dce Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 19:58:13 +0200 Subject: [PATCH 20/68] Fix refinement transformer code using pointers --- Source/DafnyCore/AST/TopLevelDeclarations.cs | 8 ++++ Source/DafnyCore/Generic/Util.cs | 2 +- .../Rewriters/RefinementTransformer.cs | 42 +++++++++---------- 3 files changed, 29 insertions(+), 23 deletions(-) diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 689c9856fff..17584a29a79 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -4,7 +4,9 @@ using System.Diagnostics.Contracts; using System.Numerics; using System.Linq; +using System.Reflection; using System.Xml; +using Microsoft.CodeAnalysis.CSharp.Syntax; using Microsoft.Dafny.Auditor; namespace Microsoft.Dafny; @@ -867,6 +869,12 @@ public string FullName { Concat(DefaultClasses). Concat(ResolvedPrefixNamedModules); + public IEnumerable> TopLevelDeclPointers => + (DefaultClass == null + ? Enumerable.Empty>() + : new[] { new Pointer(() => DefaultClass, v => DefaultClass = (DefaultClassDecl)v) }). + Concat(SourceDecls.ToPointers()).Concat(ResolvedPrefixNamedModules.ToPointers()); + protected IEnumerable DefaultClasses { get { return DefaultClass == null ? Enumerable.Empty() : new TopLevelDecl[] { DefaultClass }; } } diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index a15ac02c241..1f087f4c4c4 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -13,8 +13,8 @@ using JetBrains.Annotations; using Microsoft.Boogie; -namespace Microsoft.Dafny { +namespace Microsoft.Dafny { public static class Sets { public static ISet Empty() { return new HashSet(); diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index a1ebc58e258..2dd64c248c3 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -221,26 +221,24 @@ void PreResolveWorker(ModuleDefinition m) { Resolver.ResolveOpenedImports(refinedSigOpened, m.RefinementQId.Def, false, null); // Create a simple name-to-decl dictionary. Ignore any duplicates at this time. - var declaredNames = new Dictionary(); - var topLevelDecls = m.TopLevelDecls.ToList(); - for (int i = 0; i < topLevelDecls.Count; i++) { - var d = topLevelDecls[i]; - if (!declaredNames.ContainsKey(d.Name)) { - declaredNames.Add(d.Name, i); - } + var declaredNames = new Dictionary>(); + var pointers = m.TopLevelDeclPointers; + foreach (var pointer in pointers) { + var key = pointer.Get().Name; + declaredNames.TryAdd(key, pointer); } // Merge the declarations of prev into the declarations of m List processedDecl = new List(); foreach (var d in prev.TopLevelDecls) { processedDecl.Add(d.Name); - if (!declaredNames.TryGetValue(d.Name, out var index)) { + if (!declaredNames.TryGetValue(d.Name, out var nwPointer)) { var clone = refinementCloner.CloneDeclaration(d, m); m.SourceDecls.Add(clone); } else { - var nw = topLevelDecls[index]; + var nw = nwPointer.Get(); if (d.Name == "_default" || nw.IsRefining || d is AbstractTypeDecl) { - MergeTopLevelDecls(m, nw, d, index); + MergeTopLevelDecls(m, nwPointer, d); } else if (nw is TypeSynonymDecl) { var msg = $"a type synonym ({nw.Name}) is not allowed to replace a {d.WhatKind} from the refined module ({m.RefinementQId}), even if it denotes the same type"; Reporter.Error(MessageSource.RefinementTransformer, nw.tok, msg); @@ -255,10 +253,9 @@ void PreResolveWorker(ModuleDefinition m) { // Merge the imports of prev var prevTopLevelDecls = RefinedSig.TopLevels.Values; foreach (var d in prevTopLevelDecls) { - if (!processedDecl.Contains(d.Name) && declaredNames.TryGetValue(d.Name, out var index)) { + if (!processedDecl.Contains(d.Name) && declaredNames.TryGetValue(d.Name, out var pointer)) { // if it is redefined, we need to merge them. - var nw = topLevelDecls[index]; - MergeTopLevelDecls(m, nw, d, index); + MergeTopLevelDecls(m, pointer, d); } } m.RefinementQId.Sig = RefinedSig; @@ -298,9 +295,10 @@ private void MergeModuleExports(ModuleExportDecl nw, ModuleExportDecl d) { nw.Extends.AddRange(d.Extends); } - private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDecl d, int index) { + private void MergeTopLevelDecls(ModuleDefinition m, IPointer nwPointer, TopLevelDecl d) { + var nw = nwPointer.Get(); var commonMsg = "a {0} declaration ({1}) in a refinement module can only refine a {0} declaration or replace an abstract type declaration"; - var topLevelDecls = m.TopLevelDecls.ToList(); + // Prefix decls. if (d is ModuleDecl) { if (!(nw is ModuleDecl)) { @@ -376,7 +374,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec } } if (nw is TopLevelDeclWithMembers) { - topLevelDecls[index] = MergeClass((TopLevelDeclWithMembers)nw, od); + nwPointer.Set(MergeClass((TopLevelDeclWithMembers)nw, od)); } else if (od.Members.Count != 0) { Reporter.Error(MessageSource.RefinementTransformer, nw, "a {0} ({1}) cannot declare members, so it cannot refine an abstract type with members", @@ -392,7 +390,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec var (dd, nwd) = ((DatatypeDecl)d, (DatatypeDecl)nw); Contract.Assert(!nwd.Ctors.Any()); nwd.Ctors.AddRange(dd.Ctors.Select(refinementCloner.CloneCtor)); - topLevelDecls[index] = MergeClass((DatatypeDecl)nw, (DatatypeDecl)d); + nwPointer.Set(MergeClass((DatatypeDecl)nw, (DatatypeDecl)d)); } else if (nw is DatatypeDecl) { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } else if (d is NewtypeDecl && nw is NewtypeDecl) { @@ -404,31 +402,31 @@ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDec nwn.Constraint = dn.Constraint == null ? null : refinementCloner.CloneExpr(dn.Constraint); nwn.WitnessKind = dn.WitnessKind; nwn.Witness = dn.Witness == null ? null : refinementCloner.CloneExpr(dn.Witness); - topLevelDecls[index] = MergeClass((NewtypeDecl)nw, (NewtypeDecl)d); + nwPointer.Set(MergeClass((NewtypeDecl)nw, (NewtypeDecl)d)); } else if (nw is NewtypeDecl) { // `.Basetype` will be set in AddDefaultBaseTypeToUnresolvedNewtypes Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } else if (nw is IteratorDecl) { if (d is IteratorDecl) { - topLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d); + nwPointer.Set(MergeIterator((IteratorDecl)nw, (IteratorDecl)d)); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name); } } else if (nw is TraitDecl) { if (d is TraitDecl) { - topLevelDecls[index] = MergeClass((TraitDecl)nw, (TraitDecl)d); + nwPointer.Set(MergeClass((TraitDecl)nw, (TraitDecl)d)); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } } else if (nw is ClassDecl) { if (d is ClassDecl) { - topLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d); + nwPointer.Set(MergeClass((ClassDecl)nw, (ClassDecl)d)); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } } else if (nw is DefaultClassDecl) { if (d is DefaultClassDecl) { - topLevelDecls[index] = MergeClass((DefaultClassDecl)nw, (DefaultClassDecl)d); + m.DefaultClass = (DefaultClassDecl)MergeClass((DefaultClassDecl)nw, (DefaultClassDecl)d); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } From 151b6bf922621a33d9fb4572487c92185557db34 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 21:42:20 +0200 Subject: [PATCH 21/68] Fix transcripts --- Source/DafnyServer/DafnyHelper.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 20ab8ef3b25..2187d1f77d4 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -43,7 +43,7 @@ private bool Parse() { var uri = new Uri("transcript:///" + fname); var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }, false); reporter = new ConsoleErrorReporter(options, defaultModuleDefinition); - var program = ParseUtils.ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri.LocalPath, new StringReader(source)) }, + var program = ParseUtils.ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, reporter, CancellationToken.None); var success = reporter.ErrorCount == 0; From 96366cfaccea6e976218627048158c433351c13d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 21:42:51 +0200 Subject: [PATCH 22/68] Let module.RangeToken.StartToken also include the include directives at the start --- Source/DafnyCore/Dafny.atg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index bc6642071df..2a77fb786b1 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -932,7 +932,7 @@ PRODUCTIONS Dafny = (. IToken startToken = t; .) - { "include" (. startToken = t; .) + { "include" stringToken (. { Uri parsedFile = scanner.Uri; bool isVerbatimString; From 4592b19b255e0f0507f1847ea1f3f45ccdb692b1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 21:43:58 +0200 Subject: [PATCH 23/68] add missing pointer file --- Source/DafnyCore/Generic/IPointer.cs | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 Source/DafnyCore/Generic/IPointer.cs diff --git a/Source/DafnyCore/Generic/IPointer.cs b/Source/DafnyCore/Generic/IPointer.cs new file mode 100644 index 00000000000..8f4b7f3d729 --- /dev/null +++ b/Source/DafnyCore/Generic/IPointer.cs @@ -0,0 +1,28 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Reflection; + +namespace Microsoft.Dafny; + +public interface IPointer { + T Get(); + void Set(T value); +} + +record Pointer(Func Get, Action Set) : IPointer { + T IPointer.Get() { + return Get(); + } + + void IPointer.Set(T value) { + Set(value); + } +} + +public static class PointerExtensions { + public static IEnumerable> ToPointers(this IList values) { + return Enumerable.Range(0, values.Count) + .Select(index => new Pointer(() => values[index], value => values[index] = value)); + } +} \ No newline at end of file From bda14d48b88a8eb69dea51c7a0fb7d75c3eca550 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 21:54:34 +0200 Subject: [PATCH 24/68] Do not parse libraries twice when they're also in an include directive --- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index dbfae4cacf9..2868d2cf4e1 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -155,7 +155,7 @@ public static Program ParseFiles(string programName, IReadOnlyList fi } if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) { - var includedModules = TryParseIncludes(defaultModule.Includes.ToList(), + var includedModules = TryParseIncludes(files, defaultModule.Includes.ToList(), builtIns, errorReporter, cancellationToken); foreach (var module in includedModules) { @@ -217,6 +217,7 @@ public static void AddFileModuleToProgram(FileModuleDefinition fileModule, Defau } public static IList TryParseIncludes( + IReadOnlyList files, IEnumerable roots, BuiltIns builtIns, ErrorReporter errorReporter, @@ -224,9 +225,13 @@ CancellationToken cancellationToken ) { var stack = new Stack(); var result = new List(); - var resolvedIncludes = new HashSet(); + var resolvedFiles = new HashSet(); + foreach (var rootFile in files) { + resolvedFiles.Add(rootFile.Uri); + } + foreach (var root in roots) { - resolvedIncludes.Add(root.IncluderFilename); + resolvedFiles.Add(root.IncluderFilename); // TODO obsolete? var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, root); if (dafnyFile != null) { @@ -236,7 +241,7 @@ CancellationToken cancellationToken while (stack.Any()) { var top = stack.Pop(); - if (!resolvedIncludes.Add(top.Uri)) { + if (!resolvedFiles.Add(top.Uri)) { continue; } From 76b4929ebc0cfa8b31b7ee50effb0bf2928b578e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 22:02:26 +0200 Subject: [PATCH 25/68] Fix bug in FormatterTestBase --- Source/DafnyPipeline.Test/FormatterBaseTest.cs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index 423858a7579..7f122e35f89 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -94,10 +94,11 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString // Verify that the formatting is stable. Microsoft.Dafny.Type.ResetScopes(); - dafnyProgram = ParseUtils.Parse(reprinted, uri, reporter); ; + var newOuterModule = new DefaultModuleDefinition(new List() { uri }, false); + var newReporter = new BatchErrorReporter(options, newOuterModule); + dafnyProgram = ParseUtils.Parse(reprinted, uri, newReporter); ; - var newReporter = (BatchErrorReporter)dafnyProgram.Reporter; - Assert.Equal(initErrorCount, newReporter.ErrorCount); + Assert.Equal(initErrorCount, reporter.ErrorCount + newReporter.ErrorCount); firstToken = dafnyProgram.GetFirstTopLevelToken(); var reprinted2 = firstToken != null && firstToken.line > 0 ? Formatting.__default.ReindentProgramFromFirstToken(firstToken, From 55b2bbb51d90551b4f5702d184c46662b648221f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 22:31:48 +0200 Subject: [PATCH 26/68] More passing formatter tests --- .../AST/Grammar/SourcePreprocessor.cs | 60 ++++++++----------- 1 file changed, 25 insertions(+), 35 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs index 31db67415f1..211f3e4fde8 100644 --- a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs +++ b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs @@ -62,19 +62,12 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def Contract.Ensures(Contract.Result() != null); string newline = null; StringBuilder sb = new StringBuilder(); - List /*!*/ - ifDirectiveStates = new List(); // readState.Count is the current nesting level of #if's - int ignoreCutoff = - -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n + List /*!*/ ifDirectiveStates = new List(); // readState.Count is the current nesting level of #if's + int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n while (true) //invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count; { - string line; - if (newline == null) { - line = ReadLineAndDetermineNewline(reader, out newline); - } else { - line = reader.ReadLine(); - } + (string line, newline) = ReadLineAndDetermineNewline(reader); if (line == null) { if (ifDirectiveStates.Count != 0) { sb.AppendLine("#MalformedInput: missing #endif"); @@ -83,12 +76,14 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def break; } - string t = line.Trim(); - if (t.StartsWith("#if")) { + var addedNewline = string.IsNullOrEmpty(newline) ? Environment.NewLine : newline; + string trimmedLine = line.Trim(); + + if (trimmedLine.StartsWith("#if")) { IfDirectiveState rs = new IfDirectiveState(false, false); if (ignoreCutoff != -1) { // we're already in a state of ignoring, so continue to ignore - } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) { + } else if (IfdefConditionSaysToInclude(trimmedLine.Substring(3).TrimStart(), defines)) { // include this branch } else { ignoreCutoff = ifDirectiveStates.Count; // start ignoring @@ -96,11 +91,10 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def } ifDirectiveStates.Add(rs); - sb.Append(newline); // ignore the #if line - } else if (t.StartsWith("#elsif")) { + } else if (trimmedLine.StartsWith("#elsif")) { IfDirectiveState rs; - if (ifDirectiveStates.Count == 0 || (rs = ifDirectiveStates[ifDirectiveStates.Count - 1]).hasSeenElse) { - sb.Append("#MalformedInput: misplaced #elsif" + newline); // malformed input + if (ifDirectiveStates.Count == 0 || (rs = ifDirectiveStates[^1]).hasSeenElse) { + sb.Append("#MalformedInput: misplaced #elsif" + addedNewline); // malformed input break; } @@ -109,18 +103,17 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def //Contract.Assert(!rs.mayStillIncludeAnotherAlternative); ignoreCutoff = ifDirectiveStates.Count - 1; // start ignoring } else if (rs.mayStillIncludeAnotherAlternative && - IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) { + IfdefConditionSaysToInclude(trimmedLine.Substring(6).TrimStart(), defines)) { // include this branch, but no subsequent branch at this level ignoreCutoff = -1; rs.mayStillIncludeAnotherAlternative = false; - ifDirectiveStates[ifDirectiveStates.Count - 1] = rs; + ifDirectiveStates[^1] = rs; } - sb.Append(newline); // ignore the #elsif line - } else if (t == "#else") { + } else if (trimmedLine == "#else") { IfDirectiveState rs; if (ifDirectiveStates.Count == 0 || (rs = ifDirectiveStates[ifDirectiveStates.Count - 1]).hasSeenElse) { - sb.Append("#MalformedInput: misplaced #else" + newline); // malformed input + sb.Append("#MalformedInput: misplaced #else" + addedNewline); // malformed input break; } @@ -135,11 +128,10 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def rs.mayStillIncludeAnotherAlternative = false; } - ifDirectiveStates[ifDirectiveStates.Count - 1] = rs; - sb.Append(newline); // ignore the #else line - } else if (t == "#endif") { + ifDirectiveStates[^1] = rs; + } else if (trimmedLine == "#endif") { if (ifDirectiveStates.Count == 0) { - sb.Append("#MalformedInput: misplaced #endif" + newline); // malformed input + sb.Append("#MalformedInput: misplaced #endif" + addedNewline); // malformed input break; } @@ -149,22 +141,19 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def ignoreCutoff = -1; } - sb.Append(newline); // ignore the #endif line } else if (ignoreCutoff == -1) { sb.Append(line); - sb.Append(newline); - } else { - sb.Append(newline); // ignore the line } + sb.Append(newline); } return sb.ToString(); } - public static string ReadLineAndDetermineNewline(TextReader reader, out string newline) { + + public static (string content, string newline) ReadLineAndDetermineNewline(TextReader reader) { StringBuilder sb = new StringBuilder(); - newline = null; while (true) { int ch = reader.Read(); if (ch == -1) { @@ -172,6 +161,7 @@ public static string ReadLineAndDetermineNewline(TextReader reader, out string n } if (ch == '\r' || ch == '\n') { + string newline; if (ch == '\r') { if (reader.Peek() == '\n') { newline = "\r\n"; @@ -183,15 +173,15 @@ public static string ReadLineAndDetermineNewline(TextReader reader, out string n newline = "\n"; } - return sb.ToString(); + return (sb.ToString(), newline); } sb.Append((char)ch); } if (sb.Length > 0) { - return sb.ToString(); + return (sb.ToString(), ""); } - return null; + return (null, ""); } /// From 4b1f763e054bfcacbb1d82b2da3144052c5d48e7 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 23:17:48 +0200 Subject: [PATCH 27/68] Add another call to SetMembersBeforeResolution --- Source/DafnyCore/Dafny.atg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 2a77fb786b1..6adfbb174a5 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -988,7 +988,7 @@ TopDecl<. ModuleDefinition module, bool isTopLevel, bool isAbstract .> | SynonymTypeDecl (. module.SourceDecls.Add(td); .) | IteratorDecl (. module.SourceDecls.Add(iter); .) | TraitDecl (. module.SourceDecls.Add(trait); .) - | ClassMemberDecl + | ClassMemberDecl (. module.DefaultClass.SetMembersBeforeResolution(); .) ) . From 285dd9103458f9a8dd5d33bb56de8deea1b74250 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 May 2023 23:53:00 +0200 Subject: [PATCH 28/68] Formatting fixes and ran formatter --- Source/DafnyCore/AST/Cloner.cs | 3 +-- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 5 ++--- Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs | 4 ++-- Source/DafnyCore/AST/TopLevelDeclarations.cs | 12 ++++++------ Source/DafnyCore/Dafny.atg | 11 ++++++----- Source/DafnyCore/DafnyFile.cs | 5 ++--- Source/DafnyPipeline.Test/FormatterBaseTest.cs | 1 + 7 files changed, 20 insertions(+), 21 deletions(-) diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 0a154f27376..8e65d2bacee 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -683,8 +683,7 @@ public override Expression CloneExpr(Expression expr) { /// This cloner copies the origin module signatures to their cloned declarations /// class DeepModuleSignatureCloner : Cloner { - public DeepModuleSignatureCloner(bool cloneResolvedFields = false) : base(cloneResolvedFields) - { + public DeepModuleSignatureCloner(bool cloneResolvedFields = false) : base(cloneResolvedFields) { } public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) { diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index 2868d2cf4e1..d545e6a0b3f 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -185,8 +185,7 @@ public static Program ParseFiles(string programName, IReadOnlyList fi public static void AddFileModuleToProgram(FileModuleDefinition fileModule, DefaultModuleDefinition defaultModule) { foreach (var declToMove in fileModule.TopLevelDecls. Where(d => d != null) // Can occur when there are parse errors. Error correction is at fault but we workaround it here - ) - { + ) { declToMove.EnclosingModuleDefinition = defaultModule; if (declToMove is LiteralModuleDecl literalModuleDecl) { literalModuleDecl.ModuleDef.EnclosingModule = defaultModule; @@ -229,7 +228,7 @@ CancellationToken cancellationToken foreach (var rootFile in files) { resolvedFiles.Add(rootFile.Uri); } - + foreach (var root in roots) { resolvedFiles.Add(root.IncluderFilename); // TODO obsolete? diff --git a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs index 211f3e4fde8..00c0eb8ee4d 100644 --- a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs +++ b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs @@ -78,7 +78,7 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def var addedNewline = string.IsNullOrEmpty(newline) ? Environment.NewLine : newline; string trimmedLine = line.Trim(); - + if (trimmedLine.StartsWith("#if")) { IfDirectiveState rs = new IfDirectiveState(false, false); if (ignoreCutoff != -1) { @@ -150,7 +150,7 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def return sb.ToString(); } - + public static (string content, string newline) ReadLineAndDetermineNewline(TextReader reader) { StringBuilder sb = new StringBuilder(); diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 17584a29a79..f440a9b2e93 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -861,10 +861,10 @@ public string FullName { public readonly List ResolvedPrefixNamedModules = new(); [FilledInDuringResolution] public readonly List, LiteralModuleDecl>> PrefixNamedModules = new(); // filled in by the parser; emptied by the resolver - public virtual IEnumerable TopLevelDecls => + public virtual IEnumerable TopLevelDecls => defaultClassFirst ? DefaultClasses. Concat(SourceDecls). - Concat(ResolvedPrefixNamedModules) + Concat(ResolvedPrefixNamedModules) : SourceDecls. Concat(DefaultClasses). Concat(ResolvedPrefixNamedModules); @@ -909,7 +909,7 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : b var newTup = new Tuple, LiteralModuleDecl>(tup.Item1, (LiteralModuleDecl)cloner.CloneDeclaration(tup.Item2, this)); PrefixNamedModules.Add(newTup); } - + // For cloning modules into their compiled variants, we don't want to copy resolved fields, but we do need to copy this. foreach (var tup in original.ResolvedPrefixNamedModules) { ResolvedPrefixNamedModules.Add(cloner.CloneDeclaration(tup, this)); @@ -921,7 +921,7 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : b } public ModuleDefinition(RangeToken tok, Name name, List prefixIds, bool isAbstract, bool isFacade, - ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, + ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, bool isBuiltinName, bool defaultClassFirst = false) : base(tok) { Contract.Requires(tok != null); Contract.Requires(name != null); @@ -1148,7 +1148,6 @@ public bool IsEssentiallyEmptyModuleBody() { private IEnumerable preResolvePrefixNamedModules; public override IEnumerable PreResolveChildren => - //Includes. Enumerable.Empty(). // TODO refactor Concat(Attributes != null ? new List { Attributes } : @@ -1176,12 +1175,13 @@ public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original) } public DefaultModuleDefinition(IList rootSourceUris, bool defaultClassFirst) - : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, + : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, null, null, null, true, defaultClassFirst) { RootSourceUris = rootSourceUris; } public override bool IsDefaultModule => true; + public override IEnumerable PreResolveChildren => Includes.Concat(base.PreResolveChildren); } public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 6adfbb174a5..e4cc46bf31d 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -930,9 +930,10 @@ IGNORE cr + lf + tab /*------------------------------------------------------------------------*/ PRODUCTIONS Dafny -= (. IToken startToken = t; += (. IToken includeStartToken; + IToken fileStartToken = t; .) - { "include" + { "include" (. includeStartToken = t; .) stringToken (. { Uri parsedFile = scanner.Uri; bool isVerbatimString; @@ -943,15 +944,15 @@ Dafny string basePath = Path.GetDirectoryName(parsedFile.LocalPath); includedFile = Path.Combine(basePath, includedFile); } - var oneInclude = new Include(t, parsedFile, new Uri(includedFile)); - oneInclude.RangeToken = new RangeToken(startToken, t); + var oneInclude = new Include(t, parsedFile, new Uri("file://" + includedFile)); + oneInclude.RangeToken = new RangeToken(includeStartToken, t); theModule.Includes.Add(oneInclude); } .) } { TopDecl } (. - theModule.RangeToken = new RangeToken(startToken.Next, t); + theModule.RangeToken = new RangeToken(fileStartToken.Next, t); .) SYNC EOF diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index 6dcc727a656..258dcc8339d 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -19,9 +19,8 @@ public class DafnyFile { // TODO take a Uri instead of a filePath - public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverride = null) - : this(options, contentOverride != null ? new Uri("stdin:///") : new Uri(filePath), contentOverride) - { + public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverride = null) + : this(options, contentOverride != null ? new Uri("stdin:///") : new Uri(filePath), contentOverride) { Uri = contentOverride != null ? new Uri("stdin:///") : new Uri(filePath); BaseName = contentOverride != null ? "" : Path.GetFileName(filePath); } diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index 7f122e35f89..5cb07ebb7eb 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -42,6 +42,7 @@ enum Newlines { protected void FormatterWorksFor(string testCase, string? expectedProgramString = null, bool expectNoToken = false, bool reduceBlockiness = true) { var options = DafnyOptions.Create(output); + options.DisallowIncludes = true; var newlineTypes = Enum.GetValues(typeof(Newlines)); foreach (Newlines newLinesType in newlineTypes) { currentNewlines = newLinesType; From 244d11cab338f1cf29511c9313848e13aafde8aa Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 25 May 2023 09:13:05 +0200 Subject: [PATCH 29/68] Fix tests and small Uri fix --- Source/DafnyCore/Dafny.atg | 2 +- Source/DafnyPipeline.Test/TranslatorTest.cs | 1 - Source/DafnyPipeline.Test/Trivia.cs | 3 --- 3 files changed, 1 insertion(+), 5 deletions(-) diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 6784e6208d5..0ed24d28a72 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -944,7 +944,7 @@ Dafny string basePath = Path.GetDirectoryName(parsedFile.LocalPath); includedFile = Path.Combine(basePath, includedFile); } - var oneInclude = new Include(t, parsedFile, new Uri("file://" + includedFile)); + var oneInclude = new Include(t, parsedFile, new Uri(Path.GetFullPath(includedFile))); oneInclude.RangeToken = new RangeToken(includeStartToken, t); theModule.Includes.Add(oneInclude); } diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index c7e72bd889e..19376b424e5 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -78,7 +78,6 @@ private void ShouldHaveImplicitCode(string program, string expected, DafnyOption var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }, false); BatchErrorReporter reporter = new BatchErrorReporter(options, defaultModuleDefinition); var dafnyProgram = ParseUtils.Parse(program, uri, reporter); - ParseUtils.Parse(program, uri, reporter); if (reporter.ErrorCount > 0) { var error = reporter.AllMessages[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); diff --git a/Source/DafnyPipeline.Test/Trivia.cs b/Source/DafnyPipeline.Test/Trivia.cs index 57865d93b81..d85f8ac1db9 100644 --- a/Source/DafnyPipeline.Test/Trivia.cs +++ b/Source/DafnyPipeline.Test/Trivia.cs @@ -132,10 +132,8 @@ void Traverse(Node node) { Traverse(program); - var count = 0; void AreAllTokensOwned(Node node) { if (node.StartToken is { filename: { } }) { - count++; var t = node.StartToken; while (t != null && t != node.EndToken) { Assert.Contains(t, allTokens); @@ -149,7 +147,6 @@ void AreAllTokensOwned(Node node) { } AreAllTokensOwned(program); - Assert.Equal(9, count); // Sanity check } private string AdjustNewlines(string programString) { From ebb1150611889aa824e0af776476f63d2eae083f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 25 May 2023 10:07:02 +0200 Subject: [PATCH 30/68] Turn off direct test running --- Source/DafnyCore/AST/Grammar/ParseUtils.cs | 27 ++------------------ Source/DafnyCore/AST/Grammar/Printer.cs | 15 +++-------- Source/DafnyCore/AST/TopLevelDeclarations.cs | 18 +++++++------ Source/DafnyCore/DafnyFile.cs | 13 +++++++--- Source/DafnyDriver/DafnyDriver.cs | 5 ++-- Source/IntegrationTests/LitTests.cs | 2 +- 6 files changed, 29 insertions(+), 51 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index 9b0e2734431..f90f67a4e8c 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -77,19 +77,11 @@ private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle); System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ResolutionErrors).TypeHandle); byte[] /*!*/ buffer = cce.NonNull(Encoding.Default.GetBytes(s)); - MemoryStream ms = new MemoryStream(buffer, false); + var ms = new MemoryStream(buffer, false); var firstToken = new Token { Uri = uri }; - // if ((module.RootToken.Filepath ?? "") == "") { - // // This is the first module - // module.RootToken.Uri = uri; - // firstToken = module.RootToken; - // } else { - // firstToken = new Token(); // It's an included file - // } - Scanner scanner = new Scanner(ms, errors, uri, firstToken: firstToken); return new Parser(scanner, errors, builtIns); } @@ -114,17 +106,6 @@ public static Program ParseFiles(string programName, IReadOnlyList fi } try { - // We model a precompiled file, a library, as an include - // var include = dafnyFile.IsPrecompiled ? new Include(new Token { - // Uri = dafnyFile.Uri, - // col = 1, - // line = 0 - // }, new Uri("cli://"), dafnyFile.Uri) : null; - // if (include != null) { - // // TODO this can be removed once the include error message in ErrorReporter.Error is removed. - // defaultModuleDefinition.Includes.Add(include); - // } - var parseResult = Parse( dafnyFile.Content, dafnyFile.Uri, @@ -132,10 +113,6 @@ public static Program ParseFiles(string programName, IReadOnlyList fi errorReporter ); - if (parseResult.ErrorCount != 0) { - // logger.LogDebug("encountered {ErrorCount} errors while parsing {DocumentUri}", parseResult.ErrorCount, document.Uri); - } - AddFileModuleToProgram(parseResult.Module, defaultModule); if (defaultModule.RangeToken.StartToken.Uri == null) { defaultModule.RangeToken = parseResult.Module.RangeToken; @@ -269,7 +246,7 @@ CancellationToken cancellationToken private static DafnyFile IncludeToDafnyFile(BuiltIns builtIns, ErrorReporter errorReporter, Include include) { try { - return new DafnyFile(builtIns.Options, include.IncludedFilename.LocalPath); + return new DafnyFile(builtIns.Options, include.IncludedFilename); } catch (IllegalDafnyFile) { errorReporter.Error(MessageSource.Parser, include.tok, $"Include of file '{include.IncludedFilename}' failed."); return null; diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index e66155fb3b7..8cf2ec19b15 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -592,22 +592,15 @@ public void PrintModuleDefinition(Program program, ModuleDefinition module, Visi } void PrintTopLevelDeclsOrExportedView(Program program, ModuleDefinition module, int indent, string fileBeingPrinted) { - var decls = module.TopLevelDecls.ToList(); + var decls = module.TopLevelDecls; // only filter based on view name after resolver. if (afterResolver && options.DafnyPrintExportedViews.Count != 0) { - decls = new List(); - foreach (var nameOfView in options.DafnyPrintExportedViews) { - foreach (var decl in module.TopLevelDecls) { - if (decl.FullName.Equals(nameOfView)) { - decls.Add(decl); - } - } - } + var views = options.DafnyPrintExportedViews.ToHashSet(); + decls = decls.Where(d => views.Contains(d.FullName)); } PrintTopLevelDecls(program, decls, indent + IndentAmount, null, fileBeingPrinted); foreach (var tup in module.PrefixNamedModules) { - decls = new List() { tup.Item2 }; - PrintTopLevelDecls(program, decls, indent + IndentAmount, tup.Item1, fileBeingPrinted); + PrintTopLevelDecls(program, new TopLevelDecl[] { tup.Item2 }, indent + IndentAmount, tup.Item1, fileBeingPrinted); } } diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index f440a9b2e93..8f2d28aad14 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -910,7 +910,9 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : b PrefixNamedModules.Add(newTup); } - // For cloning modules into their compiled variants, we don't want to copy resolved fields, but we do need to copy this. + // For cloning modules into their compiled variants, we don't want to copy resolved fields, but we do need to copy this. + // We're hoping to remove the copying of modules into compiled variants altogether, + // and then this can be moved to inside the `if (cloner.CloneResolvedFields)` block foreach (var tup in original.ResolvedPrefixNamedModules) { ResolvedPrefixNamedModules.Add(cloner.CloneDeclaration(tup, this)); } @@ -1147,12 +1149,13 @@ public bool IsEssentiallyEmptyModuleBody() { private IEnumerable preResolveTopLevelDecls; private IEnumerable preResolvePrefixNamedModules; - public override IEnumerable PreResolveChildren => - Enumerable.Empty(). // TODO refactor - Concat(Attributes != null ? - new List { Attributes } : - Enumerable.Empty()).Concat(preResolveTopLevelDecls ?? TopLevelDecls).Concat( - (preResolvePrefixNamedModules ?? PrefixNamedModules.Select(tuple => tuple.Item2))); + public override IEnumerable PreResolveChildren { + get { + var attributes = Attributes != null ? new List { Attributes } : Enumerable.Empty(); + return attributes.Concat(preResolveTopLevelDecls ?? TopLevelDecls).Concat( + (preResolvePrefixNamedModules ?? PrefixNamedModules.Select(tuple => tuple.Item2))); + } + } public void PreResolveSnapshotForFormatter() { preResolveTopLevelDecls = TopLevelDecls.ToImmutableList(); @@ -1166,7 +1169,6 @@ public override IEnumerable Assumptions(Declaration decl) { public class DefaultModuleDefinition : ModuleDefinition { - // TODO remove??? public List Includes { get; } = new(); public IList RootSourceUris { get; } diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index 8dbe3e3ce15..38ee8616d10 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -28,11 +28,16 @@ public DafnyFile(DafnyOptions options, string filePath, TextReader contentOverri public DafnyFile(DafnyOptions options, Uri uri, TextReader contentOverride = null) { Uri = uri; var filePath = uri.LocalPath; - // TODO fix - BaseName = uri.IsFile ? Path.GetFileName(uri.LocalPath) : ""; - var extension = contentOverride != null ? ".dfy" : Path.GetExtension(filePath); - if (extension != null) { extension = extension.ToLower(); } + var extension = ".dfy"; + if (uri.IsFile) { + extension = Path.GetExtension(uri.LocalPath).ToLower(); + BaseName = Path.GetFileName(uri.LocalPath); + } + if (uri.Scheme == "stdin") { + contentOverride = options.Input; + BaseName = ""; + } // Normalizing symbolic links appears to be not // supported in .Net APIs, because it is very difficult in general diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 9769d34883b..751e37d20b9 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -238,8 +238,9 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(TextWriter } if (options.UseStdin) { - options.CliRootSourceUris.Add(new Uri("stdin:///")); - dafnyFiles.Add(new DafnyFile(options, "", inputReader)); + var uri = new Uri("stdin:///"); + options.CliRootSourceUris.Add(uri); + dafnyFiles.Add(new DafnyFile(options, uri)); } else if (options.CliRootSourceUris.Count == 0 && !options.Format) { options.Printer.ErrorWriteLine(options.ErrorWriter, "*** Error: No input files were specified in command-line " + string.Join("|", args) + "."); return CommandLineArgumentsResult.PREPROCESSING_ERROR; diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs index 5d780828be8..3e6d6612e68 100644 --- a/Source/IntegrationTests/LitTests.cs +++ b/Source/IntegrationTests/LitTests.cs @@ -20,7 +20,7 @@ public class LitTests { // Change this to true in order to debug the execution of commands like %dafny. // This is false by default because the main dafny CLI implementation currently has shared static state, which // causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. - private const bool InvokeMainMethodsDirectly = true; + private const bool InvokeMainMethodsDirectly = false; private static readonly Assembly DafnyDriverAssembly = typeof(Dafny.Dafny).Assembly; private static readonly Assembly TestDafnyAssembly = typeof(TestDafny.MultiBackendTest).Assembly; From 3fce874a18cda57406e82c11534c47dedd7e2f48 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 25 May 2023 10:09:04 +0200 Subject: [PATCH 31/68] Fix some allocation tests --- Test/allocated1/dafny0/Parallel.dfy | 2 +- Test/allocated1/dafny0/Reads.dfy | 2 +- Test/allocated1/dafny0/SmallTests.dfy | 2 +- Test/allocated1/dafny0/Twostate-Verification.dfy | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Test/allocated1/dafny0/Parallel.dfy b/Test/allocated1/dafny0/Parallel.dfy index 6457b7aab34..5f48294b555 100644 --- a/Test/allocated1/dafny0/Parallel.dfy +++ b/Test/allocated1/dafny0/Parallel.dfy @@ -1,5 +1,5 @@ // UNSUPPORTED: windows -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { var data: int diff --git a/Test/allocated1/dafny0/Reads.dfy b/Test/allocated1/dafny0/Reads.dfy index f08fe274068..550c7e54411 100644 --- a/Test/allocated1/dafny0/Reads.dfy +++ b/Test/allocated1/dafny0/Reads.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Checking that the reads clause also is checked over requires diff --git a/Test/allocated1/dafny0/SmallTests.dfy b/Test/allocated1/dafny0/SmallTests.dfy index 7c49d74205e..0169ef40a47 100644 --- a/Test/allocated1/dafny0/SmallTests.dfy +++ b/Test/allocated1/dafny0/SmallTests.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t" // RUN: %dafny /verifyAllModules /allocated:1 /noVerify /compile:0 "%t.dprint.dfy" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/allocated1/dafny0/Twostate-Verification.dfy b/Test/allocated1/dafny0/Twostate-Verification.dfy index 2b1344e3391..8234188cc59 100644 --- a/Test/allocated1/dafny0/Twostate-Verification.dfy +++ b/Test/allocated1/dafny0/Twostate-Verification.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /verifyAllModules /allocated:1 /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %dafny /allocated:1 /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() { From c06abb183b30adcb5456dba426e3ed71e1b4e90e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 25 May 2023 10:45:54 +0200 Subject: [PATCH 32/68] Fix project file output writing --- Source/DafnyCore/Options/ProjectFile.cs | 8 ++++---- Source/DafnyDriver/Commands/CommandRegistry.cs | 4 ++-- Source/DafnyLanguageServer/Workspace/DocumentManager.cs | 3 +-- 3 files changed, 7 insertions(+), 8 deletions(-) diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index 2ecc79bcfe4..fa1be2c0565 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -25,9 +25,9 @@ public class ProjectFile { public string[] Excludes { get; set; } public Dictionary Options { get; set; } - public static ProjectFile Open(Uri uri, TextWriter errorWriter) { + public static ProjectFile Open(Uri uri, TextWriter outputWriter, TextWriter errorWriter) { if (Path.GetFileName(uri.LocalPath) != FileName) { - Console.WriteLine($"Warning: only Dafny project files named {FileName} are recognised by the Dafny IDE."); + outputWriter.WriteLine($"Warning: only Dafny project files named {FileName} are recognised by the Dafny IDE."); } try { var file = File.Open(uri.LocalPath, FileMode.Open); @@ -67,14 +67,14 @@ public void AddFilesToOptions(DafnyOptions options) { } } - public void Validate(IEnumerable