Skip to content

Commit

Permalink
Parser cancellation (dafny-lang#4439)
Browse files Browse the repository at this point in the history 
### Changes
- Enable cancelling of parsing at the token granularity level, instead
of only at the file level
- Do not open file streams used for parsing until actually parsing

### Testing
We don't have a good way of automatically testing such a performance
change right now, but in one manual test run I saw runtime go down from
35 to 9s.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored Aug 19, 2023
1 parent cc43309 commit 83a2133
Show file tree
Hide file tree
Showing 10 changed files with 107 additions and 94 deletions.
148 changes: 73 additions & 75 deletions Source/DafnyCore/AST/Grammar/ProgramParser.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -49,6 +48,7 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
);

foreach (var dafnyFile in files) {
cancellationToken.ThrowIfCancellationRequested();
if (options.Trace) {
options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath);
}
Expand All @@ -57,35 +57,20 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> 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;
}
}

Expand Down Expand Up @@ -113,6 +98,41 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
return program;
}

private DfyParseResult ParseFileWithErrorHandling(DafnyOptions options,
Func<TextReader> 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<SystemModuleManager>[] { });
} 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<SystemModuleManager>[] { });
}
}

private void ShowWarningsForIncludeCycles(Program program) {
var graph = new Graph<Uri>();
foreach (var edgesForUri in program.Compilation.Includes.GroupBy(i => i.IncluderFilename)) {
Expand Down Expand Up @@ -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();
}
}

Expand All @@ -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}.");
Expand All @@ -247,25 +258,12 @@ private DafnyFile IncludeToDafnyFile(SystemModuleManager systemModuleManager, Er
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
protected virtual DfyParseResult ParseFile(DafnyOptions options, TextReader reader, Uri uri) /* throws System.IO.IOException */ {
protected virtual DfyParseResult ParseFile(DafnyOptions options, Func<TextReader> getReader,
Uri uri, CancellationToken cancellationToken) /* throws System.IO.IOException */ {
Contract.Requires(uri != null);
using var reader = getReader();
var text = SourcePreprocessor.ProcessDirectives(reader, new List<string>());
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<SystemModuleManager>[] { });
}
return ParseFile(options, text, uri, cancellationToken);
}

///<summary>
Expand All @@ -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.
///</summary>
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()
Expand All @@ -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);
Expand All @@ -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);
}
}
6 changes: 5 additions & 1 deletion Source/DafnyCore/Coco/Parser.frame
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -44,16 +45,18 @@ public class Parser {

public Scanner scanner;
public Errors errors;
CancellationToken cancellationToken;

public IToken t; // last recognized token
public IToken la; // lookahead token
int errDist = minErrDist;

-->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
}
Expand All @@ -72,6 +75,7 @@ public class Parser {
}

void Get() {
cancellationToken.ThrowIfCancellationRequested();
for (; ; ) {
var tmp = la;
la = scanner.Scan();
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Dafny.atg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
21 changes: 12 additions & 9 deletions Source/DafnyCore/DafnyFile.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
using System.Reflection.Metadata;
using System.Reflection.PortableExecutable;
using DafnyCore;
using JetBrains.Annotations;

namespace Microsoft.Dafny;

Expand All @@ -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<TextReader> 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<TextReader> getContentOverride = null) {
Uri = uri;
Origin = origin;
var filePath = uri.LocalPath;

var extension = ".dfy";
Expand All @@ -27,22 +30,22 @@ 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 = "<stdin>";
}

// Normalizing symbolic links appears to be not
// supported in .Net APIs, because it is very difficult in general
// So we will just use the absolute path, lowercased for all file systems.
// cf. IncludeComparer.CompareTo
CanonicalPath = contentOverride == null ? Canonicalize(filePath).LocalPath : "<stdin>";
CanonicalPath = getContentOverride == null ? Canonicalize(filePath).LocalPath : "<stdin>";
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;
Expand All @@ -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;
Expand All @@ -78,15 +81,15 @@ 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
IsPrecompiled = true;

var sourceText = GetDafnySourceAttributeText(filePath);
if (sourceText == null) { throw new IllegalDafnyFile(); }
Content = new StringReader(sourceText);
GetContent = () => new StringReader(sourceText);
} else {
throw new IllegalDafnyFile();
}
Expand Down
2 changes: 2 additions & 0 deletions Source/DafnyDriver/DafnyDoc.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,8 @@ public static DafnyDriver.ExitValue DoDocumenting(IReadOnlyList<DafnyFile> 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 => {
Expand Down
5 changes: 3 additions & 2 deletions Source/DafnyDriver/DafnyDriver.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -516,8 +516,9 @@ private static ExitValue DoFormatting(IReadOnlyList<DafnyFile> 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> { dafnyFile }, programName, options, out var dafnyProgram);
if (err != null) {
Expand Down
7 changes: 5 additions & 2 deletions Source/DafnyLanguageServer/Language/CachingParser.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,14 @@ public override Program ParseFiles(string programName, IReadOnlyList<DafnyFile>
telemetryPublisher, programName, "parsing");
}

protected override DfyParseResult ParseFile(DafnyOptions options, TextReader reader, Uri uri) {
protected override DfyParseResult ParseFile(DafnyOptions options, Func<TextReader> 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}");
Expand Down
Loading

0 comments on commit 83a2133

Please sign in to comment.