Proof dependency warnings

Source/DafnyCore/AST/Program.cs

@@ -30,7 +30,8 @@ void ObjectInvariant() {
   public SystemModuleManager SystemModuleManager;
   public DafnyOptions Options => Reporter.Options;
   public ErrorReporter Reporter { get; set; }
-  public ProofDependencyManager ProofDependencyManager { get; set; }
+
+  public ProofDependencyManager ProofDependencyManager { get; set; } = new();
 
   public Program(string name, [Captured] LiteralModuleDecl module, [Captured] SystemModuleManager systemModuleManager, ErrorReporter reporter,
     CompilationData compilation) {

Source/DafnyCore/DafnyMain.cs

@@ -13,7 +13,9 @@
 using System.Threading;
 using System.Threading.Tasks;
 using DafnyCore;
+using DafnyCore.Verifier;
 using Microsoft.Boogie;
+using Microsoft.Dafny.ProofObligationDescription;
 using Microsoft.Extensions.Logging;
 using Microsoft.Extensions.Logging.Abstractions;
 
@@ -202,6 +204,5 @@ await options.OutputWriter.WriteLineAsync(
           throw new cce.UnreachableException(); // unexpected outcome
       }
     }
-
   }
 }

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -185,6 +185,18 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
     "Emits a warning when a constructor name in a case pattern is not followed by parentheses.");
   public static readonly Option<bool> WarnShadowing = new("--warn-shadowing",
     "Emits a warning if the name of a declared variable caused another variable to be shadowed.");
+  public static readonly Option<bool> WarnContradictoryAssumptions = new("--warn-contradictory-assumptions", @"
+(experimental) Emits a warning if any assertions are proved based on contradictory assumptions (vacuously).
+May slow down verification slightly.
+May produce spurious warnings.") {
+    IsHidden = true
+  };
+  public static readonly Option<bool> WarnRedundantAssumptions = new("--warn-redundant-assumptions", @"
+(experimental) Emits a warning if any `requires` clause or `assume` statement was not needed to complete verification.
+May slow down verification slightly.
+May produce spurious warnings.") {
+    IsHidden = true
+  };
 
   public static readonly Option<bool> IncludeRuntimeOption = new("--include-runtime",
     "Include the Dafny runtime as source in the target language.");
@@ -248,6 +260,12 @@ static CommonOptionBag() {
     DafnyOptions.RegisterLegacyBinding(WarningAsErrors, (options, value) => { options.WarningsAsErrors = value; });
     DafnyOptions.RegisterLegacyBinding(VerifyIncludedFiles,
       (options, value) => { options.VerifyAllModules = value; });
+    DafnyOptions.RegisterLegacyBinding(WarnContradictoryAssumptions, (options, value) => {
+      if (value) { options.TrackVerificationCoverage = true; }
+    });
+    DafnyOptions.RegisterLegacyBinding(WarnRedundantAssumptions, (options, value) => {
+      if (value) { options.TrackVerificationCoverage = true; }
+    });
 
     DafnyOptions.RegisterLegacyBinding(Target, (options, value) => { options.CompilerName = value; });
 
@@ -347,6 +365,8 @@ static CommonOptionBag() {
       WarnMissingConstructorParenthesis,
       UseJavadocLikeDocstringRewriterOption,
       IncludeRuntimeOption,
+      WarnContradictoryAssumptions,
+      WarnRedundantAssumptions,
       DefaultFunctionOpacity
     );
   }

Source/DafnyCore/Options/ICommandSpec.cs

@@ -42,7 +42,9 @@ static ICommandSpec() {
     BoogieOptionBag.SolverLog,
     CommonOptionBag.JsonDiagnostics,
     BoogieOptionBag.VerificationErrorLimit,
-    CommonOptionBag.DefaultFunctionOpacity
+    CommonOptionBag.DefaultFunctionOpacity,
+    CommonOptionBag.WarnContradictoryAssumptions,
+    CommonOptionBag.WarnRedundantAssumptions
   }.ToList();
 
   public static IReadOnlyList<Option> TranslationOptions = new Option[] {

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -0,0 +1,98 @@
+using System.Linq;
+using DafnyCore.Verifier;
+using Microsoft.Dafny.ProofObligationDescription;
+
+namespace Microsoft.Dafny;
+
+public class ProofDependencyWarnings {
+  public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager) {
+    var verificationResults = (dafnyOptions.Printer as DafnyConsolePrinter).VerificationResults.ToList();
+    var orderedResults =
+      verificationResults.OrderBy(vr =>
+        (vr.Implementation.Tok.filename, vr.Implementation.Tok.line, vr.Implementation.Tok.col));
+    foreach (var (implementation, result) in orderedResults) {
+      WarnAboutSuspiciousDependenciesForImplementation(dafnyOptions, reporter, depManager, implementation, result);
+    }
+  }
+
+  public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, DafnyConsolePrinter.ImplementationLogEntry logEntry, DafnyConsolePrinter.VerificationResultLogEntry result) {
+    var potentialDependencies = depManager.GetPotentialDependenciesForDefinition(logEntry.Name);
+    var usedDependencies =
+      result
+        .VCResults
+        .SelectMany(vcResult => vcResult.CoveredElements.Select(depManager.GetFullIdDependency))
+        .OrderBy(dep => (dep.RangeString(), dep.Description));
+    var unusedDependencies =
+      potentialDependencies
+        .Except(usedDependencies)
+        .OrderBy(dep => (dep.RangeString(), dep.Description));
+
+    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);
+    if (dafnyOptions.Get(CommonOptionBag.WarnContradictoryAssumptions)) {
+      foreach (var dep in unusedObligations) {
+        if (ShouldWarnVacuous(logEntry.Name, dep)) {
+          reporter.Warning(MessageSource.Verifier, "", dep.Range, $"proved using contradictory assumptions: {dep.Description}");
+        }
+      }
+
+      foreach (var dep in unusedEnsures) {
+        if (ShouldWarnVacuous(logEntry.Name, dep)) {
+          reporter.Warning(MessageSource.Verifier, "", dep.Range, $"ensures clause proved using contradictory assumptions");
+        }
+      }
+    }
+
+    if (dafnyOptions.Get(CommonOptionBag.WarnRedundantAssumptions)) {
+      foreach (var dep in unusedRequires) {
+        reporter.Warning(MessageSource.Verifier, "", dep.Range, $"unnecessary requires clause");
+      }
+
+      foreach (var dep in unusedAssumeStatements) {
+        reporter.Warning(MessageSource.Verifier, "", dep.Range, $"unnecessary assumption");
+      }
+    }
+  }
+
+  /// <summary>
+  /// Some proof obligations that don't show up in the dependency list
+  /// are innocuous. Either they come about because of internal Dafny
+  /// design choices that the programmer has no control over, or they
+  /// just aren't meaningful in context. This method identifies cases
+  /// where it doesn't make sense to issue a warning. Many of these
+  /// cases should perhaps be eliminated by changing the translator
+  /// to not generate vacuous proof goals, but that may be a difficult
+  /// change to make.
+  /// </summary>
+  /// <param name="dep">the dependency to examine</param>
+  /// <returns>false to skip warning about the absence of this
+  /// dependency, true otherwise</returns>
+  private static bool ShouldWarnVacuous(string verboseName, ProofDependency dep) {
+    if (dep is ProofObligationDependency poDep) {
+      // Dafny generates some assertions about definite assignment whose
+      // proofs are always vacuous. Since these aren't written by Dafny
+      // programmers, it's safe to just skip them all.
+      if (poDep.ProofObligation is DefiniteAssignment) {
+        return false;
+      }
+
+      // Similarly here
+      if (poDep.ProofObligation is MatchIsComplete or AlternativeIsComplete) {
+        return false;
+      }
+
+    }
+
+    // Ensures clauses are often proven vacuously during well-formedness checks.
+    if (verboseName.Contains("well-formedness") && dep is EnsuresDependency) {
+      return false;
+    }
+
+    return true;
+  }
+}

Source/DafnyCore/Verifier/ProofDependency.cs

@@ -27,7 +27,7 @@ public string LocationString() {
     }
     var fn = Range.StartToken.filename;
     var sl = Range.StartToken.line;
-    var sc = Range.StartToken.col - 1;
+    var sc = Range.StartToken.col;
     return $"{fn}({sl},{sc})";
   }
 
@@ -37,9 +37,9 @@ public string RangeString() {
     }
     var fn = Range.StartToken.filename;
     var sl = Range.StartToken.line;
-    var sc = Range.StartToken.col - 1;
+    var sc = Range.StartToken.col;
     var el = Range.EndToken.line;
-    var ec = Range.EndToken.col - 1;
+    var ec = Range.EndToken.col;
     return $"{fn}({sl},{sc})-({el},{ec})";
   }
 
@@ -159,10 +159,12 @@ public class AssumptionDependency : ProofDependency {
     comment ?? $"assume {OriginalString()}";
 
   private readonly string comment;
+  public bool IsAssumeStatement { get; }
 
-  public AssumptionDependency(string comment, Expression expr) {
+  public AssumptionDependency(bool isAssumeStatement, string comment, Expression expr) {
     this.comment = comment;
     this.expr = expr;
+    this.IsAssumeStatement = isAssumeStatement;
   }
 }
 

Source/DafnyCore/Verifier/ProofDependencyManager.cs

@@ -7,6 +7,7 @@
 //-----------------------------------------------------------------------------
 using System;
 using System.Collections.Generic;
+using Dafny;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
 using Microsoft.Boogie;
@@ -17,15 +18,30 @@ namespace Microsoft.Dafny {
   public class ProofDependencyManager {
     // proof dependency tracking state
     public Dictionary<string, ProofDependency> ProofDependenciesById { get; } = new();
+    private Dictionary<string, HashSet<ProofDependency>> idsByMemberName = new();
     private UInt64 proofDependencyIdCount = 0;
+    private string currentDefinition = null;
 
     public string GetProofDependencyId(ProofDependency dep) {
       var idString = $"id{proofDependencyIdCount}";
       ProofDependenciesById[idString] = dep;
       proofDependencyIdCount++;
+      if (!idsByMemberName.TryGetValue(currentDefinition, out var currentSet)) {
+        currentSet = new HashSet<ProofDependency>();
+        idsByMemberName[currentDefinition] = currentSet;
+      }
+      currentSet.Add(dep);
       return idString;
     }
 
+    public void SetCurrentDefinition(string defName) {
+      currentDefinition = defName;
+    }
+
+    public IEnumerable<ProofDependency> GetPotentialDependenciesForDefinition(string defName) {
+      return idsByMemberName[defName];
+    }
+
     // The "id" attribute on a Boogie AST node is used by Boogie to label
     // that AST node in the SMT-Lib formula when constructing a verification
     // condition.

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -620,10 +620,10 @@ public MatchIsComplete(string matchForm, string missing) {
 
 public class AlternativeIsComplete : ProofObligationDescriptionWithNoExpr {
   public override string SuccessDescription =>
-    $"alternative cases cover all possibilties";
+    $"alternative cases cover all possibilities";
 
   public override string FailureDescription =>
-    $"alternative cases fail to cover all possibilties";
+    $"alternative cases fail to cover all possibilities";
 
   public override string ShortDescription => "alternative complete";
 }

Source/DafnyCore/Verifier/Translator.BoogieFactory.cs

@@ -198,8 +198,8 @@ 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, Bpl.QKeyValue attributes = null) {
-      return TrAssumeCmdWithDependenciesAndExtend(etran, tok, dafnyExpr, e => e, comment, 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);
     }
 
     // This method translates a Dafny expression to a Boogie expression,
@@ -208,10 +208,10 @@ 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, 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 isAssumeStatement = false, Bpl.QKeyValue attributes = null) {
       var expr = etran.TrExpr(dafnyExpr);
       var cmd = TrAssumeCmd(tok, extendExpr(expr), attributes);
-      proofDependencies?.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(comment, dafnyExpr));
+      proofDependencies?.AddProofDependencyId(cmd, dafnyExpr.tok, new AssumptionDependency(isAssumeStatement, comment, dafnyExpr));
       return cmd;
     }
 

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -528,6 +528,7 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP
       Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null);
       Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null);
 
+      proofDependencies.SetCurrentDefinition(proc.VerboseName);
       currentModule = m.EnclosingClass.EnclosingModuleDefinition;
       codeContext = m;
       isAllocContext = new IsAllocContext(options, m.IsGhost);
@@ -794,6 +795,7 @@ private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) {
       Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null);
       Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null);
 
+      proofDependencies.SetCurrentDefinition(proc.VerboseName);
       currentModule = m.EnclosingClass.EnclosingModuleDefinition;
       codeContext = m;
       isAllocContext = new IsAllocContext(options, m.IsGhost);
@@ -877,6 +879,7 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext != null);
       Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext != null);
 
+      proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName, MethodTranslationKind.OverrideCheck));
       #region first procedure, no impl yet
       //Function nf = new Function(f.tok, "OverrideCheck_" + f.Name, f.IsStatic, f.IsGhost, f.TypeArgs, f.OpenParen, f.Formals, f.ResultType, f.Req, f.Reads, f.Ens, f.Decreases, f.Body, f.Attributes, f.SignatureEllipsis);
       //AddFunction(f);
@@ -1478,6 +1481,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
       Contract.Ensures(Contract.Result<Boogie.Procedure>() != null);
       Contract.Assert(VisibleInScope(m));
 
+      proofDependencies.SetCurrentDefinition(MethodVerboseName(m.FullDafnyName, kind));
       currentModule = m.EnclosingClass.EnclosingModuleDefinition;
       codeContext = m;
       isAllocContext = new IsAllocContext(options, m.IsGhost);

Source/DafnyCore/Verifier/Translator.TrStatement.cs

@@ -595,7 +595,7 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
             // Adding the assume stmt, resetting the stmtContext
             stmtContext = StmtType.ASSUME;
             adjustFuelForExists = true;
-            b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement"));
+            b.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement", true));
             stmtContext = StmtType.NONE;
           }
         }
@@ -606,7 +606,7 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
           // Adding the assume stmt, resetting the stmtContext
           stmtContext = StmtType.ASSUME;
           adjustFuelForExists = true;
-          builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement"));
+          builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, stmt.Expr, "assume statement", true));
           stmtContext = StmtType.NONE;
         }
       } else if (stmt is ExpectStmt) {
@@ -634,7 +634,7 @@ private void TrPredicateStmt(PredicateStmt stmt, BoogieStmtListBuilder builder,
         var s = (AssumeStmt)stmt;
         stmtContext = StmtType.ASSUME;
         TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
-        builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, s.Expr, "assume statement", etran.TrAttributes(stmt.Attributes, null)));
+        builder.Add(TrAssumeCmdWithDependencies(etran, stmt.Tok, s.Expr, "assume statement", true, etran.TrAttributes(stmt.Attributes, null)));
         stmtContext = StmtType.NONE; // done with translating assume stmt.
       }
       this.fuelContext = FuelSetting.PopFuelContext();