Fix spurious vacuity warnings when assertions converted to assumptions (

dafny-lang#4604)

Some assertions are translated into assumptions in specific contexts.
Before this change, if those assertions were unused in the proof, Dafny
would warn that they may have been proved vacuously. Now it doesn’t.
It also skips warning about various internal checks that are proved in a
context that the user has no control over.

Along the way, this also changes the behavior of proof dependency
warnings so that they're produced for any definition that successfully
verifies, even if some definitions in the program have errors.

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -1,6 +1,7 @@
 using System.Linq;
 using DafnyCore.Verifier;
 using Microsoft.Dafny.ProofObligationDescription;
+using VC;
 
 namespace Microsoft.Dafny;
 
@@ -16,6 +17,10 @@ public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, Er
   }
 
   public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, DafnyConsolePrinter.ImplementationLogEntry logEntry, DafnyConsolePrinter.VerificationResultLogEntry result) {
+    if (result.Outcome != ConditionGeneration.Outcome.Correct) {
+      return;
+    }
+
     var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(logEntry.Name);
     var usedDependencies =
       result
@@ -81,8 +86,13 @@ private static bool ShouldWarnVacuous(DafnyOptions options, string verboseName,
         return false;
       }
 
-      // Similarly here
-      if (poDep.ProofObligation is MatchIsComplete or AlternativeIsComplete) {
+      // Some proof obligations occur in a context that the Dafny programmer
+      // doesn't have control of, so warning about vacuity isn't helpful.
+      if (poDep.ProofObligation
+          is MatchIsComplete
+          or AlternativeIsComplete
+          or ValidInRecursion
+          or TraitDecreases) {
         return false;
       }
 

Source/DafnyCore/Verifier/ProofDependency.cs

@@ -66,6 +66,20 @@ public ProofObligationDependency(IToken tok, PODesc.ProofObligationDescription p
   }
 }
 
+public class AssumedProofObligationDependency : ProofDependency {
+  public override RangeToken Range { get; }
+
+  public PODesc.ProofObligationDescription ProofObligation { get; }
+
+  public override string Description =>
+      $"assumption that {ProofObligation.SuccessDescription}";
+
+  public AssumedProofObligationDependency(IToken tok, PODesc.ProofObligationDescription proofObligation) {
+    Range = tok as RangeToken ?? new RangeToken(tok, tok);
+    ProofObligation = proofObligation;
+  }
+}
+
 // Represents the assumption of a requires clause in the process of
 // proving a Dafny definition.
 public class RequiresDependency : ProofDependency {

Source/DafnyCore/Verifier/Translator.cs

@@ -7491,10 +7491,11 @@ Bpl.PredicateCmd Assert(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDe
           || (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify))) {
         // produce an assume instead
         cmd = TrAssumeCmd(tok, condition, kv);
+        proofDependencies?.AddProofDependencyId(cmd, tok, new AssumedProofObligationDependency(tok, description));
       } else {
         cmd = TrAssertCmdDesc(ForceCheckToken.Unwrap(tok), condition, description, kv);
+        proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description));
       }
-      proofDependencies?.AddProofDependencyId(cmd, tok, new ProofObligationDependency(tok, description));
       return cmd;
     }
 

Source/DafnyDriver/DafnyDriver.cs

@@ -468,7 +468,7 @@ private async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!
         string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1]));
         var (verified, outcome, moduleStats) = await BoogieAsync(options, baseName, boogiePrograms, programId);
 
-        if (options.TrackVerificationCoverage && verified) {
+        if (options.TrackVerificationCoverage) {
           ProofDependencyWarnings.WarnAboutSuspiciousDependencies(options, dafnyProgram.Reporter, depManager);
         }
 

Test/logger/ProofDependencyLogging.dfy

@@ -423,6 +423,13 @@ method ObviouslyUnreachableReturnStatementMethod(t: T) returns (r:int)
     return 1; // unreachable
   }
 
+method CalcStatementWithSideConditions(x: int) {
+  calc == {
+    x / 2;
+    (x*2) / 4;
+  }
+}
+
 method DontWarnAboutVacuousAssertFalse(x: int) {
   assume x == x + 1;
   assert false;

Test/logger/ProofDependencyWarnings.dfy

@@ -1,4 +1,4 @@
-// RUN: %verify --verify-included-files --warn-contradictory-assumptions --warn-redundant-assumptions "%s" > "%t"
+// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --warn-contradictory-assumptions --warn-redundant-assumptions "%s" > "%t"
 // RUN: %diff "%t" "%s.expect"
 
 include "ProofDependencyLogging.dfy"

Test/logger/ProofDependencyWarnings.dfy.expect

@@ -17,4 +17,4 @@ ProofDependencyLogging.dfy(346,10): Warning: ensures clause proved using contrad
 ProofDependencyLogging.dfy(354,11): Warning: unnecessary requires clause
 ProofDependencyLogging.dfy(363,9): Warning: unnecessary assumption
 
-Dafny program verifier finished with 29 verified, 0 errors
+Dafny program verifier finished with 30 verified, 0 errors