diff --git a/Source/DafnyCore/AST/Grammar/ProgramParser.cs b/Source/DafnyCore/AST/Grammar/ProgramParser.cs index 4c9b394a017..f4e020e43b1 100644 --- a/Source/DafnyCore/AST/Grammar/ProgramParser.cs +++ b/Source/DafnyCore/AST/Grammar/ProgramParser.cs @@ -5,7 +5,6 @@ using System.Linq; using System.Text; using System.Threading; -using Microsoft.CodeAnalysis; using Microsoft.Extensions.Logging; using Microsoft.Extensions.Logging.Abstractions; using static Microsoft.Dafny.ParseErrors; @@ -49,6 +48,7 @@ public virtual Program ParseFiles(string programName, IReadOnlyList f ); foreach (var dafnyFile in files) { + cancellationToken.ThrowIfCancellationRequested(); if (options.Trace) { options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath); } @@ -57,35 +57,20 @@ public virtual Program ParseFiles(string programName, IReadOnlyList f options.XmlSink.WriteFileFragment(dafnyFile.Uri.LocalPath); } - try { - var parseResult = ParseFile( - options, - dafnyFile.Content, - dafnyFile.Uri - ); - if (parseResult.ErrorReporter.ErrorCount != 0) { - logger.LogDebug($"encountered {parseResult.ErrorReporter.ErrorCount} errors while parsing {dafnyFile.Uri}"); - } - - AddParseResultToProgram(parseResult, program); - if (defaultModule.RangeToken.StartToken.Uri == null) { - defaultModule.RangeToken = parseResult.Module.RangeToken; - } - - } catch (Exception e) { - logger.LogDebug(e, $"encountered an exception while parsing {dafnyFile.Uri}"); - 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); + var parseResult = ParseFileWithErrorHandling( + errorReporter.Options, + dafnyFile.GetContent, + dafnyFile.Origin, + dafnyFile.Uri, + cancellationToken + ); + if (parseResult.ErrorReporter.ErrorCount != 0) { + logger.LogDebug($"encountered {parseResult.ErrorReporter.ErrorCount} errors while parsing {dafnyFile.Uri}"); } - finally { - dafnyFile.Content.Close(); + + AddParseResultToProgram(parseResult, program); + if (defaultModule.RangeToken.StartToken.Uri == null) { + defaultModule.RangeToken = parseResult.Module.RangeToken; } } @@ -113,6 +98,41 @@ public virtual Program ParseFiles(string programName, IReadOnlyList f return program; } + private DfyParseResult ParseFileWithErrorHandling(DafnyOptions options, + Func getContent, + IToken origin, + Uri uri, + CancellationToken cancellationToken) { + try { + return ParseFile(options, getContent, uri, cancellationToken); + } catch (IOException e) { + if (origin == null) { + throw; + } + + var reporter = new BatchErrorReporter(options); + reporter.Error(MessageSource.Parser, origin, + $"Unable to open the file {uri} because {e.Message}."); + return new DfyParseResult(reporter, new FileModuleDefinition(Token.NoToken), new Action[] { }); + } catch (OperationCanceledException) { + throw; + } 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, ErrorId.p_internal_exception, internalErrorDummyToken, + "[internal error] Parser exception: " + e.Message + (!options.Verbose ? "" : + "\n" + e.StackTrace)); + return new DfyParseResult(reporter, new FileModuleDefinition(Token.NoToken), new Action[] { }); + } + } + private void ShowWarningsForIncludeCycles(Program program) { var graph = new Graph(); foreach (var edgesForUri in program.Compilation.Includes.GroupBy(i => i.IncluderFilename)) { @@ -201,25 +221,20 @@ CancellationToken cancellationToken } cancellationToken.ThrowIfCancellationRequested(); - try { - var parseIncludeResult = ParseFile( - errorReporter.Options, - top.Content, - top.Uri - ); - result.Add(parseIncludeResult); - - foreach (var include in parseIncludeResult.Module.Includes) { - var dafnyFile = IncludeToDafnyFile(systemModuleManager, errorReporter, include); - if (dafnyFile != null) { - stack.Push(dafnyFile); - } + var parseIncludeResult = ParseFileWithErrorHandling( + errorReporter.Options, + top.GetContent, + top.Origin, + top.Uri, + cancellationToken + ); + result.Add(parseIncludeResult); + + foreach (var include in parseIncludeResult.Module.Includes) { + var dafnyFile = IncludeToDafnyFile(systemModuleManager, errorReporter, include); + if (dafnyFile != null) { + stack.Push(dafnyFile); } - } catch (Exception) { - // ignored - } - finally { - top.Content.Close(); } } @@ -228,12 +243,8 @@ CancellationToken cancellationToken private DafnyFile IncludeToDafnyFile(SystemModuleManager systemModuleManager, ErrorReporter errorReporter, Include include) { try { - return new DafnyFile(systemModuleManager.Options, include.IncludedFilename, - fileSystem.ReadFile(include.IncludedFilename)); - } catch (IOException e) { - errorReporter.Error(MessageSource.Parser, include.tok, - $"Unable to open the include {include.IncludedFilename} because {e.Message}."); - return null; + return new DafnyFile(systemModuleManager.Options, include.IncludedFilename, include.tok, + () => fileSystem.ReadFile(include.IncludedFilename)); } catch (IllegalDafnyFile) { errorReporter.Error(MessageSource.Parser, include.tok, $"Unable to open the include {include.IncludedFilename}."); @@ -247,25 +258,12 @@ private DafnyFile IncludeToDafnyFile(SystemModuleManager systemModuleManager, Er /// Returns the number of parsing errors encountered. /// Note: first initialize the Scanner. /// - protected virtual DfyParseResult ParseFile(DafnyOptions options, TextReader reader, Uri uri) /* throws System.IO.IOException */ { + protected virtual DfyParseResult ParseFile(DafnyOptions options, Func getReader, + Uri uri, CancellationToken cancellationToken) /* throws System.IO.IOException */ { Contract.Requires(uri != null); + using var reader = getReader(); 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, ErrorId.p_internal_exception, internalErrorDummyToken, - "[internal error] Parser exception: " + e.Message + (!options.Verbose ? "" : - "\n" + e.StackTrace)); - return new DfyParseResult(reporter, null, new Action[] { }); - } + return ParseFile(options, text, uri, cancellationToken); } /// @@ -274,9 +272,9 @@ protected virtual DfyParseResult ParseFile(DafnyOptions options, TextReader read /// 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) { + private static DfyParseResult ParseFile(DafnyOptions options, string /*!*/ s, Uri /*!*/ uri, CancellationToken cancellationToken) { var batchErrorReporter = new BatchErrorReporter(options); - Parser parser = SetupParser(s, uri, batchErrorReporter); + Parser parser = SetupParser(s, uri, batchErrorReporter, cancellationToken); parser.Parse(); if (parser.theModule.DefaultClass.Members.Count == 0 && parser.theModule.Includes.Count == 0 && !parser.theModule.SourceDecls.Any() @@ -287,7 +285,7 @@ private static DfyParseResult ParseFile(DafnyOptions options, string /*!*/ s, Ur return new DfyParseResult(batchErrorReporter, parser.theModule, parser.SystemModuleModifiers); } - private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, ErrorReporter /*!*/ errorReporter) { + private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, ErrorReporter /*!*/ errorReporter, CancellationToken cancellationToken) { Contract.Requires(s != null); Contract.Requires(uri != null); System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle); @@ -301,11 +299,11 @@ private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, ErrorReporter / var errors = new Errors(errorReporter); var scanner = new Scanner(ms, errors, uri, firstToken: firstToken); - return new Parser(errorReporter.Options, scanner, errors); + return new Parser(errorReporter.Options, scanner, errors, cancellationToken); } public Program Parse(string source, Uri uri, ErrorReporter reporter) { - var files = new[] { new DafnyFile(reporter.Options, uri, new StringReader(source)) }; + var files = new[] { new DafnyFile(reporter.Options, uri, null, () => new StringReader(source)) }; return ParseFiles(uri.ToString(), files, reporter, CancellationToken.None); } } diff --git a/Source/DafnyCore/Coco/Parser.frame b/Source/DafnyCore/Coco/Parser.frame index 5aec38bbfdd..7c79e92b395 100644 --- a/Source/DafnyCore/Coco/Parser.frame +++ b/Source/DafnyCore/Coco/Parser.frame @@ -33,6 +33,7 @@ Coco/R itself) does not fall under the GNU General Public License. using System; using System.Diagnostics.Contracts; +using System.Threading; -->namespace @@ -44,6 +45,7 @@ public class Parser { public Scanner scanner; public Errors errors; + CancellationToken cancellationToken; public IToken t; // last recognized token public IToken la; // lookahead token @@ -51,9 +53,10 @@ public class Parser { -->declarations - public Parser(Scanner scanner, Errors errors) { + public Parser(Scanner scanner, Errors errors, CancellationToken cancellationToken) { this.scanner = scanner; this.errors = errors; + this.cancellationToken = cancellationToken; this.la = scanner.FirstToken; this.t = scanner.FirstToken; // just to satisfy its non-null constraint } @@ -72,6 +75,7 @@ public class Parser { } void Get() { + cancellationToken.ThrowIfCancellationRequested(); for (; ; ) { var tmp = la; la = scanner.Scan(); diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index ee0f32311d1..c24d3c90996 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -178,8 +178,8 @@ public void ApplyOptionsFromAttributes(Attributes attrs) { } } -public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors) - : this(scanner, errors) // the real work +public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, CancellationToken cancellationToken) + : this(scanner, errors, cancellationToken) // the real work { // initialize readonly fields dummyExpr = new LiteralExpr(Token.NoToken); diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index cabba34701e..47800c4ae4d 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -5,6 +5,7 @@ using System.Reflection.Metadata; using System.Reflection.PortableExecutable; using DafnyCore; +using JetBrains.Annotations; namespace Microsoft.Dafny; @@ -14,11 +15,13 @@ public class DafnyFile { public string BaseName { get; private set; } public bool IsPreverified { get; set; } public bool IsPrecompiled { get; set; } - public TextReader Content { get; set; } + public Func GetContent { get; set; } public Uri Uri { get; } + [CanBeNull] public IToken Origin { get; } - public DafnyFile(DafnyOptions options, Uri uri, TextReader contentOverride = null) { + public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null, Func getContentOverride = null) { Uri = uri; + Origin = origin; var filePath = uri.LocalPath; var extension = ".dfy"; @@ -27,7 +30,7 @@ public DafnyFile(DafnyOptions options, Uri uri, TextReader contentOverride = nul BaseName = Path.GetFileName(uri.LocalPath); } if (uri.Scheme == "stdin") { - contentOverride = options.Input; + getContentOverride = () => options.Input; BaseName = ""; } @@ -35,14 +38,14 @@ public DafnyFile(DafnyOptions options, Uri uri, TextReader contentOverride = nul // 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 = contentOverride == null ? Canonicalize(filePath).LocalPath : ""; + CanonicalPath = getContentOverride == null ? Canonicalize(filePath).LocalPath : ""; FilePath = CanonicalPath; var filePathForErrors = options.UseBaseNameForFileName ? Path.GetFileName(filePath) : filePath; - if (contentOverride != null) { + if (getContentOverride != null) { IsPreverified = false; IsPrecompiled = false; - Content = contentOverride; + GetContent = getContentOverride; } else if (extension == ".dfy" || extension == ".dfyi") { IsPreverified = false; IsPrecompiled = false; @@ -57,7 +60,7 @@ public DafnyFile(DafnyOptions options, Uri uri, TextReader contentOverride = nul options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: file {filePathForErrors} not found"); throw new IllegalDafnyFile(true); } else { - Content = new StreamReader(filePath); + GetContent = () => new StreamReader(filePath); } } else if (extension == ".doo") { IsPreverified = true; @@ -78,7 +81,7 @@ public DafnyFile(DafnyOptions options, Uri uri, TextReader contentOverride = nul // 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. - Content = new StringReader(dooFile.ProgramText); + GetContent = () => new StringReader(dooFile.ProgramText); } else if (extension == ".dll") { IsPreverified = true; // Technically only for C#, this is for backwards compatability @@ -86,7 +89,7 @@ public DafnyFile(DafnyOptions options, Uri uri, TextReader contentOverride = nul var sourceText = GetDafnySourceAttributeText(filePath); if (sourceText == null) { throw new IllegalDafnyFile(); } - Content = new StringReader(sourceText); + GetContent = () => new StringReader(sourceText); } else { throw new IllegalDafnyFile(); } diff --git a/Source/DafnyDriver/DafnyDoc.cs b/Source/DafnyDriver/DafnyDoc.cs index 2632b14102f..443b9272e9b 100644 --- a/Source/DafnyDriver/DafnyDoc.cs +++ b/Source/DafnyDriver/DafnyDoc.cs @@ -50,6 +50,8 @@ public static DafnyDriver.ExitValue DoDocumenting(IReadOnlyList dafny outputdir = DefaultOutputDir; } + + // Collect all the dafny files; dafnyFiles already includes files from a .toml project file var exitValue = DafnyDriver.ExitValue.SUCCESS; dafnyFiles = dafnyFiles.Concat(dafnyFolders.SelectMany(folderPath => { diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 6f9b161221a..08161641ba2 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -516,8 +516,9 @@ private static ExitValue DoFormatting(IReadOnlyList dafnyFiles, Dafny dafnyFile = new DafnyFile(options, new Uri(tempFileName)); } - var originalText = dafnyFile.Content.ReadToEnd(); - dafnyFile.Content = new StringReader(originalText); + using var content = dafnyFile.GetContent(); + var originalText = content.ReadToEnd(); + dafnyFile.GetContent = () => new StringReader(originalText); // Might not be totally optimized but let's do that for now var err = DafnyMain.Parse(new List { dafnyFile }, programName, options, out var dafnyProgram); if (err != null) { diff --git a/Source/DafnyLanguageServer/Language/CachingParser.cs b/Source/DafnyLanguageServer/Language/CachingParser.cs index 7322a37d3e6..d89aa103164 100644 --- a/Source/DafnyLanguageServer/Language/CachingParser.cs +++ b/Source/DafnyLanguageServer/Language/CachingParser.cs @@ -26,11 +26,14 @@ public override Program ParseFiles(string programName, IReadOnlyList telemetryPublisher, programName, "parsing"); } - protected override DfyParseResult ParseFile(DafnyOptions options, TextReader reader, Uri uri) { + protected override DfyParseResult ParseFile(DafnyOptions options, Func getReader, + Uri uri, CancellationToken cancellationToken) { + + using var reader = getReader(); var (newReader, hash) = ComputeHashFromReader(uri, reader, HashAlgorithm.Create("SHA256")!); if (!parseCache.TryGet(hash, out var result)) { logger.LogDebug($"Parse cache miss for {uri}"); - result = base.ParseFile(options, newReader, uri); + result = base.ParseFile(options, () => newReader, uri, cancellationToken); parseCache.Set(hash, result); } else { logger.LogDebug($"Parse cache hit for {uri}"); diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index d88a29a0d11..822a543d475 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -1,9 +1,11 @@ using Microsoft.Extensions.Logging; using System; using System.Collections.Generic; +using System.Diagnostics; using System.IO; using System.Linq; using System.Threading; +using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.Workspace; namespace Microsoft.Dafny.LanguageServer.Language { @@ -43,7 +45,7 @@ public Program Parse(Compilation compilation, ErrorReporter reporter, Cancellati List dafnyFiles = new(); foreach (var rootSourceUri in rootSourceUris) { try { - dafnyFiles.Add(new DafnyFile(reporter.Options, rootSourceUri, fileSystem.ReadFile(rootSourceUri))); + dafnyFiles.Add(new DafnyFile(reporter.Options, rootSourceUri, null, () => fileSystem.ReadFile(rootSourceUri))); if (logger.IsEnabled(LogLevel.Trace)) { logger.LogTrace($"Parsing file with uri {rootSourceUri} and content\n{fileSystem.ReadFile(rootSourceUri).ReadToEnd()}"); } diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 41ef045c000..c8e8e26e492 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -44,7 +44,7 @@ public bool Verify() { private bool Parse() { var uri = new Uri("transcript:///" + fname); reporter = new ConsoleErrorReporter(options); - var program = new ProgramParser().ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, + var program = new ProgramParser().ParseFiles(fname, new DafnyFile[] { new(reporter.Options, uri, null, () => new StringReader(source)) }, reporter, CancellationToken.None); var success = reporter.ErrorCount == 0; diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 2f6978bd899..13fa0d7da79 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -86,7 +86,7 @@ public static Type CopyWithReplacements(Type type, List from, List uri ??= new Uri(Path.Combine(Path.GetTempPath(), Path.GetRandomFileName())); var reporter = new BatchErrorReporter(options); - var program = new ProgramParser().ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri, new StringReader(source)) }, + var program = new ProgramParser().ParseFiles(uri.LocalPath, new DafnyFile[] { new(reporter.Options, uri, null, () => new StringReader(source)) }, reporter, CancellationToken.None); if (!resolve) {