Merge branch 'master' into fix-issue-5554-soundness

Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs

@@ -0,0 +1,76 @@
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using OmniSharp.Extensions.LanguageServer.Protocol.Document;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using System.Collections.Generic;
+using System.Linq;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Completion {
+  public class AtCompletionTest : ClientBasedLanguageServerTest {
+
+    private async Task<List<CompletionItem>> RequestCompletionAsync(TextDocumentItem documentItem, Position position) {
+      var completionList = await client.RequestCompletion(
+        new CompletionParams {
+          TextDocument = documentItem.Uri,
+          Position = position
+        },
+        CancellationToken
+      ).AsTask();
+      return completionList.OrderBy(completion => completion.Label).ToList();
+    }
+
+    [Fact]
+    public async Task CompleteNoAtAttributeDuringAtCall() {
+      var source = @"
+method Foo() { label start: previous@(x); }".TrimStart();
+      var documentItem = CreateAndOpenTestDocument(source, "CompleteAtCall.dfy");
+
+      var completionList = await RequestCompletionAsync(documentItem, (0, 37));
+      Assert.Empty(completionList);
+    }
+
+    private static void AssertEqualToAllCompletions(List<CompletionItem> completionList) {
+      Assert.Equal(Attributes.BuiltinAtAttributes.Count, completionList.Count);
+      for (var i = 0; i < completionList.Count; i++) {
+        Assert.Equal(Attributes.BuiltinAtAttributes[0].Name, completionList[0].Label);
+        Assert.Equal(CompletionItemKind.Constructor, completionList[1].Kind);
+      }
+    }
+
+    [Fact]
+    public async Task CompleteAtAttributeAtBeginningOfFile() {
+      var source = "@";
+      var documentItem = CreateTestDocument(source, "CompleteAt.dfy");
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var completionList = await RequestCompletionAsync(documentItem, (0, 1));
+      AssertEqualToAllCompletions(completionList);
+    }
+
+    [Fact]
+    public async Task CompleteAtAttributeBeforeMethod() {
+      var source = @"
+/* Does what is expected */ @ method Foo() { }".TrimStart();
+      var documentItem = CreateTestDocument(source, "CompleteAtBeforeMethod.dfy");
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var completionList = await RequestCompletionAsync(documentItem, (0, 29));
+      AssertEqualToAllCompletions(completionList);
+    }
+
+    [Fact]
+    public async Task CompleteAtAttributeBeforeMethodAfterNewline() {
+      var source = @"
+/* Does what is expected */".TrimStart() + "\n" +
+"@ method Foo() { }".TrimStart();
+      var documentItem = CreateTestDocument(source, "CompleteOnThisReturnsClassMembers.dfy");
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var completionList = await RequestCompletionAsync(documentItem, (1, 1));
+      AssertEqualToAllCompletions(completionList);
+    }
+
+    public AtCompletionTest(ITestOutputHelper output) : base(output) {
+    }
+  }
+}

Source/DafnyLanguageServer.Test/Synchronization/EditDocumentTest.cs

@@ -223,7 +223,8 @@ await SetUp(dafnyOptions => {
     var buffer = new TextBuffer("");
     foreach (var midPart in sourceParts) {
       for (var midIndex = 0; midIndex < midPart.Length; midIndex += stepSize) {
-        var part = midPart.Substring(midIndex, Math.Min(midPart.Length, midIndex + stepSize) - midIndex);
+        var length = Math.Min(midPart.Length, midIndex + stepSize) - midIndex;
+        var part = midPart.Substring(midIndex, length);
         var cursorIndex = index + part.Length;
 
         var position = buffer.FromIndex(index);
@@ -234,8 +235,9 @@ await SetUp(dafnyOptions => {
         ApplyChange(ref document, new Range(position, position), part);
 
         await WaitUntilResolutionFinished(document);
-        var completionItems = await RequestCompletionAsync(document, new Position(0, midIndex + stepSize));
-        var hover = await RequestHover(document, new Position(0, midIndex + stepSize));
+        var position2 = buffer.FromIndex(midIndex + length);
+        var completionItems = await RequestCompletionAsync(document, position2);
+        var hover = await RequestHover(document, position2);
         index = cursorIndex;
       }
     }

Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs

@@ -44,15 +44,6 @@ private static VersionedTextDocumentIdentifier CreateTestDocumentId() {
       };
     }
 
-    private static DocumentTextBuffer CreateTestDocument() {
-      return new DocumentTextBuffer(new TextDocumentItem() {
-        Uri = DocumentUri.Parse("untitled:untitled1"),
-        LanguageId = "dafny",
-        Version = 1,
-        Text = ""
-      });
-    }
-
     [Fact]
     public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
       var source = new CancellationTokenSource();

Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs

@@ -12,27 +12,30 @@
 using System.Linq;
 using System.Threading;
 using System.Threading.Tasks;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
 namespace Microsoft.Dafny.LanguageServer.Handlers {
   public class DafnyCompletionHandler : CompletionHandlerBase {
     private readonly ILogger<DafnyCompletionHandler> logger;
     private readonly IProjectDatabase projects;
+    private readonly LanguageServerFilesystem filesystem;
     private readonly ISymbolGuesser symbolGuesser;
     private DafnyOptions options;
 
     public DafnyCompletionHandler(ILogger<DafnyCompletionHandler> logger, IProjectDatabase projects,
-      ISymbolGuesser symbolGuesser, DafnyOptions options) {
+      ISymbolGuesser symbolGuesser, DafnyOptions options, LanguageServerFilesystem filesystem) {
       this.logger = logger;
       this.projects = projects;
       this.symbolGuesser = symbolGuesser;
       this.options = options;
+      this.filesystem = filesystem;
     }
 
     protected override CompletionRegistrationOptions CreateRegistrationOptions(CompletionCapability capability, ClientCapabilities clientCapabilities) {
       return new CompletionRegistrationOptions {
         DocumentSelector = DocumentSelector.ForLanguage("dafny"),
         ResolveProvider = false,
-        TriggerCharacters = new Container<string>(".")
+        TriggerCharacters = new Container<string>(".", "@")
       };
     }
 
@@ -49,7 +52,7 @@ public override async Task<CompletionList> Handle(CompletionParams request, Canc
         logger.LogWarning("location requested for unloaded document {DocumentUri}", request.TextDocument.Uri);
         return new CompletionList();
       }
-      return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options).Process();
+      return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options, filesystem).Process();
     }
 
     private class CompletionProcessor {
@@ -59,22 +62,29 @@ private class CompletionProcessor {
       private readonly IdeState state;
       private readonly CompletionParams request;
       private readonly CancellationToken cancellationToken;
+      private readonly LanguageServerFilesystem filesystem;
 
       public CompletionProcessor(ISymbolGuesser symbolGuesser, ILogger<DafnyCompletionHandler> logger, IdeState state,
-        CompletionParams request, CancellationToken cancellationToken, DafnyOptions options) {
+        CompletionParams request, CancellationToken cancellationToken, DafnyOptions options,
+        LanguageServerFilesystem filesystem) {
         this.symbolGuesser = symbolGuesser;
         this.state = state;
         this.request = request;
         this.cancellationToken = cancellationToken;
         this.options = options;
         this.logger = logger;
+        this.filesystem = filesystem;
       }
 
       public CompletionList Process() {
         if (IsDotExpression()) {
           return CreateDotCompletionList();
         }
 
+        if (IsAtAttribute()) {
+          return CreateAtAttributeCompletionList();
+        }
+
         if (logger.IsEnabled(LogLevel.Trace)) {
           var program = (Program)state.ResolvedProgram!;
           var writer = new StringWriter();
@@ -86,11 +96,43 @@ public CompletionList Process() {
         return new CompletionList();
       }
 
+      private string GetLastTwoCharactersBeforePositionIncluded(TextBuffer text, DafnyPosition position) {
+        var index = text.ToIndex(position.GetLspPosition());
+        var indexTwoCharactersBefore = Math.Max(0, index - 2);
+        if (index > text.Text.Length) {
+          return "";
+        }
+
+        return text.Text.Substring(indexTwoCharactersBefore, index - indexTwoCharactersBefore);
+      }
+
       private bool IsDotExpression() {
         var node = state.Program.FindNode<INode>(request.TextDocument.Uri.ToUri(), request.Position.ToDafnyPosition());
         return node?.RangeToken.EndToken.val == ".";
       }
 
+      private bool IsAtAttribute() {
+        var position = request.Position.ToDafnyPosition();
+        var fileContent = filesystem.GetBuffer(request.TextDocument.Uri.ToUri());
+        if (fileContent == null) {
+          // Impossible case because this only happens if the file is not opened.
+          return false;
+        }
+        var lastTwoChars = GetLastTwoCharactersBeforePositionIncluded(fileContent, position);
+        var isAtAttribute =
+          lastTwoChars == "@" ||
+          lastTwoChars.Length >= 2 && lastTwoChars[1] == '@' && char.IsWhiteSpace(lastTwoChars[0]);
+        return isAtAttribute;
+      }
+
+      private CompletionList CreateAtAttributeCompletionList() {
+        var completionItems =
+          Attributes.BuiltinAtAttributes.Select(b =>
+            CreateCompletionItem(b.Name)
+          ).ToList();
+        return new CompletionList(completionItems);
+      }
+
       private CompletionList CreateDotCompletionList() {
         IEnumerable<ILegacySymbol> members;
         if (symbolGuesser.TryGetTypeBefore(state,
@@ -122,6 +164,15 @@ private static bool IsConstructor(ILegacySymbol symbol) {
         return symbol is MethodSymbol method && method.Name == "_ctor";
       }
 
+      private CompletionItem CreateCompletionItem(string attributeName) {
+        return new CompletionItem {
+          Label = attributeName,
+          Kind = CompletionItemKind.Constructor,
+          InsertText = attributeName,
+          Detail = ""
+        };
+      }
+
       private CompletionItem CreateCompletionItem(ILegacySymbol symbol) {
         return new CompletionItem {
           Label = symbol.Name,

Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs

@@ -62,7 +62,7 @@ public override TextDocumentAttributes GetTextDocumentAttributes(DocumentUri uri
     public override async Task<Unit> Handle(DidOpenTextDocumentParams notification, CancellationToken cancellationToken) {
       logger.LogDebug("received open notification {DocumentUri}", notification.TextDocument.Uri);
       try {
-        await projects.OpenDocument(new DocumentTextBuffer(notification.TextDocument));
+        await projects.OpenDocument(notification.TextDocument);
       } catch (InvalidOperationException e) {
         if (!e.Message.Contains("because it is already open")) {
           telemetryPublisher.PublishUnhandledException(e);

Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs

@@ -89,6 +89,14 @@ public void CloseDocument(TextDocumentIdentifier document) {
     }
   }
 
+  public TextBuffer? GetBuffer(Uri uri) {
+    if (openFiles.TryGetValue(uri, out var entry)) {
+      return entry.Buffer;
+    }
+
+    return null;
+  }
+
   public TextReader ReadFile(Uri uri) {
     if (openFiles.TryGetValue(uri, out var entry)) {
       return new StringReader(entry.Buffer.Text);

Source/DafnyLanguageServer/Workspace/ProjectManager.cs

@@ -2,6 +2,7 @@
 using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.CommandLine;
+using System.IO;
 using System.Linq;
 using System.Numerics;
 using System.Reactive.Concurrency;

Source/DafnyLanguageServer/Workspace/TextBuffer.cs

@@ -57,7 +57,15 @@ public Position FromIndex(int index) {
   }
 
   private BufferLine IndexToLine(int index) {
-    return indexToLineTree.Query(index).Single();
+    try {
+      return indexToLineTree.Query(index).Single();
+    } catch (InvalidOperationException) {
+      try {// Just in case we are on Windows and we happen to query an index between "\r" and "\n"
+        return indexToLineTree.Query(index - 1).Single();
+      } catch (InvalidOperationException) {
+        throw new ArgumentException($"index {index} is outside of the text buffer");
+      }
+    }
   }
 
   public int ToIndex(Position position) {