review

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -293,10 +293,15 @@ May produce spurious warnings.
 May produce spurious suggestions. Use with --show-hints on the CLI.") {
     IsHidden = true
   };
-  public static readonly Option<bool> AnalyseProofs = new("--analyse-proofs", @"
-(experimental) Implies --warn-contradictory-assumptions, --warn-redundant-assumptions, and --suggest-proof-refactoring") {
-    IsHidden = true
-  };
+  public static readonly Option<bool> AnalyzeProofs = new("--analyze-proofs", @"
+Uses data from to prover to suggest ways to refine the proof:
+Warning if any assertions are proved based on contradictory assumptions (vacuously).
+Warning if any `requires` clause or `assume` statement was not needed to complete verification.
+Suggestions for moving assertions into by-proofs and hiding unused function definitions.
+May slow down verification slightly, or make it more brittle.
+May produce spurious warnings.
+Use the `{:contradiction}` attribute to mark any `assert` statement intended to be part of a proof by contradiction.
+");
   public static readonly Option<string> VerificationCoverageReport = new("--verification-coverage-report",
     "Emit verification coverage report to a given directory, in the same format as a test coverage report.") {
     ArgumentHelpName = "directory"
@@ -527,6 +532,9 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     DafnyOptions.RegisterLegacyBinding(SuggestProofRefactoring, (options, value) => {
       if (value) { options.TrackVerificationCoverage = true; }
     });
+    DafnyOptions.RegisterLegacyBinding(AnalyzeProofs, (options, value) => {
+      if (value) { options.TrackVerificationCoverage = true; }
+    });
 
     DafnyOptions.RegisterLegacyBinding(Target, (options, value) => { options.CompilerName = value; });
 
@@ -635,7 +643,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     OptionRegistry.RegisterOption(WarnContradictoryAssumptions, OptionScope.Module);
     OptionRegistry.RegisterOption(WarnRedundantAssumptions, OptionScope.Module);
     OptionRegistry.RegisterOption(SuggestProofRefactoring, OptionScope.Module);
-    OptionRegistry.RegisterOption(AnalyseProofs, OptionScope.Module);
+    OptionRegistry.RegisterOption(AnalyzeProofs, OptionScope.Module);
     OptionRegistry.RegisterOption(VerificationCoverageReport, OptionScope.Cli);
     OptionRegistry.RegisterOption(NoTimeStampForCoverageReport, OptionScope.Cli);
     OptionRegistry.RegisterOption(DefaultFunctionOpacity, OptionScope.Module);

Source/DafnyCore/Options/DafnyCommands.cs

@@ -42,7 +42,7 @@ static DafnyCommands() {
     CommonOptionBag.WarnContradictoryAssumptions,
     CommonOptionBag.WarnRedundantAssumptions,
     CommonOptionBag.SuggestProofRefactoring,
-    CommonOptionBag.AnalyseProofs,
+    CommonOptionBag.AnalyzeProofs,
     CommonOptionBag.NoTimeStampForCoverageReport,
     CommonOptionBag.VerificationCoverageReport,
     CommonOptionBag.ExtractCounterexample,

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -56,7 +56,7 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(string name,
 
   private static IEnumerable<Function> GetUnusedFunctions(string implementationName, IEnumerable<TrackedNodeComponent> coveredElements,
     IEnumerable<Axiom> axioms) {
-    if (!((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[implementationName].Decl is Method)) {
+    if (!((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyzeProofs)) && manager.idsByMemberName[implementationName].Decl is Method)) {
       return new List<Function>();
     }
 
@@ -102,7 +102,7 @@ private static void WarnAboutSuspiciousDependencies(string scopeName,
         .ThenBy(dep => dep.Description).ToList();
 
     foreach (var unusedDependency in unusedDependencies) {
-      if (options.Get(CommonOptionBag.WarnContradictoryAssumptions) || options.Get(CommonOptionBag.AnalyseProofs)) {
+      if (options.Get(CommonOptionBag.WarnContradictoryAssumptions) || options.Get(CommonOptionBag.AnalyzeProofs)) {
         if (unusedDependency is ProofObligationDependency obligation) {
           if (ShouldWarnVacuous(scopeName, obligation)) {
             var message = $"proved using contradictory assumptions: {obligation.Description}";
@@ -121,7 +121,7 @@ private static void WarnAboutSuspiciousDependencies(string scopeName,
         }
       }
 
-      if (options.Get(CommonOptionBag.WarnRedundantAssumptions) || options.Get(CommonOptionBag.AnalyseProofs)) {
+      if (options.Get(CommonOptionBag.WarnRedundantAssumptions) || options.Get(CommonOptionBag.AnalyzeProofs)) {
         if (unusedDependency is RequiresDependency requires) {
           reporter.Warning(MessageSource.Verifier, "", requires.Range, $"unnecessary requires clause");
         }
@@ -135,7 +135,7 @@ private static void WarnAboutSuspiciousDependencies(string scopeName,
       }
     }
 
-    if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[scopeName].Decl is Method method) {
+    if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyzeProofs)) && manager.idsByMemberName[scopeName].Decl is Method method) {
       SuggestFunctionHiding(unusedFunctions, method);
       SuggestByProofRefactoring(scopeName, assertCoverage.ToList());
     }
@@ -150,20 +150,18 @@ private static void SuggestFunctionHiding(IEnumerable<Function> unusedFunctions,
 
   private static void SuggestByProofRefactoring(string scopeName,
     IReadOnlyList<VerificationRunResultPartialCopy> verificationRunResults) {
-    foreach (var (dep, lAsserts) in ComputeAssertionsProvenUsingFact(scopeName, verificationRunResults)) {
-      var factIsOnlyUsedByOneAssertion = lAsserts.Count == 1;
+    foreach (var (fact, asserts) in ComputeAssertionsProvenUsingFact(scopeName, verificationRunResults)) {
+      var factIsOnlyUsedByOneAssertion = asserts.Count == 1;
       if (!factIsOnlyUsedByOneAssertion) {
         continue;
       }
 
-      AssertCmdPartialCopy cmd = null;
-      foreach (var assert in lAsserts) {
-        cmd = assert;
-      }
+      AssertCmdPartialCopy partialAssert = asserts.Single();
 
-      manager.ProofDependenciesById.TryGetValue(cmd.Id, out var consumer);
+      manager.ProofDependenciesById.TryGetValue(partialAssert!.Id, out var assertDepProvenByFact);
 
-      if (consumer != null && (dep == consumer || consumer.Range.Intersects(dep.Range))) {
+      var factAlreadyInByBlock = assertDepProvenByFact != null && (fact == assertDepProvenByFact || assertDepProvenByFact.Range.Intersects(fact.Range));
+      if (factAlreadyInByBlock) {
         continue;
       }
 
@@ -173,30 +171,30 @@ private static void SuggestByProofRefactoring(string scopeName,
       var recommendation = "";
       var completeInformation = true;
 
-      switch (dep) {
+      switch (fact) {
         case AssumedProofObligationDependency:
         case AssumptionDependency: {
-            range = dep.Range;
+            range = fact.Range;
             factProvider = "fact";
             recommendation = "moving it into";
             break;
           }
         case RequiresDependency: {
-            range = dep.Range;
+            range = fact.Range;
             factProvider = "requires clause";
             recommendation = "labelling it and revealing it in";
             break;
           }
         default: completeInformation = false; break;
       }
 
-      switch (consumer) {
+      switch (assertDepProvenByFact) {
         case CallDependency call: {
             factConsumer = $"precondtion{(call.call.Method.Req.Count > 1 ? "s" : "")} of the method call {call.Range.Next.TokenToString(options)}";
             break;
           }
         case ProofObligationDependency { ProofObligation: AssertStatementDescription }: {
-            factConsumer = $"assertion {consumer.RangeString()}";
+            factConsumer = $"assertion {assertDepProvenByFact.RangeString()}";
             break;
           }
         default: completeInformation = false; break;