From ced23bae9ff106b20ac722e34a07b2f17a98c847 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 26 Jul 2023 18:51:30 +0200 Subject: [PATCH] Refactoring: simplify computing the priority of implementation tasks (#4311) Store a token for the name symbol when creating a Boogie Implementation, and use this to compute the priority of evaluating implementation tasks 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). --- Source/DafnyCore/AST/Tokens.cs | 15 +++++++----- .../Verifier/Translator.ClassMembers.cs | 6 ++--- Source/DafnyCore/Verifier/Translator.cs | 24 ++++++++++++------- .../Lookup/HoverVerificationTest.cs | 6 ++--- .../Language/BoogieExtensions.cs | 24 ++++++++++++++++--- .../Workspace/CompilationManager.cs | 6 ++--- .../Workspace/Documents/Compilation.cs | 3 ++- .../DafnyLanguageServer/Workspace/IdeState.cs | 3 ++- .../Workspace/ProjectManager.cs | 14 ++++------- 9 files changed, 64 insertions(+), 37 deletions(-) diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index 59bbf12aa35..a7abeced0ac 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -285,7 +285,7 @@ public override IToken WithVal(string newVal) { } public BoogieRangeToken ToToken() { - return new BoogieRangeToken(StartToken, EndToken); + return new BoogieRangeToken(StartToken, EndToken, null); } public bool Contains(int position) { @@ -300,15 +300,18 @@ public bool Intersects(RangeToken other) { public class BoogieRangeToken : TokenWrapper { // The wrapped token is the startTok - public IToken StartToken => WrappedToken; + public IToken StartToken { get; } public IToken EndToken { get; } + public IToken NameToken { get; } // Used for range reporting - public override string val => new string(' ', Math.Max(EndToken.pos + EndToken.val.Length - pos, 1)); + public override string val => new(' ', Math.Max(EndToken.pos + EndToken.val.Length - pos, 1)); - public BoogieRangeToken(IToken startTok, IToken endTok) : base( - startTok) { - this.EndToken = endTok; + public BoogieRangeToken(IToken startTok, IToken endTok, IToken nameToken) : base( + nameToken ?? startTok) { + StartToken = startTok; + EndToken = endTok; + NameToken = nameToken; } public override IToken WithVal(string newVal) { diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 1ae0a8154c5..991a1fe7a79 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -728,7 +728,7 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP if (EmitImplementation(m.Attributes)) { // emit impl only when there are proof obligations. QKeyValue kv = etran.TrAttributes(m.Attributes, null); - Boogie.Implementation impl = AddImplementationWithVerboseName(m.tok, proc, + Boogie.Implementation impl = AddImplementationWithVerboseName(GetToken(m), proc, inParams, outParams, localVariables, stmts, kv); if (InsertChecksums) { @@ -813,7 +813,7 @@ private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) { // emit the impl only when there are proof obligations. QKeyValue kv = etran.TrAttributes(m.Attributes, null); - Boogie.Implementation impl = AddImplementationWithVerboseName(m.tok, proc, inParams, outParams, localVariables, stmts, kv); + Boogie.Implementation impl = AddImplementationWithVerboseName(GetToken(m), proc, inParams, outParams, localVariables, stmts, kv); if (InsertChecksums) { InsertChecksum(m, impl); @@ -969,7 +969,7 @@ private void AddFunctionOverrideCheckImpl(Function f) { // emit the impl only when there are proof obligations. QKeyValue kv = etran.TrAttributes(f.Attributes, null); - AddImplementationWithVerboseName(f.tok, proc, + AddImplementationWithVerboseName(GetToken(f), proc, Util.Concat(Util.Concat(typeInParams, inParams_Heap), implInParams), implOutParams, localVariables, stmts, kv); } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 7ccd19b54ac..71a64eaf5c5 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -1773,7 +1773,7 @@ void AddWellformednessCheck(IteratorDecl iter, Procedure proc) { if (EmitImplementation(iter.Attributes)) { QKeyValue kv = etran.TrAttributes(iter.Attributes, null); - AddImplementationWithVerboseName(iter.tok, proc, inParams, new List(), + AddImplementationWithVerboseName(GetToken(iter), proc, inParams, new List(), localVariables, stmts, kv); } @@ -1855,7 +1855,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { // emit the impl only when there are proof obligations. QKeyValue kv = etran.TrAttributes(iter.Attributes, null); - AddImplementationWithVerboseName(iter.tok, proc, inParams, + AddImplementationWithVerboseName(GetToken(iter), proc, inParams, new List(), localVariables, stmts, kv); } @@ -3405,8 +3405,16 @@ void MarkDefiniteAssignmentTracker(IToken tok, string name, BoogieStmtListBuilde } } - internal IToken GetToken(Node node) { - return flags.ReportRanges ? node.RangeToken.ToToken() : node.Tok; + internal IToken GetToken(INode node) { + if (flags.ReportRanges) { + // Filter against IHasUsages to only select declarations, not usages. + if (node is IDeclarationOrUsage declarationOrUsage && node is not IHasUsages) { + return new BoogieRangeToken(node.RangeToken.StartToken, node.RangeToken.EndToken, declarationOrUsage.NameToken); + } + return node.RangeToken.ToToken(); + } else { + return node.Tok; + } } void CheckDefiniteAssignment(IdentifierExpr expr, BoogieStmtListBuilder builder) { @@ -4449,7 +4457,7 @@ void AddWellformednessCheck(Function f) { if (EmitImplementation(f.Attributes)) { // emit the impl only when there are proof obligations. QKeyValue kv = etran.TrAttributes(f.Attributes, null); - var impl = AddImplementationWithVerboseName(f.tok, proc, + var impl = AddImplementationWithVerboseName(GetToken(f), proc, Concat(Concat(Bpl.Formal.StripWhereClauses(typeInParams), inParams_Heap), implInParams), implOutParams, locals, implBody, kv); @@ -4601,7 +4609,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { // emit the impl only when there are proof obligations. QKeyValue kv = etran.TrAttributes(decl.Attributes, null); - AddImplementationWithVerboseName(decl.tok, proc, implInParams, new List(), locals, implBody, kv); + AddImplementationWithVerboseName(GetToken(decl), proc, implInParams, new List(), locals, implBody, kv); } // TODO: Should a checksum be inserted here? @@ -4680,7 +4688,7 @@ void AddWellformednessCheck(ConstantField decl) { QKeyValue kv = etran.TrAttributes(decl.Attributes, null); var implBody = builder.Collect(decl.tok); - AddImplementationWithVerboseName(decl.tok, proc, implInParams, + AddImplementationWithVerboseName(GetToken(decl), proc, implInParams, new List(), locals, implBody, kv); } @@ -4753,7 +4761,7 @@ void AddWellformednessCheck(DatatypeCtor ctor) { // emit the impl only when there are proof obligations. QKeyValue kv = etran.TrAttributes(ctor.Attributes, null); var implBody = builder.Collect(ctor.tok); - AddImplementationWithVerboseName(ctor.tok, proc, implInParams, + AddImplementationWithVerboseName(GetToken(ctor), proc, implInParams, new List(), locals, implBody, kv); } diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 85ebcf17e07..559647b0b0a 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -333,7 +333,7 @@ await AssertHoverMatches(documentItem, (10, 16), ); } - [Fact(Timeout = MaxTestExecutionTimeMs)] + [Fact] public async Task DoNotExtendPastExpressions() { var documentItem = await GetDocumentItem(@" datatype Test = Test(i: int) @@ -357,9 +357,9 @@ await AssertHoverMatches(documentItem, (9, 20), Could not prove: `i > 0` " ); await AssertHoverMatches(documentItem, (10, 20), - @"**Error:**???assertion might not hold??? + @"**Error:**???assertion might not hold??? Could not prove: `i > 1` " - ); + ); await AssertHoverMatches(documentItem, (10, 20), @"**Success:**???function precondition satisfied??? Inside `Valid()` diff --git a/Source/DafnyLanguageServer/Language/BoogieExtensions.cs b/Source/DafnyLanguageServer/Language/BoogieExtensions.cs index 451d5296ff1..884f97a4f00 100644 --- a/Source/DafnyLanguageServer/Language/BoogieExtensions.cs +++ b/Source/DafnyLanguageServer/Language/BoogieExtensions.cs @@ -38,15 +38,33 @@ public static Range ToLspRange(this RangeToken range) { /// The token to get the range of. /// An optional other token to get the end of the range of. /// The LSP range of the token. - public static Range GetLspRange(this Boogie.IToken startToken, Boogie.IToken? endToken = null) { - endToken ??= startToken; - endToken = endToken is BoogieRangeToken rangeToken ? rangeToken.EndToken : endToken; + public static Range GetLspRange(this IToken startToken, IToken endToken) { + return GetLspRangeGeneric(startToken, endToken); + } + + private static Range GetLspRangeGeneric(this Boogie.IToken startToken, Boogie.IToken endToken) { return new Range( GetLspPosition(startToken), ToLspPosition(endToken.line, endToken.col + endToken.val.Length) ); } + /// + /// Gets the LSP range of the specified token. + /// + /// The token to get the range of. + /// An optional other token to get the end of the range of. + /// The LSP range of the token. + public static Range GetLspRange(this Boogie.IToken startToken, bool nameRange = false) { + if (startToken is BoogieRangeToken boogieRangeToken) { + return nameRange + ? (boogieRangeToken.NameToken ?? boogieRangeToken.StartToken).GetLspRange() + : GetLspRangeGeneric(boogieRangeToken.StartToken, boogieRangeToken.EndToken); + } + var endToken = startToken; + return GetLspRangeGeneric(startToken, endToken); + } + public static Position GetLspPosition(this DafnyPosition position) { return new Position(position.Line, position.Column); } diff --git a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs index 5916faed850..3e50266e2fb 100644 --- a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs +++ b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs @@ -161,11 +161,11 @@ public async Task PrepareVerificationTasksAsync( var implementationId = GetImplementationId(task.Implementation); try { if (task.CacheStatus is Completed completed) { - var view = new ImplementationView(task.Implementation.tok.GetLspRange(), status, + var view = new ImplementationView(task.Implementation.tok.GetLspRange(true), status, GetDiagnosticsFromResult(loaded, completed.Result).ToList()); initialViews.Add(implementationId, view); } else { - var view = new ImplementationView(task.Implementation.tok.GetLspRange(), status, Array.Empty()); + var view = new ImplementationView(task.Implementation.tok.GetLspRange(true), status, Array.Empty()); initialViews.Add(implementationId, view); } } catch (ArgumentException) { @@ -271,7 +271,7 @@ public void FinishedNotifications(CompilationAfterTranslation compilation) { private void HandleStatusUpdate(CompilationAfterTranslation compilation, IImplementationTask implementationTask, IVerificationStatus boogieStatus) { var id = GetImplementationId(implementationTask.Implementation); var status = StatusFromBoogieStatus(boogieStatus); - var implementationRange = implementationTask.Implementation.tok.GetLspRange(); + var implementationRange = implementationTask.Implementation.tok.GetLspRange(true); logger.LogDebug($"Received status {boogieStatus} for {implementationTask.Implementation.Name}, version {compilation.Counterexamples}"); if (boogieStatus is Running) { verificationProgressReporter.ReportVerifyImplementationRunning(compilation, implementationTask.Implementation); diff --git a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs index a5290a24040..cce8604b937 100644 --- a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs +++ b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs @@ -56,7 +56,8 @@ public virtual IdeState ToIdeState(IdeState previousState) { } } - public record ImplementationView(Range Range, PublishedVerificationStatus Status, IReadOnlyList Diagnostics); + public record ImplementationView(Range Range, PublishedVerificationStatus Status, + IReadOnlyList Diagnostics); public record BufferLine(int LineNumber, int StartIndex, int EndIndex); } diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 52f64f033e3..c63dbb54deb 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -13,7 +13,8 @@ namespace Microsoft.Dafny.LanguageServer.Workspace; -public record IdeImplementationView(Range Range, PublishedVerificationStatus Status, IReadOnlyList Diagnostics); +public record IdeImplementationView(Range Range, PublishedVerificationStatus Status, + IReadOnlyList Diagnostics); /// /// Contains information from the latest document, and from older documents if some information is missing, diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs index ee6a7217c7a..e4a01c9b5ea 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs @@ -285,18 +285,14 @@ private async Task VerifyEverythingAsync(Uri? uri) { } private IEnumerable GetChangedVerifiablesFromRanges(CompilationAfterTranslation translated, IEnumerable changedRanges) { - IntervalTree GetTree(Uri uri) { - // Refactor: use the translated Boogie program - // instead of redoing part of that translation with the `DocumentVerificationTree` - // https://github.com/dafny-lang/dafny/issues/4264 - var tree = new DocumentVerificationTree(translated.Program, uri); - VerificationProgressReporter.UpdateTree(options, translated, tree); var intervalTree = new IntervalTree(); - foreach (var childTree in tree.Children) { - intervalTree.Add(childTree.Range.Start, childTree.Range.End, childTree.Position); + foreach (var task in translated.VerificationTasks) { + var token = (BoogieRangeToken)task.Implementation.tok; + if (token.Uri == uri) { + intervalTree.Add(token.StartToken.GetLspPosition(), token.EndToken.GetLspPosition(), token.NameToken.GetLspPosition()); + } } - return intervalTree; }