review

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -9,6 +9,17 @@
 
 namespace Microsoft.Dafny;
 
+public record AssertCmdPartialCopy(Boogie.IToken Tok, string Description, string Id);
+public record VerificationRunResultPartialCopy(
+  int VCNum,
+  DateTime StartTime,
+  TimeSpan RunTime,
+  SolverOutcome Outcome,
+  List<AssertCmdPartialCopy> Asserts,
+  IEnumerable<TrackedNodeComponent> CoveredElements,
+  IEnumerable<Axiom> AvailableAxioms,
+  int ResourceCount);
+
 public class DafnyConsolePrinter : ConsolePrinter {
   public new DafnyOptions Options {
     get => options;
@@ -21,16 +32,6 @@ public class DafnyConsolePrinter : ConsolePrinter {
   private DafnyOptions options;
 
   public record ImplementationLogEntry(string Name, Boogie.IToken Tok);
-  public record AssertCmdPartialCopy(Boogie.IToken Tok, string Description, string Id);
-  public record VerificationRunResultPartialCopy(
-    int VCNum,
-    DateTime StartTime,
-    TimeSpan RunTime,
-    SolverOutcome Outcome,
-    List<AssertCmdPartialCopy> Asserts,
-    IEnumerable<TrackedNodeComponent> CoveredElements,
-    IEnumerable<Axiom> AvailableAxioms,
-    int ResourceCount);
   public record VerificationResultLogEntry(
     VcOutcome Outcome,
     TimeSpan RunTime,

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -40,7 +40,7 @@ public static void WarnAboutSuspiciousDependenciesUsingStoredPartialResults(Dafn
       if (result.Outcome != VcOutcome.Correct) {
         continue;
       }
-      var unusedFunctions = UnusedFunctions(implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms));
+      var unusedFunctions = GetUnusedFunctions(implementation.Name, result.VCResults.SelectMany(r => r.CoveredElements), result.VCResults.SelectMany(r => r.AvailableAxioms));
       WarnAboutSuspiciousDependencies(implementation.Name, result.VCResults, unusedFunctions);
     }
   }
@@ -50,36 +50,27 @@ public static void WarnAboutSuspiciousDependenciesForImplementation(string name,
     if (results.Any(r => r.Outcome != SolverOutcome.Valid)) {
       return;
     }
-    var unusedFunctions = UnusedFunctions(name, results.SelectMany(r => r.CoveredElements), results.Select(DafnyConsolePrinter.DistillVCResult).SelectMany(r => r.AvailableAxioms));
+    var unusedFunctions = GetUnusedFunctions(name, results.SelectMany(r => r.CoveredElements), results.SelectMany(r => r.DeclarationsAfterPruning.OfType<Axiom>()));
     WarnAboutSuspiciousDependencies(name, results.Select(DafnyConsolePrinter.DistillVCResult).ToList(), unusedFunctions);
   }
 
-  private static List<Function> UnusedFunctions(string implementationName, IEnumerable<TrackedNodeComponent> coveredElements,
+  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)) {
       return new List<Function>();
     }
 
-    var unusedFunctions = new List<Function>();
-    if (manager.idsByMemberName[implementationName].Decl is not Method method) {
-      return unusedFunctions;
+    if (manager.idsByMemberName[implementationName].Decl is not Method) {
+      return new List<Function>();
     }
 
     var usedFunctions = coveredElements.Select(manager.GetFullIdDependency).OfType<FunctionDefinitionDependency>()
-      .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b));
-
-    unusedFunctions = VisibleFunctions().Except(usedFunctions).ToList();
-
-    return unusedFunctions;
+      .Select(dep => dep.function).Distinct();
 
-    HashSet<Function> VisibleFunctions() {
-      var functions = new HashSet<Function>();
-
-      foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) {
-        functions.Add(visibleFunction);
-      }
+    return GetVisibleFunctions().Except(usedFunctions);
 
-      return functions;
+    HashSet<Function> GetVisibleFunctions() {
+      return axioms.Select(GetFunctionFromAttributed).Where(f => f != null).ToHashSet();
 
       Function GetFunctionFromAttributed(ICarriesAttributes construct) {
         var values = construct.FindAllAttributes("id");
@@ -96,7 +87,7 @@ Function GetFunctionFromAttributed(ICarriesAttributes construct) {
   }
 
   private static void WarnAboutSuspiciousDependencies(string scopeName,
-    IReadOnlyList<DafnyConsolePrinter.VerificationRunResultPartialCopy> assertCoverage, List<Function> unusedFunctions) {
+    IReadOnlyList<VerificationRunResultPartialCopy> assertCoverage, IEnumerable<Function> unusedFunctions) {
     var potentialDependencies = manager.GetPotentialDependenciesForDefinition(scopeName);
     var coveredElements = assertCoverage.SelectMany(tp => tp.CoveredElements);
     var usedDependencies =
@@ -144,28 +135,28 @@ private static void WarnAboutSuspiciousDependencies(string scopeName,
       }
     }
 
-    if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[scopeName].Decl is Method m) {
-      SuggestFunctionHiding(unusedFunctions, m);
+    if ((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[scopeName].Decl is Method method) {
+      SuggestFunctionHiding(unusedFunctions, method);
       SuggestByProofRefactoring(scopeName, assertCoverage.ToList());
     }
   }
 
-  private static void SuggestFunctionHiding(List<Function> unusedFunctions, Method m) {
+  private static void SuggestFunctionHiding(IEnumerable<Function> unusedFunctions, Method method) {
     if (unusedFunctions.Any()) {
-      reporter.Info(MessageSource.Verifier, m.Body.StartToken,
-        $"Consider hiding {(unusedFunctions.Count > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}");
+      reporter.Info(MessageSource.Verifier, method.Body.StartToken,
+        $"Consider hiding {(unusedFunctions.Count() > 1 ? "these functions, which are" : "this function, which is")} unused by the proof: {unusedFunctions.Comma()}");
     }
   }
 
   private static void SuggestByProofRefactoring(string scopeName,
-    IReadOnlyList<DafnyConsolePrinter.VerificationRunResultPartialCopy> verificationRunResults) {
-    foreach (var (dep, lAsserts) in ComputeAssertionsUsedByFact(scopeName, verificationRunResults)) {
+    IReadOnlyList<VerificationRunResultPartialCopy> verificationRunResults) {
+    foreach (var (dep, lAsserts) in ComputeAssertionsProvenUsingFact(scopeName, verificationRunResults)) {
       var factIsOnlyUsedByOneAssertion = lAsserts.Count == 1;
       if (!factIsOnlyUsedByOneAssertion) {
         continue;
       }
 
-      DafnyConsolePrinter.AssertCmdPartialCopy cmd = null;
+      AssertCmdPartialCopy cmd = null;
       foreach (var assert in lAsserts) {
         cmd = assert;
       }
@@ -201,7 +192,7 @@ private static void SuggestByProofRefactoring(string scopeName,
 
       switch (consumer) {
         case CallDependency call: {
-            factConsumer = $"precondtion{(call.call.Method.Req.Count > 1 ? "s" : "")} of the method call {call.RangeString()}";
+            factConsumer = $"precondtion{(call.call.Method.Req.Count > 1 ? "s" : "")} of the method call {call.Range.Next.TokenToString(options)}";
             break;
           }
         case ProofObligationDependency { ProofObligation: AssertStatementDescription }: {
@@ -218,31 +209,32 @@ private static void SuggestByProofRefactoring(string scopeName,
     }
   }
 
-  private static Dictionary<ProofDependency, HashSet<DafnyConsolePrinter.AssertCmdPartialCopy>>
-    ComputeAssertionsUsedByFact(string scopeName, IReadOnlyList<DafnyConsolePrinter.VerificationRunResultPartialCopy> vcResults) {
-    var assertionsUsedByFact = manager.GetPotentialDependenciesForDefinition(scopeName)
+  private static Dictionary<ProofDependency, HashSet<AssertCmdPartialCopy>>
+    ComputeAssertionsProvenUsingFact(string scopeName, IReadOnlyList<VerificationRunResultPartialCopy> verificationRunResults) {
+    var assertionsProvenUsingFact = manager.GetPotentialDependenciesForDefinition(scopeName)
+      // Filter out noise
       .Where(dep => dep is not EnsuresDependency)
-      .ToDictionary(dep => dep, _ => new HashSet<DafnyConsolePrinter.AssertCmdPartialCopy> { });
+      .ToDictionary(dep => dep, _ => new HashSet<AssertCmdPartialCopy> { });
 
-    foreach (var (usedFacts, asserts) in vcResults.Select(r => (r.CoveredElements, r.Asserts))) {
-      foreach (var factReference in usedFacts) {
+    foreach (var verificationRun in verificationRunResults) {
+      foreach (var factReference in verificationRun.CoveredElements) {
         var factDependency = manager.GetFullIdDependency(factReference);
         var excludedDependencies = factDependency is EnsuresDependency;
         if (excludedDependencies) {
           continue;
         }
 
-        assertionsUsedByFact.TryAdd(factDependency, new HashSet<DafnyConsolePrinter.AssertCmdPartialCopy>());
+        assertionsProvenUsingFact.TryAdd(factDependency, new HashSet<AssertCmdPartialCopy>());
 
-        bool NotSelfReferential(DafnyConsolePrinter.AssertCmdPartialCopy assert) =>
+        bool IsNotSelfReferential(AssertCmdPartialCopy assert) =>
            !manager.ProofDependenciesById.TryGetValue(assert.Id, out var assertDependency)
                  || !(factDependency == assertDependency || factDependency is CallRequiresDependency req && req.call == assertDependency);
 
-        assertionsUsedByFact[factDependency].UnionWith(asserts.Where(NotSelfReferential));
+        assertionsProvenUsingFact[factDependency].UnionWith(verificationRun.Asserts.Where(IsNotSelfReferential));
       }
     }
 
-    return assertionsUsedByFact;
+    return assertionsProvenUsingFact;
   }
 
   /// <summary>

Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs

@@ -35,12 +35,12 @@ public DummyProofObligationDescription(string success) {
   }
 
 
-  private JsonNode SerializeVcResult(IEnumerable<ProofDependency> potentialDependencies, DafnyConsolePrinter.VerificationRunResultPartialCopy verificationRunResult) {
+  private JsonNode SerializeVcResult(IEnumerable<ProofDependency> potentialDependencies, VerificationRunResultPartialCopy verificationRunResult) {
     var runResult = VCResultLogEntryToPartialVerificationRunResult(verificationRunResult);
     return JsonVerificationLogger.SerializeVcResult(depManager, potentialDependencies?.ToList(), runResult);
   }
 
-  public static VerificationTaskResult VCResultLogEntryToPartialVerificationRunResult(DafnyConsolePrinter.VerificationRunResultPartialCopy verificationRunResult) {
+  public static VerificationTaskResult VCResultLogEntryToPartialVerificationRunResult(VerificationRunResultPartialCopy verificationRunResult) {
     var mockNumber = 42;
     var mockAsserts = verificationRunResult.Asserts.Select(t => new AssertCmd(t.Tok, null, new DummyProofObligationDescription(t.Description)));
     var runResult = new VerificationRunResult(verificationRunResult.VCNum, mockNumber, verificationRunResult.StartTime, verificationRunResult.Outcome, verificationRunResult.RunTime, mockNumber, null!,

Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs

@@ -72,7 +72,7 @@ public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyMa
       ));
     }
 
-    private static IEnumerable<TestResult> VerificationToTestResults(IEnumerable<(DafnyConsolePrinter.ImplementationLogEntry, List<DafnyConsolePrinter.VerificationRunResultPartialCopy>)> verificationResults) {
+    private static IEnumerable<TestResult> VerificationToTestResults(IEnumerable<(DafnyConsolePrinter.ImplementationLogEntry, List<VerificationRunResultPartialCopy>)> verificationResults) {
       var testResults = new List<TestResult>();
 
       foreach (var ((verbName, currentFile), vcResults) in verificationResults) {

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

@@ -1,5 +1,5 @@
 ByProofRefactoring.dfy(11,0): Info: Consider hiding this function, which is unused by the proof: P
-ByProofRefactoring.dfy(18,2): Info: This fact was only used to prove the precondtion of the method call ByProofRefactoring.dfy(19,3)-(19,6). Consider moving it into a by-proof.
+ByProofRefactoring.dfy(18,2): Info: This fact was only used to prove the precondtion of the method call ByProofRefactoring.dfy(19,3). Consider moving it into a by-proof.
 ByProofRefactoring.dfy(31,2): Info: This fact was only used to prove the assertion ByProofRefactoring.dfy(32,3)-(32,13). Consider moving it into a by-proof.
 ByProofRefactoring.dfy(44,0): Info: Consider hiding this function, which is unused by the proof: P
 ByProofRefactoring.dfy(43,11): Info: This requires clause was only used to prove the assertion ByProofRefactoring.dfy(45,3)-(45,13). Consider labelling it and revealing it in a by-proof.