feat: More hovering information on the LSP (#3282)

Fixes #3281 
Fixes dafny-lang/ide-vscode#335
Fixes dafny-lang/ide-vscode#317
Fixes dafny-lang/ide-vscode#210

Example code:
```dafny
predicate P(i: int) {
  i <= 0
}

predicate Q(i: int, j: int) {
  i == j || -i == j
}

function method Toast(i: int): int
  requires P(i)

method Test(i: int) returns (j: nat)
  ensures Q(i, j)
{
  if i < 0 {
    return -i;
  } else {
    return Toast(i);
  }
}
```

| Before: | After |
| --------|-------|
| Hovering Q(i,j)
![image](https://user-images.githubusercontent.com/3601079/209727765-e3c9c32b-dd27-4707-893b-8534b9ec0698.png)
|
![image](https://user-images.githubusercontent.com/3601079/209727590-2f833693-4b9d-44cf-afa8-fe43388e0c3d.png)
|
| Hovering the second return
![image](https://user-images.githubusercontent.com/3601079/209727748-5d291a36-7334-4b9c-8c08-c68718fd50f9.png)
|
![image](https://user-images.githubusercontent.com/3601079/209727565-19b8a1c6-0f78-41a3-ad85-7e0cbc1538c8.png)
|
| Hovering the call to Toast()
![image](https://user-images.githubusercontent.com/3601079/209727700-2e66f345-dd1f-47c5-92ce-cea811d2b8ce.png)
|
![image](https://user-images.githubusercontent.com/3601079/209727556-cbfe43c5-9fe2-49c9-a107-7111ef42b00c.png)
|
| Also, on the diagnostics side (and it's clickable!)
![image](https://user-images.githubusercontent.com/3601079/209844964-be5a31df-dddd-421a-937f-39a26fa8ce76.png)
|
![image](https://user-images.githubusercontent.com/3601079/209845060-09dd8fb5-5cd8-4e92-8302-beb93a837412.png)
|
| The resolver error appears after all obsolete verification
error<br>![image](https://user-images.githubusercontent.com/3601079/209727781-b3d88e9b-8bad-4e3b-b8fc-e9119837629e.png)
|
![image](https://user-images.githubusercontent.com/3601079/209728682-206bf18a-dfd8-40c5-a10d-8b5a4ccdd4c1.png)
|

I added language server tests and tested it in VSCode, and it works as
expected.

<!-- Are you moving a large amount of code? Read CONTRIBUTING.md to
learn how to do that while maintaining git history -->

<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>

Source/DafnyCore/AST/DafnyAst.cs

@@ -121,9 +121,8 @@ void UpdateStartEndTokRecursive(INode node) {
  UpdateStartEndToken(node.EndToken);
  } else {
  UpdateStartEndToken(node.tok);
+ node.Children.Iter(UpdateStartEndTokRecursive);
  }
-
- node.Children.Iter(UpdateStartEndTokRecursive);
  }
 
  UpdateStartEndTokRecursive(this);

Source/DafnyCore/AST/Expressions/Expressions.cs

@@ -1647,6 +1647,8 @@ public UnaryOpExpr(IToken tok, Opcode op, Expression e)
  Contract.Requires(op != Opcode.Fresh || this is FreshExpr);
  this.Op = op;
  }
+
+ public override bool IsImplicit => Op == Opcode.Lit;
 }
 
 public class FreshExpr : UnaryOpExpr, ICloneable<FreshExpr> {

Source/DafnyCore/AST/Substituter.cs

@@ -55,7 +55,12 @@ public virtual Expression Substitute(Expression expr) {
  } else if (expr is WildcardExpr) {
  // nothing to substitute
  } else if (expr is ThisExpr) {
- return receiverReplacement == null ? expr : receiverReplacement;
+ return receiverReplacement == null ?
+ expr : new ParensExpression(expr.tok, receiverReplacement) {
+ ResolvedExpression = receiverReplacement,
+ RangeToken = expr.RangeToken,
+ Type = receiverReplacement.Type
+ };
  } else if (expr is IdentifierExpr) {
  IdentifierExpr e = (IdentifierExpr)expr;
  Expression substExpr;
@@ -378,10 +383,14 @@ ExtendedPattern SubstituteForPattern(ExtendedPattern pattern) {
  if (test != e.Test || thn != e.Thn || els != e.Els) {
  newExpr = new ITEExpr(expr.tok, e.IsBindingGuard, test, thn, els);
  }
-
  } else if (expr is ConcreteSyntaxExpression concreteSyntaxExpression) {
  Contract.Assert(concreteSyntaxExpression.ResolvedExpression != null);
- return Substitute(concreteSyntaxExpression.ResolvedExpression);
+ var resolvedExpression = Substitute(concreteSyntaxExpression.ResolvedExpression);
+ return new ParensExpression(expr.tok, resolvedExpression) {
+ ResolvedExpression = resolvedExpression,
+ RangeToken = expr.RangeToken,
+ Type = resolvedExpression.Type
+ };
 
  } else if (expr is Translator.BoogieFunctionCall) {
  var e = (Translator.BoogieFunctionCall)expr;

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -2,7 +2,9 @@
 using System.Collections.Generic;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using JetBrains.Annotations;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.Configuration;
@@ -15,18 +17,17 @@
 
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup {
  [TestClass]
- public class HoverVerificationTest : DafnyLanguageServerTestBase {
+ public class HoverVerificationTest : SynchronizationTestBase {
  private const int MaxTestExecutionTimeMs = 30000;
 
- private ILanguageClient client;
  private TestNotificationReceiver<CompilationStatusParams> notificationReceiver;
 
  [TestInitialize]
- public Task SetUp() => SetUp(null);
+ public new Task SetUp() => SetUp(null);
 
  public async Task SetUp(Action<DafnyOptions> modifyOptions) {
  notificationReceiver = new();
- client = await InitializeClient(options => {
+ Client = await InitializeClient(options => {
  options
  .AddHandler(DafnyRequestNames.CompilationStatus, NotificationHandler.For<CompilationStatusParams>(notificationReceiver.NotificationReceived));
  }, modifyOptions);
@@ -57,6 +58,7 @@ This is assertion #1 of 4 in method Abs
  // because the IDE extension already does it.
  await AssertHoverMatches(documentItem, (5, 4),
  @"[**Error:**](???) A postcondition might not hold on this return path. 
+Could not prove: y >= 0 
 This is assertion #1 of 4 in method Abs 
 Resource usage: ??? RU"
  );
@@ -200,6 +202,197 @@ await AssertHoverMatches(documentItem, (0, 7),
  );
  }
 
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task DoNotExtendPastExpressions2() {
+ var documentItem = await GetDocumentItem(@"
+function method Id<T>(t: T): T { t }
+datatype Test = Test(i: int)
+{
+ method Tester(other: Test) {
+ assert Valid(other);
+ assert CanAct(Id(other));
+ }
+ static predicate Valid(t: Test) {
+ t.i > 0
+ }
+ static predicate CanAct(t: Test) requires Valid(t) {
+ t.i > 1
+ }
+}
+", "testfile2.dfy");
+ await AssertHoverMatches(documentItem, (4, 20),
+ @"**Error:**???assertion might not hold???
+Could not prove: t.i > 0 "
+ );
+ await AssertHoverMatches(documentItem, (5, 20),
+ @"**Error:**???assertion might not hold???
+Could not prove: t.i > 1 "
+ );
+ await AssertHoverMatches(documentItem, (5, 20),
+ @"**Success:**???function precondition satisfied???
+Did prove: Valid(t) 
+Did prove: t.i > 0 "
+ );
+ }
+
+ [TestMethod/*, Timeout(MaxTestExecutionTimeMs)*/]
+ public async Task DoNotExtendPastExpressions3() {
+ var documentItem = await GetDocumentItem(@"
+datatype ValidTester = Tester(next: ValidTester2) | Tester2(next: ValidTester2) | Test3(next: ValidTester2)
+{
+ predicate Valid() {
+ ((this.Tester? || this.Tester2?) && this.next.Valid()) || (this.Test3? && !this.next.Valid())
+ }
+
+ function method apply(): int requires Valid() {
+ 2
+ }
+ static method Test(c: ValidTester) {
+ var x := c.apply();
+ }
+}
+
+datatype ValidTester2 = MoreTest(i: int, next: ValidTester2) | End {
+ predicate Valid(defaultValue: int := 0) {
+ 0 <= defaultValue && (this.End? || (this.MoreTest? && this.next.Valid() && i > 0))
+ }
+}
+", "testfile2.dfy");
+ await AssertHoverMatches(documentItem, (10, 16),
+ @"**Error:**???function precondition might not hold???
+Could not prove: Valid() 
+Could not prove: ((this.Tester? || this.Tester2?) && this.next.Valid()) || (this.Test3? && !this.next.Valid()) "
+ );
+ }
+
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task DoNotExtendPastExpressions() {
+ var documentItem = await GetDocumentItem(@"
+datatype Test = Test(i: int)
+{
+ predicate Valid() {
+ i > 0
+ }
+ predicate CanAct() requires Valid() {
+ i > 1
+ }
+ method Tester(other: Test) {
+ assert other.Valid();
+ assert Id(other).CanAct();
+ }
+}
+function method Id<T>(t: T): T { t }
+
+", "testfile2.dfy");
+ await AssertHoverMatches(documentItem, (9, 20),
+ @"**Error:**???assertion might not hold???
+Could not prove: i > 0 "
+ );
+ await AssertHoverMatches(documentItem, (10, 20),
+ @"**Error:**???assertion might not hold???
+Could not prove: i > 1 "
+ );
+ await AssertHoverMatches(documentItem, (10, 20),
+ @"**Success:**???function precondition satisfied???
+Did prove: Valid() 
+Did prove: i > 0 "
+ );
+ }
+
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task DisplayNestedFailingPostconditionsAndPreconditions() {
+ var documentItem = await GetDocumentItem(@"
+predicate P(i: int) {
+ i <= 0
+}
+
+predicate Q(i: int, j: int) {
+ i == j || -i == j
+}
+
+function method Toast(i: int): int
+ requires P(i)
+
+method Test(i: int) returns (j: nat)
+ ensures Q(i, j)
+{
+ if i < 0 {
+ return -i;
+ } else {
+ return Toast(i);
+ }
+}
+", "testfile2.dfy");
+ await AssertHoverMatches(documentItem, (12, 11),
+ @"**Error:**???This postcondition might not hold on a return path.???
+Could not prove: i == j || -i == j???
+Return path: testfile2.dfy(18, 5)"
+ );
+ await AssertHoverMatches(documentItem, (17, 6),
+ @"**Error:**???A postcondition might not hold on this return path.???
+Could not prove: Q(i, j)???
+Could not prove: i == j || -i == j"
+ );
+ await AssertHoverMatches(documentItem, (17, 13),
+ @"**Error:**???function precondition might not hold???
+Could not prove: P(i)???
+Could not prove: i <= 0"
+ );
+ }
+
+ [TestMethod/*, Timeout(MaxTestExecutionTimeMs)*/]
+ public async Task DisplayWorksOnPreviouslyFailingExample() {
+ var documentItem = await GetDocumentItem(@"
+module ProblemModule {
+ datatype X =
+ | Cons(head: int, tail: X)
+ | Nil
+ {
+ predicate method Valid() {
+ this.Cons? && tail.Valid()
+ }
+ }
+}
+
+method Test() returns (j: int)
+ ensures j == 1
+{
+ return 2;
+}
+", "testfile2.dfy");
+ await AssertHoverMatches(documentItem, (14, 5),
+ @"**Error:**???A postcondition might not hold on this return path.???
+Could not prove: j == 1"
+ );
+ }
+
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task DoNotDisplayVerificationIfSyntaxError() {
+ var documentItem = await GetDocumentItem(@"
+predicate P(i: int) {
+ i <= 0
+}
+
+method Test(i: int)
+{
+ assert P(1);
+}
+", "testfile2.dfy");
+ await AssertHoverMatches(documentItem, (6, 11),
+ @"**Error:**???assertion might not hold 
+Could not prove: i <= 0"
+ );
+ await ApplyChangesAndWaitCompletionAsync(
+ documentItem,
+ new TextDocumentContentChangeEvent {
+ Range = ((0, 0), (0, 0)),
+ Text = @"/"
+ });
+ await AssertHoverMatches(documentItem, (6, 11),
+ null
+ );
+ }
+
  [TestMethod, Timeout(5 * MaxTestExecutionTimeMs)]
  public async Task IndicateClickableWarningSignsOnMethodHoverWhenResourceLimitReached10MThreshold() {
  var documentItem = await GetDocumentItem(@"
@@ -232,22 +425,27 @@ await AssertHoverMatches(documentItem, (0, 22),
  private async Task<TextDocumentItem> GetDocumentItem(string source, string filename) {
  source = source.TrimStart();
  var documentItem = CreateTestDocument(source, filename);
- await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+ await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
  await Documents.GetLastDocumentAsync(documentItem);
  return documentItem;
  }
 
- private async Task AssertHoverMatches(TextDocumentItem documentItem, Position hoverPosition, string expected) {
+ private async Task AssertHoverMatches(TextDocumentItem documentItem, Position hoverPosition, [CanBeNull] string expected) {
  var hover = await RequestHover(documentItem, hoverPosition);
- Assert.IsNotNull(hover);
+ if (expected == null) {
+ Assert.IsTrue(hover == null || hover.Contents.MarkupContent is null or { Value: "" },
+ "Did not expect a message at {0}", hoverPosition);
+ return;
+ }
+ Assert.IsNotNull(hover, "No hover message found at {0}", hoverPosition);
  var markup = hover.Contents.MarkupContent;
  Assert.IsNotNull(markup);
  Assert.AreEqual(MarkupKind.Markdown, markup.Kind);
  AssertMatchRegex(expected.ReplaceLineEndings("\n"), markup.Value);
  }
 
  private void AssertMatchRegex(string expected, string value) {
- var regexExpected = Regex.Escape(expected).Replace(@"\?\?\?", ".*");
+ var regexExpected = Regex.Escape(expected).Replace(@"\?\?\?", "[\\s\\S]*");
  var matched = new Regex(regexExpected).Match(value).Success;
  if (!matched) {
  // A simple helper to determine what portion of the regex did not match
@@ -262,7 +460,7 @@ private void AssertMatchRegex(string expected, string value) {
  }
 
  private Task<Hover> RequestHover(TextDocumentItem documentItem, Position position) {
- return client.RequestHover(
+ return Client.RequestHover(
  new HoverParams {
  TextDocument = documentItem.Uri,
  Position = position

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -91,6 +91,34 @@ public async Task EmptyFileNoCodeWarning() {
  Assert.AreEqual(new Range(0, 0, 0, 0), diagnostics[0].Range);
  }
 
+ [TestMethod]
+ public async Task OpeningFailingFunctionPreconditionHasRelatedDiagnostics() {
+ var source = @"
+predicate P(i: int) {
+ i <= 0
+}
+
+function method Call(i: int): int
+ requires P(i)
+
+method Test(i: int) returns (j: int)
+ requires i > 0
+{
+ return Call(2/i);
+}".TrimStart();
+ var documentItem = CreateTestDocument(source);
+ await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+ var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
+ Assert.AreEqual(1, diagnostics.Length);
+ Assert.IsNotNull(diagnostics[0].RelatedInformation);
+ var relatedInformation =
+ diagnostics[0].RelatedInformation.ToArray();
+ Assert.AreEqual(2, relatedInformation.Length);
+ Assert.AreEqual("Could not prove: P(i)", relatedInformation[0].Message);
+ Assert.AreEqual("Could not prove: i <= 0", relatedInformation[1].Message);
+ await AssertNoDiagnosticsAreComing(CancellationToken);
+ }
+
  [TestMethod]
  public async Task OpeningFlawlessDocumentReportsNoDiagnostics() {
  var source = @"

Source/DafnyLanguageServer.Test/Synchronization/SynchronizationTestBase.cs

@@ -7,7 +7,7 @@
 
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization {
  public class SynchronizationTestBase : DafnyLanguageServerTestBase {
- protected ILanguageClient Client { get; private set; }
+ protected ILanguageClient Client { get; set; }
 
  protected Task ApplyChangeAndWaitCompletionAsync(TextDocumentItem documentItem, Range range, string newText) {
  return ApplyChangesAndWaitCompletionAsync(

Source/DafnyLanguageServer.Test/Various/StandaloneLanguageServerBinaryTest.cs

@@ -41,11 +41,12 @@ public async Task InitialisationWorks() {
  private Process StartLanguageServer() {
  var serverBinary = Path.Join(Path.GetDirectoryName(Assembly.GetExecutingAssembly().Location), "DafnyLanguageServer.dll");
 
- var processInfo = new ProcessStartInfo("dotnet", serverBinary) {
+ var processInfo = new ProcessStartInfo("dotnet") {
  RedirectStandardOutput = true,
  RedirectStandardError = true,
  RedirectStandardInput = true,
- UseShellExecute = false
+ UseShellExecute = false,
+ ArgumentList = { serverBinary }
  };
 
  return Process.Start(processInfo)!;