fix: "Failing precondition" on tooltip instead of "return path" (#2654)

dafny-lang · Aug 31, 2022 · d6b6927 · d6b6927
1 parent 17fbc2d
commit d6b6927
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 9 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -5,6 +5,7 @@
 - fix: Fixed a crash when parsing `newtype` in the parser (https://github.com/dafny-lang/dafny/pull/2649)
 - fix: Added missing error reporting position on string prefix check (https://github.com/dafny-lang/dafny/pull/2652)
 - fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
+- fix: Better messages on hovering failing postconditions in IDE (https://github.com/dafny-lang/dafny/pull/2654)
 - fix: Better error reporting on counter-examples if an option is not provided (https://github.com/dafny-lang/dafny/pull/2650)
 
 # 3.8.0

diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs
@@ -14,7 +14,7 @@
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup {
   [TestClass]
   public class HoverVerificationTest : DafnyLanguageServerTestBase {
-    private const int MaxTestExecutionTimeMs = 10000;
+    private const int MaxTestExecutionTimeMs = 30000;
 
     private ILanguageClient client;
     private TestNotificationReceiver<CompilationStatusParams> notificationReceiver;
@@ -96,7 +96,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**:
@@ -129,7 +129,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**:
@@ -147,7 +147,6 @@ public async Task MeaningfulMessageWhenMethodWithoutAssert() {
 method f(x: int) {
   print x;
 }", "testfile.dfy");
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method f**:
 
@@ -158,13 +157,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");
+      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");
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method f**:
 
@@ -181,7 +196,6 @@ method f(x: int) {
   assert false;
   assert false;
 }", "testfile2.dfy");
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method f**:
 
@@ -208,7 +222,6 @@ requires p > 0 && q > 0
   }
   assert {:split_here} true;
 } ", "testfileSlow.dfy");
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 22),
         @"**Verification performance metrics for method SquareRoot2NotRational**:
 

diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs
@@ -185,8 +185,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 => "",
@@ -251,6 +251,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;
     }