More granular proof dependencies (dafny-lang#4851)

# Description

This PR refactors the proof dependency data types and the warning
generation code to do several things:

* Distinguish between the various types of assumption that can show up.
We currently report redundancies only for assumptions that come directly
from assume and assert statements and for requires clauses. Other types
are difficult for the user to control, but will likely be useful to
treat separately in the future.
* Distinguish between the split parts of `requires` and `ensures`
clauses.
* Clarify that unnecessary assumptions and assertions may be only partly
unnecessary. A next step will be to indicate which part is unnecessary,
but that turns out to require changing verification conditions in a way
that may affect performance and brittleness, so I'm going to leave that
for a separate PR that I hope to land after we release 4.4.

Fixes dafny-lang#4719 

# How has this been tested?
This changes the expected output of a few existing tests.

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

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -36,10 +36,7 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions
     var unusedObligations = unusedDependencies.OfType<ProofObligationDependency>();
     var unusedRequires = unusedDependencies.OfType<RequiresDependency>();
     var unusedEnsures = unusedDependencies.OfType<EnsuresDependency>();
-    var unusedAssumeStatements =
-      unusedDependencies
-        .OfType<AssumptionDependency>()
-        .Where(d => d is AssumptionDependency ad && ad.IsAssumeStatement);
+    var unusedAssumptions = unusedDependencies.OfType<AssumptionDependency>();
     if (dafnyOptions.Get(CommonOptionBag.WarnContradictoryAssumptions)) {
       foreach (var dependency in unusedObligations) {
         if (ShouldWarnVacuous(dafnyOptions, logEntry.Name, dependency)) {
@@ -59,11 +56,12 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions
         reporter.Warning(MessageSource.Verifier, "", dep.Range, $"unnecessary requires clause");
       }
 
-      foreach (var dep in unusedAssumeStatements) {
+      foreach (var dep in unusedAssumptions) {
         if (ShouldWarnUnused(dep)) {
-          reporter.Warning(MessageSource.Verifier, "", dep.Range, $"unnecessary assumption");
+          reporter.Warning(MessageSource.Verifier, "", dep.Range, $"unnecessary (or partly unnecessary) {dep.Description}");
         }
       }
+
     }
   }
 
@@ -123,7 +121,10 @@ private static bool ShouldWarnVacuous(DafnyOptions options, string verboseName,
   /// Some assumptions that don't show up in the dependency list
   /// are innocuous. In particular, `assume true` is often used
   /// as a place to attach attributes such as `{:split_here}`.
-  /// Don't warn about such assumptions.
+  /// Don't warn about such assumptions. Also don't warn about
+  /// assumptions that aren't explicit (coming from `assume` or
+  /// `assert` statements), for now, because they are difficult
+  /// for the user to control.
   /// </summary>
   /// <param name="dep">the dependency to examine</param>
   /// <returns>false to skip warning about the absence of this
@@ -132,9 +133,11 @@ private static bool ShouldWarnUnused(ProofDependency dep) {
     if (dep is AssumptionDependency assumeDep) {
       if (assumeDep.Expr is not null &&
           Expression.IsBoolLiteral(assumeDep.Expr, out var lit) &&
-          lit == true) {
+          lit) {
         return false;
       }
+
+      return assumeDep.WarnWhenUnused;
     }
 
     return true;

Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs

@@ -198,8 +198,9 @@ public static Bpl.AssumeCmd TrAssumeCmd(Bpl.IToken tok, Bpl.Expr expr, Bpl.QKeyV
       return attributes == null ? new Bpl.AssumeCmd(tok, expr) : new Bpl.AssumeCmd(tok, expr, attributes);
     }
 
-    private Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, string comment = null, bool isAssumeStatement = false, Bpl.QKeyValue attributes = null) {
-      return TrAssumeCmdWithDependenciesAndExtend(etran, tok, dafnyExpr, e => e, comment, isAssumeStatement, attributes);
+    private Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, string comment = null,
+      bool warnWhenUnused = false, Bpl.QKeyValue attributes = null) {
+      return TrAssumeCmdWithDependenciesAndExtend(etran, tok, dafnyExpr, e => e, comment, warnWhenUnused, attributes);
     }
 
     // This method translates a Dafny expression to a Boogie expression,
@@ -208,10 +209,11 @@ private Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bp
     // expressions, for instance), creates an assume statement in Boogie,
     // and then adds information to track that assumption as a potential
     // proof dependency.
-    private Bpl.AssumeCmd TrAssumeCmdWithDependenciesAndExtend(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func<Bpl.Expr, Bpl.Expr> extendExpr, string comment = null, bool isAssumeStatement = false, Bpl.QKeyValue attributes = null) {
+    private Bpl.AssumeCmd TrAssumeCmdWithDependenciesAndExtend(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func<Bpl.Expr, Bpl.Expr> extendExpr,
+      string comment = null, bool warnWhenUnused = false, Bpl.QKeyValue attributes = null) {
       var expr = etran.TrExpr(dafnyExpr);
       var cmd = TrAssumeCmd(tok, extendExpr(expr), attributes);
-      proofDependencies?.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(isAssumeStatement, comment, dafnyExpr));
+      proofDependencies?.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(warnWhenUnused, comment, dafnyExpr));
       return cmd;
     }
 

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -10,6 +10,7 @@
 using System.Linq;
 using System.Numerics;
 using System.Diagnostics.Contracts;
+using DafnyCore.Verifier;
 using Bpl = Microsoft.Boogie;
 using Microsoft.Boogie;
 using static Microsoft.Dafny.Util;

Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs

@@ -649,7 +649,7 @@ private void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, Lis
           // Adding the assume stmt, resetting the stmtContext
           stmtContext = StmtType.ASSUME;
           adjustFuelForExists = true;
-          b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement", true));
+          b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assert statement", true));
           stmtContext = StmtType.NONE;
         }
       }
@@ -661,7 +661,7 @@ private void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, Lis
         // Adding the assume stmt, resetting the stmtContext
         stmtContext = StmtType.ASSUME;
         adjustFuelForExists = true;
-        builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement", true));
+        builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assert statement", true));
         stmtContext = StmtType.NONE;
       }
 

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -3423,7 +3423,6 @@ Bpl.PredicateCmd AssertNS(IToken tok, Bpl.Expr condition, PODesc.ProofObligation
           (RefinementToken.IsInherited(refinesTok, currentModule) && (codeContext == null || !codeContext.MustReverify))) {
         // produce a "skip" instead
         cmd = TrAssumeCmd(tok, Bpl.Expr.True, kv);
-        proofDependencies?.AddProofDependencyId(cmd, tok, new AssumedProofObligationDependency(tok, desc));
       } else {
         tok = ForceCheckToken.Unwrap(tok);
         var args = new List<object>();
@@ -3441,7 +3440,7 @@ Bpl.Ensures EnsuresWithDependencies(IToken tok, bool free, Expression dafnyCondi
       Contract.Ensures(Contract.Result<Bpl.Ensures>() != null);
 
       var ens = Ensures(tok, free, condition, errorMessage, successMessage, comment);
-      proofDependencies?.AddProofDependencyId(ens, tok, new EnsuresDependency(dafnyCondition));
+      proofDependencies?.AddProofDependencyId(ens, tok, new EnsuresDependency(tok, dafnyCondition));
       return ens;
     }
 
@@ -3466,7 +3465,7 @@ Bpl.Requires RequiresWithDependencies(IToken tok, bool free, Expression dafnyCon
       Contract.Ensures(Contract.Result<Bpl.Ensures>() != null);
 
       var req = Requires(tok, free, condition, errorMessage, successMessage, comment);
-      proofDependencies?.AddProofDependencyId(req, tok, new RequiresDependency(dafnyCondition));
+      proofDependencies?.AddProofDependencyId(req, tok, new RequiresDependency(tok, dafnyCondition));
       return req;
     }
 

Source/DafnyCore/Verifier/ProofDependency.cs

@@ -85,29 +85,35 @@ public AssumedProofObligationDependency(IToken tok, PODesc.ProofObligationDescri
 public class RequiresDependency : ProofDependency {
   private Expression requires;
 
+  private IToken tok;
+
   public override RangeToken Range =>
-    requires.RangeToken;
+    tok as RangeToken ?? requires.RangeToken;
 
   public override string Description =>
     $"requires clause";
 
-  public RequiresDependency(Expression requires) {
+  public RequiresDependency(IToken token, Expression requires) {
     this.requires = requires;
+    this.tok = token;
   }
 }
 
 // Represents the goal of proving an ensures clause of a Dafny definition.
 public class EnsuresDependency : ProofDependency {
   private readonly Expression ensures;
 
+  private readonly IToken tok;
+
   public override RangeToken Range =>
-    ensures.RangeToken;
+    tok as RangeToken ?? ensures.RangeToken;
 
   public override string Description =>
     "ensures clause";
 
-  public EnsuresDependency(Expression ensures) {
+  public EnsuresDependency(IToken token, Expression ensures) {
     this.ensures = ensures;
+    this.tok = token;
   }
 }
 
@@ -168,18 +174,18 @@ public class AssumptionDependency : ProofDependency {
     Expr.RangeToken;
 
   public override string Description =>
-    comment ?? $"assume {OriginalString()}";
+    comment ?? OriginalString();
+
+  public bool WarnWhenUnused { get; }
 
   private readonly string comment;
 
   public Expression Expr { get; }
 
-  public bool IsAssumeStatement { get; }
-
-  public AssumptionDependency(bool isAssumeStatement, string comment, Expression expr) {
+  public AssumptionDependency(bool warnWhenUnused, string comment, Expression expr) {
+    this.WarnWhenUnused = warnWhenUnused;
     this.comment = comment;
     this.Expr = expr;
-    this.IsAssumeStatement = isAssumeStatement;
   }
 }
 

Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs

@@ -32,7 +32,7 @@ public async Task RedundantAssumptionsGetWarnings() {
       Assert.Contains(diagnostics, diagnostic =>
         diagnostic.Severity == DiagnosticSeverity.Warning &&
         diagnostic.Range == new Range(3, 11, 3, 16) &&
-        diagnostic.Message == "unnecessary assumption"
+        diagnostic.Message == "unnecessary (or partly unnecessary) assume statement"
         );
       Assert.Contains(diagnostics, diagnostic =>
         diagnostic.Severity == DiagnosticSeverity.Warning &&
@@ -42,7 +42,7 @@ public async Task RedundantAssumptionsGetWarnings() {
       Assert.Contains(diagnostics, diagnostic =>
         diagnostic.Severity == DiagnosticSeverity.Warning &&
         diagnostic.Range == new Range(12, 11, 12, 17) &&
-        diagnostic.Message == "unnecessary assumption"
+        diagnostic.Message == "unnecessary (or partly unnecessary) assume statement"
       );
     }
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy

@@ -116,8 +116,8 @@
 // CHECK: Results for M.CallContradictoryMethodMethod \(correctness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(345,12\)-\(345,16\): requires clause
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,16\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(333,25\) from call
 // CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): requires clause at ProofDependencyLogging.dfy\(332,12\)-\(332,16\) from call
 //
 // CHECK: Results for M.FalseAntecedentRequiresClauseMethod \(correctness\)
@@ -131,7 +131,7 @@
 //
 // CHECK: Results for M.FalseAntecedentEnsuresClauseMethod \(correctness\)
 // CHECK:     Proof dependencies:
-// CHECK:       ProofDependencyLogging.dfy\(368,11\)-\(368,25\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(368,21\)-\(368,25\): ensures clause
 // CHECK:       ProofDependencyLogging.dfy\(370,3\)-\(370,13\): assignment \(or return\)
 //
 // CHECK: Results for M.ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\)

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_combined.html.expect

@@ -133,8 +133,8 @@
 // CHECK: Results for M.CallContradictoryMethodMethod \(correctness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(345,12\)-\(345,16\): requires clause
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,16\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(333,25\) from call
 // CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): requires clause at ProofDependencyLogging.dfy\(332,12\)-\(332,16\) from call
 //
 // CHECK: Results for M.FalseAntecedentRequiresClauseMethod \(correctness\)
@@ -148,7 +148,7 @@
 //
 // CHECK: Results for M.FalseAntecedentEnsuresClauseMethod \(correctness\)
 // CHECK:     Proof dependencies:
-// CHECK:       ProofDependencyLogging.dfy\(368,11\)-\(368,25\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(368,21\)-\(368,25\): ensures clause
 // CHECK:       ProofDependencyLogging.dfy\(370,3\)-\(370,13\): assignment \(or return\)
 //
 // CHECK: Results for M.ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\)

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_combined_limited.html.expect

@@ -133,8 +133,8 @@
 // CHECK: Results for M.CallContradictoryMethodMethod \(correctness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(345,12\)-\(345,16\): requires clause
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,16\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(333,25\) from call
 // CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): requires clause at ProofDependencyLogging.dfy\(332,12\)-\(332,16\) from call
 //
 // CHECK: Results for M.FalseAntecedentRequiresClauseMethod \(correctness\)
@@ -148,7 +148,7 @@
 //
 // CHECK: Results for M.FalseAntecedentEnsuresClauseMethod \(correctness\)
 // CHECK:     Proof dependencies:
-// CHECK:       ProofDependencyLogging.dfy\(368,11\)-\(368,25\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(368,21\)-\(368,25\): ensures clause
 // CHECK:       ProofDependencyLogging.dfy\(370,3\)-\(370,13\): assignment \(or return\)
 //
 // CHECK: Results for M.ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\)

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_tests_expected.html.expect

@@ -133,8 +133,8 @@
 // CHECK: Results for M.CallContradictoryMethodMethod \(correctness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(345,12\)-\(345,16\): requires clause
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,16\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(333,25\) from call
 // CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): requires clause at ProofDependencyLogging.dfy\(332,12\)-\(332,16\) from call
 //
 // CHECK: Results for M.FalseAntecedentRequiresClauseMethod \(correctness\)
@@ -148,7 +148,7 @@
 //
 // CHECK: Results for M.FalseAntecedentEnsuresClauseMethod \(correctness\)
 // CHECK:     Proof dependencies:
-// CHECK:       ProofDependencyLogging.dfy\(368,11\)-\(368,25\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(368,21\)-\(368,25\): ensures clause
 // CHECK:       ProofDependencyLogging.dfy\(370,3\)-\(370,13\): assignment \(or return\)
 //
 // CHECK: Results for M.ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\)

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy_verification.html.expect

@@ -133,8 +133,8 @@
 // CHECK: Results for M.CallContradictoryMethodMethod \(correctness\)
 // CHECK:     Proof dependencies:
 // CHECK:       ProofDependencyLogging.dfy\(345,12\)-\(345,16\): requires clause
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
-// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,25\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,12\)-\(333,16\) from call
+// CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): ensures clause at ProofDependencyLogging.dfy\(333,21\)-\(333,25\) from call
 // CHECK:       ProofDependencyLogging.dfy\(348,9\)-\(348,47\): requires clause at ProofDependencyLogging.dfy\(332,12\)-\(332,16\) from call
 //
 // CHECK: Results for M.FalseAntecedentRequiresClauseMethod \(correctness\)
@@ -148,7 +148,7 @@
 //
 // CHECK: Results for M.FalseAntecedentEnsuresClauseMethod \(correctness\)
 // CHECK:     Proof dependencies:
-// CHECK:       ProofDependencyLogging.dfy\(368,11\)-\(368,25\): ensures clause
+// CHECK:       ProofDependencyLogging.dfy\(368,21\)-\(368,25\): ensures clause
 // CHECK:       ProofDependencyLogging.dfy\(370,3\)-\(370,13\): assignment \(or return\)
 //
 // CHECK: Results for M.ObviouslyUnreachableIfExpressionBranchFunc \(well-formedness\)

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy.expect

@@ -1,8 +1,8 @@
-ProofDependencyLogging.dfy(176,11): Warning: unnecessary assumption
+ProofDependencyLogging.dfy(176,11): Warning: unnecessary (or partly unnecessary) assume statement
 ProofDependencyLogging.dfy(186,13): Warning: proved using contradictory assumptions: assertion always holds
-ProofDependencyLogging.dfy(185,11): Warning: unnecessary assumption
+ProofDependencyLogging.dfy(185,11): Warning: unnecessary (or partly unnecessary) assume statement
 ProofDependencyLogging.dfy(193,13): Warning: proved using contradictory assumptions: assertion always holds
-ProofDependencyLogging.dfy(191,11): Warning: unnecessary assumption
+ProofDependencyLogging.dfy(191,11): Warning: unnecessary (or partly unnecessary) assume statement
 ProofDependencyLogging.dfy(202,11): Warning: proved using contradictory assumptions: assertion always holds
 ProofDependencyLogging.dfy(203,4): Warning: proved using contradictory assumptions: value always satisfies the subset constraints of 'nat'
 ProofDependencyLogging.dfy(211,11): Warning: proved using contradictory assumptions: assertion always holds
@@ -15,6 +15,6 @@ ProofDependencyLogging.dfy(299,11): Warning: unnecessary requires clause
 ProofDependencyLogging.dfy(321,11): Warning: unnecessary requires clause
 ProofDependencyLogging.dfy(346,10): Warning: ensures clause proved using contradictory assumptions
 ProofDependencyLogging.dfy(354,11): Warning: unnecessary requires clause
-ProofDependencyLogging.dfy(363,9): Warning: unnecessary assumption
+ProofDependencyLogging.dfy(363,9): Warning: unnecessary (or partly unnecessary) assert statement
 
 Dafny program verifier finished with 32 verified, 0 errors