From 3c4be2facb4716ffea78f86ff7a376cdd6feab2d Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 01:29:32 +0200 Subject: [PATCH] review --- Source/DafnyCore/DafnyConsolePrinter.cs | 21 +++--- Source/DafnyCore/ProofDependencyWarnings.cs | 68 ++++++++----------- .../Legacy/LegacyJsonVerificationLogger.cs | 4 +- .../Legacy/LegacyVerificationResultLogger.cs | 2 +- .../logger/ByProofRefactoring.dfy.expect | 2 +- 5 files changed, 45 insertions(+), 52 deletions(-) diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index b948d235b1..258aaf04c3 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/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 Asserts, + IEnumerable CoveredElements, + IEnumerable 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 Asserts, - IEnumerable CoveredElements, - IEnumerable AvailableAxioms, - int ResourceCount); public record VerificationResultLogEntry( VcOutcome Outcome, TimeSpan RunTime, diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index 7b2a9a7c82..c202f32ad3 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/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())); WarnAboutSuspiciousDependencies(name, results.Select(DafnyConsolePrinter.DistillVCResult).ToList(), unusedFunctions); } - private static List UnusedFunctions(string implementationName, IEnumerable coveredElements, + private static IEnumerable GetUnusedFunctions(string implementationName, IEnumerable coveredElements, IEnumerable axioms) { if (!((options.Get(CommonOptionBag.SuggestProofRefactoring) || options.Get(CommonOptionBag.AnalyseProofs)) && manager.idsByMemberName[implementationName].Decl is Method)) { return new List(); } - var unusedFunctions = new List(); - if (manager.idsByMemberName[implementationName].Decl is not Method method) { - return unusedFunctions; + if (manager.idsByMemberName[implementationName].Decl is not Method) { + return new List(); } var usedFunctions = coveredElements.Select(manager.GetFullIdDependency).OfType() - .Select(dep => dep.function).Deduplicate((a, b) => a.Equals(b)); - - unusedFunctions = VisibleFunctions().Except(usedFunctions).ToList(); - - return unusedFunctions; + .Select(dep => dep.function).Distinct(); - HashSet VisibleFunctions() { - var functions = new HashSet(); - - foreach (var visibleFunction in axioms.Select(GetFunctionFromAttributed).Where(f => f != null)) { - functions.Add(visibleFunction); - } + return GetVisibleFunctions().Except(usedFunctions); - return functions; + HashSet 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 assertCoverage, List unusedFunctions) { + IReadOnlyList assertCoverage, IEnumerable 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 unusedFunctions, Method m) { + private static void SuggestFunctionHiding(IEnumerable 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 verificationRunResults) { - foreach (var (dep, lAsserts) in ComputeAssertionsUsedByFact(scopeName, verificationRunResults)) { + IReadOnlyList 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> - ComputeAssertionsUsedByFact(string scopeName, IReadOnlyList vcResults) { - var assertionsUsedByFact = manager.GetPotentialDependenciesForDefinition(scopeName) + private static Dictionary> + ComputeAssertionsProvenUsingFact(string scopeName, IReadOnlyList verificationRunResults) { + var assertionsProvenUsingFact = manager.GetPotentialDependenciesForDefinition(scopeName) + // Filter out noise .Where(dep => dep is not EnsuresDependency) - .ToDictionary(dep => dep, _ => new HashSet { }); + .ToDictionary(dep => dep, _ => new HashSet { }); - 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()); + assertionsProvenUsingFact.TryAdd(factDependency, new HashSet()); - 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; } /// diff --git a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs index 683092cf02..93087fe8e5 100644 --- a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs +++ b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs @@ -35,12 +35,12 @@ public DummyProofObligationDescription(string success) { } - private JsonNode SerializeVcResult(IEnumerable potentialDependencies, DafnyConsolePrinter.VerificationRunResultPartialCopy verificationRunResult) { + private JsonNode SerializeVcResult(IEnumerable 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!, diff --git a/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs b/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs index 4f182bdf84..928e8d6d3c 100644 --- a/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs +++ b/Source/DafnyDriver/Legacy/LegacyVerificationResultLogger.cs @@ -72,7 +72,7 @@ public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyMa )); } - private static IEnumerable VerificationToTestResults(IEnumerable<(DafnyConsolePrinter.ImplementationLogEntry, List)> verificationResults) { + private static IEnumerable VerificationToTestResults(IEnumerable<(DafnyConsolePrinter.ImplementationLogEntry, List)> verificationResults) { var testResults = new List(); foreach (var ((verbName, currentFile), vcResults) in verificationResults) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect index 41c1df51d0..948d0eaff0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ByProofRefactoring.dfy.expect +++ b/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.