From 225a420c68818afe2beca1bb3cf3dda934fab428 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Mon, 29 Aug 2022 14:30:38 -0500
Subject: [PATCH] fix: "Failing precondition" on tooltip instead of "return
 path" Fixes #2653. Also made the tests more robust by removing the need of
 Task.Delay

---
 .../Lookup/HoverVerificationTest.cs           | 28 +++++++++++++++----
 .../Handlers/DafnyHoverHandler.cs             | 10 +++++--
 2 files changed, 30 insertions(+), 8 deletions(-)

diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs
index d336abc0f72..2662057b659 100644
--- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs
+++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs
@@ -99,7 +99,7 @@ This is the only assertion in [batch](???) #2 of 3 in method f
       await AssertHoverMatches(documentItem, (2, 12),
         @"<span style='color:green'>**Success:**</span> assertion always holds  
 This is the only assertion in [batch](???) #3 of 3 in method f  
-[Batch](???) #3 resource usage: ??? RU  "
+[Batch](???) #3 resource usage: ??? RU"
       );
       await AssertHoverMatches(documentItem, (0, 36),
         @"**Verification performance metrics for method f**:
@@ -132,7 +132,7 @@ await AssertHoverMatches(documentItem, (2, 12),
       await AssertHoverMatches(documentItem, (3, 26),
         @"[**Error:**](???) assertion might not hold  
 This is assertion #1 of 2 in [batch](???) #2 of 2 in function f  
-[Batch](???) #2 resource usage: ??? RU  "
+[Batch](???) #2 resource usage: ??? RU"
       );
       await AssertHoverMatches(documentItem, (0, 36),
         @"**Verification performance metrics for function f**:
@@ -150,7 +150,6 @@ public async Task MeaningfulMessageWhenMethodWithoutAssert() {
 method f(x: int) {
   print x;
 }", "testfile.dfy", CompilationStatus.VerificationSucceeded);
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method f**:
 
@@ -161,13 +160,29 @@ await AssertHoverMatches(documentItem, (0, 10),
     }
 
 
+    [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+    public async Task MeaningfulMessageForFailingPreconditions() {
+      var documentItem = await GetDocumentItem(@"
+method Test1() {
+    Test2(0);  // Hover #1
+}
+
+method Test2(i: int)
+  requires i > 0 {
+
+}", "testfile.dfy", CompilationStatus.VerificationFailed);
+      await AssertHoverMatches(documentItem, (1, 10),
+        @"???
+Failing precondition:???"
+      );
+    }
+
     [TestMethod, Timeout(MaxTestExecutionTimeMs)]
     public async Task MeaningfulMessageWhenMethodWithOneAssert() {
       var documentItem = await GetDocumentItem(@"
 method f(x: int) {
   assert false;
 }", "testfile1.dfy", CompilationStatus.VerificationFailed);
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method f**:
 
@@ -184,7 +199,6 @@ method f(x: int) {
   assert false;
   assert false;
 }", "testfile2.dfy", CompilationStatus.VerificationFailed);
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method f**:
 
@@ -211,7 +225,6 @@ requires p > 0 && q > 0
   }
   assert {:split_here} true;
 } ", "testfileSlow.dfy", CompilationStatus.VerificationFailed);
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 22),
         @"**Verification performance metrics for method SquareRoot2NotRational**:
 
@@ -229,6 +242,9 @@ private async Task<TextDocumentItem> GetDocumentItem(string source, string filen
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
       var lastStatus = await WaitUntilDafnyFinishes(documentItem);
       Assert.AreEqual(expectedStatus, lastStatus);
+      foreach (var document in Documents.Documents) {
+        await document.LastDocument;
+      }
       return documentItem;
     }
 
diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs
index 2a4ff71580a..f96a635feb9 100644
--- a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs
+++ b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs
@@ -182,8 +182,8 @@ private string GetAssertionInformation(Position position, AssertionVerificationT
 
 
       var currentlyHoveringPostcondition =
-        !(assertionNode.GetCounterExample() is ReturnCounterexample returnCounterexample2 &&
-          returnCounterexample2.FailingReturn.tok.GetLspRange().Contains(position));
+        assertionNode.GetCounterExample() is ReturnCounterexample returnCounterexample2 &&
+          !returnCounterexample2.FailingReturn.tok.GetLspRange().Contains(position);
 
       var obsolescence = assertionNode.StatusCurrent switch {
         CurrentStatus.Current => "",
@@ -248,6 +248,12 @@ string GetDescription(Boogie.ProofObligationDescription? description) {
           : "");
       }
 
+      if (assertionNode.GetCounterExample() is CallCounterexample) {
+        information += "  \n" + (assertionNode.SecondaryPosition != null
+          ? $"Failing precondition: {Path.GetFileName(assertionNode.Filename)}({assertionNode.SecondaryPosition.Line + 1}, {assertionNode.SecondaryPosition.Character + 1})"
+          : "");
+      }
+
       return information;
     }