Refactoring: simplify computing the priority of implementation tasks (d…

…afny-lang#4311) Store a token for the name symbol when creating a Boogie Implementation, and use this to compute the priority of evaluating implementation tasks <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>
RustanLeino · Jul 26, 2023 · ced23ba · ced23ba
1 parent 59ce520
commit ced23ba
Show file tree

Hide file tree

Showing 9 changed files with 64 additions and 37 deletions.
diff --git 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
@@ -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
@@ -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<Variable>(),
+        AddImplementationWithVerboseName(GetToken(iter), proc, inParams, new List<Variable>(),
           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<Variable>(), 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<Variable>(), locals, implBody, kv);
+        AddImplementationWithVerboseName(GetToken(decl), proc, implInParams, new List<Variable>(), 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<Variable>(), 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<Variable>(), locals, implBody, kv);
       }
 

diff --git 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
@@ -38,15 +38,33 @@ public static Range ToLspRange(this RangeToken range) {
     /// <param name="startToken">The token to get the range of.</param>
     /// <param name="endToken">An optional other token to get the end of the range of.</param>
     /// <returns>The LSP range of the token.</returns>
-    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)
       );
     }
 
+    /// <summary>
+    /// Gets the LSP range of the specified token.
+    /// </summary>
+    /// <param name="startToken">The token to get the range of.</param>
+    /// <param name="endToken">An optional other token to get the end of the range of.</param>
+    /// <returns>The LSP range of the token.</returns>
+    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
@@ -161,11 +161,11 @@ public async Task<CompilationAfterTranslation> 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<DafnyDiagnostic>());
+          var view = new ImplementationView(task.Implementation.tok.GetLspRange(true), status, Array.Empty<DafnyDiagnostic>());
           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
@@ -56,7 +56,8 @@ public virtual IdeState ToIdeState(IdeState previousState) {
     }
   }
 
-  public record ImplementationView(Range Range, PublishedVerificationStatus Status, IReadOnlyList<DafnyDiagnostic> Diagnostics);
+  public record ImplementationView(Range Range, PublishedVerificationStatus Status,
+    IReadOnlyList<DafnyDiagnostic> Diagnostics);
 
   public record BufferLine(int LineNumber, int StartIndex, int EndIndex);
 }
diff --git 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<Diagnostic> Diagnostics);
+public record IdeImplementationView(Range Range, PublishedVerificationStatus Status,
+  IReadOnlyList<Diagnostic> Diagnostics);
 
 /// <summary>
 /// 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
@@ -285,18 +285,14 @@ private async Task VerifyEverythingAsync(Uri? uri) {
   }
 
   private IEnumerable<FilePosition> GetChangedVerifiablesFromRanges(CompilationAfterTranslation translated, IEnumerable<Location> changedRanges) {
-
     IntervalTree<Position, Position> 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<Position, Position>();
-      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;
     }