diff --git a/Source/DafnyCore.Test/DooFileTest.cs b/Source/DafnyCore.Test/DooFileTest.cs index 3c9eee0a2e0..f62657c7279 100644 --- a/Source/DafnyCore.Test/DooFileTest.cs +++ b/Source/DafnyCore.Test/DooFileTest.cs @@ -31,9 +31,8 @@ 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 }, false); Microsoft.Dafny.Type.ResetScopes(); - var errorReporter = new ConsoleErrorReporter(options, outerModule); + var errorReporter = new ConsoleErrorReporter(options); var program = ParseUtils.Parse(dafnyProgramText, rootUri, errorReporter); Assert.Equal(0, errorReporter.ErrorCount); return program; diff --git a/Source/DafnyCore/AST/BuiltIns.cs b/Source/DafnyCore/AST/BuiltIns.cs index 63a2f8620d4..8ca1bbf6dfb 100644 --- a/Source/DafnyCore/AST/BuiltIns.cs +++ b/Source/DafnyCore/AST/BuiltIns.cs @@ -67,9 +67,12 @@ public static Attributes AxiomAttribute() { public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) { Contract.Requires(1 <= dims); Contract.Requires(arg != null); - return ArrayType(Token.NoToken, dims, new List() { arg }, allowCreationOfNewClass); + var (result, mod) = ArrayType(Token.NoToken, dims, new List { arg }, allowCreationOfNewClass); + mod(this); + return result; } - public UserDefinedType ArrayType(IToken tok, int dims, List optTypeArgs, bool allowCreationOfNewClass, bool useClassNameType = false) { + + public static (UserDefinedType type, Action ModifyBuiltins) ArrayType(IToken tok, int dims, List optTypeArgs, bool allowCreationOfNewClass, bool useClassNameType = false) { Contract.Requires(tok != null); Contract.Requires(1 <= dims); Contract.Requires(optTypeArgs == null || optTypeArgs.Count > 0); // ideally, it is 1, but more will generate an error later, and null means it will be filled in automatically @@ -77,22 +80,29 @@ public UserDefinedType ArrayType(IToken tok, int dims, List optTypeArgs, b var arrayName = ArrayClassName(dims); if (useClassNameType) { - arrayName = arrayName + "?"; + arrayName += "?"; } - if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) { - ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile()); + + void ModifyBuiltins(BuiltIns builtIns) { + if (!allowCreationOfNewClass || builtIns.arrayTypeDecls.ContainsKey(dims)) { + return; + } + + ArrayClassDecl arrayClass = new ArrayClassDecl(dims, builtIns.SystemModule, builtIns.DontCompile()); for (int d = 0; d < dims; d++) { string name = dims == 1 ? "Length" : "Length" + d; Field len = new SpecialField(RangeToken.NoToken, name, SpecialField.ID.ArrayLength, dims == 1 ? null : (object)d, false, false, false, Type.Int, null); - len.EnclosingClass = arrayClass; // resolve here + len.EnclosingClass = arrayClass; // resolve here arrayClass.Members.Add(len); } - arrayTypeDecls.Add(dims, 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 + + builtIns.arrayTypeDecls.Add(dims, arrayClass); + builtIns.SystemModule.SourceDecls.Add(arrayClass); + builtIns.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); - return udt; + + var udt = new UserDefinedType(tok, arrayName, optTypeArgs); + return (udt, ModifyBuiltins); } public static string ArrayClassName(int dims) { diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 06c9b8adc04..beb6d24cd68 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -110,7 +110,7 @@ public string Name { /// Get the first token that is in the same file as the DefaultModule.RootToken.FileName /// (skips included tokens) public IToken GetFirstTopLevelToken() { - var rootToken = DefaultModule.RangeToken.StartToken; + var rootToken = DefaultModuleDef.RangeToken.StartToken; if (rootToken.Next == null) { return null; } @@ -137,32 +137,6 @@ public override IEnumerable Assumptions(Declaration decl) { } } - public class Include : TokenNode, IComparable { - public Uri IncluderFilename { get; } - public Uri IncludedFilename { get; } - public string CanonicalPath { get; } - public bool ErrorReported; - - public Include(IToken tok, Uri includer, Uri theFilename) { - this.tok = tok; - this.IncluderFilename = includer; - this.IncludedFilename = theFilename; - this.CanonicalPath = DafnyFile.Canonicalize(theFilename.LocalPath).LocalPath; - this.ErrorReported = false; - } - - public int CompareTo(object obj) { - if (obj is Include include) { - return CanonicalPath.CompareTo(include.CanonicalPath); - } else { - throw new NotImplementedException(); - } - } - - public override IEnumerable Children => Enumerable.Empty(); - public override IEnumerable PreResolveChildren => Enumerable.Empty(); - } - /// /// An expression introducting bound variables /// diff --git a/Source/DafnyCore/AST/Grammar/ParseUtils.cs b/Source/DafnyCore/AST/Grammar/ParseUtils.cs index d4e24669ba7..af6617e733d 100644 --- a/Source/DafnyCore/AST/Grammar/ParseUtils.cs +++ b/Source/DafnyCore/AST/Grammar/ParseUtils.cs @@ -8,96 +8,27 @@ namespace Microsoft.Dafny; -public record DfyParseResult(int ErrorCount, FileModuleDefinition Module); +public record DfyParseResult(BatchErrorReporter ErrorReporter, FileModuleDefinition Module, + IReadOnlyList> ModifyBuiltins); 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, ErrorReporter /*!*/ errorReporter) /* throws System.IO.IOException */ { - Contract.Requires(uri != null); - var text = SourcePreprocessor.ProcessDirectives(reader, new List()); - 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; - } - } - - /// - /// 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.SourceDecls.Any() - && (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); - } - - private 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(Encoding.Default.GetBytes(s)); - var ms = new MemoryStream(buffer, false); - var firstToken = new Token { - Uri = uri - }; - - Scanner scanner = new Scanner(ms, errors, uri, firstToken: firstToken); - return new Parser(scanner, errors, builtIns); - } - - 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, CancellationToken cancellationToken) { var options = errorReporter.Options; var builtIns = new BuiltIns(options); - var defaultModule = errorReporter.OuterModule; - foreach (var dafnyFile in files) { + var defaultModule = new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList(), options.VerifyAllModules); + 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(defaultModule, null), + builtIns, + errorReporter, verifiedRoots, compiledRoots + ); + + foreach (var dafnyFile in files) { if (options.Trace) { options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath); } @@ -107,24 +38,13 @@ public static Program ParseFiles(string programName, IReadOnlyList fi } try { - 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. - defaultModule.Includes.Add(include); - } - - var parseResult = Parse( + var parseResult = ParseFile( + options, dafnyFile.Content, - dafnyFile.Uri, - builtIns, - errorReporter + dafnyFile.Uri ); - AddFileModuleToProgram(parseResult.Module, defaultModule); + AddParseResultToProgram(parseResult, program); if (defaultModule.RangeToken.StartToken.Uri == null) { defaultModule.RangeToken = parseResult.Module.RangeToken; } @@ -146,7 +66,7 @@ public static Program ParseFiles(string programName, IReadOnlyList fi builtIns, errorReporter, cancellationToken); foreach (var module in includedModules) { - AddFileModuleToProgram(module, defaultModule); + AddParseResultToProgram(module, program); } } @@ -156,22 +76,27 @@ public static Program ParseFiles(string programName, IReadOnlyList fi 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 - ); - if (errorReporter.ErrorCount == 0) { DafnyMain.MaybePrintProgram(program, options.DafnyPrintFile, false); } + + return program; } - public static void AddFileModuleToProgram(FileModuleDefinition fileModule, DefaultModuleDefinition defaultModule) { + public static void AddParseResultToProgram(DfyParseResult parseResult, Program program) { + var defaultModule = program.DefaultModuleDef; + var fileModule = parseResult.Module; + + foreach (var modify in parseResult.ModifyBuiltins) { + modify(program.BuiltIns); + } + + foreach (var diagnostic in parseResult.ErrorReporter.AllMessages) { + program.Reporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token, + diagnostic.Message); + } + 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 ) { @@ -204,7 +129,7 @@ public static void AddFileModuleToProgram(FileModuleDefinition fileModule, Defau defaultModule.DefaultClass.SetMembersBeforeResolution(); } - public static IList TryParseIncludes( + public static IList TryParseIncludes( IReadOnlyList files, IEnumerable roots, BuiltIns builtIns, @@ -212,7 +137,7 @@ public static IList TryParseIncludes( CancellationToken cancellationToken ) { var stack = new Stack(); - var result = new List(); + var result = new List(); var resolvedFiles = new HashSet(); foreach (var rootFile in files) { resolvedFiles.Add(rootFile.Uri); @@ -233,13 +158,12 @@ CancellationToken cancellationToken cancellationToken.ThrowIfCancellationRequested(); try { - var parseIncludeResult = Parse( + var parseIncludeResult = ParseFile( + errorReporter.Options, top.Content, - top.Uri, - builtIns, - errorReporter + top.Uri ); - result.Add(parseIncludeResult.Module); + result.Add(parseIncludeResult); foreach (var include in parseIncludeResult.Module.Includes) { var dafnyFile = IncludeToDafnyFile(builtIns, errorReporter, include); @@ -267,4 +191,71 @@ private static DafnyFile IncludeToDafnyFile(BuiltIns builtIns, ErrorReporter err return null; } } + + /// + /// 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. + /// + private static DfyParseResult ParseFile(DafnyOptions options, TextReader reader, Uri uri) /* throws System.IO.IOException */ { + Contract.Requires(uri != null); + var text = SourcePreprocessor.ProcessDirectives(reader, new List()); + try { + return ParseFile(options, text, uri); + } catch (Exception e) { + var internalErrorDummyToken = new Token { + Uri = uri, + line = 1, + col = 1, + pos = 0, + val = string.Empty + }; + var reporter = new BatchErrorReporter(options); + reporter.Error(MessageSource.Parser, internalErrorDummyToken, + "[internal error] Parser exception: " + e.Message); + return new DfyParseResult(reporter, null, new Action[] { }); + } + } + + /// + /// 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. + /// + private static DfyParseResult ParseFile(DafnyOptions options, string /*!*/ s, Uri /*!*/ uri) { + var batchErrorReporter = new BatchErrorReporter(options); + Parser parser = SetupParser(s, uri, batchErrorReporter); + parser.Parse(); + + 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)) { + batchErrorReporter.Warning(MessageSource.Parser, null, new Token(1, 1) { Uri = uri }, "File contains no code"); + } + + return new DfyParseResult(batchErrorReporter, parser.theModule, parser.BuiltinsModifiers); + } + + private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, ErrorReporter /*!*/ errorReporter) { + Contract.Requires(s != null); + Contract.Requires(uri != null); + System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle); + System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ResolutionErrors).TypeHandle); + byte[] /*!*/ buffer = cce.NonNull(Encoding.Default.GetBytes(s)); + var ms = new MemoryStream(buffer, false); + var firstToken = new Token { + Uri = uri + }; + + var errors = new Errors(errorReporter); + + var scanner = new Scanner(ms, errors, uri, firstToken: firstToken); + return new Parser(errorReporter.Options, scanner, errors); + } + + 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); + } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Include.cs b/Source/DafnyCore/AST/Include.cs new file mode 100644 index 00000000000..531daee49f5 --- /dev/null +++ b/Source/DafnyCore/AST/Include.cs @@ -0,0 +1,29 @@ +using System; +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Dafny; + +public class Include : TokenNode, IComparable { + public Uri IncluderFilename { get; } + public Uri IncludedFilename { get; } + public string CanonicalPath { get; } + + public Include(IToken tok, Uri includer, Uri theFilename) { + this.tok = tok; + this.IncluderFilename = includer; + this.IncludedFilename = theFilename; + this.CanonicalPath = DafnyFile.Canonicalize(theFilename.LocalPath).LocalPath; + } + + public int CompareTo(object obj) { + if (obj is Include include) { + return CanonicalPath.CompareTo(include.CanonicalPath); + } else { + throw new NotImplementedException(); + } + } + + public override IEnumerable Children => Enumerable.Empty(); + public override IEnumerable PreResolveChildren => Enumerable.Empty(); +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs b/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs index 6815cc4e7f4..8f2d28aad14 100644 --- a/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/Modules/TopLevelDeclarations.cs @@ -1172,16 +1172,16 @@ public class DefaultModuleDefinition : ModuleDefinition { 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, bool defaultClassFirst) : base(RangeToken.NoToken, new Name("_module"), new List(), false, false, null, null, null, true, defaultClassFirst) { RootSourceUris = rootSourceUris; } - public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original) : base(cloner, original, original.NameNode) { - RootSourceUris = original.RootSourceUris; - } - public override bool IsDefaultModule => true; public override IEnumerable PreResolveChildren => Includes.Concat(base.PreResolveChildren); } diff --git a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs index 939073359dc..f0529d74b5c 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs @@ -55,7 +55,7 @@ internal override void PostResolve(Program program) { } foreach (var compileModule in program.CompileModules) { var reporter = Reporter; - Reporter = new ErrorReporterSink(program.Options, program.DefaultModuleDef); + Reporter = new ErrorReporterSink(program.Options); FlattenNode(compileModule); Reporter = reporter; } diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 0ed24d28a72..a8cc04657d3 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -27,7 +27,7 @@ readonly FrameExpression/*!*/ dummyFrameExpr; readonly Statement/*!*/ dummyStmt; readonly Statement/*!*/ dummyIfStmt; public readonly FileModuleDefinition theModule; -readonly BuiltIns theBuiltIns; +public readonly List> BuiltinsModifiers = new(); DafnyOptions theOptions; int anonymousIds = 0; @@ -178,7 +178,7 @@ public void ApplyOptionsFromAttributes(Attributes attrs) { } } -public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, BuiltIns builtIns) +public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors) : this(scanner, errors) // the real work { // initialize readonly fields @@ -190,8 +190,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, BuiltIns builtIns) dummyIfStmt = new IfStmt(Token.NoToken.ToRange(), false, null, dummyBlockStmt, null); theModule = new FileModuleDefinition(); - theBuiltIns = builtIns; - theOptions = new DafnyOptions(builtIns.Options); + theOptions = new DafnyOptions(options); } bool IsIdentifier(int kind) { @@ -2231,7 +2230,8 @@ TypeAndToken // Extracting the dimension out of array2 or array10? var dimString = tokString.Substring(5, tokString.Length - (q?6:5)); // 5 is length of "array" int dims = StringToInt(dimString, 1, "arrays of that many dimensions", startToken); - ty = theBuiltIns.ArrayType(tok, dims, gt, true, q); + (ty, var bMod) = BuiltIns.ArrayType(tok, dims, gt, true, q); + BuiltinsModifiers.Add(bMod); .) | TupleType | NamedType @@ -2257,7 +2257,7 @@ TypeAndToken gt = tupleArgTypes; } var arity = gt.Count; - theBuiltIns.CreateArrowTypeDecl(arity); + BuiltinsModifiers.Add(b => b.CreateArrowTypeDecl(arity)); if (arrowKind == 0) { ty = new ArrowType(tok, gt, t2); } else { @@ -2296,7 +2296,8 @@ TupleType<.out Type ty, out IToken tok, out List tupleArgTypes, out List tok != null); - var tmp = theBuiltIns.TupleType(tok, dims, true, argumentGhostness); // make sure the tuple type exists + var tokCopy = tok; + BuiltinsModifiers.Add(b => b.TupleType(tokCopy, dims, true, argumentGhostness)); // make sure the tuple type exists ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(argumentGhostness), dims == 0 ? null : tupleArgTypes); } .) @@ -2652,10 +2653,10 @@ FunctionDecl } f.BodyStartTok = bodyStart; f.TokenWithTrailingDocString = tokenWithTrailingDocString; - theBuiltIns.CreateArrowTypeDecl(formals.Count); + BuiltinsModifiers.Add(b => b.CreateArrowTypeDecl(formals.Count)); if (isLeastPredicate || isGreatestPredicate) { // also create an arrow type for the corresponding prefix predicate - theBuiltIns.CreateArrowTypeDecl(formals.Count + 1); + BuiltinsModifiers.Add(b => b.CreateArrowTypeDecl(formals.Count + 1)); } .) . @@ -3053,7 +3054,8 @@ NewArray<. out List ee, out Expression arrayElementInit, out List "]" (. // make sure an array class with this dimensionality exists - var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true); + var eeCopy = ee; + BuiltinsModifiers.Add(b => b.ArrayType(eeCopy.Count, new IntType(), true)); .) [ "(" Expression ")" @@ -3452,7 +3454,7 @@ SingleExtendedPattern<.out ExtendedPattern pat.> { "," ExtendedPattern (. arguments.Add(pat); .) }] ")" (. // make sure the tuple type exists - theBuiltIns.TupleType(id, arguments.Count, true); + BuiltinsModifiers.Add(b => b.TupleType(id, arguments.Count, true)); //use the TupleTypeCtors string ctor = BuiltIns.TupleTypeCtorName(arguments.Count); pat = new IdPattern(id, ctor, arguments); @@ -4338,7 +4340,7 @@ LambdaExpression "=>" Expression (. e = new LambdaExpr(x, new RangeToken(x, t), bvs, req, reads, body); - theBuiltIns.CreateArrowTypeDecl(bvs.Count); + BuiltinsModifiers.Add(b => b.CreateArrowTypeDecl(bvs.Count)); .) . @@ -4384,7 +4386,7 @@ ParensExpression } var argumentGhostness = ghostness.ToList(); // make sure the corresponding tuple type exists - var tmp = theBuiltIns.TupleType(x, args.Count, true, argumentGhostness); + BuiltinsModifiers.Add(b => b.TupleType(x, args.Count, true, argumentGhostness)); e = new DatatypeValue(x, BuiltIns.TupleTypeName(argumentGhostness), BuiltIns.TupleTypeCtorName(args.Count), args); } .) @@ -4936,7 +4938,7 @@ Suffix (. if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists - var tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true); + BuiltinsModifiers.Add(b => b.ArrayType(multipleIndices.Count, new IntType(), true)); } else { if (!anyDots && e0 == null) { /* a parsing error occurred */ diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index 84a34a8b270..e0593db8527 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -62,8 +62,8 @@ public static string Parse(IReadOnlyList files, string programName, D var defaultModuleDefinition = 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), + DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(options), + DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(options), _ => throw new ArgumentOutOfRangeException() }; @@ -98,23 +98,6 @@ public static string Resolve(Program program) { 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, TextWriter output, diff --git a/Source/DafnyCore/Generic/BatchErrorReporter.cs b/Source/DafnyCore/Generic/BatchErrorReporter.cs index 4d6b6c01e58..deaeb21772e 100644 --- a/Source/DafnyCore/Generic/BatchErrorReporter.cs +++ b/Source/DafnyCore/Generic/BatchErrorReporter.cs @@ -4,11 +4,12 @@ namespace Microsoft.Dafny; public class BatchErrorReporter : ErrorReporter { - public Dictionary> AllMessages; + public Dictionary> AllMessagesByLevel; + public readonly List AllMessages = new(); - public BatchErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { + public BatchErrorReporter(DafnyOptions options) : base(options) { ErrorsOnly = false; - AllMessages = new Dictionary> { + AllMessagesByLevel = new Dictionary> { [ErrorLevel.Error] = new(), [ErrorLevel.Warning] = new(), [ErrorLevel.Info] = new() @@ -20,16 +21,19 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro // discard the message return false; } - AllMessages[level].Add(new DafnyDiagnostic(errorId, tok, msg, source, level, new List())); + + var dafnyDiagnostic = new DafnyDiagnostic(errorId, tok, msg, source, level, new List()); + AllMessages.Add(dafnyDiagnostic); + AllMessagesByLevel[level].Add(dafnyDiagnostic); return true; } public override int Count(ErrorLevel level) { - return AllMessages[level].Count; + return AllMessagesByLevel[level].Count; } public override int CountExceptVerifierAndCompiler(ErrorLevel level) { - return AllMessages[level].Count(message => message.Source != MessageSource.Verifier && + return AllMessagesByLevel[level].Count(message => message.Source != MessageSource.Verifier && message.Source != MessageSource.Compiler); } } diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index 9ec27181a17..982d22d9557 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -23,11 +23,9 @@ public record DafnyDiagnostic(string ErrorId, IToken Token, string Message, IReadOnlyList RelatedInformation); public abstract class ErrorReporter { - public DefaultModuleDefinition OuterModule { get; } public DafnyOptions Options { get; } - protected ErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule) { - this.OuterModule = outerModule; + protected ErrorReporter(DafnyOptions options) { this.Options = options; } @@ -46,14 +44,6 @@ 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) { - Message(source, ErrorLevel.Error, null, include.tok, "the included file " + Path.GetFileName(tok.ActualFilename) + " contains error(s)"); - include.ErrorReported = true; - } - } Message(source, ErrorLevel.Error, errorId, tok, msg); } @@ -222,12 +212,12 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro return false; } - public ConsoleErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { + public ConsoleErrorReporter(DafnyOptions options) : base(options) { } } public class ErrorReporterSink : ErrorReporter { - public ErrorReporterSink(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { } + public ErrorReporterSink(DafnyOptions options) : base(options) { } public override bool Message(MessageSource source, ErrorLevel level, string errorId, IToken tok, string msg) { return false; @@ -251,7 +241,7 @@ public class ErrorReporterWrapper : BatchErrorReporter { private string msgPrefix; public readonly ErrorReporter WrappedReporter; - public ErrorReporterWrapper(ErrorReporter reporter, string msgPrefix) : base(reporter.Options, reporter.OuterModule) { + public ErrorReporterWrapper(ErrorReporter reporter, string msgPrefix) : base(reporter.Options) { this.msgPrefix = msgPrefix; this.WrappedReporter = reporter; } diff --git a/Source/DafnyCore/JsonDiagnostics.cs b/Source/DafnyCore/JsonDiagnostics.cs index b3bedcffc41..7d82ab0c089 100644 --- a/Source/DafnyCore/JsonDiagnostics.cs +++ b/Source/DafnyCore/JsonDiagnostics.cs @@ -118,6 +118,6 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro return false; } - public JsonConsoleErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { + public JsonConsoleErrorReporter(DafnyOptions options) : base(options) { } } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index 97f6ae52820..3772be3e71f 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -74,8 +74,8 @@ TopLevelDecl BuiltInTypeDecl(string name) { } if (IsArrayName(name, out var dims)) { // make sure the array class has been created - var at = resolver.builtIns.ArrayType(Token.NoToken, dims, - new List { new InferredTypeProxy() }, true); + BuiltIns.ArrayType(Token.NoToken, dims, + new List { new InferredTypeProxy() }, true).ModifyBuiltins(resolver.builtIns); decl = resolver.builtIns.arrayTypeDecls[dims]; } else if (IsBitvectorName(name, out var width)) { var bvDecl = new ValuetypeDecl(name, resolver.builtIns.SystemModule, t => t.IsBitVectorType, diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index b3dcdc2b44e..90c5aa80596 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -5795,7 +5795,8 @@ Type ResolvedArrayType(IToken tok, int dims, Type arg, ResolutionContext resolut Contract.Requires(tok != null); Contract.Requires(1 <= dims); Contract.Requires(arg != null); - var at = builtIns.ArrayType(tok, dims, new List { arg }, false, useClassNameType); + var (at, modBuiltins) = BuiltIns.ArrayType(tok, dims, new List { arg }, false, useClassNameType); + modBuiltins(builtIns); ResolveType(tok, at, resolutionContext, ResolveTypeOptionEnum.DontInfer, null); return at; } @@ -5984,7 +5985,7 @@ public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract, // The "method not found" errors which will be generated here were already reported while // resolving the statement, so we don't want them to reappear and redirect them into a sink. var origReporter = this.reporter; - this.reporter = new ErrorReporterSink(Options, origReporter.OuterModule); + this.reporter = new ErrorReporterSink(Options); var isFailure = ResolveMember(tok, tp, "IsFailure", out _); var propagateFailure = ResolveMember(tok, tp, "PropagateFailure", out _); diff --git a/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs b/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs index 1199a23dbbc..48d3d57cd2e 100644 --- a/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs +++ b/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs @@ -32,7 +32,7 @@ public override int CountExceptVerifierAndCompiler(ErrorLevel level) { return Count(level); } - public FirstErrorCollector(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { + public FirstErrorCollector(DafnyOptions options) : base(options) { } } @@ -101,7 +101,7 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN if (!constraintIsCompilable) { IToken finalToken = boundVar.tok; if (constraint.tok.line != 0) { - var errorCollector = new FirstErrorCollector(reporter.Options, reporter.OuterModule); + var errorCollector = new FirstErrorCollector(reporter.Options); ExpressionTester.CheckIsCompilable(null, errorCollector, constraint, new CodeContextWrapper(subsetTypeDecl, true)); if (errorCollector.Collected) { finalToken = new NestedToken(finalToken, errorCollector.FirstCollectedToken, diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index 2dd64c248c3..2f24477cd4d 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -426,7 +426,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, IPointer nwPoi } } else if (nw is DefaultClassDecl) { if (d is DefaultClassDecl) { - m.DefaultClass = (DefaultClassDecl)MergeClass((DefaultClassDecl)nw, (DefaultClassDecl)d); + nwPointer.Set((DefaultClassDecl)MergeClass((DefaultClassDecl)nw, (DefaultClassDecl)d)); } else { Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index ee7f1308961..08f6f36e79b 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -575,7 +575,7 @@ public async Task OpeningDocumentThatIncludesDocumentWithSyntaxErrorsReportsPars Assert.Single(diagnostics); Assert.Equal("Parser", diagnostics[0].Source); Assert.Equal(DiagnosticSeverity.Error, diagnostics[0].Severity); - Assert.Equal(new Range((0, 8), (0, 25)), diagnostics[0].Range); + Assert.Equal(new Range((0, 0), (0, 7)), diagnostics[0].Range); await AssertNoDiagnosticsAreComing(CancellationToken); } @@ -602,9 +602,9 @@ public async Task OpeningDocumentWithSemanticErrorsInIncludeReportsResolverError await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.Single(diagnostics); - Assert.Equal("Resolver", diagnostics[0].Source); + Assert.Equal("Parser", diagnostics[0].Source); Assert.Equal(DiagnosticSeverity.Error, diagnostics[0].Severity); - Assert.Equal(new Range((0, 8), (0, 27)), diagnostics[0].Range); + Assert.Equal(new Range((0, 0), (0, 7)), diagnostics[0].Range); await AssertNoDiagnosticsAreComing(CancellationToken); } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs index fa8d704488f..378b5c491d7 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs @@ -83,8 +83,8 @@ method Recurse(x: int) returns (r: int) { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var document = await Documents.GetLastDocumentAsync(documentItem.Uri); Assert.NotNull(document); - Assert.Equal(1, document.Diagnostics.Count(d => d.Level == ErrorLevel.Error)); - var message = document.Diagnostics.First(d => d.Level == ErrorLevel.Error); + Assert.Equal(1, document.AllFileDiagnostics.Count(d => d.Level == ErrorLevel.Error)); + var message = document.AllFileDiagnostics.First(d => d.Level == ErrorLevel.Error); Assert.Equal(MessageSource.Verifier, message.Source); } diff --git a/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs b/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs index dcd3fcd2ad6..086a8678810 100644 --- a/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/DafnyLangSymbolResolverTest.cs @@ -18,10 +18,10 @@ public DafnyLangSymbolResolverTest() { class CollectingErrorReporter : BatchErrorReporter { public Dictionary> GetErrors() { - return this.AllMessages; + return this.AllMessagesByLevel; } - public CollectingErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { + public CollectingErrorReporter(DafnyOptions options) : base(options) { } } diff --git a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs index d36131fe201..f6f00f3f5d5 100644 --- a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs @@ -40,10 +40,10 @@ public GhostStateDiagnosticCollectorTest(ITestOutputHelper output) { class CollectingErrorReporter : BatchErrorReporter { public Dictionary> GetErrors() { - return this.AllMessages; + return this.AllMessagesByLevel; } - public CollectingErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { + public CollectingErrorReporter(DafnyOptions options) : base(options) { } } @@ -62,7 +62,7 @@ public void EnsureResilienceAgainstErrors() { var options = DafnyOptions.DefaultImmutableOptions; var rootUri = new Uri(Directory.GetCurrentDirectory()); var dummyModuleDecl = new DummyModuleDecl(new List() { rootUri }); - var reporter = new CollectingErrorReporter(options, (DefaultModuleDefinition)dummyModuleDecl.ModuleDef); + var reporter = new CollectingErrorReporter(options); var program = new Dafny.Program("dummy", dummyModuleDecl, null, reporter, Sets.Empty(), Sets.Empty()); var ghostDiagnostics = ghostStateDiagnosticCollector.GetGhostStateDiagnostics( new SignatureAndCompletionTable(null!, new CompilationUnit(rootUri, program), diff --git a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs index b60aa674664..8d4696b3caf 100644 --- a/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/ParserExceptionTest.cs @@ -29,8 +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 }, false); - var errorReporter = new ParserExceptionSimulatingErrorReporter(options, outerModule); + var errorReporter = new ParserExceptionSimulatingErrorReporter(options); parser.Parse(new DocumentTextBuffer(documentItem), errorReporter, default); Assert.Equal($"/{TestFilePath}(1,0): Error: [internal error] Parser exception: Simulated parser internal error", errorReporter.LastMessage); } @@ -63,7 +62,7 @@ public override int CountExceptVerifierAndCompiler(ErrorLevel level) { throw new NotImplementedException(); } - public ParserExceptionSimulatingErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule) : base(options, outerModule) { + public ParserExceptionSimulatingErrorReporter(DafnyOptions options) : base(options) { } } diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index 84cfae5a31e..25fb7a43ff3 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -63,7 +63,7 @@ public async Task GetLastDiagnostics(TextDocumentItem documentItem Diagnostic[] result; do { result = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(cancellationToken); - } while (!document!.Diagnostics.Select(d => d.ToLspDiagnostic()).SequenceEqual(result)); + } while (!document!.AllFileDiagnostics.Select(d => d.ToLspDiagnostic()).SequenceEqual(result)); return result; } diff --git a/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs b/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs index 749ede2ee50..d226bb9a572 100644 --- a/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/ConcurrentInteractionsTest.cs @@ -86,8 +86,8 @@ DidChangeTextDocumentParams MakeChange(int? version, Range range, string text) { var document = await Documents.GetLastDocumentAsync(documentItem.Uri); Assert.NotNull(document); Assert.Equal(documentItem.Version + 11, document.Version); - Assert.Single(document.Diagnostics); - Assert.Equal("assertion might not hold", document.Diagnostics.First().Message); + Assert.Single(document.AllFileDiagnostics); + Assert.Equal("assertion might not hold", document.AllFileDiagnostics.First().Message); } [Fact(Timeout = MaxTestExecutionTimeMs)] diff --git a/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs b/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs index 5004cda00e3..83306763d96 100644 --- a/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/MultiFileTest.cs @@ -52,7 +52,7 @@ method Test() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var document = await Documents.GetLastDocumentAsync(documentItem.Uri); Assert.NotNull(document); - Assert.Single(document.Diagnostics); + Assert.Single(document.AllFileDiagnostics); } public MultiFileTest(ITestOutputHelper output) : base(output) { diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs index b0e90344039..ce96bb1a415 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs @@ -153,7 +153,7 @@ public DafnyCodeActionInput(DocumentAfterParsing document) { public Dafny.Program Program => Document.Program; public DocumentAfterParsing Document { get; } - public IReadOnlyList Diagnostics => Document.Diagnostics.ToList(); + public IReadOnlyList Diagnostics => Document.AllFileDiagnostics.ToList(); public VerificationTree VerificationTree => Document.GetInitialDocumentVerificationTree(); public string Extract(Range range) { diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index f94fadad33c..958d4e249e7 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -69,7 +69,7 @@ private Dafny.Program NewDafnyProgram(TextDocumentItem document, ErrorReporter e Type.ResetScopes(); return new Dafny.Program( document.Uri.ToString(), - new LiteralModuleDecl(errorReporter.OuterModule, null), + new LiteralModuleDecl(new DefaultModuleDefinition(new List(), false), null), // BuiltIns cannot be initialized without Type.ResetScopes() before. new BuiltIns(errorReporter.Options), errorReporter, Sets.Empty(), Sets.Empty() diff --git a/Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs b/Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs index 41d2e978bfe..c7102148c5b 100644 --- a/Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs +++ b/Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs @@ -3,6 +3,7 @@ using OmniSharp.Extensions.LanguageServer.Protocol; using System; using System.Collections.Generic; +using System.Collections.Immutable; using System.IO; using System.Linq; using System.Threading; @@ -27,12 +28,12 @@ public class DiagnosticErrorReporter : ErrorReporter { /// /// The uri of the entry document is necessary to report general compiler errors as part of this document. /// - public DiagnosticErrorReporter(DafnyOptions options, DefaultModuleDefinition outerModule, string documentSource, DocumentUri entryDocumentUri) : base(options, outerModule) { + public DiagnosticErrorReporter(DafnyOptions options, string documentSource, DocumentUri entryDocumentUri) : base(options) { this.entryDocumentSource = documentSource; this.entryDocumentUri = entryDocumentUri; } - public IReadOnlyDictionary> AllDiagnostics => diagnostics; + public IReadOnlyDictionary> AllDiagnosticsCopy => diagnostics.ToImmutableDictionary(); public IReadOnlyList GetDiagnostics(DocumentUri documentUri) { rwLock.EnterReadLock(); diff --git a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs b/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs index 886ea00a133..8d77373c6ae 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/SignatureAndCompletionTable.cs @@ -44,7 +44,7 @@ public class SignatureAndCompletionTable { public static SignatureAndCompletionTable Empty(DafnyOptions options, DocumentTextBuffer textDocument) { var outerModule = new DefaultModuleDefinition(new List() { textDocument.Uri.ToUri() }, false); - var errorReporter = new DiagnosticErrorReporter(options, outerModule, textDocument.Text, textDocument.Uri); + var errorReporter = new DiagnosticErrorReporter(options, textDocument.Text, textDocument.Uri); return new SignatureAndCompletionTable( NullLogger.Instance, new CompilationUnit(textDocument.Uri.ToUri(), new Dafny.Program( diff --git a/Source/DafnyLanguageServer/Workspace/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Compilation.cs index 42194d64e95..77f590ed49d 100644 --- a/Source/DafnyLanguageServer/Workspace/Compilation.cs +++ b/Source/DafnyLanguageServer/Workspace/Compilation.cs @@ -126,7 +126,7 @@ private async Task TranslateAsync() { public async Task PrepareVerificationTasksAsync( DocumentAfterResolution loaded, CancellationToken cancellationToken) { - if (loaded.ParseAndResolutionDiagnostics.Any(d => + if (loaded.AllFileDiagnostics.Any(d => d.Level == ErrorLevel.Error && d.Source != MessageSource.Compiler && d.Source != MessageSource.Verifier)) { @@ -158,7 +158,7 @@ public async Task PrepareVerificationTasksAsync( var translated = new DocumentAfterTranslation(services, loaded.TextDocumentItem, loaded.Program, - loaded.ParseAndResolutionDiagnostics, loaded.SymbolTable, loaded.SignatureAndCompletionTable, loaded.GhostDiagnostics, verificationTasks, + loaded.ResolutionDiagnostics, loaded.SymbolTable, loaded.SignatureAndCompletionTable, loaded.GhostDiagnostics, verificationTasks, new(), initialViews, migratedVerificationTree ?? new DocumentVerificationTree(loaded.TextDocumentItem)); @@ -297,7 +297,7 @@ private void HandleStatusUpdate(DocumentAfterTranslation document, IImplementati private bool ReportGutterStatus => options.Get(ServerCommand.LineVerificationStatus); private List GetDiagnosticsFromResult(DocumentAfterResolution document, VerificationResult result) { - var errorReporter = new DiagnosticErrorReporter(options, document.Program.DefaultModuleDef, document.TextDocumentItem.Text, document.Uri); + var errorReporter = new DiagnosticErrorReporter(options, document.TextDocumentItem.Text, document.Uri); foreach (var counterExample in result.Errors) { errorReporter.ReportBoogieError(counterExample.CreateErrorInformation(result.Outcome, options.ForceBplErrors)); } @@ -370,7 +370,7 @@ public void MarkVerificationFinished() { public async Task GetTextEditToFormatCode() { // TODO https://github.com/dafny-lang/dafny/issues/3416 var parsedDocument = await ResolvedDocument; - if (parsedDocument.Diagnostics.Any(diagnostic => + if (parsedDocument.AllFileDiagnostics.Any(diagnostic => diagnostic.Level == ErrorLevel.Error && diagnostic.Source == MessageSource.Parser )) { diff --git a/Source/DafnyLanguageServer/Workspace/Document.cs b/Source/DafnyLanguageServer/Workspace/Document.cs deleted file mode 100644 index 6a5643fb1b4..00000000000 --- a/Source/DafnyLanguageServer/Workspace/Document.cs +++ /dev/null @@ -1,148 +0,0 @@ -using System; -using OmniSharp.Extensions.LanguageServer.Protocol; -using OmniSharp.Extensions.LanguageServer.Protocol.Models; -using System.Collections.Generic; -using System.Linq; -using Microsoft.Boogie; -using Microsoft.Dafny.LanguageServer.Language; -using Microsoft.Dafny.LanguageServer.Language.Symbols; -using Microsoft.Dafny.LanguageServer.Workspace.Notifications; -using Microsoft.Extensions.DependencyInjection; -using Microsoft.Extensions.Logging; -using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; - -namespace Microsoft.Dafny.LanguageServer.Workspace { - - /// - /// Internal representation of a specific version of a Dafny document. - /// - /// Only one instance should exist of a specific version. - /// Asynchronous compilation tasks use this instance to synchronise on. - /// - /// When verification starts, no new instances of Compilation will be created for this version. - /// There can be different verification threads that update the state of this object. - /// - public class Document { - public DocumentTextBuffer TextDocumentItem { get; } - public DocumentUri Uri => TextDocumentItem.Uri; - public int Version => TextDocumentItem.Version!.Value; - - public Document(DocumentTextBuffer textDocumentItem) { - TextDocumentItem = textDocumentItem; - } - - public virtual IEnumerable Diagnostics => Enumerable.Empty(); - - public IdeState InitialIdeState(DafnyOptions options) { - return ToIdeState(new IdeState(TextDocumentItem, Array.Empty(), - SymbolTable.Empty(), SignatureAndCompletionTable.Empty(options, TextDocumentItem), new Dictionary(), - Array.Empty(), - false, Array.Empty(), - GetInitialDocumentVerificationTree())); - } - - public virtual VerificationTree GetInitialDocumentVerificationTree() { - return new DocumentVerificationTree(TextDocumentItem); - } - - /// - /// Collects information to present to the IDE - /// - public virtual IdeState ToIdeState(IdeState previousState) { - return previousState with { - TextDocumentItem = TextDocumentItem, - ImplementationsWereUpdated = false, - }; - } - } - - public class DocumentAfterParsing : Document { - private readonly IReadOnlyList parseDiagnostics; - - public DocumentAfterParsing(DocumentTextBuffer textDocumentItem, - Dafny.Program program, - IReadOnlyList parseDiagnostics) : base(textDocumentItem) { - this.parseDiagnostics = parseDiagnostics; - Program = program; - } - - public override IEnumerable Diagnostics => parseDiagnostics; - - public Dafny.Program Program { get; } - - public override IdeState ToIdeState(IdeState previousState) { - return previousState with { - TextDocumentItem = TextDocumentItem, - ResolutionDiagnostics = Diagnostics.Select(d => d.ToLspDiagnostic()), - ImplementationsWereUpdated = false, - }; - } - } - - public class DocumentAfterTranslation : DocumentAfterResolution { - public DocumentAfterTranslation( - IServiceProvider services, - DocumentTextBuffer textDocumentItem, - Dafny.Program program, - IReadOnlyList parseAndResolutionDiagnostics, - SymbolTable? symbolTable, - SignatureAndCompletionTable signatureAndCompletionTable, - IReadOnlyList ghostDiagnostics, - IReadOnlyList verificationTasks, - List counterexamples, - Dictionary implementationIdToView, - VerificationTree verificationTree) - : base(textDocumentItem, program, parseAndResolutionDiagnostics, symbolTable, signatureAndCompletionTable, ghostDiagnostics) { - VerificationTree = verificationTree; - VerificationTasks = verificationTasks; - Counterexamples = counterexamples; - ImplementationIdToView = implementationIdToView; - - GutterProgressReporter = new VerificationProgressReporter( - services.GetRequiredService>(), - this, - services.GetRequiredService(), - services.GetRequiredService()); - } - - public override VerificationTree GetInitialDocumentVerificationTree() { - return VerificationTree; - } - - public override IdeState ToIdeState(IdeState previousState) { - IEnumerable> implementationViewsWithMigratedDiagnostics = ImplementationIdToView.Select(kv => { - IEnumerable diagnostics = kv.Value.Diagnostics.Select(d => d.ToLspDiagnostic()); - if (kv.Value.Status < PublishedVerificationStatus.Error) { - diagnostics = previousState.ImplementationIdToView.GetValueOrDefault(kv.Key)?.Diagnostics ?? diagnostics; - } - - var value = new IdeImplementationView(kv.Value.Range, kv.Value.Status, diagnostics.ToList()); - return new KeyValuePair(kv.Key, value); - }); - return base.ToIdeState(previousState) with { - ImplementationsWereUpdated = true, - VerificationTree = VerificationTree, - Counterexamples = new List(Counterexamples), - ImplementationIdToView = new Dictionary(implementationViewsWithMigratedDiagnostics) - }; - } - - public override IEnumerable Diagnostics => base.Diagnostics.Concat( - ImplementationIdToView.SelectMany(kv => kv.Value.Diagnostics) ?? Enumerable.Empty()); - - /// - /// Contains the real-time status of all verification efforts. - /// Can be migrated from a previous document - /// The position and the range are never sent to the client. - /// - public VerificationTree VerificationTree { get; set; } - public IReadOnlyList VerificationTasks { get; set; } - public IVerificationProgressReporter GutterProgressReporter { get; set; } - public List Counterexamples { get; set; } - public Dictionary ImplementationIdToView { get; set; } - } - - public record ImplementationView(Range Range, PublishedVerificationStatus Status, IReadOnlyList Diagnostics); - - public record BufferLine(int LineNumber, int StartIndex, int EndIndex); -} diff --git a/Source/DafnyLanguageServer/Workspace/Documents/Document.cs b/Source/DafnyLanguageServer/Workspace/Documents/Document.cs new file mode 100644 index 00000000000..46e807bd286 --- /dev/null +++ b/Source/DafnyLanguageServer/Workspace/Documents/Document.cs @@ -0,0 +1,59 @@ +using System; +using OmniSharp.Extensions.LanguageServer.Protocol; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Boogie; +using Microsoft.Dafny.LanguageServer.Language.Symbols; +using Microsoft.Dafny.LanguageServer.Workspace.Notifications; +using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; + +namespace Microsoft.Dafny.LanguageServer.Workspace { + + /// + /// Internal representation of a specific version of a Dafny document. + /// + /// Only one instance should exist of a specific version. + /// Asynchronous compilation tasks use this instance to synchronise on. + /// + /// When verification starts, no new instances of Compilation will be created for this version. + /// There can be different verification threads that update the state of this object. + /// + public class Document { + public DocumentTextBuffer TextDocumentItem { get; } + public DocumentUri Uri => TextDocumentItem.Uri; + public int Version => TextDocumentItem.Version!.Value; + + public Document(DocumentTextBuffer textDocumentItem) { + TextDocumentItem = textDocumentItem; + } + + public virtual IEnumerable AllFileDiagnostics => Enumerable.Empty(); + + public IdeState InitialIdeState(DafnyOptions options) { + return ToIdeState(new IdeState(TextDocumentItem, Array.Empty(), + SymbolTable.Empty(), SignatureAndCompletionTable.Empty(options, TextDocumentItem), new Dictionary(), + Array.Empty(), + false, Array.Empty(), + GetInitialDocumentVerificationTree())); + } + + public virtual VerificationTree GetInitialDocumentVerificationTree() { + return new DocumentVerificationTree(TextDocumentItem); + } + + /// + /// Collects information to present to the IDE + /// + public virtual IdeState ToIdeState(IdeState previousState) { + return previousState with { + TextDocumentItem = TextDocumentItem, + ImplementationsWereUpdated = false, + }; + } + } + + public record ImplementationView(Range Range, PublishedVerificationStatus Status, IReadOnlyList Diagnostics); + + public record BufferLine(int LineNumber, int StartIndex, int EndIndex); +} diff --git a/Source/DafnyLanguageServer/Workspace/Documents/DocumentAfterParsing.cs b/Source/DafnyLanguageServer/Workspace/Documents/DocumentAfterParsing.cs new file mode 100644 index 00000000000..fcbdcfb6fb5 --- /dev/null +++ b/Source/DafnyLanguageServer/Workspace/Documents/DocumentAfterParsing.cs @@ -0,0 +1,50 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Dafny.LanguageServer.Language; +using OmniSharp.Extensions.LanguageServer.Protocol; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; + +namespace Microsoft.Dafny.LanguageServer.Workspace; + +public class DocumentAfterParsing : Document { + public IReadOnlyDictionary> ResolutionDiagnostics { get; } + + public DocumentAfterParsing(DocumentTextBuffer textDocumentItem, + Dafny.Program program, + IReadOnlyDictionary> diagnostics) : base(textDocumentItem) { + this.ResolutionDiagnostics = diagnostics; + Program = program; + } + + public override IEnumerable AllFileDiagnostics => FileResolutionDiagnostics; + + private IEnumerable FileResolutionDiagnostics => ResolutionDiagnostics.GetOrDefault(TextDocumentItem.Uri, Enumerable.Empty); + + public Dafny.Program Program { get; } + + public override IdeState ToIdeState(IdeState previousState) { + return previousState with { + TextDocumentItem = TextDocumentItem, + ResolutionDiagnostics = ComputeFileAndIncludesResolutionDiagnostics(), + ImplementationsWereUpdated = false, + }; + } + + protected IEnumerable ComputeFileAndIncludesResolutionDiagnostics() { + var includeErrorDiagnostics = GetIncludeErrorDiagnostics(); + return FileResolutionDiagnostics.Concat(includeErrorDiagnostics).Select(d => d.ToLspDiagnostic()); + } + + private IEnumerable GetIncludeErrorDiagnostics() { + foreach (var include in Program.Includes) { + var messageForIncludedFile = + ResolutionDiagnostics.GetOrDefault(include.IncludedFilename, Enumerable.Empty); + if (messageForIncludedFile.Any(m => m.Level == ErrorLevel.Error)) { + var diagnostic = new DafnyDiagnostic(null, Program.GetFirstTopLevelToken(), "the included file " + include.IncludedFilename.LocalPath + " contains error(s)", + MessageSource.Parser, ErrorLevel.Error, new DafnyRelatedInformation[] { }); + yield return diagnostic; + } + } + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Workspace/DocumentAfterResolution.cs b/Source/DafnyLanguageServer/Workspace/Documents/DocumentAfterResolution.cs similarity index 73% rename from Source/DafnyLanguageServer/Workspace/DocumentAfterResolution.cs rename to Source/DafnyLanguageServer/Workspace/Documents/DocumentAfterResolution.cs index 07c32ae4b2b..f55a9804129 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentAfterResolution.cs +++ b/Source/DafnyLanguageServer/Workspace/Documents/DocumentAfterResolution.cs @@ -2,7 +2,9 @@ using System.Collections.Generic; using System.Collections.Immutable; using System.Linq; +using Microsoft.Dafny.LanguageServer.Language; using Microsoft.Dafny.LanguageServer.Language.Symbols; +using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; namespace Microsoft.Dafny.LanguageServer.Workspace; @@ -10,29 +12,24 @@ namespace Microsoft.Dafny.LanguageServer.Workspace; public class DocumentAfterResolution : DocumentAfterParsing { public DocumentAfterResolution(DocumentTextBuffer textDocumentItem, Dafny.Program program, - IReadOnlyList parseAndResolutionDiagnostics, + IReadOnlyDictionary> diagnostics, SymbolTable? symbolTable, SignatureAndCompletionTable signatureAndCompletionTable, IReadOnlyList ghostDiagnostics) : - base(textDocumentItem, program, ImmutableArray.Empty) { - ParseAndResolutionDiagnostics = parseAndResolutionDiagnostics; + base(textDocumentItem, program, diagnostics) { SymbolTable = symbolTable; SignatureAndCompletionTable = signatureAndCompletionTable; GhostDiagnostics = ghostDiagnostics; } - - public IReadOnlyList ParseAndResolutionDiagnostics { get; } public SymbolTable? SymbolTable { get; } public SignatureAndCompletionTable SignatureAndCompletionTable { get; } public IReadOnlyList GhostDiagnostics { get; } - public override IEnumerable Diagnostics => ParseAndResolutionDiagnostics; - public override IdeState ToIdeState(IdeState previousState) { return previousState with { TextDocumentItem = TextDocumentItem, ImplementationsWereUpdated = false, - ResolutionDiagnostics = ParseAndResolutionDiagnostics.Select(d => d.ToLspDiagnostic()), + ResolutionDiagnostics = ComputeFileAndIncludesResolutionDiagnostics(), SymbolTable = SymbolTable ?? previousState.SymbolTable, SignatureAndCompletionTable = SignatureAndCompletionTable.Resolved ? SignatureAndCompletionTable : previousState.SignatureAndCompletionTable, GhostDiagnostics = GhostDiagnostics diff --git a/Source/DafnyLanguageServer/Workspace/Documents/DocumentAfterTranslation.cs b/Source/DafnyLanguageServer/Workspace/Documents/DocumentAfterTranslation.cs new file mode 100644 index 00000000000..3ae2601834d --- /dev/null +++ b/Source/DafnyLanguageServer/Workspace/Documents/DocumentAfterTranslation.cs @@ -0,0 +1,76 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Boogie; +using Microsoft.Dafny.LanguageServer.Language; +using Microsoft.Dafny.LanguageServer.Language.Symbols; +using Microsoft.Dafny.LanguageServer.Workspace.Notifications; +using Microsoft.Extensions.DependencyInjection; +using Microsoft.Extensions.Logging; +using OmniSharp.Extensions.LanguageServer.Protocol; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; + +namespace Microsoft.Dafny.LanguageServer.Workspace; + +public class DocumentAfterTranslation : DocumentAfterResolution { + public DocumentAfterTranslation( + IServiceProvider services, + DocumentTextBuffer textDocumentItem, + Dafny.Program program, + IReadOnlyDictionary> diagnostics, + SymbolTable? symbolTable, + SignatureAndCompletionTable signatureAndCompletionTable, + IReadOnlyList ghostDiagnostics, + IReadOnlyList verificationTasks, + List counterexamples, + Dictionary implementationIdToView, + VerificationTree verificationTree) + : base(textDocumentItem, program, diagnostics, symbolTable, signatureAndCompletionTable, ghostDiagnostics) { + VerificationTree = verificationTree; + VerificationTasks = verificationTasks; + Counterexamples = counterexamples; + ImplementationIdToView = implementationIdToView; + + GutterProgressReporter = new VerificationProgressReporter( + services.GetRequiredService>(), + this, + services.GetRequiredService(), + services.GetRequiredService()); + } + + public override VerificationTree GetInitialDocumentVerificationTree() { + return VerificationTree; + } + + public override IdeState ToIdeState(IdeState previousState) { + IEnumerable> implementationViewsWithMigratedDiagnostics = ImplementationIdToView.Select(kv => { + IEnumerable diagnostics = kv.Value.Diagnostics.Select(d => Util.ToLspDiagnostic(d)); + if (kv.Value.Status < PublishedVerificationStatus.Error) { + diagnostics = previousState.ImplementationIdToView.GetValueOrDefault(kv.Key)?.Diagnostics ?? diagnostics; + } + + var value = new IdeImplementationView(kv.Value.Range, kv.Value.Status, diagnostics.ToList()); + return new KeyValuePair(kv.Key, value); + }); + return base.ToIdeState(previousState) with { + ImplementationsWereUpdated = true, + VerificationTree = VerificationTree, + Counterexamples = new List(Counterexamples), + ImplementationIdToView = new Dictionary(implementationViewsWithMigratedDiagnostics) + }; + } + + public override IEnumerable AllFileDiagnostics => base.AllFileDiagnostics.Concat( + ImplementationIdToView.SelectMany(kv => kv.Value.Diagnostics)); + + /// + /// Contains the real-time status of all verification efforts. + /// Can be migrated from a previous document + /// The position and the range are never sent to the client. + /// + public VerificationTree VerificationTree { get; set; } + public IReadOnlyList VerificationTasks { get; set; } + public IVerificationProgressReporter GutterProgressReporter { get; set; } + public List Counterexamples { get; set; } + public Dictionary ImplementationIdToView { get; set; } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index 3846d072aa1..c4faf0d1373 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -82,11 +82,10 @@ 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() }, false); - var errorReporter = new DiagnosticErrorReporter(options, outerModule, textDocument.Text, textDocument.Uri); + var errorReporter = new DiagnosticErrorReporter(options, textDocument.Text, textDocument.Uri); statusPublisher.SendStatusNotification(textDocument, CompilationStatus.Parsing); var program = parser.Parse(textDocument, errorReporter, cancellationToken); - var documentAfterParsing = new DocumentAfterParsing(textDocument, program, errorReporter.GetDiagnostics(textDocument.Uri)); + var documentAfterParsing = new DocumentAfterParsing(textDocument, program, errorReporter.AllDiagnosticsCopy); if (errorReporter.HasErrors) { statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ParsingFailed); return documentAfterParsing; @@ -107,7 +106,7 @@ private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuff return new DocumentAfterResolution(textDocument, program, - errorReporter.GetDiagnostics(textDocument.Uri), + errorReporter.AllDiagnosticsCopy, newSymbolTable, symbolTable, ghostDiagnostics diff --git a/Source/DafnyPipeline.Test/DocstringTest.cs b/Source/DafnyPipeline.Test/DocstringTest.cs index 9e7dd057282..6ec0da8e26c 100644 --- a/Source/DafnyPipeline.Test/DocstringTest.cs +++ b/Source/DafnyPipeline.Test/DocstringTest.cs @@ -437,7 +437,7 @@ protected void DocstringWorksFor(string source, List<(string nodeTokenValue, str var dafnyProgram = Utils.Parse(options, programString, false); BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; if (reporter.ErrorCount > 0) { - var error = reporter.AllMessages[ErrorLevel.Error][0]; + var error = reporter.AllMessagesByLevel[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); } diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index 5cb07ebb7eb..bae70c73ef9 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -55,14 +55,13 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString : removeTrailingNewlineRegex.Replace(programString, ""); var uri = new Uri("virtual:virtual"); - var outerModule = new DefaultModuleDefinition(new List() { uri }, false); - BatchErrorReporter reporter = new BatchErrorReporter(options, outerModule); + var reporter = new BatchErrorReporter(options); Microsoft.Dafny.Type.ResetScopes(); var dafnyProgram = ParseUtils.Parse(programNotIndented, uri, reporter); if (reporter.ErrorCount > 0) { - var error = reporter.AllMessages[ErrorLevel.Error][0]; + var error = reporter.AllMessagesByLevel[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); } @@ -95,8 +94,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString // Verify that the formatting is stable. Microsoft.Dafny.Type.ResetScopes(); - var newOuterModule = new DefaultModuleDefinition(new List() { uri }, false); - var newReporter = new BatchErrorReporter(options, newOuterModule); + var newReporter = new BatchErrorReporter(options); dafnyProgram = ParseUtils.Parse(reprinted, uri, newReporter); ; Assert.Equal(initErrorCount, reporter.ErrorCount + newReporter.ErrorCount); diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs index f324fd8362d..7cfa42bbe93 100644 --- a/Source/DafnyPipeline.Test/PluginsTest.cs +++ b/Source/DafnyPipeline.Test/PluginsTest.cs @@ -66,7 +66,7 @@ public void EnsurePluginIsExecuted() { DafnyMain.Resolve(dafnyProgram); Assert.Equal(1, reporter.Count(ErrorLevel.Error)); - Assert.Equal("Impossible to continue because whatever", reporter.AllMessages[ErrorLevel.Error][0].Message); + Assert.Equal("Impossible to continue because whatever", reporter.AllMessagesByLevel[ErrorLevel.Error][0].Message); } [Fact] @@ -81,7 +81,7 @@ public void EnsurePluginIsExecutedEvenWithoutConfiguration() { BatchErrorReporter reporter = (BatchErrorReporter)dafnyProgram.Reporter; DafnyMain.Resolve(dafnyProgram); Assert.Equal(1, reporter.ErrorCount); - Assert.Equal("Impossible to continue", reporter.AllMessages[ErrorLevel.Error][0].Message); + Assert.Equal("Impossible to continue", reporter.AllMessagesByLevel[ErrorLevel.Error][0].Message); } [Fact] diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs index 19376b424e5..747d8baffa1 100644 --- a/Source/DafnyPipeline.Test/TranslatorTest.cs +++ b/Source/DafnyPipeline.Test/TranslatorTest.cs @@ -75,16 +75,15 @@ 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 }, false); - BatchErrorReporter reporter = new BatchErrorReporter(options, defaultModuleDefinition); + BatchErrorReporter reporter = new BatchErrorReporter(options); var dafnyProgram = ParseUtils.Parse(program, uri, reporter); if (reporter.ErrorCount > 0) { - var error = reporter.AllMessages[ErrorLevel.Error][0]; + var error = reporter.AllMessagesByLevel[ErrorLevel.Error][0]; Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); } DafnyMain.Resolve(dafnyProgram); if (reporter.ErrorCount > 0) { - var error = reporter.AllMessages[ErrorLevel.Error][0]; + var error = reporter.AllMessagesByLevel[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 8ca6c8375b9..d09a242aadc 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -41,8 +41,7 @@ public bool Verify() { private bool Parse() { var uri = new Uri("transcript:///" + fname); - var defaultModuleDefinition = new DefaultModuleDefinition(new List() { uri }, false); - reporter = new ConsoleErrorReporter(options, defaultModuleDefinition); + reporter = new ConsoleErrorReporter(options); var program = ParseUtils.ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, reporter, CancellationToken.None); diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 7ec8ddc2e9a..e9491d8fd80 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -78,8 +78,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 }, false); - var reporter = new BatchErrorReporter(options, defaultModuleDefinition); + var reporter = new BatchErrorReporter(options); var program = ParseUtils.ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, reporter, CancellationToken.None); @@ -89,7 +88,7 @@ public static Type CopyWithReplacements(Type type, List from, List } // Substitute function methods with function-by-methods - new AddByMethodRewriter(new ConsoleErrorReporter(options, defaultModuleDefinition)).PreResolve(program); + new AddByMethodRewriter(new ConsoleErrorReporter(options)).PreResolve(program); new Resolver(program).ResolveProgram(program); return program; } diff --git a/Test/allocated1/Allocated2.dfy.expect b/Test/allocated1/Allocated2.dfy.expect index 2b6f3d41344..d391285423a 100644 --- a/Test/allocated1/Allocated2.dfy.expect +++ b/Test/allocated1/Allocated2.dfy.expect @@ -1,5 +1,4 @@ The /allocated: option is deprecated -Allocated2.dfy(4,8): Error: the included file AllocatedCommon.dfyi contains error(s) AllocatedCommon.dfyi(23,26): Error: a function definition is not allowed to depend on the set of allocated references AllocatedCommon.dfyi(24,26): Error: a function definition is not allowed to depend on the set of allocated references AllocatedCommon.dfyi(25,26): Error: a function definition is not allowed to depend on the set of allocated references @@ -38,4 +37,4 @@ AllocatedCommon.dfyi(214,11): Error: a function definition is not allowed to dep AllocatedCommon.dfyi(215,11): Error: a function definition is not allowed to depend on the set of allocated references AllocatedCommon.dfyi(222,11): Error: a function definition is not allowed to depend on the set of allocated references AllocatedCommon.dfyi(223,11): Error: a function definition is not allowed to depend on the set of allocated references -39 resolution/type errors detected in Allocated2.dfy +38 resolution/type errors detected in Allocated2.dfy diff --git a/Test/allocated1/dafny0/CompilationErrors.dfy.expect b/Test/allocated1/dafny0/CompilationErrors.dfy.expect index 04d64844a52..ed3c7845249 100644 --- a/Test/allocated1/dafny0/CompilationErrors.dfy.expect +++ b/Test/allocated1/dafny0/CompilationErrors.dfy.expect @@ -5,7 +5,6 @@ CompilationErrors.dfy(83,4): Warning: note, this loop has no body (loop frame: x CompilationErrors.dfy(85,4): Warning: note, this loop has no body (loop frame: i, x) Dafny program verifier finished with 5 verified, 0 errors -CompilationErrors.dfy(3,8): Error: the included file CompilationErrors.dfy contains error(s) CompilationErrors.dfy(6,13): Error: Method _module._default.M has no body CompilationErrors.dfy(7,7): Error: Method _module._default.P has no body CompilationErrors.dfy(19,15): Error: Function _module._default.F has no body diff --git a/Test/allocated1/dafny0/Fuel.dfy.expect b/Test/allocated1/dafny0/Fuel.dfy.expect index 498aedbec44..44855fdcde3 100644 --- a/Test/allocated1/dafny0/Fuel.dfy.expect +++ b/Test/allocated1/dafny0/Fuel.dfy.expect @@ -1,5 +1,4 @@ The /allocated: option is deprecated -Fuel.dfy(3,8): Error: the included file Fuel.dfy contains error(s) Fuel.dfy(129,8): Error: Fuel can only increase within a given scope. Fuel.dfy(407,8): Error: Fuel can only increase within a given scope. Fuel.dfy(17,22): Error: assertion might not hold diff --git a/Test/dafny4/git-issue16.dfy.expect b/Test/dafny4/git-issue16.dfy.expect index 69d2226eb3c..b1ce39cefb9 100644 --- a/Test/dafny4/git-issue16.dfy.expect +++ b/Test/dafny4/git-issue16.dfy.expect @@ -1,3 +1,2 @@ -git-issue16.dfy(4,8): Error: the included file git-issue16.dfyi contains error(s) git-issue16.dfyi(2,5): Error: arguments must have comparable types (got int and bool) -2 resolution/type errors detected in git-issue16.dfy +1 resolution/type errors detected in git-issue16.dfy diff --git a/Test/git-issues/git-issue-3294.dfy.expect b/Test/git-issues/git-issue-3294.dfy.expect index 9df67ca0175..53f65df4b6e 100644 --- a/Test/git-issues/git-issue-3294.dfy.expect +++ b/Test/git-issues/git-issue-3294.dfy.expect @@ -1,3 +1,2 @@ -git-issue-3294.dfy(0,0): Error: the included file git-issue-3294.dfy contains error(s) git-issue-3294.dfy(7,4): Error: member IsFailure does not exist in FailureRestrictedType, in :- statement -2 resolution/type errors detected in git-issue-3294.dfy +1 resolution/type errors detected in git-issue-3294.dfy diff --git a/Test/git-issues/git-issue-3513/git-issue-3513.dfy.expect b/Test/git-issues/git-issue-3513/git-issue-3513.dfy.expect index 835f91df72f..4cf1f2f7133 100644 --- a/Test/git-issues/git-issue-3513/git-issue-3513.dfy.expect +++ b/Test/git-issues/git-issue-3513/git-issue-3513.dfy.expect @@ -1,8 +1,7 @@ git-issue-3513.dfy(9,9): Error: module A does not exist 1 resolution/type errors detected in git-issue-3513.dfy -A.dfy(0,0): Error: the included file A.dfy contains error(s) A.dfy(4,9): Error: module B does not exist -2 resolution/type errors detected in the_program +1 resolution/type errors detected in the_program Dafny program verifier did not attempt verification diff --git a/Test/separate-verification/assumptions.dfy.expect b/Test/separate-verification/assumptions.dfy.expect index 85c5c7955bc..f79e372dfe2 100644 --- a/Test/separate-verification/assumptions.dfy.expect +++ b/Test/separate-verification/assumptions.dfy.expect @@ -8,7 +8,6 @@ TestAuditor.dfy(95,4): Warning: /!\ No terms found to trigger on. TestAuditor.dfy(126,2): Warning: /!\ No terms found to trigger on. Dafny program verifier did not attempt verification -assumptions.dfy(6,8): Error: the included file TestAuditor.dfy contains error(s) TestAuditor.dfy(89,27): Error: Trait method calls may not terminate (uses [{:termination false}]). TestAuditor.dfy(22,6): Error: Ghost declaration has no body and has an ensures clause. TestAuditor.dfy(27,15): Error: Ghost declaration has no body and has an ensures clause. @@ -28,6 +27,5 @@ TestAuditor.dfy(124,2): Error: Definition has [assume {:axiom}] statement in bod TestAuditor.dfy(126,2): Error: Definition contains [forall] statement with no body. TestAuditor.dfy(130,2): Error: Definition contains loop with no body. TestAuditor.dfy(137,2): Error: Assertion has explicit temporary [{:only}] attribute. -TestAuditor.dfy(11,8): Error: the included file IgnoredAssumptions.dfy contains error(s) IgnoredAssumptions.dfy(2,15): Error: Ghost declaration has no body and has an ensures clause. Wrote textual form of partial target program to assumptions-lib/assumptions.doo