Address comments on dafny-lang#4604 (dafny-lang#4609)

We merged dafny-lang#4604 quickly, since it included a fix to unblock CI, but
there were a couple of things that could be improved. This addresses
comments from @keyboardDrummer plus things I noticed in the process of
addressing them.

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

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -90,17 +90,13 @@ private static bool ShouldWarnVacuous(DafnyOptions options, string verboseName,
 
       // 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) {
+      if (poDep.ProofObligation.ProvedOutsideUserCode) {
         return false;
       }
 
       // Don't warn about `assert false` being proved vacuously. If it's proved,
       // it must be vacuous, but it's also probably an attempt to prove that a
-      // given alternative is unreachable.
+      // given branch is unreachable (often, but not always, in ghost code).
       var assertedExpr = poDep.ProofObligation.GetAssertedExpr(options);
       if (assertedExpr is not null &&
           Expression.IsBoolLiteral(assertedExpr, out var lit) &&
@@ -110,6 +106,8 @@ or ValidInRecursion
     }
 
     // Ensures clauses are often proven vacuously during well-formedness checks.
+    // There's unfortunately no way to identify these checks once Dafny has
+    // been translated to Boogie other than looking at the name.
     if (verboseName.Contains("well-formedness") && dep is EnsuresDependency) {
       return false;
     }
@@ -137,4 +135,4 @@ private static bool ShouldWarnUnused(ProofDependency dep) {
 
     return true;
   }
-}
+}

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -20,6 +20,8 @@ protected static Expression ToSubstitutableExpression(BoundVar bvar) {
     var expression = new IdentifierExpr(bvar.tok, bvar);
     return new ParensExpression(bvar.tok, expression) { Type = bvar.Type, ResolvedExpression = expression };
   }
+
+  public virtual bool ProvedOutsideUserCode => false;
 }
 
 //// Arithmetic and logical operators, conversions
@@ -222,7 +224,7 @@ public IsInteger(string prefix = "") {
 
 public class NonNull : ProofObligationDescription {
   public override string SuccessDescription =>
-    $"{PluralSuccess}{what} object is never null";
+    $"{PluralSuccess}{what} is never null";
 
   public override string FailureDescription =>
     $"{PluralFailure}{what} might be null";
@@ -418,6 +420,8 @@ public class EnsuresStronger : ProofObligationDescription {
     "the method must provide an equal or more detailed postcondition than in its parent trait";
 
   public override string ShortDescription => "ensures stronger";
+
+  public override bool ProvedOutsideUserCode => true;
 }
 
 public class RequiresWeaker : ProofObligationDescription {
@@ -428,6 +432,8 @@ public class RequiresWeaker : ProofObligationDescription {
     "the method must provide an equal or more permissive precondition than in its parent trait";
 
   public override string ShortDescription => "requires weaker";
+
+  public override bool ProvedOutsideUserCode => true;
 }
 
 public class ForallPostcondition : ProofObligationDescription {
@@ -482,6 +488,8 @@ public class TraitDecreases : ProofObligationDescription {
 
   public override string ShortDescription => "trait decreases";
 
+  public override bool ProvedOutsideUserCode => true;
+
   private readonly string whatKind;
 
   public TraitDecreases(string whatKind) {
@@ -554,6 +562,8 @@ public class DecreasesBoundedBelow : ProofObligationDescription {
 
   public override string ShortDescription => "bounded decreases expression";
 
+  public override bool ProvedOutsideUserCode => true;
+
   private string component => N == 1 ? "expression" : $"expression at index {k}";
   private readonly string zeroStr;
   private readonly string suffix;
@@ -592,6 +602,8 @@ public class FunctionContractOverride : ProofObligationDescription {
 
   public override string ShortDescription => "contract override valid";
 
+  public override bool ProvedOutsideUserCode => true;
+
   private readonly bool isEnsures;
   private string RestrictionDesc =>
     isEnsures ? "more detailed postcondition" : "more permissive precondition";
@@ -612,6 +624,8 @@ public class MatchIsComplete : ProofObligationDescription {
 
   public override string ShortDescription => "match complete";
 
+  public override bool ProvedOutsideUserCode => true;
+
   private readonly string matchForm;
   private readonly string missing;
   public MatchIsComplete(string matchForm, string missing) {
@@ -628,6 +642,8 @@ public class AlternativeIsComplete : ProofObligationDescription {
     $"alternative cases fail to cover all possibilities";
 
   public override string ShortDescription => "alternative complete";
+
+  public override bool ProvedOutsideUserCode => true;
 }
 
 public class PatternShapeIsValid : ProofObligationDescription {
@@ -766,6 +782,8 @@ witnessString is null
 
   public override string ShortDescription => "witness check";
 
+  public override bool ProvedOutsideUserCode => true;
+
   private readonly string errMsg = "cannot find witness that shows type is inhabited";
   private readonly string hintMsg =
     "; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type";
@@ -821,6 +839,8 @@ public class ValidInRecursion : ProofObligationDescription {
 
   public override string ShortDescription => "valid in recursion";
 
+  public override bool ProvedOutsideUserCode => true;
+
   private readonly string what;
   private readonly string hint;
 
@@ -1118,6 +1138,8 @@ public class ConcurrentFrameEmpty : ProofObligationDescription {
 
   public override string ShortDescription => "concurrency safety";
 
+  public override bool ProvedOutsideUserCode => true;
+
   private readonly string frameName;
 
   public ConcurrentFrameEmpty(string frameName) {

Test/logger/ProofDependencyLogging.dfy

@@ -435,6 +435,20 @@ method DontWarnAboutVacuousAssertFalse(x: int) {
   assert false;
 }
 
+// CHECK: Results for GetX \(well-formedness\)
+// CHECK:     Proof dependencies:
+// CHECK:       ProofDependencyLogging.dfy\(449,5\)-\(449,5\): target object is never null
+
+class C {
+  var x: int
+}
+
+function GetX(c: C): int
+  reads c
+{
+  c.x
+}
+
 method DontWarnAboutUnusedAssumeTrue(x: int) {
   assume true;
   assert 1 + x == x + 1;

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 31 verified, 0 errors
+Dafny program verifier finished with 32 verified, 0 errors